Quantified FPA formula incorrectly marked as SAT with MBQI

[nunoplopes]

This query is UNSAT with E-matching (correct) and SAT with MBQI (wrong):

(declare-fun undef_2 () (_ FloatingPoint 8 24))
(declare-fun blks_val () (Array (_ BitVec 80) (_ BitVec 85)))
(assert (forall ((undef_1 (_ FloatingPoint 8 24)))
             (let ((a!1 (forall ((|#idx0| (_ BitVec 80)))
                          (= ((_ extract 84 84) (select blks_val |#idx0|)) #b0)))
                   (a!2 (fp.to_ieee_bv (fp.neg ((_ to_fp 8 24) (fp.to_ieee_bv undef_1)))))
                   (a!3 (fp.to_ieee_bv (fp.neg ((_ to_fp 8 24) (fp.to_ieee_bv undef_2))))))
             (let ((a!4 (not (= ((_ to_fp 8 24) a!3) ((_ to_fp 8 24) a!2)))))
               (and a!1 a!4)))))

(check-sat)

Output:

$ z3 bug.smt2
unsat
$ z3 smt.ematching=false bug.smt2
sat

Not sure if it's the same bug as #2596?

[NikolajBjorner]

Seems duplicate. I see

mk_model
k!4 -> (_ +zero 8 24)
fp.to_ieee_bv -> {
(_ +zero 8 24) -> #x7fc00000
(_ -zero 8 24) -> #x7f800002
else -> #x7fc00000
}
Thus, an interpreted function is added to the model used for MBQI.

[nunoplopes]

Oh I see, thanks!

[NikolajBjorner]

But this example should be unsat. Looking at the formula it contains a contradiction that is indepedendent of the to_ieee model inclusion. I haven't reproduced the "sat" answer.

[nunoplopes]

Yes, it should be unsat. Sorry, I got that flipped in the description.
I was sometimes able to flip to SAT using model.partial=true. ATM, I can reproduce the problem in Cygwin & CentOS.

[NikolajBjorner]

no repro in my environment. Is it selectively reproducing on Cygwin/CentOS, or are these the only systems you have tried. Also the full set of parameters for repro is useful. Otherwise, I am just fumbling to reproduce what random parameters you have been playing with.

C:\z3\build>z3 2631.smt2 model.partial=true
unsat

C:\z3\build>z3 2631.smt2 model.partial=true smt.mbqi=false
unsat

C:\z3\build>z3 2631.smt2 model.partial=true smt.mbqi=false smt.auto_config=false
unknown

[nunoplopes]

It repros deterministically here on those 2 systems (the only I've tried). The only thing I need here is smt.ematching=false:

$ z3 bug.smt2
unsat
$ z3 smt.ematching=false bug.smt2
sat

[NikolajBjorner]

OK, ematching finds the crucial instance undef_2.
MBQI fails to find it, so it is again about the floating point models.
The bug is therefore most likely a duplicate of the issue with floating point model conversion.

[NikolajBjorner]

@wintersteiger this would be related to, if not duplicate of, #2596.

[wintersteiger]

Yes, likely duplicate. Interpreted functions are added for the unspecified special cases of some FPA functions, which I think should be fine in the context of MBQI, but I'm not sure.

[NikolajBjorner]

Marking as duplicate of #2596