mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-01 03:11:30 +00:00
Code Activity

Fix fp.to_real encoding for denormal floating-point values

Browse source 
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>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-24 05:22:54 +00:00
parent 243275c638
commit de3cf18899
1 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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