From 243275c63813873c2af86ff97a1e211515f48a82 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 24 Feb 2026 04:44:27 +0000 Subject: [PATCH 1/4] Initial plan From de3cf1889924557cf7ff650a4828bcb9b7efabfe Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 24 Feb 2026 05:22:54 +0000 Subject: [PATCH 2/4] Fix fp.to_real encoding for denormal floating-point values The mk_to_real function in fpa2bv_converter.cpp was missing the normalization shift adjustment (lz) when computing the real-valued exponent for denormal floating-point numbers. When unpack(x, sgn, sig, exp, lz, normalize=true) normalizes a denormal by shifting the significand left by lz positions, the returned exp does not account for this shift. All other callers (mk_mul, mk_div, mk_fma) correctly subtract lz from the exponent, but mk_to_real was missing this. The fix subtracts zero-extended lz from the sign-extended exp to get the true exponent, matching the convention used by other FP operations. Fixes incorrect model with (_ FloatingPoint 2 24) and fp.to_real. Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/fpa/fpa2bv_converter.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 288bcab4e..451ea6771 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2948,12 +2948,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); From add65451fdc6dc1ad005d32a0970eee3be90268d Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 25 Feb 2026 22:04:03 +0000 Subject: [PATCH 3/4] Add fpa regression test for fp.to_real denormal encoding fix Adds src/test/fpa.cpp with test_fp_to_real_denormal() exercising the bug reported in the issue: denormal floating-point values in (_ FloatingPoint 2 24) were getting wrong fp.to_real values because mk_to_real was not subtracting the normalization shift lz from the exponent. Tests verify: - The specific denormal from the bug report is NOT > 1.0 - Two other denormals have correct real values (0.5 and 0.125) - A normal value is correctly identified as > 1.0 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/test/CMakeLists.txt | 1 + src/test/fpa.cpp | 73 +++++++++++++++++++++++++++++++++++++++++ src/test/main.cpp | 1 + 3 files changed, 75 insertions(+) create mode 100644 src/test/fpa.cpp diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 31dd88078..1d5b5ce18 100644 --- a/src/test/CMakeLists.txt +++ b/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 diff --git a/src/test/fpa.cpp b/src/test/fpa.cpp new file mode 100644 index 000000000..589f43bdb --- /dev/null +++ b/src/test/fpa.cpp @@ -0,0 +1,73 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +--*/ + +// Regression tests for floating-point arithmetic encoding and model generation. + +#include "api/z3.h" +#include "util/debug.h" +#include + +// 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 = + "(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); + } + 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 = + "(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); + } + 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 = + "(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); + } + 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 = + "(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); + } + Z3_del_context(ctx); +} + +void tst_fpa() { + test_fp_to_real_denormal(); +} diff --git a/src/test/main.cpp b/src/test/main.cpp index a8158b99e..c5d55ebe1 100644 --- a/src/test/main.cpp +++ b/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); } From b4f7d057d3ff747a280f8bb0be6da0b203d755e4 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 26 Feb 2026 03:21:33 +0000 Subject: [PATCH 4/4] Add model_validate and invalid-check to fpa regression tests Add (set-option :model_validate true) to each SMT-LIB2 spec in src/test/fpa.cpp, and add ENSURE checks that the output does not contain the string "invalid". Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/test/fpa.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/test/fpa.cpp b/src/test/fpa.cpp index 589f43bdb..355c0a3e0 100644 --- a/src/test/fpa.cpp +++ b/src/test/fpa.cpp @@ -21,10 +21,12 @@ static void test_fp_to_real_denormal() { 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); @@ -33,11 +35,13 @@ static void test_fp_to_real_denormal() { 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); @@ -46,11 +50,13 @@ static void test_fp_to_real_denormal() { 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); @@ -59,11 +65,13 @@ static void test_fp_to_real_denormal() { 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); }