mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Bugfix for MPF fma.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-09-14 14:07:11 +01:00
parent d0fa4e992f
commit d6e2fa6a60
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/util/mpf.cpp
View file

@ -877,10 +877,11 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
// Remove the extra bits, keeping a sticky bit.
m_mpz_manager.set(sticky_rem, 0);
if (o.sbits >= (4+extra))
m_mpz_manager.machine_div_rem(o.significand, m_powers2(4+extra), o.significand, sticky_rem);
unsigned minbits = (4 + extra);
if (o.sbits >= minbits)
m_mpz_manager.machine_div_rem(o.significand, m_powers2(o.sbits - minbits), o.significand, sticky_rem);
else
m_mpz_manager.mul2k(o.significand, (4+extra) - o.sbits, o.significand);
m_mpz_manager.mul2k(o.significand, minbits - o.sbits, o.significand);
if (!m_mpz_manager.is_zero(sticky_rem) && m_mpz_manager.is_even(o.significand))
m_mpz_manager.inc(o.significand);