From 7d7e03e377f1087202a8728fe0ee77b5d88b33ce Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Oct 2016 16:23:33 -0700
Subject: [PATCH] rewind qhead to ensure re-propagation after cancellation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_consequences.cpp | 1 +
 src/smt/smt_context.cpp      | 8 ++++++--
 src/util/rlimit.cpp          | 1 +
 3 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index ef90aac4c..1c1d236ad 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -258,6 +258,7 @@ namespace smt {
             TRACE("context", tout << is_sat << "\n";);
             return is_sat;
         }
+
         obj_map<expr, expr*> var2val;
         index_set _assumptions;
         for (unsigned i = 0; i < assumptions.size(); ++i) {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index fed6e71bc..154f3a6a3 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1749,8 +1749,10 @@ namespace smt {
             unsigned qhead = m_qhead;
             if (!bcp())
                 return false;
-            if (get_cancel_flag()) 
+            if (get_cancel_flag()) {
+                m_qhead = qhead;
                 return true;
+            }
             SASSERT(!inconsistent());
             propagate_relevancy(qhead);
             if (inconsistent()) 
@@ -1768,8 +1770,10 @@ namespace smt {
             m_qmanager->propagate();
             if (inconsistent())
                 return false;
-            if (resource_limits_exceeded())
+            if (resource_limits_exceeded()) {
+                m_qhead = qhead;
                 return true;
+            }
             if (!can_propagate()) {
                 CASSERT("diseq_bug", inconsistent() || check_missing_diseq_conflict());
                 CASSERT("eqc_bool", check_eqc_bool_assignment());
diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
index 37b1f7904..9f6c692cc 100644
--- a/src/util/rlimit.cpp
+++ b/src/util/rlimit.cpp
@@ -29,6 +29,7 @@ uint64 reslimit::count() const {
     return m_count;
 }
 
+
 bool reslimit::inc() {
     ++m_count;
     return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit);