Merge pull request #8748 from Z3Prover/copilot/fix-floating-point-model-validation

Fix fp.to_real bitvector encoding for denormal floating-point values

src/ast/fpa/fpa2bv_converter.cpp

@@ -2953,12 +2953,16 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
     dbg_decouple("fpa2bv_to_real_rsig", rsig);
 
     expr_ref exp_n(m), exp_p(m), exp_is_neg(m), exp_abs(m);
-    exp_is_neg = m.mk_eq(m_bv_util.mk_extract(ebits - 1, ebits - 1, exp), bv1);
-    dbg_decouple("fpa2bv_to_real_exp_is_neg", exp_is_neg);
     exp_p = m_bv_util.mk_sign_extend(1, exp);
+    // Subtract the normalization shift for denormals (lz is 0 for normals)
+    expr_ref lz_ext(m);
+    lz_ext = m_bv_util.mk_zero_extend(1, lz);
+    exp_p = m_bv_util.mk_bv_sub(exp_p, lz_ext);
+    exp_is_neg = m.mk_eq(m_bv_util.mk_extract(ebits, ebits, exp_p), bv1);
+    dbg_decouple("fpa2bv_to_real_exp_is_neg", exp_is_neg);
     exp_n = m_bv_util.mk_bv_neg(exp_p);
     exp_abs = m.mk_ite(exp_is_neg, exp_n, exp_p);
-    dbg_decouple("fpa2bv_to_real_exp_abs", exp);
+    dbg_decouple("fpa2bv_to_real_exp_abs", exp_abs);
     SASSERT(m_bv_util.get_bv_size(exp_abs) == ebits + 1);
 
     expr_ref exp2(m), exp2_mul_2(m), prev_bit(m);

src/test/CMakeLists.txt

@@ -58,6 +58,7 @@ add_executable(test-z3
   f2n.cpp
   finite_set.cpp
   finite_set_rewriter.cpp
+  fpa.cpp
   factor_rewriter.cpp
   finder.cpp
   fixed_bit_vector.cpp

src/test/fpa.cpp

@@ -0,0 +1,81 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+--*/
+
+// Regression tests for floating-point arithmetic encoding and model generation.
+
+#include "api/z3.h"
+#include "util/debug.h"
+#include <string.h>
+
+// Test that fp.to_real produces correct values for denormal floating-point numbers.
+// Regression test for: incorrect model with (_ FloatingPoint 2 24) and fp.to_real.
+// Denormal numbers require subtracting the normalization shift (lz) from the exponent;
+// without this fix, denormals in fp.to_real were ~2^lz times too large.
+static void test_fp_to_real_denormal() {
+    Z3_context ctx;
+
+    // Test 1: the specific denormal from the bug report (fp #b0 #b00 #b00111011011111001011101)
+    // has fp.to_real ~= 0.232, which must NOT be > 1.0
+    ctx = Z3_mk_context(nullptr);
+    {
+        const char * spec =
+            "(set-option :model_validate true)\n"
+            "(assert (> (fp.to_real (fp #b0 #b00 #b00111011011111001011101)) 1.0))\n"
+            "(check-sat)\n";
+        const char * result = Z3_eval_smtlib2_string(ctx, spec);
+        ENSURE(strstr(result, "unsat") != nullptr);
+        ENSURE(strstr(result, "invalid") == nullptr);
+    }
+    Z3_del_context(ctx);
+
+    // Test 2: denormal with leading significand bit = 1, fp.to_real should be 0.5
+    // (fp #b0 #b00 #b10000000000000000000000) in (_ FloatingPoint 2 24)
+    ctx = Z3_mk_context(nullptr);
+    {
+        const char * spec =
+            "(set-option :model_validate true)\n"
+            "(assert (= (fp.to_real (fp #b0 #b00 #b10000000000000000000000)) (/ 1.0 2.0)))\n"
+            "(check-sat)\n";
+        const char * result = Z3_eval_smtlib2_string(ctx, spec);
+        ENSURE(strstr(result, "sat") != nullptr);
+        ENSURE(strstr(result, "unsat") == nullptr);
+        ENSURE(strstr(result, "invalid") == nullptr);
+    }
+    Z3_del_context(ctx);
+
+    // Test 3: denormal with significand bit pattern giving fp.to_real = 0.125
+    // (fp #b0 #b00 #b00100000000000000000000) in (_ FloatingPoint 2 24)
+    ctx = Z3_mk_context(nullptr);
+    {
+        const char * spec =
+            "(set-option :model_validate true)\n"
+            "(assert (= (fp.to_real (fp #b0 #b00 #b00100000000000000000000)) (/ 1.0 8.0)))\n"
+            "(check-sat)\n";
+        const char * result = Z3_eval_smtlib2_string(ctx, spec);
+        ENSURE(strstr(result, "sat") != nullptr);
+        ENSURE(strstr(result, "unsat") == nullptr);
+        ENSURE(strstr(result, "invalid") == nullptr);
+    }
+    Z3_del_context(ctx);
+
+    // Test 4: a normal value (fp #b0 #b01 #b11111111111111111111111) must be > 1.0
+    // This is the maximum finite normal number in (_ FloatingPoint 2 24)
+    ctx = Z3_mk_context(nullptr);
+    {
+        const char * spec =
+            "(set-option :model_validate true)\n"
+            "(assert (> (fp.to_real (fp #b0 #b01 #b11111111111111111111111)) 1.0))\n"
+            "(check-sat)\n";
+        const char * result = Z3_eval_smtlib2_string(ctx, spec);
+        ENSURE(strstr(result, "sat") != nullptr);
+        ENSURE(strstr(result, "unsat") == nullptr);
+        ENSURE(strstr(result, "invalid") == nullptr);
+    }
+    Z3_del_context(ctx);
+}
+
+void tst_fpa() {
+    test_fp_to_real_denormal();
+}

src/test/main.cpp

@@ -287,4 +287,5 @@ int main(int argc, char ** argv) {
     TST(ho_matcher);
     TST(finite_set);
     TST(finite_set_rewriter);
+    TST(fpa);
 }