[Solution Soundness Bug] Incorrect SAT in Float32 FP/Real round-trip arithmetic.

Z3 reports sat for an unsat formula.

Input:

(set-logic ALL)
(declare-const F Int)

(assert
  (and
    (< F 1)
    (>
      (let ((f ((_ to_fp 8 24) RTN (to_real F))))
        (ite
          (fp.isInfinite f)
          0
          (to_int
            (fp.to_real
              (fp.roundToIntegral RTN f)))))
      0)))

(check-sat)

Output:

$ z3 test.smt2 model_validate=true
sat
(error "line 18 column 10: an invalid model was generated")
$ cvc5 test.smt2
unsat

The formula is unsatisfiable.

Because F is an integer and F < 1, we have F <= 0. Converting it to Float32 with RTN therefore produces either -oo or a finite non-positive float. In the former case the ite returns 0; in the latter case, fp.roundToIntegral RTN, fp.to_real, and to_int cannot make the value positive. Thus the asserted expression cannot be greater than 0.

Without model validation, adding (get-model) produces the following model:

sat
(
  (define-fun F () Int
    0)
  (define-fun /0 ((x!0 Real) (x!1 Real)) Real
    (ite (and (= x!0 1.0) (= x!1 17592186044416.0)) (/ 1.0 17592186044416.0)
      (/ 1.0 85070591730234615865843651857942052864.0)))
)

With a debug build the same behavior takes noticeably longer to trigger, but the outcome is identical. cvc5 returns unsat on this input. On release builds, 4.16.0 answers unknown, while 5.0.0 answers sat.

Commit: 1c899374739f7c1cdbe6ba72dd61aa1d7daaee27