mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-02-12 15:49:20 -08:00
parent eec1da5a15 64d085c188
commit 83f0fd5cc2
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -3300,11 +3300,11 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
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_bv_neg(m_bv_util.mk_numeral(1, 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)));
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)))); 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), in_range = m.mk_and(m.mk_not(ovfl),
m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(ll, pre_rounded),
m_bv_util.mk_sle(pre_rounded, ul)); 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_ovfl", ovfl);
dbg_decouple("fpa2bv_to_bv_in_range_ul", ul); dbg_decouple("fpa2bv_to_bv_in_range_ul", ul);