mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Fixed sign bug in mpf fp.fma. Relates to #872.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-07-28 21:39:44 +01:00
parent a30c343d7a
commit e677030b74
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

@ -841,7 +841,7 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
SASSERT(m_mpz_manager.ge(mr.significand(), m_powers2(2*x.sbits - 2))); SASSERT(m_mpz_manager.ge(mr.significand(), m_powers2(2*x.sbits - 2)));
// Introduce extra bits into c in _[0].[sbits-1] s.t. c in _[0].[2*sbits-2] // Introduce extra bits into c in _[0].[sbits-1] s.t. c in _[0].[2*sbits-2]
c.set(x.ebits + 2, 2 * x.sbits - 1, c.sign(), c.exponent(), c.significand()); c.set(x.ebits+2, 2*x.sbits-1, c.sign(), c.exponent(), c.significand());
m_mpz_manager.mul2k(c.significand(), x.sbits - 1); m_mpz_manager.mul2k(c.significand(), x.sbits - 1);
TRACE("mpf_dbg", tout << "C_= " << to_string(c) << std::endl; TRACE("mpf_dbg", tout << "C_= " << to_string(c) << std::endl;
@ -888,7 +888,7 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
if (m_mpz_manager.is_neg(res.significand())) { if (m_mpz_manager.is_neg(res.significand())) {
m_mpz_manager.abs(res.significand()); m_mpz_manager.abs(res.significand());
res.get().sign |= c.sign(); res.get().sign = !res.sign();
} }
} }
else { else {