From 26114845257bdff6653fe0488a989debaa044666 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 Aug 2020 08:35:15 -0700 Subject: [PATCH] fix #4642 Signed-off-by: Nikolaj Bjorner --- src/util/mpf.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 56d7db042..8983da3ce 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -745,8 +745,7 @@ void mpf_manager::div(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & } void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf const &z, mpf & o) { - SASSERT(x.sbits == y.sbits && x.ebits == y.ebits && - x.sbits == y.sbits && z.ebits == z.ebits); + SASSERT(x.sbits == y.sbits && x.ebits == y.ebits); TRACE("mpf_dbg", tout << "X = " << to_string(x) << std::endl;); TRACE("mpf_dbg", tout << "Y = " << to_string(y) << std::endl;);