mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Fixed model evaluation/simplification for to_ieee_bv.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-16 17:46:52 +00:00
parent 7ec70c1686
commit 6b2d84b2be
1 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -850,8 +850,16 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu
bu.mk_concat(bu.mk_numeral(0, x.get_sbits() - 2),
bu.mk_numeral(1, 1))));
}
else
result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits());
else {
app_ref unspec(m()), mask(m()), extra(m());
unspec = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits());
mask = bu.mk_concat(bu.mk_numeral(0, 1),
bu.mk_concat(bu.mk_numeral(-1, x.get_ebits()),
bu.mk_concat(bu.mk_numeral(0, x.get_sbits() - 2),
bu.mk_numeral(1, 1))));
expr * args[2] = { unspec, mask };
result = m().mk_app(bu.get_fid(), OP_BOR, 2, args);
}
return BR_REWRITE_FULL;
}
else {