diff --git a/src/smt/smt_checker.cpp b/src/smt/smt_checker.cpp
index 2e405f95a..d2c1758d3 100644
--- a/src/smt/smt_checker.cpp
+++ b/src/smt/smt_checker.cpp
@@ -22,23 +22,25 @@ Revision History:
 
 namespace smt {
 
-    bool checker::all_args(app * a, bool is_true) {
+    bool checker::all_args(app *a, unsigned depth, bool is_true) {
         for (expr* arg : *a) {
-            if (!check(arg, is_true))
+            if (!check(arg, depth + 1, is_true))
                 return false;
         }
         return true;
     }
 
-    bool checker::any_arg(app * a, bool is_true) {
+    bool checker::any_arg(app *a, unsigned depth, bool is_true) {
         for (expr* arg : *a) {
-            if (check(arg, is_true))
+            if (check(arg, depth + 1, is_true))
                 return true;
         }
         return false;
     }
 
-    bool checker::check_core(expr * n, bool is_true) {
+    bool checker::check_core(expr *n, unsigned depth, bool is_true) {
+        if (depth > 600)
+            return false;
         SASSERT(m_manager.is_bool(n));
         if (m_context.b_internalized(n) && m_context.is_relevant(n)) {
             lbool val = m_context.get_assignment(n);
@@ -54,11 +56,11 @@ namespace smt {
             case OP_FALSE:
                 return !is_true;
             case OP_NOT:
-                return check(a->get_arg(0), !is_true);
+                return check(a->get_arg(0), depth + 1, !is_true);
             case OP_OR:
-                return is_true ? any_arg(a, true) : all_args(a, false);
+                return is_true ? any_arg(a, depth, true) : all_args(a, depth, false);
             case OP_AND:
-                return is_true ? all_args(a, true) : any_arg(a, false);
+                return is_true ? all_args(a, depth, true) : any_arg(a, depth, false);
             case OP_EQ:
                 if (!m_manager.is_iff(a)) {
                     enode * lhs = get_enode_eq_to(a->get_arg(0));
@@ -74,27 +76,27 @@ namespace smt {
                 }
                 else if (is_true) {
                     return 
-                        (check(a->get_arg(0), true) &&
-                         check(a->get_arg(1), true)) ||
-                        (check(a->get_arg(0), false) &&
-                         check(a->get_arg(1), false));
+                        (check(a->get_arg(0), depth + 1, true) &&
+                         check(a->get_arg(1), depth + 1, true)) ||
+                        (check(a->get_arg(0), depth + 1, false) &&
+                         check(a->get_arg(1), depth + 1, false));
                 }
                 else {
                     return 
-                        (check(a->get_arg(0), true) &&
-                         check(a->get_arg(1), false)) ||
-                        (check(a->get_arg(0), false) &&
-                         check(a->get_arg(1), true));
+                        (check(a->get_arg(0), depth + 1, true) &&
+                         check(a->get_arg(1), depth + 1, false)) ||
+                        (check(a->get_arg(0), depth + 1, false) &&
+                         check(a->get_arg(1), depth + 1, true));
                 }
             case OP_ITE: {
                 if (m_context.lit_internalized(a->get_arg(0)) && m_context.is_relevant(a->get_arg(0))) {
                     switch (m_context.get_assignment(a->get_arg(0))) {
-                    case l_false: return check(a->get_arg(2), is_true);
+                    case l_false: return check(a->get_arg(2), depth + 1, is_true);
                     case l_undef: return false;
-                    case l_true:  return check(a->get_arg(1), is_true);
+                    case l_true:  return check(a->get_arg(1), depth + 1, is_true);
                     }
                 }
-                return check(a->get_arg(1), is_true) && check(a->get_arg(2), is_true);
+                return check(a->get_arg(1), depth + 1, is_true) && check(a->get_arg(2), depth + 1, is_true);
             }
             default:
                 break;
@@ -108,11 +110,11 @@ namespace smt {
         return false;
     }
     
-    bool checker::check(expr * n, bool is_true) {
+    bool checker::check(expr *n, unsigned depth, bool is_true) {
         bool r;
         if (n->get_ref_count() > 1 && m_is_true_cache[is_true].find(n, r))
             return r;
-        r = check_core(n, is_true);
+        r = check_core(n, depth, is_true);
         if (n->get_ref_count() > 1)
             m_is_true_cache[is_true].insert(n, r);
         return r;
@@ -156,7 +158,7 @@ namespace smt {
     bool checker::is_sat(expr * n, unsigned num_bindings, enode * const * bindings) {
         flet<unsigned>        l1(m_num_bindings, num_bindings);
         flet<enode * const *> l2(m_bindings, bindings);
-        bool r = check(n, true);
+        bool r = check(n, 0, true);
         m_is_true_cache[0].reset();
         m_is_true_cache[1].reset();
         m_to_enode_cache.reset();
@@ -166,7 +168,7 @@ namespace smt {
     bool checker::is_unsat(expr * n, unsigned num_bindings, enode * const * bindings) {
         flet<unsigned>        l1(m_num_bindings, num_bindings);
         flet<enode * const *> l2(m_bindings, bindings);
-        bool r = check(n, false);
+        bool r = check(n, 0,false);
         m_is_true_cache[0].reset();
         m_is_true_cache[1].reset();
         m_to_enode_cache.reset();
diff --git a/src/smt/smt_checker.h b/src/smt/smt_checker.h
index f2f25e92e..3cd83a106 100644
--- a/src/smt/smt_checker.h
+++ b/src/smt/smt_checker.h
@@ -37,10 +37,10 @@ namespace smt {
         unsigned               m_num_bindings;
         enode * const *        m_bindings;
 
-        bool all_args(app * a, bool is_true);
-        bool any_arg(app * a, bool is_true);
-        bool check_core(expr * n, bool is_true);
-        bool check(expr * n, bool is_true);
+        bool all_args(app *a, unsigned depth, bool is_true);
+        bool any_arg(app *a, unsigned depth, bool is_true);
+        bool check_core(expr * n, unsigned depth, bool is_true);
+        bool check(expr *n, unsigned depth, bool is_true);
         enode * get_enode_eq_to_core(app * n);
         enode * get_enode_eq_to(expr * n);