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
335 stars 62 forks source link

Assertion violation at src/btordbg.c:375 #153

Open rainoftime opened 3 years ago

rainoftime commented 3 years ago

Hi, for the following formula, boolector 6fce0ac

(set-logic BV)
(declare-fun _substvar_651_ () Bool)
(declare-const v6 Bool)
(declare-const v28 Bool)
(declare-const bv_41-0 (_ BitVec 41))
(assert (or (xor (forall ((q5 Bool) (q6 (_ BitVec 41)) (q7 (_ BitVec 8)) (q8 Bool) (q9 (_ BitVec 41))) (distinct (_ bv0 41) bv_41-0)) false true true true (= (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) q0)) v6) true v28) _substvar_651_))
(check-sat)

$ boolector xx.smt2
boolector: /home/peisen/test/tofuzz/boolector/src/btordbg.c:375: btor_dbg_precond_regular_binary_bv_exp: Assertion `btor_node_get_sort_id (e0) == btor_node_get_sort_id (e1)' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted
mpreiner commented 1 month ago

Boolector is not actively maintained and developed anymore. It was succeeded by Bitwuzla and the repository is now archived.