diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index fda51f0fa..b84d5567c 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -258,11 +258,21 @@ public:
         }
     }
 
+    bool is_var_const_pair(expr* e, expr* c, unsigned& k) {
+        rational r;
+        if (is_uninterp_const(e) && a.is_numeral(c, r) && r.is_unsigned() && !m_nonfd.is_marked(e)) {
+            k = r.get_unsigned();
+            return true;
+        }
+        else {
+            return false;
+        }
+    }
+
     bool is_upper(expr* f) {
         expr* e1, *e2;
-        rational r;
-        if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && 
-            is_uninterp_const(e1) && a.is_numeral(e2, r) && r.is_unsigned() && !m_nonfd.is_marked(e1)) {
+        unsigned k;
+        if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && is_var_const_pair(e1, e2, k)) {
             SASSERT(m_bounds.has_upper(e1));
             return true;
         } 
@@ -271,9 +281,8 @@ public:
 
     bool is_lower(expr* f) {
         expr* e1, *e2;
-        rational r;
-        if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && 
-            is_uninterp_const(e2) && a.is_numeral(e1, r) && r.is_unsigned() && !m_nonfd.is_marked(e2)) {
+        unsigned k;
+        if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && is_var_const_pair(e2, e1, k)) {
             SASSERT(m_bounds.has_lower(e2));
             return true;
         } 
@@ -284,7 +293,6 @@ public:
         return is_lower(f) || is_upper(f);
     }
 
-
     void collect_fd(expr* f) {
         if (is_bound(f)) return;
         m_todo.push_back(f);
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index d7cd26896..91d27ed27 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -33,8 +33,6 @@ void mem_finalize();
 out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
 }
 
-exceeded_memory_allocations::exceeded_memory_allocations():z3_error(ERR_ALLOC_EXCEEDED) {
-}
 
 static volatile bool g_memory_out_of_memory  = false;
 static bool       g_memory_initialized       = false;
@@ -69,13 +67,8 @@ static void throw_out_of_memory() {
 }
 
 static void throw_alloc_counts_exceeded() {
-    #pragma omp critical (z3_memory_manager) 
-    {
-        // reset the count to avoid re-throwing while
-        // the exception is being thrown.
-        g_memory_alloc_count = 0;
-    }
-    throw exceeded_memory_allocations();
+    std::cout << "Maximal allocation counts " << g_memory_max_alloc_count << " have been exceeded\n";
+    exit(ERR_ALLOC_EXCEEDED);
 }