diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index f1cf1d598..ebbf235fb 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -904,8 +904,6 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
         SASSERT(m_mpz_manager.lt(res.significand(), m_powers2(2 * x.sbits + 1 + 3)));
         if (m_mpz_manager.ge(res.significand(), m_powers2(2 * x.sbits + 3)))
         {
-            SASSERT(exp(res) < mk_max_exp(x.ebits)); // NYI.
-
             res.get().exponent++;
             renorm_sticky = !m_mpz_manager.is_even(res.significand());
             m_mpz_manager.machine_div2k(res.significand(), 1);
@@ -923,26 +921,32 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
 
         TRACE("mpf_dbg", tout << "R*= " << to_string_binary(res, 2, 0) << " (renormalized, delta=" << renorm_delta << ")" << std::endl;);
 
-        set(o, x.ebits, x.sbits, res.sign(), res.exponent(), mpz(0));
+        if (exp(res) <= mk_max_exp(x.ebits))
+        {
+            set(o, x.ebits, x.sbits, res.sign(), res.exponent(), mpz(0));
 
-        if (x.sbits >= 4) {
-            m_mpz_manager.machine_div_rem(res.significand(), m_powers2(x.sbits - 4 + 3), o.significand, sticky_rem);
-            renorm_sticky |= !m_mpz_manager.is_zero(sticky_rem);
+            if (x.sbits >= 4) {
+                m_mpz_manager.machine_div_rem(res.significand(), m_powers2(x.sbits - 4 + 3), o.significand, sticky_rem);
+                renorm_sticky |= !m_mpz_manager.is_zero(sticky_rem);
+            }
+            else {
+                m_mpz_manager.mul2k(res.significand(), 4 - x.sbits + 3, o.significand);
+            }
+
+            if (renorm_sticky && m_mpz_manager.is_even(o.significand))
+                m_mpz_manager.inc(o.significand);
+
+            TRACE("mpf_dbg", tout << "sum[-1:sbits+2] = " << m_mpz_manager.to_string(o.significand) << std::endl;
+                            tout << "R = " << to_string_binary(o, 1, 3) << std::endl;);
+
+            if (m_mpz_manager.is_zero(o.significand))
+                mk_zero(x.ebits, x.sbits, rm == MPF_ROUND_TOWARD_NEGATIVE, o);
+            else
+                round(rm, o);
         }
         else {
-            m_mpz_manager.mul2k(res.significand(), 4 - x.sbits + 3, o.significand);
+            mk_inf(x.ebits, x.sbits, res.sign(), o);
         }
-
-        if (renorm_sticky && m_mpz_manager.is_even(o.significand))
-            m_mpz_manager.inc(o.significand);
-
-        TRACE("mpf_dbg", tout << "sum[-1:sbits+2] = " << m_mpz_manager.to_string(o.significand) << std::endl;
-                         tout << "R = " << to_string_binary(o, 1, 3) << std::endl;);
-
-        if (m_mpz_manager.is_zero(o.significand))
-            mk_zero(x.ebits, x.sbits, rm == MPF_ROUND_TOWARD_NEGATIVE, o);
-        else
-            round(rm, o);
     }
 
 }