diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 83ba843ac..f69f27214 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -1586,9 +1586,10 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
     mk_nzero(f, nzero); 
     mk_pzero(f, pzero);
 
-    expr_ref x_is_zero(m), x_is_pos(m);
+    expr_ref x_is_zero(m), x_is_pos(m), x_is_neg(m);
     mk_is_zero(x, x_is_zero);
     mk_is_pos(x, x_is_pos);
+    mk_is_neg(x, x_is_neg);
     
     dbg_decouple("fpa2bv_r2i_x_is_zero", x_is_zero);
     dbg_decouple("fpa2bv_r2i_x_is_pos", x_is_pos);    
@@ -1655,9 +1656,13 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
     mk_ite(c422, xone, v42, v42);
     mk_ite(c421, xzero, v42, v42);
     
-    mk_ite(m.mk_eq(a_sgn, one_1), nzero, pone, v4);
-    mk_ite(m.mk_or(rm_is_rte, rm_is_rta), v42, v4, v4);
-    mk_ite(m.mk_or(rm_is_rtz, rm_is_rtn), xzero, v4, v4);
+    expr_ref v4_rtn(m), v4_rtp(m);
+    mk_ite(x_is_neg, nzero, pone, v4_rtp);
+    mk_ite(x_is_neg, none, pzero, v4_rtn);
+
+    mk_ite(rm_is_rtp, v4_rtp, v42, v4);
+    mk_ite(rm_is_rtn, v4_rtn, v4, v4);
+    mk_ite(rm_is_rtz, xzero, v4, v4);
 
     SASSERT(is_well_sorted(m, v4));
     
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index 1dab7b995..e66f6d270 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -1006,11 +1006,22 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o
     else if (is_zero(x))
         mk_zero(x.ebits, x.sbits, x.sign, o); // -0.0 -> -0.0, says IEEE754, Sec 5.9.
     else if (x.exponent < 0) {
-        if (rm == MPF_ROUND_TOWARD_ZERO ||
-            rm == MPF_ROUND_TOWARD_NEGATIVE)
+        if (rm == MPF_ROUND_TOWARD_ZERO)
             mk_zero(x.ebits, x.sbits, x.sign, o);
-        else if (rm == MPF_ROUND_NEAREST_TEVEN ||
-                 rm == MPF_ROUND_NEAREST_TAWAY) {
+        else if (rm == MPF_ROUND_TOWARD_NEGATIVE) {
+            if (x.sign)
+                mk_one(x.ebits, x.sbits, true, o);
+            else
+                mk_zero(x.ebits, x.sbits, false, o);
+        }
+        else if (rm == MPF_ROUND_TOWARD_POSITIVE) {
+            if (x.sign)
+                mk_zero(x.ebits, x.sbits, true, o);
+            else
+                mk_one(x.ebits, x.sbits, false, o);
+        }
+        else {
+            SASSERT(rm == MPF_ROUND_NEAREST_TEVEN || rm == MPF_ROUND_NEAREST_TAWAY);
             bool tie = m_mpz_manager.is_zero(x.significand) && x.exponent == -1;
             TRACE("mpf_dbg", tout << "tie = " << tie << std::endl;);
             if (tie && rm == MPF_ROUND_NEAREST_TEVEN)
@@ -1019,15 +1030,8 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o
                 mk_one(x.ebits, x.sbits, x.sign, o);
             else if (x.exponent < -1)
                 mk_zero(x.ebits, x.sbits, x.sign, o);
-            else 
-                mk_one(x.ebits, x.sbits, x.sign, o);
-        }
-        else {
-            SASSERT(rm == MPF_ROUND_TOWARD_POSITIVE);
-            if (x.sign) 
-                mk_nzero(x.ebits, x.sbits, o);
             else
-                mk_one(x.ebits, x.sbits, false, o);
+                mk_one(x.ebits, x.sbits, x.sign, o);
         }
     }
     else if (x.exponent >= x.sbits - 1)