From de3cf1889924557cf7ff650a4828bcb9b7efabfe Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 24 Feb 2026 05:22:54 +0000 Subject: [PATCH] Fix fp.to_real encoding for denormal floating-point values 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> --- src/ast/fpa/fpa2bv_converter.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 288bcab4e..451ea6771 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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);