From e677030b7469933a14c02376a7935a307a919482 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 28 Jul 2017 21:39:44 +0100 Subject: [PATCH] Fixed sign bug in mpf fp.fma. Relates to #872. --- src/util/mpf.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 245186f52..be19cbb9b 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -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))); // 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); 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())) { m_mpz_manager.abs(res.significand()); - res.get().sign |= c.sign(); + res.get().sign = !res.sign(); } } else {