mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix #6336
This commit is contained in:
parent
809838fede
commit
3c8c80bbac
|
@ -3431,8 +3431,14 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
|
|||
}
|
||||
else {
|
||||
expr_ref ll(m);
|
||||
ll = m_bv_util.mk_sign_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1)));
|
||||
ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, bv_sz-1)));
|
||||
ll = bv1;
|
||||
if (bv_sz > 1)
|
||||
ll = m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz - 1));
|
||||
ll = m_bv_util.mk_sign_extend(3, ll);
|
||||
if (bv_sz > 1)
|
||||
ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, bv_sz - 1)));
|
||||
else
|
||||
ul = m_bv_util.mk_numeral(0, 4);
|
||||
ovfl = m.mk_or(ovfl, m_bv_util.mk_sle(pre_rounded, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, bv_sz + 3))));
|
||||
pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded);
|
||||
in_range = m.mk_and(m.mk_not(ovfl),
|
||||
|
|
Loading…
Reference in a new issue