search

SRI-CSL / yices2

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

Assertion error at solvers/quant/quant_solver.c:639 #365

Closed rainoftime closed 3 years ago

rainoftime commented 3 years ago

yices2 09d18a4fa49fedf

(set-logic UF)
(declare-fun uf4 (Bool Bool Bool Bool) Bool)
(declare-fun v8 () Bool)
(declare-fun v9 () Bool)
(assert (uf4 true false true false))
(assert (forall ((q23 Bool)) (or (xor v9 q23 q23 v8 q23) (exists ((q9 Bool)) q9))))
(check-sat)
yices_smt2: solvers/quant/quant_solver.c:639: ematch_cnstr_instantiate: Assertion `rhst != (-1)' failed.
BrunoDutertre commented 3 years ago

Fixed in 282b2681c14ff767e7c0efcff3d2458cf7ee1eb0