From 7477e96e597030d8951e78fc4eed7c4e870e1a16 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Apr 2020 23:18:15 -0700 Subject: [PATCH] fix #3519 Signed-off-by: Nikolaj Bjorner --- src/ast/fpa/fpa2bv_converter.cpp | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index e1f06e4b2..1d621d787 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1109,7 +1109,7 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r // else the actual remainder. // max. exponent difference is (2^ebits) - 3 const mpz & two_to_ebits = fu().fm().m_powers2(ebits); - mpz max_exp_diff; + scoped_mpz max_exp_diff(m_mpz_manager); m_mpz_manager.sub(two_to_ebits, 3, max_exp_diff); if (m_mpz_manager.gt(max_exp_diff, INT32_MAX)) // because zero-extend allows only int params... @@ -1139,7 +1139,7 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r // (using the lazy bit-blaster helps on simple instances). expr_ref lshift(m), rshift(m), shifted(m), huge_rem(m), huge_div(m), huge_div_is_even(m); expr_ref a_sig_ext_l = a_sig, b_sig_ext_l = b_sig; - mpz remaining; + scoped_mpz remaining(m_mpz_manager); m_mpz_manager.set(remaining, max_exp_diff); while (m_mpz_manager.gt(remaining, INT32_MAX)) { SASSERT(false); // zero-extend ast's expect int params which would overflow. @@ -1156,14 +1156,15 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r a_sig_ext = m_bv_util.mk_concat(a_sig_ext_l, m_bv_util.mk_numeral(0, 3)); b_sig_ext = m_bv_util.mk_concat(b_sig_ext_l, m_bv_util.mk_numeral(0, 3)); - mpz max_exp_diff_adj; + scoped_mpz max_exp_diff_adj(m_mpz_manager); m_mpz_manager.add(max_exp_diff, sbits, max_exp_diff_adj); m_mpz_manager.sub(max_exp_diff_adj, ebits, max_exp_diff_adj); m_mpz_manager.add(max_exp_diff_adj, 1, max_exp_diff_adj); expr_ref edr_tmp = exp_diff, nedr_tmp = neg_exp_diff; m_mpz_manager.set(remaining, max_exp_diff_adj); + unsigned num_rounds = 0; while (m_mpz_manager.gt(remaining, INT32_MAX)) { - SASSERT(false); // zero-extend ast's expect int params which would overflow. + throw default_exception("zero extension overflow floating point types are too large"); edr_tmp = m_bv_util.mk_zero_extend(INT32_MAX, edr_tmp); nedr_tmp = m_bv_util.mk_zero_extend(INT32_MAX, nedr_tmp); m_mpz_manager.sub(remaining, INT32_MAX, remaining); @@ -1175,10 +1176,6 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r lshift = edr_tmp; rshift = nedr_tmp; - m_mpz_manager.del(remaining); - m_mpz_manager.del(max_exp_diff); - m_mpz_manager.del(max_exp_diff_adj); - shifted = m.mk_ite(exp_diff_is_neg, m_bv_util.mk_bv_ashr(a_sig_ext, rshift), m_bv_util.mk_bv_shl(a_sig_ext, lshift)); huge_rem = m_bv_util.mk_bv_urem(shifted, b_sig_ext);