Add issue 10175 floating-point regressions

regressions/smt2/10175-wide.expected.out

@@ -0,0 +1,5 @@
+unsat
+unsat
+unsat
+unsat
+unsat

regressions/smt2/10175-wide.smt2

@@ -0,0 +1,45 @@
+; Exact quotient across a wrapped denormal count.
+(set-logic QF_FP)
+(push)
+(declare-fun d_2_8 () (_ FloatingPoint 2 8))
+(assert (fp.eq d_2_8 (fp #b0 #b00 #b0001000)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b00 #b0010000) d_2_8)
+  (fp #b0 #b10 #b0000000))))
+(check-sat)
+(pop)
+; Two-bit workspace growth: max finite / min subnormal.
+(push)
+(declare-fun d_2_16_upper () (_ FloatingPoint 2 16))
+(assert (fp.eq d_2_16_upper (fp #b0 #b00 #b000000000000001)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b10 #b111111111111111) d_2_16_upper)
+  (fp #b0 #b10 #b111111111111111))))
+(check-sat)
+(pop)
+; Two-bit workspace growth: min subnormal / max finite.
+(push)
+(declare-fun d_2_16_lower () (_ FloatingPoint 2 16))
+(assert (fp.eq d_2_16_lower (fp #b0 #b10 #b111111111111111)))
+(assert (not (fp.eq
+  (fp.div RTP (fp #b0 #b00 #b000000000000001) d_2_16_lower)
+  (fp #b0 #b00 #b000000000000001))))
+(check-sat)
+(pop)
+; Exponent above the rounder's signed workspace: max finite / min subnormal.
+(push)
+(declare-fun d_2_8_upper () (_ FloatingPoint 2 8))
+(assert (fp.eq d_2_8_upper (fp #b0 #b00 #b0000001)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b10 #b1111111) d_2_8_upper)
+  (fp #b0 #b10 #b1111111))))
+(check-sat)
+(pop)
+; Exponent below the rounder's signed workspace: min subnormal / max finite.
+(push)
+(declare-fun d_2_8_lower () (_ FloatingPoint 2 8))
+(assert (fp.eq d_2_8_lower (fp #b0 #b10 #b1111111)))
+(assert (not (fp.eq
+  (fp.div RTP (fp #b0 #b00 #b0000001) d_2_8_lower)
+  (fp #b0 #b00 #b0000001))))
+(check-sat)

regressions/smt2/10175.expected.out

@@ -0,0 +1,19 @@
+unsat
+unsat
+unsat
+unsat
+unsat
+unsat
+unsat
+unsat
+unsat
+unsat
+unsat
+unsat
+unsat
+unsat
+unsat
+unsat
+unsat
+unsat
+sat

regressions/smt2/10175.smt2

@@ -0,0 +1,170 @@
+; Regression for Z3 issue #10175.
+(set-logic QF_FP)
+(set-option :model_validate true)
+; pre-wrap control: exact quotient is 2.0.
+(push)
+(declare-fun d_2_4 () (_ FloatingPoint 2 4))
+(assert (fp.eq d_2_4 (fp #b0 #b00 #b001)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b00 #b010) d_2_4)
+  (fp #b0 #b10 #b000))))
+(check-sat)
+(pop)
+; first wrapped count: exact quotient is 2.0.
+(push)
+(declare-fun d_2_5 () (_ FloatingPoint 2 5))
+(assert (fp.eq d_2_5 (fp #b0 #b00 #b0001)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b00 #b0010) d_2_5)
+  (fp #b0 #b10 #b0000))))
+(check-sat)
+(pop)
+; reported format: exact quotient is 2.0.
+(push)
+(declare-fun d_2_6 () (_ FloatingPoint 2 6))
+(assert (fp.eq d_2_6 (fp #b0 #b00 #b00010)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b00 #b00100) d_2_6)
+  (fp #b0 #b10 #b00000))))
+(check-sat)
+(pop)
+; largest format covered by ebits+2 exponent workspace: exact quotient is 2.0.
+(push)
+(declare-fun d_2_7 () (_ FloatingPoint 2 7))
+(assert (fp.eq d_2_7 (fp #b0 #b00 #b000100)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b00 #b001000) d_2_7)
+  (fp #b0 #b10 #b000000))))
+(check-sat)
+(pop)
+; FP(2,7) upper exponent endpoint: max finite / min subnormal = 254.
+(push)
+(declare-fun d_2_7_upper () (_ FloatingPoint 2 7))
+(assert (fp.eq d_2_7_upper (fp #b0 #b00 #b000001)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b10 #b111111) d_2_7_upper)
+  (fp #b0 #b10 #b111111))))
+(check-sat)
+(pop)
+; FP(2,7) lower exponent endpoint: min subnormal / max finite = 1/254.
+(push)
+(declare-fun d_2_7_lower () (_ FloatingPoint 2 7))
+(assert (fp.eq d_2_7_lower (fp #b0 #b10 #b111111)))
+(assert (not (fp.eq
+  (fp.div RTP (fp #b0 #b00 #b000001) d_2_7_lower)
+  (fp #b0 #b00 #b000001))))
+(check-sat)
+(pop)
+; pre-wrap control: exact quotient is 2.0.
+(push)
+(declare-fun d_3_8 () (_ FloatingPoint 3 8))
+(assert (fp.eq d_3_8 (fp #b0 #b000 #b0000001)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b000 #b0000010) d_3_8)
+  (fp #b0 #b100 #b0000000))))
+(check-sat)
+(pop)
+; first wrapped count: exact quotient is 2.0.
+(push)
+(declare-fun d_3_9 () (_ FloatingPoint 3 9))
+(assert (fp.eq d_3_9 (fp #b0 #b000 #b00000001)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b000 #b00000010) d_3_9)
+  (fp #b0 #b100 #b00000000))))
+(check-sat)
+(pop)
+; largest wide-LZ format covered by the ebits+2 exponent workspace: exact quotient is 2.0.
+(push)
+(declare-fun d_3_11 () (_ FloatingPoint 3 11))
+(assert (fp.eq d_3_11 (fp #b0 #b000 #b0000000100)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b000 #b0000001000) d_3_11)
+  (fp #b0 #b100 #b0000000000))))
+(check-sat)
+(pop)
+; First FP(3,*) exponent outside the ebits+2 workspace: max finite / min subnormal.
+(push)
+(declare-fun d_3_12_upper () (_ FloatingPoint 3 12))
+(assert (fp.eq d_3_12_upper (fp #b0 #b000 #b00000000001)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b110 #b11111111111) d_3_12_upper)
+  (fp #b0 #b110 #b11111111111))))
+(check-sat)
+(pop)
+; Opposite FP(3,12) endpoint: min subnormal / max finite.
+(push)
+(declare-fun d_3_12_lower () (_ FloatingPoint 3 12))
+(assert (fp.eq d_3_12_lower (fp #b0 #b110 #b11111111111)))
+(assert (not (fp.eq
+  (fp.div RTP (fp #b0 #b000 #b00000000001) d_3_12_lower)
+  (fp #b0 #b000 #b00000000001))))
+(check-sat)
+(pop)
+; pre-wrap control: exact quotient is 2.0.
+(push)
+(declare-fun d_4_16 () (_ FloatingPoint 4 16))
+(assert (fp.eq d_4_16 (fp #b0 #b0000 #b000000000000001)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b0000 #b000000000000010) d_4_16)
+  (fp #b0 #b1000 #b000000000000000))))
+(check-sat)
+(pop)
+; first wrapped count: exact quotient is 2.0.
+(push)
+(declare-fun d_4_17 () (_ FloatingPoint 4 17))
+(assert (fp.eq d_4_17 (fp #b0 #b0000 #b0000000000000001)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b0000 #b0000000000000010) d_4_17)
+  (fp #b0 #b1000 #b0000000000000000))))
+(check-sat)
+(pop)
+; largest wide-LZ format covered by the ebits+2 exponent workspace: exact quotient is 2.0.
+(push)
+(declare-fun d_4_19 () (_ FloatingPoint 4 19))
+(assert (fp.eq d_4_19 (fp #b0 #b0000 #b000000000000000100)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b0000 #b000000000000001000) d_4_19)
+  (fp #b0 #b1000 #b000000000000000000))))
+(check-sat)
+(pop)
+; First FP(4,*) exponent outside the ebits+2 workspace: max finite / min subnormal.
+(push)
+(declare-fun d_4_20_upper () (_ FloatingPoint 4 20))
+(assert (fp.eq d_4_20_upper (fp #b0 #b0000 #b0000000000000000001)))
+(assert (not (fp.eq
+  (fp.div RTZ (fp #b0 #b1110 #b1111111111111111111) d_4_20_upper)
+  (fp #b0 #b1110 #b1111111111111111111))))
+(check-sat)
+(pop)
+; Opposite FP(4,20) endpoint: min subnormal / max finite.
+(push)
+(declare-fun d_4_20_lower () (_ FloatingPoint 4 20))
+(assert (fp.eq d_4_20_lower (fp #b0 #b1110 #b1111111111111111111)))
+(assert (not (fp.eq
+  (fp.div RTP (fp #b0 #b0000 #b0000000000000000001) d_4_20_lower)
+  (fp #b0 #b0000 #b0000000000000000001))))
+(check-sat)
+(pop)
+; Reported negative-overflow case: -3.25 / 1/16 = -52 in FP(2,6).
+(push)
+(declare-fun d_rtz () (_ FloatingPoint 2 6))
+(assert (fp.eq d_rtz (fp #b0 #b00 #b00010)))
+(assert (fp.eq (fp.div RTZ (fp #b1 #b10 #b10100) d_rtz) (_ -oo 2 6)))
+(check-sat)
+(pop)
+; Original issue path through real-to-FP conversion and model validation.
+(push)
+(define-fun a () (_ FloatingPoint 2 6) (_ -oo 2 6))
+(declare-fun b () (_ FloatingPoint 2 6))
+(define-fun c () (_ FloatingPoint 2 6) ((_ to_fp 2 6) RTZ -3.25))
+(assert (and
+  (fp.eq b ((_ to_fp 2 6) RTZ 0.0625))
+  (fp.eq a (fp.div RTZ c b))))
+(check-sat)
+(pop)
+(push)
+(declare-fun d_rtn () (_ FloatingPoint 2 6))
+(assert (fp.eq d_rtn (fp #b0 #b00 #b00010)))
+(assert (fp.eq (fp.div RTN (fp #b1 #b10 #b10100) d_rtn) (_ -oo 2 6)))
+(check-sat)
+(pop)