From 27971e3f68c70933302c48f7c89159d228034ef7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2019 04:36:48 -0700 Subject: [PATCH] exception behavior in C++11 threads? Signed-off-by: Nikolaj Bjorner --- src/smt/tactic/smt_tactic.cpp | 1 + src/tactic/tactical.cpp | 2 ++ 2 files changed, 3 insertions(+) diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index dea1a6c0b..5445d6089 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -208,6 +208,7 @@ public: m_ctx->collect_statistics(m_stats); throw; } + SASSERT(m_ctx); m_ctx->collect_statistics(m_stats); proof * pr = m_ctx->get_proof(); TRACE("smt_tactic", tout << r << " " << pr << "\n";); diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 82ecb819e..063f3dbe1 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -416,6 +416,7 @@ public: tactic & t = *(ts.get(i)); try { + // IF_VERBOSE(0, verbose_stream() << "start\n"); t(in_copy, _result); bool first = false; { @@ -431,6 +432,7 @@ public: managers[j]->limit().cancel(); } } + IF_VERBOSE(0, verbose_stream() << "first\n"); ast_translation translator(*(managers[i]), m, false); for (goal* g : _result) { result.push_back(g->translate(translator));