search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
368 stars 46 forks source link

Assertion violation at solvers/simplex/simplex.c:10308 #218

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago 
(set-logic QF_LIA)
(declare-const i0 Int)
(assert (> (mod i0 795) i0))
(check-sat)
(push 1)

yices commit 36f29be

sat
yices_smt2: solvers/simplex/simplex.c:10308: simplex_push: Assertion `solver->decision_level == solver->base_level && solver->bstack.prop_ptr == solver->bstack.fix_ptr && solver->save_rows && eassertion_queue_is_empty(&solver->egraph_queue)' failed.
BrunoDutertre commented 4 years ago

Fixed by 465eaa5b95dbd7f93bf781018944575b936799f1.