From a26a0da1dcedf6dff88835d64df803a2c1342b4a Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 13 May 2026 00:11:00 +0000 Subject: [PATCH] Fix soundness bug in fpa2bv_converter::mk_to_real for negative exponents MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The mk_to_real function in fpa2bv_converter.cpp incorrectly computed the exponent scaling factor for floats with negative exponents. The code was computing 2^(1/|exp|) instead of 1/(2^|exp|) = 2^(-|exp|). Root cause: after the loop that computed exp2 = |unbiased_exp| as an integer, the code did: one_div_exp2 = 1/exp2 (computed 1/|exp|, NOT 1/2^|exp|) exp2 = ite(exp_is_neg, one_div_exp2, exp2) two_exp2 = mk_power(two, exp2) -> gives 2^(1/|exp|) for negative exp For example, for exp=-3 (as in Float32(0xBE7BE653)): OLD (buggy): two_exp2 = 2^(1/3) ≈ 1.26 (wrong) NEW (fixed): two_exp2 = 1/8 (correct: 2^(-3) = 1/8) Fix: compute two_exp2 = 2^|exp| first, then use 1/two_exp2 for negative exponents: two_exp2 = mk_power(two, exp2) (2^|exp|) one_div_two_exp2 = 1/two_exp2 (1/2^|exp| = 2^(-|exp|)) two_exp2 = ite(exp_is_neg, one_div_two_exp2, two_exp2) This bug affected: 1. QF_FPLRA: to_fp(RTZ, r) for symbolic real r in an interval containing the exact rational value of a float returned UNSAT instead of SAT 2. fp.to_real: incorrect results for floats with negative exponents, including denormals (which had the same issue via the lz subtraction) Adds regression test in src/test/fpa.cpp for the to_fp (from real) case. Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/56265d81-608a-4768-8c4d-30bd740d89fb Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/fpa/fpa2bv_converter.cpp | 12 +++++------- src/test/fpa.cpp | 23 +++++++++++++++++++++++ 2 files changed, 28 insertions(+), 7 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 5e02a101e..d7ba25904 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2976,13 +2976,11 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar prev_bit = bit; } - expr_ref one_div_exp2(m); - one_div_exp2 = m_arith_util.mk_div(one, exp2); - exp2 = m.mk_ite(exp_is_neg, one_div_exp2, exp2); - dbg_decouple("fpa2bv_to_real_exp2", exp2); - - expr_ref res(m), two_exp2(m), minus_res(m), sgn_is_1(m); + expr_ref res(m), two_exp2(m), one_div_two_exp2(m), minus_res(m), sgn_is_1(m); two_exp2 = m_arith_util.mk_power(two, exp2); + one_div_two_exp2 = m_arith_util.mk_div(one, two_exp2); + two_exp2 = m.mk_ite(exp_is_neg, one_div_two_exp2, two_exp2); + dbg_decouple("fpa2bv_to_real_exp2", two_exp2); res = m_arith_util.mk_mul(rsig, two_exp2); minus_res = m_arith_util.mk_uminus(res); sgn_is_1 = m.mk_eq(sgn, bv1); @@ -2990,7 +2988,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar dbg_decouple("fpa2bv_to_real_sig_times_exp2", res); TRACE(fpa2bv_to_real, tout << "rsig = " << mk_ismt2_pp(rsig, m) << std::endl; - tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;); + tout << "two_exp2 = " << mk_ismt2_pp(two_exp2, m) << std::endl;); expr_ref unspec(m); mk_to_real_unspecified(f, num, args, unspec); diff --git a/src/test/fpa.cpp b/src/test/fpa.cpp index 217cb641b..632865cee 100644 --- a/src/test/fpa.cpp +++ b/src/test/fpa.cpp @@ -60,6 +60,28 @@ static void test_fp_to_real_denormal() { true); } +// Regression test for soundness bug in to_fp (from real) with symbolic real interval. +// When the rounding mode is RTZ and the real variable is constrained to an interval +// that includes the exact rational value of a float, Z3 should return SAT. +// This was broken because mk_to_real computed 2^(1/|exp|) instead of 1/(2^|exp|) +// for floats with negative exponents, causing a conflict in the NRA solver. +static void test_to_fp_from_real_interval() { + // The interval (-4127125/16777216, -16508499/67108864] contains -16508499/67108864 + // which is the exact rational value of fp #b1 #b01111100 #b11110111110011001010011. + // to_fp(RTZ, r) for r in this closed interval must equal that float. + run_fp_test( + "(set-logic QF_FPLRA)\n" + "(declare-const x Float32)\n" + "(assert (= x (fp #b1 #b01111100 #b11110111110011001010011)))\n" + "(declare-const r Real)\n" + "(assert (and (> r (- (/ 4127125.0 16777216.0))) (<= r (- (/ 16508499.0 67108864.0)))))\n" + "(declare-const w Float32)\n" + "(assert (= w ((_ to_fp 8 24) RTZ r)))\n" + "(assert (= x w))\n" + "(check-sat)\n", + true); +} + static void test_recfun_defined_function_soundness() { run_fp_test( "(set-option :model_validate true)\n" @@ -75,5 +97,6 @@ static void test_recfun_defined_function_soundness() { void tst_fpa() { test_fp_to_real_denormal(); + test_to_fp_from_real_interval(); test_recfun_defined_function_soundness(); }