`unknown` on trivially valid goals over `to_fp(to_real(x))`. Every assignment is a model, but Z3 finds none

[Zac-HD]

I found this while working on pschanely/CrossHair#482, and had Claude investigate and draft this report for me. It looks like it's just a few more cases which #6548 / #6968 missed.

Z3 version: 4.15.4.0 (pip z3-solver==4.15.4.0), Python 3.11, Linux x86_64.

Repro (Python bindings)

import z3

x = z3.Int("x")
f = z3.fpRealToFP(z3.RNE(), z3.ToReal(x), z3.Float64())

s = z3.Solver()
s.add(z3.Not(z3.fpIsNaN(f)))
print(s.check())            # unknown  (expected: sat)
print(s.reason_unknown())   # smt tactic failed to show goal to be sat/unsat
                            #   (incomplete (theory arithmetic))

The goal is valid: (_ to_fp 11 53) rm (to_real x) never yields NaN, so every assignment of x is a model. e.g. x = 0 gives +zero, for which fp.isNaN is false. fpEQ shows the same behavior, which is how we hit this in practice:

s = z3.Solver()
s.add(z3.Not(z3.fpEQ(f, z3.fpNaN(z3.Float64()))))
print(s.check())            # unknown  (expected: sat — again valid)

The unsatisfiable polarity of the same terms is answered correctly:

s = z3.Solver()
s.add(z3.fpIsNaN(f))
print(s.check())            # unsat (correct)

So unknown only arises on the side where the solver must produce a model, even though any value of x would do.

Variations

Assertion	Result
Not(fpIsNaN(to_fp(to_real(x)))), x: Int	unknown
Not(fpIsNaN(to_fp(r))), r: Real	unknown
Not(fpEQ(to_fp(to_real(x)), NaN)), x: Int	unknown
fpIsNaN(to_fp(to_real(x)))	unsat ✓
Not(fpIsNaN(to_fp(to_real(x)))) ∧ x == 3	sat ✓

Arbitrarily constraining the integer value moves us from unknown to sat.