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/bv/bvsolver.c:785 #222

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago 
(set-logic QF_AUFBV)
(declare-const bv_10-0 (_ BitVec 10))
(declare-const arr (Array (_ BitVec 40) (_ BitVec 10)))
(assert (bvsgt (bvsub bv_10-0 (bvmul bv_10-0 bv_10-0)) bv_10-0))
(check-sat)
(check-sat)
(assert (bvsge (select arr ((_ repeat 8) ((_ extract 9 5) (bvmul bv_10-0 bv_10-0)))) (_ bv0 10)))

yices commit b643c19

sat
sat
yices_smt2: solvers/bv/bvsolver.c:785: select_bvvar_get_pseudo_map: Assertion `bvvar_is_bitblasted(&solver->vtbl, x) || bvvar_in_select_queue(solver, x)' failed.
BrunoDutertre commented 4 years ago

Fixed by 019d06999f8150118eee84ac24ec29c97467729b.