diff --git a/src/sat/sat_cut_simplifier.cpp b/src/sat/sat_cut_simplifier.cpp
index 1eedb6aa9..87fa291db 100644
--- a/src/sat/sat_cut_simplifier.cpp
+++ b/src/sat/sat_cut_simplifier.cpp
@@ -41,7 +41,7 @@ namespace sat {
             unsigned nc = s.m_stats.m_num_cuts  - m_num_cuts;
             unsigned ni = s.m_stats.m_num_learned_implies - m_num_learned_implies;
             IF_VERBOSE(2, 
-                       verbose_stream() << "(sat.aig-simplifier";
+                       verbose_stream() << "(sat.cut-simplifier";
                        if (nu > 0) verbose_stream() << " :num-units " << nu;
                        if (ne > 0) verbose_stream() << " :num-eqs "   << ne;
                        if (ni > 0) verbose_stream() << " :num-bin " << ni;
@@ -475,7 +475,7 @@ namespace sat {
             }
             ++i;
         }
-        IF_VERBOSE(2, verbose_stream() << "(sat.aig-simplifier num simulated eqs " << num_eqs << ")\n");
+        IF_VERBOSE(2, verbose_stream() << "(sat.cut-simplifier num simulated eqs " << num_eqs << ")\n");
     }
 
     void cut_simplifier::track_binary(bin_rel const& p) {
diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp
index 4e7809530..6d97c958c 100644
--- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp
+++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp
@@ -252,7 +252,7 @@ private:
             SASSERT(is_uninterp_const(e));
             func_decl* f = to_app(e)->get_decl();
 
-            if (bm.has_lower(e, lo, s1) && bm.has_upper(e, hi, s2) && lo <= hi && !s1 && !s2) {
+            if (bm.has_lower(e, lo, s1) && bm.has_upper(e, hi, s2) && lo <= hi && !s1 && !s2 && m_arith.is_int(e)) {
                 func_decl* fbv;
                 rational offset;
                 if (!m_int2bv.find(f, fbv)) {