diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 60120bea2..1543ce629 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -959,14 +959,14 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args,
     c3 = y_is_inf;
     v3 = x;
 
-    // (x is 0) -> x
-    c4 = x_is_zero;
-    v4 = pzero;
-    
     // (y is 0) -> NaN.
-    c5 = y_is_zero;
-    v5 = nan;
+    c4 = y_is_zero;
+    v4 = nan;
 
+    // (x is 0) -> x
+    c5 = x_is_zero;
+    v5 = pzero;
+        
     // else the actual remainder.
     unsigned ebits = m_util.get_ebits(f->get_range());
     unsigned sbits = m_util.get_sbits(f->get_range());    
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index 9b6db5213..428cfb318 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -1161,10 +1161,10 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
         mk_nan(x.ebits, x.sbits, o);
     else if (is_inf(y))
         set(o, x);
-    else if (is_zero(x))        
-        set(o, x);
     else if (is_zero(y))
         mk_nan(x.ebits, x.sbits, o);
+    else if (is_zero(x))        
+        set(o, x);    
     else {        
         o.ebits = x.ebits;
         o.sbits = x.sbits;