Solution soundness bug in FP logic

[muchang]

For this formula, z3 gives an incorrect sat, while the model validator cannot detect.

[503] % cvc4 -q small.smt2
unsat
[504] % z3release model_validate=true small.smt2
sat
[505] % cat small.smt2
(assert (forall ((a Float32)) (not (fp.isNegative (fp.min a (_ +zero 8 24))))))
(check-sat)
[506] %

Commit: 621e992

[NikolajBjorner]

MBQI doesn't integrate with model updates in

z3/src/ast/fpa/bv2fpa_converter.cpp

Line 408 in 173257b

void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {

There, a definition for fp.min is added to the model, it gets used to specialize the formula passed into MBQI.

z3 4880.smt2 /v:1 smt.relevancy=0 /tr:quantifier /tr:model_checker /tr:smt_model_checker /tr:model /tr:bv2fpa

[rainoftime]

Another soundness issue with BVFP

(assert (forall ((Y (_ FloatingPoint 8 24))) (or (distinct (_ bv1 8) ((_ fp.to_sbv 8) roundNearestTiesToEven Y)) (fp.eq Y (fp (_ bv0 1) (_ bv0 8) (_ bv0 23))))))
(check-sat)

[wintersteiger]

I'm not sure CVC is right here, surely min(a, 0) is allowed to be negative for some a. The min is also unspecified when both arguments are zero, that's what those specials are for.

@rainoftime: the formula you just added has nothing to do with fp.min, nor does it come with a bug description. What's wrong with that one?

[NikolajBjorner]

Regarding the assertion:

(assert (forall ((a Float32)) (not (fp.isNegative (fp.min a (_ +zero 8 24))))))

It is unsat, right?
Z3 reports sat.

[zhendongsu]

Yes, it should be unsat since if a = (_ -oo 8 24) for example, (not (fp.isNegative (fp.min a (_ +zero 8 24)))) evaluates to false.

[524] % z3 t.smt2 
unsat
[525] % cvc5 -q t.smt2 
unsat
[526] % cat t.smt2 
(assert (not (fp.isNegative (fp.min (_ -oo 8 24) (_ +zero 8 24)))))
(check-sat)
[527] % 

[NikolajBjorner]

yes, thanks a lot for the example.

[rainoftime]

@wintersteiger

It is another formula that may trigger "Solution soundness bug in FP logic" (Perhaps it could be filed in another issue?)

[NikolajBjorner]

maybe to_ieee and to_real also need interpreted versions for MBQI to be sound.
But above cases are now handled (second diverges, but that is separate from being unsound).

[wintersteiger]

I've added the remaining ones in #6077. Although, to be honest, I would much prefer to teach MBQI to handle partially unspecified functions, I just don't have the time right now.