diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 68b684283..b2b20b8a7 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2972,14 +2972,15 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
     sig_sz = m_bv_util.get_bv_size(sig);
     SASSERT(sig_sz >= (bv_sz + 3));
 
-    expr_ref exp_m_lz(m), shift(m), shift_neg(m), bv0_e2(m), shift_abs(m);
+    expr_ref exp_m_lz(m), shift(m), shift_neg(m), bv0_e2(m), shift_abs(m), shift_neg_dec(m);
     exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp),
                                    m_bv_util.mk_zero_extend(2, lz));
     shift = m_bv_util.mk_bv_sub(exp_m_lz,
                                 m_bv_util.mk_numeral(bv_sz, ebits + 2));
     shift_neg = m_bv_util.mk_bv_neg(shift);
     bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2);
-    shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift);
+    shift_neg_dec = m_bv_util.mk_sle(shift, bv0_e2);
+    shift_abs = m.mk_ite(shift_neg_dec, shift_neg, shift);
     SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2);
     SASSERT(m_bv_util.get_bv_size(shift_neg) == ebits + 2);
     SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2);    
@@ -3001,7 +3002,9 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
     expr_ref huge_sig(m), huge_shift(m), huge_shifted_sig(m);
     huge_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_sz));
     huge_shift = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sig_sz), shift_abs);
-    huge_shifted_sig = m_bv_util.mk_bv_lshr(huge_sig, huge_shift);
+    huge_shifted_sig = m.mk_ite(shift_neg_dec,
+                        m_bv_util.mk_bv_shl(huge_sig, huge_shift),
+                        m_bv_util.mk_bv_lshr(huge_sig, huge_shift));
     dbg_decouple("fpa2bv_to_sbv_huge_shifted_sig", huge_shifted_sig);
     SASSERT(m_bv_util.get_bv_size(huge_shifted_sig) == 2 * sig_sz);
 
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index 36974519c..6d51b68ce 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -877,10 +877,11 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
 
         // Remove the extra bits, keeping a sticky bit. 
         m_mpz_manager.set(sticky_rem, 0);
-        if (o.sbits >= (4+extra))
-            m_mpz_manager.machine_div_rem(o.significand, m_powers2(4+extra), o.significand, sticky_rem);
+        unsigned minbits = (4 + extra);
+        if (o.sbits >= minbits)
+            m_mpz_manager.machine_div_rem(o.significand, m_powers2(o.sbits - minbits), o.significand, sticky_rem);
         else
-            m_mpz_manager.mul2k(o.significand, (4+extra) - o.sbits, o.significand);
+            m_mpz_manager.mul2k(o.significand, minbits - o.sbits, o.significand);
         
         if (!m_mpz_manager.is_zero(sticky_rem) && m_mpz_manager.is_even(o.significand))
             m_mpz_manager.inc(o.significand);