From 3aea63edb1e114ef68b813b44298cd73221afb12 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 May 2016 17:27:37 -0700 Subject: [PATCH] check for cancellation before internalizing and during to avoid errors. Issue #625 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 07f4440ff..046e2028e 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2939,7 +2939,7 @@ namespace smt { if (!m_asserted_formulas.inconsistent()) { unsigned sz = m_asserted_formulas.get_num_formulas(); unsigned qhead = m_asserted_formulas.get_qhead(); - while (qhead < sz) { + while (qhead < sz && !m_manager.canceled()) { expr * f = m_asserted_formulas.get_formula(qhead); proof * pr = m_asserted_formulas.get_formula_proof(qhead); internalize_assertion(f, pr, 0);