From c1aa33339d2e95c6b8099debe75bd457ebd47b20 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Thu, 25 Feb 2016 09:32:10 +0000
Subject: [PATCH] bv_bounds: early exit in is_bound in case the expr is not
 boolean ~2% speedup

---
 src/tactic/bv/bv_bounds_tactic.cpp | 3 +++
 1 file changed, 3 insertions(+)

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;