mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

log exceptions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-15 10:28:52 -07:00
parent 4237f9d86b
commit 2b9b9a9623
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/solver/parallel_tactical2.cpp
View file

@ -598,14 +598,13 @@ class parallel_solver {
unsigned best_idx = select_best_core_min_job_unlocked();
m_core_min_jobs.swap(best_idx, m_core_min_jobs.size() - 1);
core_min_job* job = m_core_min_jobs.detach_back();
scoped_ptr<core_min_job> job = m_core_min_jobs.detach_back();
m_core_min_jobs.pop_back();
SASSERT(job);
source = job->source;
core.reset();
for (expr* c : job->core)
core.push_back(g2l(c));
dealloc(job);
return source != nullptr;
}
@ -999,6 +998,10 @@ class parallel_solver {
catch (z3_exception& ex) {
if (!m.limit().is_canceled() && !is_cancellation_exception(ex.what()))
b.set_exception(ex.what());
}
catch (...) {
IF_VERBOSE(0, verbose_stream() << "Unknown exception in check_cube\n";);
throw;
}
LOG_WORKER(1, " DONE checking cube " << r << "\n";);
return r;