mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

fix #3519

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-04 23:18:15 -07:00
parent 5516e420a1
commit 7477e96e59
1 changed files with 5 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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);