mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-10 19:07:18 +00:00
Code Activity

Fix soundness bug in fpa2bv mk_to_real: wrong exponent power for negative exponents (#9513)

Browse source 
`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>
This commit is contained in:
Copilot 2026-05-13 06:11:36 -04:00 • committed by GitHub
parent 6dfb5ab44f
commit 2f7ff62173
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 29 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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