mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Fixed overflow problem in fp.to_?bv. Thanks to Florian Schanda for reporting this bug.
This commit is contained in:
parent
793642f48d
commit
328ad248b6
|
@ -3241,18 +3241,20 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
|
|||
dbg_decouple("fpa2bv_to_bv_inc", inc);
|
||||
dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded);
|
||||
|
||||
pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded);
|
||||
|
||||
expr_ref ll(m), ul(m), in_range(m);
|
||||
expr_ref ul(m), ovfl(m), in_range(m);
|
||||
if (!is_signed) {
|
||||
ll = m_bv_util.mk_numeral(0, bv_sz+3);
|
||||
ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_numeral(-1, bv_sz));
|
||||
in_range = m.mk_and(m.mk_not(x_is_neg), m_bv_util.mk_ule(pre_rounded, ul));
|
||||
}
|
||||
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_numeral(-1, bv_sz-1));
|
||||
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), m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul));
|
||||
dbg_decouple("fpa2bv_to_bv_in_range_ll", ll);
|
||||
}
|
||||
in_range = m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul));
|
||||
dbg_decouple("fpa2bv_to_bv_in_range_ul", ul);
|
||||
dbg_decouple("fpa2bv_to_bv_in_range", in_range);
|
||||
|
||||
expr_ref rounded(m);
|
||||
|
|
Loading…
Reference in a new issue