Refutation soundness bug on bit-vector formulas

[rainoftime]

Hi, for the following formula,
boolector 6fce0ac yields unsat,
but both cvc4 and z3 give sat

(set-logic BV)
(declare-fun _substvar_245_ () Bool)
(assert (not (forall ((q21 Bool) (q22 (_ BitVec 4)) (q23 (_ BitVec 8))) (not (= q21 true true (not (forall ((q2 (_ BitVec 4)) (q3 (_ BitVec 4)) (q4 Bool) (q5 (_ BitVec 4)) (q6 (_ BitVec 4)) (q7 (_ BitVec 4))) q4)) _substvar_245_ q21 q21 q21 true q21)))))
(check-sat)

[rainoftime]

Another formula

(set-logic BV)
(declare-fun _substvar_2530_ () Bool)
(declare-const v8 Bool)
(assert (or (forall ((q110 (_ BitVec 7))) (not (exists ((q81 Bool) (q82 (_ BitVec 8))) q81))) (not (exists ((q83 (_ BitVec 7)) (q84 (_ BitVec 8))) (forall ((q67 (_ BitVec 8)) (q68 Bool) (q69 (_ BitVec 7)) (q70 (_ BitVec 7)) (q71 Bool)) (not (exists ((q56 (_ BitVec 4)) (q57 (_ BitVec 8)) (q58 (_ BitVec 4))) v8)))))))
(assert (or (not (forall ((q91 (_ BitVec 7)) (q92 (_ BitVec 4)) (q93 (_ BitVec 4))) (=> (distinct q91 (_ bv81 7)) _substvar_2530_))) (not (exists ((q8 Bool) (q9 Bool)) v8))))
(check-sat)

[vedadux]

I took the time to look at this, and have found a much simpler example where the exact same problem happens:

(assert (exists ((q Bool)) (= true (not (forall ((p Bool)) p)) q)))
(check-sat)

Here, the forall block evaluates to false, meaning that the exists block is satisfiable with q = true.
The solver Z3 gives the correct answer sat, while Boolector gives unsat.
This is all with Boolector version 3.2.2, commit 0783aa8

[mpreiner]

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