mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

Bugfix for fp.to_sbv. Thanks to Florian Schanda for reporting this bug.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2018-04-05 19:55:41 +01:00
parent 724f86d43e
commit 02bf2530b5
1 changed files with 13 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3241,24 +3241,29 @@ 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_inc", inc);
dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded); dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded);
expr_ref ul(m), ovfl(m), in_range(m); expr_ref incd(m), pr_is_zero(m), ovfl(m);
if (!is_signed) {
expr_ref incd(m), pr_is_zero(m);
incd = m.mk_eq(rounding_decision, bv1); incd = m.mk_eq(rounding_decision, bv1);
pr_is_zero = m.mk_eq(pre_rounded, m_bv_util.mk_numeral(0, bv_sz + 3)); pr_is_zero = m.mk_eq(pre_rounded, m_bv_util.mk_numeral(0, bv_sz + 3));
ovfl = m.mk_and(incd, pr_is_zero);
expr_ref ul(m), in_range(m);
if (!is_signed) {
ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_numeral(-1, bv_sz)); 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), in_range = m.mk_and(m.mk_not(x_is_neg), m.mk_not(ovfl),
m.mk_not(m.mk_and(incd, pr_is_zero)),
m_bv_util.mk_ule(pre_rounded, ul)); m_bv_util.mk_ule(pre_rounded, ul));
} }
else { else {
expr_ref ll(m); 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))); 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)); 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); ovfl = m.mk_or(ovfl, m_bv_util.mk_sle(pre_rounded, m_bv_util.mk_numeral(-1, bv_sz + 3)));
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)); 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); dbg_decouple("fpa2bv_to_bv_in_range_ll", ll);
pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded);
} }
dbg_decouple("fpa2bv_to_bv_in_range_ovfl", ovfl);
dbg_decouple("fpa2bv_to_bv_in_range_ul", ul); dbg_decouple("fpa2bv_to_bv_in_range_ul", ul);
dbg_decouple("fpa2bv_to_bv_in_range", in_range); dbg_decouple("fpa2bv_to_bv_in_range", in_range);