mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
exception behavior in C++11 threads?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
9f3089b098
commit
27971e3f68
|
@ -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";);
|
||||
|
|
|
@ -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));
|
||||
|
|
Loading…
Reference in a new issue