mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

Bugfix for fp.rem when the result is zero.

Browse source 
Fixes #91
This commit is contained in:
Christoph M. Wintersteiger 2015-05-19 16:51:56 +01:00
parent 8f86542f26
commit 0197f6e010
1 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1018,9 +1018,11 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args,
m_bv_util.mk_numeral(0, 3));
res_exp = m_bv_util.mk_sign_extend(2, b_exp);
// CMW: Actual rounding is not necessary here, this is
// just convenience to get rid of the extra bits.
expr_ref rm(m);
rm = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3);
round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7);
rm = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3);
round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7);
// And finally, we tie them together.
mk_ite(c6, v6, v7, result);
@ -1030,6 +1032,11 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args,
mk_ite(c2, v2, result, result);
mk_ite(c1, v1, result, result);
expr_ref result_is_zero(m), zeros(m);
mk_is_zero(result, result_is_zero);
mk_ite(x_is_pos, pzero, nzero, zeros);
mk_ite(result_is_zero, zeros, result, result);
SASSERT(is_well_sorted(m, result));
TRACE("fpa2bv_rem", tout << "REM = " << mk_ismt2_pp(result, m) << std::endl; );