From 44b0a6ddbcc75c2252c21965c8f473136784acf7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 14 May 2016 18:42:10 +0100 Subject: [PATCH] Tentative fix for #586. --- src/ast/fpa/fpa2bv_converter.cpp | 3 +-- src/util/mpf.cpp | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 8220e64ae..e6b9dda07 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1928,8 +1928,7 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & tie_pttrn = m_bv_util.mk_concat(one_1, m_bv_util.mk_numeral(0, sbits-1)); m_simp.mk_eq(rem, tie_pttrn, tie2); div_last = m_bv_util.mk_extract(0, 0, div); - tie2_c = m.mk_ite(tie2, m.mk_or(m.mk_and(rm_is_rte, m.mk_eq(div_last, one_1)), - m.mk_and(rm_is_rta, m.mk_eq(div_last, zero_1))), + tie2_c = m.mk_ite(tie2, m.mk_or(m.mk_and(rm_is_rte, m.mk_eq(div_last, one_1)), rm_is_rta), m_bv_util.mk_ule(tie_pttrn, rem)); m_simp.mk_ite(tie2_c, div_p1, div, v51); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 14fb1c535..2a1f0362c 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1095,7 +1095,7 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o TRACE("mpf_dbg", tout << "tie= " << tie << "; tie = " << more_than_tie << std::endl;); if (tie) { if ((rm == MPF_ROUND_NEAREST_TEVEN && m_mpz_manager.is_odd(div)) || - (rm == MPF_ROUND_NEAREST_TAWAY && m_mpz_manager.is_even(div))) { + (rm == MPF_ROUND_NEAREST_TAWAY)) { TRACE("mpf_dbg", tout << "div++ (1)" << std::endl;); m_mpz_manager.inc(div); }