diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
index 69c9a6290..2727a8e73 100644
--- a/src/ast/fpa/fpa2bv_rewriter.h
+++ b/src/ast/fpa/fpa2bv_rewriter.h
@@ -185,7 +185,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
             bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range());
             
             for (unsigned i = 0; i < num; i++)
-                is_float_uf |= m_conv.is_float(f->get_domain()[i]) || m_conv.is_rm(f->get_domain()[i]);
+                is_float_uf |= m_conv.is_float(args[i]) || m_conv.is_rm(args[i]);
 
             if (is_float_uf)
             {
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 0fadc62ca..46c9d962d 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -652,10 +652,8 @@ namespace smt {
                
         if (fu.is_float(xe) && fu.is_float(ye))
             m_converter.mk_eq(xc, yc, c);
-        else if (fu.is_rm(xe) && fu.is_rm(ye))
+        else 
             c = m.mk_eq(xc, yc);
-        else
-            UNREACHABLE();
         
         m_th_rw(c);
         assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c));
@@ -692,10 +690,8 @@ namespace smt {
             m_converter.mk_eq(xc, yc, c);
             c = m.mk_not(c);
         }
-        else if (fu.is_rm(xe) && fu.is_rm(ye))
-            c = m.mk_not(m.mk_eq(xc, yc));
         else
-            UNREACHABLE();
+            c = m.mk_not(m.mk_eq(xc, yc));
 
         m_th_rw(c);
         assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c));