From 702af71a2d4d95099d9cd2adc7a70b6d03f47068 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Aug 2015 23:14:34 +0200 Subject: [PATCH] Check more frequently for cancelation flags to address grep0095.stp.smt2 in issue #178. Z3 spends time in pre-processing simplification, which indicates there is some opportunity to tune this portion of the code Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 ++ src/smt/tactic/smt_tactic.cpp | 3 +++ 2 files changed, 5 insertions(+) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 55e750980..b0abc0de0 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2773,6 +2773,7 @@ namespace smt { } void context::assert_expr_core(expr * e, proof * pr) { + if (m_cancel_flag) return; SASSERT(is_well_sorted(m_manager, e)); TRACE("begin_assert_expr", tout << mk_pp(e, m_manager) << "\n";); TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m_manager) << "\n";); @@ -2802,6 +2803,7 @@ namespace smt { } void context::internalize_assertions() { + if (m_cancel_flag) return; TRACE("internalize_assertions", tout << "internalize_assertions()...\n";); timeit tt(get_verbosity_level() >= 100, "smt.preprocessing"); reduce_assertions(); diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index c441a7d45..725d38ed5 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -229,6 +229,9 @@ public: m_ctx->assert_expr(in->form(i)); } } + if (m_ctx->canceled()) { + throw tactic_exception("smt_tactic canceled"); + } lbool r; if (assumptions.empty())