mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 15:15:35 +00:00
Code Activity

Fix soundness bug in fpa2bv_converter::mk_to_real for negative exponents

Browse source 
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>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-13 00:11:00 +00:00 • committed by GitHub
parent 4a14a67b0e
commit a26a0da1dc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 28 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -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);

23
src/test/fpa.cpp
View file

@ -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();
}