[Refutational Soundness Bug] Incorrect UNSAT in Float32 FP/Real round-trip arithmetic.

[wingsyuyi-satori]

Z3 debug build incorrectly reports unsat on the following satisfiable formula.

Input:

(declare-fun a () Float32)
(declare-fun t () Float32)

(assert (fp.eq a ((_ to_fp 8 24) RNE 1.0)))
(assert (fp.eq t ((_ to_fp 8 24) RNE 0.8)))

(assert
  (fp.eq
    (fp.add RNE a t)
      ((_ to_fp 8 24)
        RNE
        (+ 1.0 (fp.to_real t)))))
(check-sat)

Output:

z3 test.smt2 
unsat

On the left, we take values obtained from real numbers, convert them into Float32, and then perform computations directly in floating-point arithmetic.

On the right, we first convert those Float32 values back into real numbers, perform the computation in exact real arithmetic, and then convert the result back into Float32.

The assertion states that both approaches should produce the same Float32 result.

This is easily resolvable, as shown by the valid model produced by cvc5.

sat
(
(define-fun a () (_ FloatingPoint 8 24) (fp #b0 #b01111111 #b00000000000000000000000))
(define-fun t () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b10011001100110011001101))
)

Substituting the model back into the benchmark also yields sat in both Z3 and cvc5.

Commit: 6fd303c