search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
325 stars 63 forks source link

Assertion violation at btordbg.c:323 #114

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic ABV)
(declare-const bv_14-0 (_ BitVec 14))
(declare-const arr--8732212593330861448_-8732212593324366298-0 (Array (_ BitVec 14) (_ BitVec 8)))
(assert (exists ((q2 Bool) (q3 Bool) (q4 Bool)) q3))
(assert (exists ((q8 (_ BitVec 1))) (distinct arr--8732212593330861448_-8732212593324366298-0 (store arr--8732212593330861448_-8732212593324366298-0 (bvnand bv_14-0 bv_14-0) (_ bv0 8)))))
(check-sat)

boolector (commit 76aafdf) throws an assertion violation

boolector: /home/peisen/test/tofuzz/boolector/src/btordbg.c:323: btor_dbg_precond_eq_exp: Assertion `real_e0->is_array == real_e1->is_array' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted (core dumped)
aniemetz commented 4 years ago

Duplicate of #113.