Assertion violation at src/preprocess/btornormquant.c:373

[rainoftime]

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

[mpreiner]

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