From d03a4bc306ae59ef27d6508a3670cb7f7fd8e900 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 2 Oct 2014 14:33:42 -0700
Subject: [PATCH] check cancel flag after bcp. BCP returns in incomplete state
 after it check's the cancel flag. Propagate returns 'true' in this case so
 that the main loop exits

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 02ee06985..f3f2d4948 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1615,6 +1615,8 @@ namespace smt {
             unsigned qhead = m_qhead;
             if (!bcp())
                 return false;
+            if (m_cancel_flag) 
+                return true;
             SASSERT(!inconsistent());
             propagate_relevancy(qhead);
             if (inconsistent())