diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h
index 64643bcf4..76e479535 100644
--- a/src/math/subpaving/subpaving_t_def.h
+++ b/src/math/subpaving/subpaving_t_def.h
@@ -1747,9 +1747,8 @@ void context_t<C>::propagate(node * n, bound * b) {
 
 template<typename C>
 void context_t<C>::propagate(node * n) {
-    while (m_qhead < m_queue.size()) {
-        if (inconsistent(n))
-            break;
+    unsigned num_nodes = num_vars();
+    while (!inconsistent(n) && m_qhead < m_queue.size() && 2*m_qhead < num_nodes) {
         checkpoint();
         bound * b = m_queue[m_qhead];
         SASSERT(is_bound_of(b, n));