From ab9bcfdcce79d44627e96fd39c43097a1c17fc98 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 21 Feb 2020 20:36:58 -0800
Subject: [PATCH] fix #3055, bound iterations of subpaving

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/subpaving/subpaving_t_def.h | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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));