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 src/btordbg.c:322 #158

Open rainoftime opened 3 years ago

rainoftime commented 3 years ago

Hi, for the following formula, boolector 6fce0ac

(set-logic BV)
(declare-fun _substvar_7291_ () Bool)
(declare-fun _substvar_7499_ () Bool)
(declare-const bv_3-0 (_ BitVec 3))
(declare-const v16 Bool)
(assert (or (not (exists ((q58 Bool) (q59 (_ BitVec 6))) (=> (xor true q58 true q58 q58 false q58 false q58 true (exists ((q50 (_ BitVec 8)) (q51 (_ BitVec 1))) (not (distinct ((_ extract 0 0) bv_3-0) q51 (bvcomp (_ bv0 52) (_ bv0 52)))))) false))) v16 (forall ((q61 Bool) (q62 (_ BitVec 40)) (q63 (_ BitVec 5)) (q64 (_ BitVec 3))) (or _substvar_7291_ (not (exists ((q58 Bool) (q59 (_ BitVec 6))) (=> (xor true q58 true q58 q58 false q58 false q58 true (exists ((q50 (_ BitVec 8)) (q51 (_ BitVec 1))) (not (distinct ((_ extract 0 0) bv_3-0) q51 (bvcomp (_ bv0 52) (_ bv0 52)))))) false))) _substvar_7499_))))
(check-sat)

$ boolector xx.smt2
boolector: /home/peisen/test/tofuzz/boolector/src/btordbg.c:322: btor_dbg_precond_eq_exp: Assertion `btor_node_get_sort_id (real_e0) == btor_node_get_sort_id (real_e1)' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted