mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Fixed overflow bug in fp.to_ubv. Thanks to Florian Schanda for reporting this bug.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2018-04-05 17:21:17 +01:00
parent 3de41e5179
commit bd00d98398
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -3243,8 +3243,13 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
expr_ref ul(m), ovfl(m), in_range(m);
if (!is_signed) {
expr_ref incd(m), pr_is_zero(m);
incd = m.mk_eq(rounding_decision, bv1);
pr_is_zero = m.mk_eq(pre_rounded, 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));
in_range = m.mk_and(m.mk_not(x_is_neg),
m.mk_not(m.mk_and(incd, pr_is_zero)),
m_bv_util.mk_ule(pre_rounded, ul));
}
else {
expr_ref ll(m);