From 2f7ff6217322386590db9ba3c04c6bf604cc3b2e Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 13 May 2026 06:11:36 -0400 Subject: [PATCH] Fix soundness bug in fpa2bv mk_to_real: wrong exponent power for negative exponents (#9513) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `fpa2bv_converter::mk_to_real` computed `2^(1/|exp|)` instead of `1/(2^|exp|)` for floats with negative exponents, causing the NRA solver to reach contradictory conclusions and return spurious `unsat` for satisfiable QF_FPLRA formulas. ## Root Cause After the loop that evaluates `exp2 = |unbiased_exp|` as an integer, the code took `1/exp2` (reciprocal of the integer) before calling `mk_power`, yielding `2^(1/3)` instead of `2^(-3) = 1/8` for a float with exponent -3: ```cpp // Buggy one_div_exp2 = mk_div(one, exp2); // 1/|exp|, not 1/2^|exp| exp2 = mk_ite(exp_is_neg, one_div_exp2, exp2); two_exp2 = mk_power(two, exp2); // 2^(1/3) ≠ 1/8 for exp=-3 ``` ## Fix Compute the power of 2 first, then invert it: ```cpp // Fixed two_exp2 = mk_power(two, exp2); // 2^|exp| one_div_two_exp2 = mk_div(one, two_exp2); // 1/(2^|exp|) two_exp2 = mk_ite(exp_is_neg, one_div_two_exp2, two_exp2); // correct 2^exp ``` ## Impact - **QF_FPLRA**: `to_fp(RTZ, r)` with a symbolic real `r` constrained to an interval containing a float's exact rational value now correctly returns `sat`. - **fp.to_real**: Fixes incorrect real-valued encoding for all floats with negative exponents, including denormals (which adjust the exponent by subtracting leading-zero count). A regression test covering the reported case is added to `src/test/fpa.cpp`. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/fpa/fpa2bv_converter.cpp | 13 ++++++------- src/test/fpa.cpp | 23 +++++++++++++++++++++++ 2 files changed, 29 insertions(+), 7 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 5e02a101e..d2431174e 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2976,13 +2976,12 @@ 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 two_exp2(m), one_div_two_exp2(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); + expr_ref res(m), minus_res(m), sgn_is_1(m); 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 +2989,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(); }