diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index d7ba25904..d2431174e 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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);