Inconsistent answers on problems involving NaN and uninterpreted functions

[BrunoDutertre]

I have seen problems involving floating points terms t1 and t2 both equal to NaN that cause
inconsistent answers.

• on (not (= t1 t2)), z3 answers unsat.
• on (not (= (f t1) (f t2)) where f is an uninterpreted function, z3 answers sat.

Here's an example:

(set-logic ALL)
(declare-const c RoundingMode)
(declare-const x Float64)
(assert (not (= (fp.add c x (_ NaN 11 53))
                (fp.add c (_ NaN 11 53) x))))
(check-sat)

This gives unsat

Variant with uninterpreted function:

(set-logic ALL)
(declare-const c RoundingMode)
(declare-const x Float64)
(declare-sort T 0)
(declare-fun f (Float64) T)
(assert (not (= (f (fp.add c x (_ NaN 11 53)))
		(f (fp.add c (_ NaN 11 53) x)))))
(check-sat)

This gives sat

[BrunoDutertre]

With option model_validate=true, z3 produces an error on the variant with uninterpreted function:

> z3 model_validate=true test2.smt2
sat
(error "line 8 column 10: an invalid model was generated")

[LeventErkok]

I think the first example is OK actually. = on floats act as real equality, i.e., NaN == NaN. So, you get unsat. You should use fp.eq if you want floating-point equality, which stipulates NaN /= NaN.

I agree that the second example is bizarre, it should be unsat.

UPDATE: Never mind; upon second reading of your text, you never claimed the first one was bad. I agree; the first example is unsat correctly, the second should be too.

[BrunoDutertre]

Yes, I should have clarified that unsat is the right answer in both cases.

[nunoplopes]

You may want to pass rewriter.hi_fp_unspecified=true to disable NaN producing UFs.
(I use it and I've been happy since then)

[BrunoDutertre]

Thanks for the tip. I'll keep this in mind, but it doesn't work here. The problem here is NaN as input to UFs, not UF producing NaN.

[wintersteiger]

This is most likely a bug in my translation of UFs that depend on floats to UFs that depend on bit-vectors. It's definitely possible, if not likely, that I didn't treat NaNs correctly there. I'll try to make some time to sort this out soon.