$./dReal --debug simpler.smt2
...
THandler::assertLits(): asserting (<= -10 leg1.q_i) with sign = 0
Egraph::assertLit()(<= -10 leg1.q_i)
nra_solver::assertLit: (<= -10 leg1.q_i), reason: false, polarity: 1,
level: 32, ded.size = 0
nra_solver::pushBacktrackPoint 33
THandler::assertLits(): asserting (<= leg2.dy 10) with sign = 0
Egraph::assertLit()(<= leg2.dy 10)
nra_solver::assertLit: (<= leg2.dy 10), reason: false, polarity: 1,
level: 33, ded.size = 0
nra_solver::pushBacktrackPoint 34
THandler::assertLits(): asserting (<= -10 leg2.dy) with sign = 0
Egraph::assertLit()(<= -10 leg2.dy)
nra_solver::assertLit: (<= -10 leg2.dy), reason: false, polarity: 1,
level: 34, ded.size = 0
nra_solver::pushBacktrackPoint 35
THandler::assertLits(): asserting (<= leg1.dx 10) with sign = 0
Egraph::assertLit()(<= leg1.dx 10)
nra_solver::assertLit: (<= leg1.dx 10), reason: false, polarity: 1,
level: 35, ded.size = 0
nra_solver::pushBacktrackPoint 36
THandler::assertLits(): asserting (<= -10 leg1.dx) with sign = 0
Egraph::assertLit()(<= -10 leg1.dx)
nra_solver::assertLit: (<= -10 leg1.dx), reason: false, polarity: 1,
level: 36, ded.size = 0
nra_solver::check(complete = false)
build_system_factory:
build_system_factory: Add Variable leg1.beamwidth
build_system_factory: Add Variable leg1.dx
build_system_factory: Add Variable leg1.dy
build_system_factory: Add Variable leg1.dz
build_system_factory: Add Variable leg1.q_a
build_system_factory: Add Variable leg1.q_i
build_system_factory: Add Variable leg1.q_j
build_system_factory: Add Variable leg1.q_k
build_system_factory: Add Variable leg2.beamwidth
build_system_factory: Add Variable leg2.dx
build_system_factory: Add Variable leg2.dy
build_system_factory: Add Variable leg2.dz
build_system_factory: Add Variable leg2.length
build_system_factory: Add Variable leg2.q_a
build_system_factory: Add Variable leg2.q_i
build_system_factory: Add Variable leg2.q_j
build_system_factory: Add Variable leg2.q_k
build_system_factory: Add Variable: DONE
build_system_factory: Add Constraint: algebraic_constraint (= (+ (*
leg1.beamwidth (+ (* 2 leg1.q_i leg1.q_k) (* -2 leg1.q_a leg1.q_j)))
leg1.dz) (+ (* leg2.beamwidth (+ (* 2 leg2.q_i leg2.q_k) (* -2
leg2.q_a leg2.q_j))) leg2.dz (* leg2.length (+ (* 2 leg2.q_a leg2.q_i)
(* 2 leg2.q_j leg2.q_k)))))
build_system_factory: Add Constraint: expr:
(((leg1.beamwidth*(((2*leg1.q_i)*leg1.q_k)+((-2*leg1.q_a)*leg1.q_j)))+leg1.dz)-(((leg2.beamwidth*(((2*leg2.q_i)*leg2.q_k)+((-2*leg2.q_a)*leg2.q_j)))+leg2.dz)+(leg2.length*(((2*leg2.q_a)*leg2.q_i)+((2*leg2.q_j)*leg2.q_k)))))=0
build_system_factory: Add Constraint: algebraic_constraint (= (+ (*
leg1.beamwidth (+ (* 2 leg1.q_a leg1.q_k) (* 2 leg1.q_i leg1.q_j)))
leg1.dy) (+ (* leg2.beamwidth (+ (* 2 leg2.q_i leg2.q_j) (* 2 leg2.q_a
leg2.q_k))) leg2.dy (* leg2.length (+ (* -1 (^ leg2.q_i 2)) (* -1 (^
leg2.q_k 2)) (^ leg2.q_a 2) (^ leg2.q_j 2)))))
build_system_factory: Add Constraint: expr:
(((leg1.beamwidth*(((2*leg1.q_a)*leg1.q_k)+((2*leg1.q_i)*leg1.q_j)))+leg1.dy)-(((leg2.beamwidth*(((2*leg2.q_i)*leg2.q_j)+((2*leg2.q_a)*leg2.q_k)))+leg2.dy)+(leg2.length*((((-1*leg2.q_i^2)+(-1*leg2.q_k^2))+leg2.q_a^2)+leg2.q_j^2))))=0
build_system_factory: Add Constraint: algebraic_constraint (= (+ (*
leg1.beamwidth (+ (^ leg1.q_a 2) (* -1 (^ leg1.q_j 2)) (^ leg1.q_i 2)
(* -1 (^ leg1.q_k 2)))) leg1.dx) (+ (* leg2.beamwidth (+ (* -1 (^
leg2.q_k 2)) (^ leg2.q_a 2) (^ leg2.q_i 2) (* -1 (^ leg2.q_j 2)))) (*
leg2.length (+ (* -2 leg2.q_a leg2.q_k) (* 2 leg2.q_i leg2.q_j)))
leg2.dx))
build_system_factory: Add Constraint: expr:
(((leg1.beamwidth*(((leg1.q_a^2+(-1*leg1.q_j^2))+leg1.q_i^2)+(-1*leg1.q_k^2)))+leg1.dx)-(((leg2.beamwidth*((((-1*leg2.q_k^2)+leg2.q_a^2)+leg2.q_i^2)+(-1*leg2.q_j^2)))+(leg2.length*(((-2*leg2.q_a)*leg2.q_k)+((2*leg2.q_i)*leg2.q_j))))+leg2.dx))=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg2.dz 10)
build_system_factory: Add Constraint: expr: (leg2.dz-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg2.dz)
build_system_factory: Add Constraint: expr: (-10-leg2.dz)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg2.q_a 10)
build_system_factory: Add Constraint: expr: (leg2.q_a-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg2.q_a)
build_system_factory: Add Constraint: expr: (-10-leg2.q_a)<=0
build_system_factory: Add Constraint: algebraic_constraint (<=
leg2.beamwidth 10)
build_system_factory: Add Constraint: expr: (leg2.beamwidth-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= 0 leg2.beamwidth)
build_system_factory: Add Constraint: expr: (0-leg2.beamwidth)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg2.q_k 10)
build_system_factory: Add Constraint: expr: (leg2.q_k-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg2.q_k)
build_system_factory: Add Constraint: expr: (-10-leg2.q_k)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg2.q_i 10)
build_system_factory: Add Constraint: expr: (leg2.q_i-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg2.q_i)
build_system_factory: Add Constraint: expr: (-10-leg2.q_i)<=0
build_system_factory: Add Constraint: algebraic_constraint (<=
leg1.beamwidth 10)
build_system_factory: Add Constraint: expr: (leg1.beamwidth-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= 0 leg1.beamwidth)
build_system_factory: Add Constraint: expr: (0-leg1.beamwidth)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg1.dz 10)
build_system_factory: Add Constraint: expr: (leg1.dz-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg1.dz)
build_system_factory: Add Constraint: expr: (-10-leg1.dz)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg1.q_j 10)
build_system_factory: Add Constraint: expr: (leg1.q_j-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg1.q_j)
build_system_factory: Add Constraint: expr: (-10-leg1.q_j)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg2.dx 10)
build_system_factory: Add Constraint: expr: (leg2.dx-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg2.dx)
build_system_factory: Add Constraint: expr: (-10-leg2.dx)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg1.q_a 10)
build_system_factory: Add Constraint: expr: (leg1.q_a-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg1.q_a)
build_system_factory: Add Constraint: expr: (-10-leg1.q_a)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg1.q_k 10)
build_system_factory: Add Constraint: expr: (leg1.q_k-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg1.q_k)
build_system_factory: Add Constraint: expr: (-10-leg1.q_k)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg1.dy 10)
build_system_factory: Add Constraint: expr: (leg1.dy-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg1.dy)
build_system_factory: Add Constraint: expr: (-10-leg1.dy)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg2.q_j 10)
build_system_factory: Add Constraint: expr: (leg2.q_j-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg2.q_j)
build_system_factory: Add Constraint: expr: (-10-leg2.q_j)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg2.length 10)
build_system_factory: Add Constraint: expr: (leg2.length-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= 0 leg2.length)
build_system_factory: Add Constraint: expr: (0-leg2.length)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg1.q_i 10)
build_system_factory: Add Constraint: expr: (leg1.q_i-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg1.q_i)
build_system_factory: Add Constraint: expr: (-10-leg1.q_i)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg2.dy 10)
build_system_factory: Add Constraint: expr: (leg2.dy-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg2.dy)
build_system_factory: Add Constraint: expr: (-10-leg2.dy)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= leg1.dx 10)
build_system_factory: Add Constraint: expr: (leg1.dx-10)<=0
build_system_factory: Add Constraint: algebraic_constraint (<= -10 leg1.dx)
build_system_factory: Add Constraint: expr: (-10-leg1.dx)<=0
build_system_factory: Add Constraint: DONE
build_system_factory: DONE
contractor_ibex:
Segmentation fault: 11