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

Improve readability: split variable declaration in mk_to_real

Browse source 
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:12:06 +00:00 • committed by GitHub
parent a26a0da1dc
commit e5e7cea767
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2976,11 +2976,12 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
prev_bit = bit;
}
expr_ref res(m), two_exp2(m), one_div_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);