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

bugfix for fpa2bv converter

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-26 15:59:00 +00:00
parent d558eaa321
commit 5b39d8fa0d
1 changed files with 289 additions and 289 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1077,7 +1077,7 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args,
// CMW: Actual rounding is not necessary here, this is // CMW: Actual rounding is not necessary here, this is
// just convenience to get rid of the extra bits. // just convenience to get rid of the extra bits.
expr_ref bv_rm(m); expr_ref bv_rm(m);
m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); bv_rm = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3);
round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v7); round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v7);
// And finally, we tie them together. // And finally, we tie them together.