fix #4642

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 17, 2020 · 2611484 · 2611484
1 parent 33d96c1
commit 2611484
Showing 1 changed file with 1 addition and 2 deletions.
diff --git 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;);