diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp
index 1adedb2d7..df26422c8 100644
--- a/src/ast/float_decl_plugin.cpp
+++ b/src/ast/float_decl_plugin.cpp
@@ -106,7 +106,7 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) {
     return false;
 }
 
-bool float_decl_plugin::is_rm(expr * n, mpf_rounding_mode & val) {
+bool float_decl_plugin::is_rm_value(expr * n, mpf_rounding_mode & val) {
     if (is_app_of(n, m_family_id, OP_RM_NEAREST_TIES_TO_AWAY)) {
         val = MPF_ROUND_NEAREST_TAWAY;
         return true;
diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h
index 3786b76ee..58c37080d 100644
--- a/src/ast/float_decl_plugin.h
+++ b/src/ast/float_decl_plugin.h
@@ -169,7 +169,8 @@ public:
     app * mk_value(mpf const & v);
     bool is_value(expr * n) { return is_app_of(n, m_family_id, OP_FLOAT_VALUE); }
     bool is_value(expr * n, mpf & val);
-    bool is_rm(expr * n, mpf_rounding_mode & val);
+    bool is_rm_value(expr * n, mpf_rounding_mode & val);
+    bool is_rm_value(expr * n) { mpf_rounding_mode t; return is_rm_value(n, t); }
 
     mpf const & get_value(unsigned id) const { 
         SASSERT(m_value_table.contains(id));
@@ -198,7 +199,9 @@ public:
     sort * mk_float_sort(unsigned ebits, unsigned sbits);
     sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); }
     bool is_float(sort * s) { return is_sort_of(s, m_fid, FLOAT_SORT); }
-    bool is_rm(sort * s) { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }    
+    bool is_rm(sort * s) { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }
+    bool is_float(expr * e) { return is_float(m_manager.get_sort(e)); }
+    bool is_rm(expr * e) { return is_rm(m_manager.get_sort(e)); }
     unsigned get_ebits(sort * s);
     unsigned get_sbits(sort * s);
 
@@ -217,8 +220,8 @@ public:
 
     app * mk_value(mpf const & v) { return m_plugin->mk_value(v); }
     bool is_value(expr * n) { return m_plugin->is_value(n); }
-    bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); }    
-    bool is_rm(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm(n, v); }
+    bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); }     
+    bool is_rm_value(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm_value(n, v); }
 
     app * mk_pzero(unsigned ebits, unsigned sbits);
     app * mk_nzero(unsigned ebits, unsigned sbits);
diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp
index ecd06ff38..a4212d579 100644
--- a/src/ast/rewriter/float_rewriter.cpp
+++ b/src/ast/rewriter/float_rewriter.cpp
@@ -82,7 +82,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
 
     if (num_args == 2) {
         mpf_rounding_mode rm;
-        if (!m_util.is_rm(args[0], rm))
+        if (!m_util.is_rm_value(args[0], rm))
             return BR_FAILED;
         
         rational q;
@@ -109,12 +109,12 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
             return BR_FAILED;
     }
     else if (num_args == 3 && 
-             m_util.is_rm(m().get_sort(args[0])) && 
+             m_util.is_rm(args[0]) && 
              m_util.au().is_real(args[1]) &&
              m_util.au().is_int(args[2])) {
 
         mpf_rounding_mode rm;
-        if (!m_util.is_rm(args[0], rm))
+        if (!m_util.is_rm_value(args[0], rm))
             return BR_FAILED;
 
         rational q;
@@ -129,8 +129,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
         mpf v;
 	    m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator());
         result = m_util.mk_value(v);
-        m_util.fm().del(v);        
-        // TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
+        m_util.fm().del(v);
         return BR_DONE;
     }
     else {
@@ -140,7 +139,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
 
 br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm()), v3(m_util.fm());
         if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
             scoped_mpf t(m_util.fm());
@@ -161,7 +160,7 @@ br_status float_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref
 
 br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm()), v3(m_util.fm());
         if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
             scoped_mpf t(m_util.fm());
@@ -176,7 +175,7 @@ br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref
 
 br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm()), v3(m_util.fm());
         if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
             scoped_mpf t(m_util.fm());
@@ -287,7 +286,7 @@ br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
 
 br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm());
         if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3) && m_util.is_value(arg4, v4)) {
             scoped_mpf t(m_util.fm());
@@ -302,7 +301,7 @@ br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, exp
 
 br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm());
         if (m_util.is_value(arg2, v2)) {
             scoped_mpf t(m_util.fm());
@@ -317,7 +316,7 @@ br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
 
 br_status float_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) {
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm());
         if (m_util.is_value(arg2, v2)) {
             scoped_mpf t(m_util.fm());