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(fp): correct negative exponent handling in fp.to_real conversion

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/81c038ae-52f7-4f2f-a14b-a661a81a7a0a

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-13 00:40:18 +00:00 • committed by GitHub
parent 4e3fbbe0d2
commit 6b22e37606
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 15 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2976,13 +2976,10 @@ 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);
two_exp2 = m_arith_util.mk_power(two, exp2);
expr_ref res(m), two_exp2(m), signed_exp(m), minus_res(m), sgn_is_1(m);
signed_exp = m.mk_ite(exp_is_neg, m_arith_util.mk_uminus(exp2), exp2);
two_exp2 = m_arith_util.mk_power(two, signed_exp);
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);

11
src/test/fpa.cpp
View file

@ -58,6 +58,17 @@ static void test_fp_to_real_denormal() {
"(assert (> (fp.to_real (fp #b0 #b01 #b11111111111111111111111)) 1.0))\n"
"(check-sat)\n",
true);
// Test 5: regression for soundness bug in fp.to_real with QF_FPLRA.
// The rational is exactly representable by (fp #b0 #b00000000 #b01001101101110000010001),
// so this equality must be satisfiable.
run_fp_test(
"(set-logic QF_FPLRA)\n"
"(set-option :model_validate true)\n"
"(assert (= (fp.to_real (fp #b0 #b00000000 #b01001101101110000010001))\n"
" (/ 2546705.0 713623846352979940529142984724747568191373312.0)))\n"
"(check-sat)\n",
true);
}
static void test_recfun_defined_function_soundness() {