mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Merge pull request #608 from wintersteiger/fprti-rna-fix

Browse source 
Fix for #586, RNA rounding for fp.roundToIntegral.
This commit is contained in:
Christoph M. Wintersteiger 2016-05-16 16:21:35 +01:00
commit 89598e0141
2 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/util/mpf.cpp
View file

@ -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 = " << less_than_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);
}