diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp
index 0a4411847..587b9df9a 100644
--- a/src/tactic/bv/bv_bounds_tactic.cpp
+++ b/src/tactic/bv/bv_bounds_tactic.cpp
@@ -162,6 +162,9 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
     map         *m_bound;
 
     bool is_bound(expr *e, expr*& v, interval& b) {
+        if (!m.is_bool(e))
+            return false;
+
         rational n;
         expr *lhs, *rhs;
         unsigned sz;