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/preprocess/btornormquant.c:373 #154

Open rainoftime opened 3 years ago

rainoftime commented 3 years ago

Hi, for the following formula, boolector 6fce0ac

(set-logic BV)
(declare-fun _substvar_226_ () Bool)
(declare-fun _substvar_268_ () Bool)
(declare-const bv_4-1 (_ BitVec 4))
(declare-const v14 Bool)
(declare-const v20 Bool)
(assert (or _substvar_226_ (xor v14 (not (exists ((q17 (_ BitVec 4)) (q18 (_ BitVec 5)) (q19 (_ BitVec 14))) (= q17 bv_4-1 bv_4-1 bv_4-1 #x9))) true)))
(assert (or (xor v14 (not (exists ((q17 (_ BitVec 4)) (q18 (_ BitVec 5)) (q19 (_ BitVec 14))) (= q17 bv_4-1 bv_4-1 bv_4-1 #x9))) true) _substvar_268_ v20))
(check-sat)

$ boolector xx.smt2
boolector: /home/peisen/test/tofuzz/boolector/src/preprocess/btornormquant.c:373: fix_quantifier_polarities: Assertion `BTOR_COUNT_STACK (args) >= real_cur->arity' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted