mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-01 11:51:20 +00:00
Code Activity

Fix rounding bug in mpf_manager. Fixes #2970.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2020-07-16 12:39:12 +00:00
parent ccdae7af24
commit d3ae40130a
No known key found for this signature in database
GPG key ID: BCF6360F86294467
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/util/mpf.cpp
View file

@ -351,10 +351,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
signed ds = sbits - x.sbits + 3; // plus rounding bits signed ds = sbits - x.sbits + 3; // plus rounding bits
if (ds > 0) if (ds > 0)
{
m_mpz_manager.mul2k(o.significand, ds); m_mpz_manager.mul2k(o.significand, ds);
round(rm, o);
}
else if (ds < 0) else if (ds < 0)
{ {
bool sticky = false; bool sticky = false;
@ -366,8 +363,9 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
} }
if (sticky && m_mpz_manager.is_even(o.significand)) if (sticky && m_mpz_manager.is_even(o.significand))
m_mpz_manager.inc(o.significand); m_mpz_manager.inc(o.significand);
round(rm, o);
} }
round(rm, o);
} }
} }