mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

Fixed MPF to_sbv. Thanks to Florian Schanda for reporting this bug.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2018-04-05 15:23:16 +01:00
parent 3f7453f5c5
commit 793642f48d
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/util/mpf.cpp
View file

@ -1194,7 +1194,7 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o
m_mpz_manager.set(z, t.significand());
mpf_exp_t e = (mpf_exp_t)t.exponent() - t.sbits() + 1;
if (e < 0) {
bool last = false, round = false, sticky = m_mpz_manager.is_odd(z);
bool last = m_mpz_manager.is_odd(z), round = false, sticky = false;
for (; e != 0; e++) {
m_mpz_manager.machine_div2k(z, 1);
sticky |= round;
@ -1204,7 +1204,7 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o
bool inc = false;
switch (rm) {
case MPF_ROUND_NEAREST_TEVEN: inc = round && (last || sticky); break;
case MPF_ROUND_NEAREST_TAWAY: inc = round && (!last || sticky); break; // CMW: Check!
case MPF_ROUND_NEAREST_TAWAY: inc = round; break;
case MPF_ROUND_TOWARD_POSITIVE: inc = (!x.sign && (round || sticky)); break;
case MPF_ROUND_TOWARD_NEGATIVE: inc = (x.sign && (round || sticky)); break;
case MPF_ROUND_TOWARD_ZERO: inc = false; break;