[Refutational Soundness Bug] Incorrect UNSAT in Real-to-FP conversion with RNE/RNA overflow

[wingsyuyi-satori]

Hello, I encountered a refutational soundness bug where Z3 incorrectly returns unsat for a satisfiable input involving Real-to-FloatingPoint conversion (to_fp). The issue appears specific to RNE and RNA rounding modes when handling negative overflow.

Input:

(set-logic ALL)
(declare-fun x () Real)

;; Hint 1: Range constraint (Z3 still fails, cvc5 succeeds)
;(assert (< x -1000000000000000000000000000000000000001.0))

;; Hint 2: Equality constraint (Z3 succeeds)
;(assert (= x -1000000000000000000000000000000000000002.0))

(assert 
  (not 
    (<= 0.0 
      (ite (fp.isInfinite ((_ to_fp 8 24) RNE x)) 
           x 
           0.0
      )
    )
  )
)
(check-sat)
(get-value (x))

Observed Behavior:

1. Default (No hints): Z3 returns unsat. cvc5 timeouts.
2. With Hint 1 (Range < -1e40): Z3 still returns unsat. (Note: cvc5 correctly returns sat with this hint).
3. With Hint 2 (Equality = -1e40): Z3 correctly returns sat.
4. With RTN rounding: If RNE is changed to RTN, Z3 correctly returns sat.

Expected Behavior:
The input should be sat for RNE, RNA, and RTN rounding modes.

Analysis:
The input requires x to be a large negative number such that to_fp overflows to -oo, causing fp.isInfinite to be true.
According to the IEEE 754-2008 standard (Section 7.4 Overflow):

a) roundTiesToEven and roundTiesToAway carry all overflows to ∞ with the sign of the intermediate result.
...
c) roundTowardNegative carries positive overflows to the format’s largest finite number, and carries negative overflows to −∞.
d) roundTowardPositive carries negative overflows to the format’s most negative finite number, and carries positive overflows to +∞.

Z3 currently handles RTN correctly (case c), but fails to produce infinity for RNE and RNA (case a) in this example.

Further Observation:
I suspect a symmetric issue exists for positive overflow: RNE and RNA similarly fail to produce positive infinity in the reverse case, whereas RTP (Round Toward Positive) functions correctly. This suggests the underlying issue with "Nearest" rounding modes likely affects both positive and negative overflow boundaries. You may want to investigate this symmetric case as well.

Commit:
eca8e19