A wrong result for the query containing multiplication

[martinjonas]

For the formula

(set-logic QF_BV)

(declare-fun a () (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(declare-fun c () (_ BitVec 32))

(assert (bvugt a #x0000A000))
(assert (bvugt b #x0000A000))
(assert (bvuge c #xFFFFFFF0))

(assert (= c (bvmul a b)))

(check-sat)

the output of mcBV is

Z3> Error, literal in conflict clause is not false (-43=True)
unsat

but the formula is satisfiable (as witnessed by Z3 or Boolector).

The error occurs with

• mcBV -- version 1.0,
• Z3 library -- git revision b080e3a
• mono -- version 4.4.0

[martinjonas]

Actually, a smaller example is sufficient to reproduce the bug

(set-logic QF_BV)

(declare-fun a () (_ BitVec 8))
(declare-fun b () (_ BitVec 8))
(declare-fun c () (_ BitVec 8))

(assert (bvugt a #x0A))
(assert (bvugt b #x0A))
(assert (bvuge c #xF0))

(assert (= c (bvmul a b)))

(check-sat)

[wintersteiger]

Thanks for reporting this issue, that's indeed a bug that we need to fix. I added a partial fix in my own fork for now (wintersteiger@3a6520f), but that is really partial at this time because it still throws explanation validation errors (but much later than before).

@AleksandarZeljic : could you take a look at this? I would have thought this type of problem would be solved by the bounds-based decision heuristics fairly quickly, but after my fixes it enumerates wildly and for quite some time.