Assertion violation at sat_solver.cc:185

dreal / dreal4

Automated Reasoning in Nonlinear Theories of Reals

https://dreal.github.io

Apache License 2.0

151 stars 32 forks source link

Assertion violation at sat_solver.cc:185 #180

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula

(set-logic QF_NRA)
(assert (forall ((q Real)) true))
(check-sat)

dreal4 (Commit 0780274) throws an assertion violation

dreal: dreal/solver/sat_solver.cc:185: void dreal::SatSolver::AddLiteral(const dreal::drake::symbolic::Formula&): Assertion `is_variable(f) || (is_negation(f) && is_variable(get_operand(f)))' failed.
Aborted (core dumped)

soonho-tri commented 4 years ago

Fixed by #215