Solution soundness bug on BV formulas (--quant-ms)

[rainoftime]

Hi, for the following formula

(set-logic BV)
(declare-const bv_47-0 (_ BitVec 47))
(assert (forall ((q20 (_ BitVec 10)) (q21 (_ BitVec 10)) (q22 (_ BitVec 10)) (q23 (_ BitVec 47)) (q24 (_ BitVec 47)) (q25 (_ BitVec 9))) (=> (= q24 q23 bv_47-0 bv_47-0 bv_47-0) (
bvult q25 (_ bv268 9)))))
(check-sat)

boolector 6fce0ac yields sat,
but both cvc4 and z3 return unsat

This formula seems trivially unsat because q25 only appears once in the body.

---

Another one

(set-logic BV)
(declare-fun _substvar_10_ () (_ BitVec 8))
(assert (forall ((q8 (_ BitVec 8)) (q9 (_ BitVec 8)) (q10 (_ BitVec 7))) (=> (= q9 _substvar_10_ q9 q8 q8) (= (_ bv0 7) q10 (_ bv0 7)))))
(check-sat)

[rainoftime]

@aniemetz This issue seems to be related to miniscoping. With the option --quant-ms=0, boolector can return unsat.
Could you have a check?

[mpreiner]

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