mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-09 09:21:56 +00:00
Code Activity

fix deadlock

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-08 14:12:34 -07:00
parent b02161ef51
commit 63b4503c15
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/smt_parallel2.cpp
View file

@ -315,6 +315,7 @@ namespace smt {
return; return;
m_state = state::is_sat; m_state = state::is_sat;
p.ctx.set_model(m.translate(l2g)); p.ctx.set_model(m.translate(l2g));
cv.notify_all();
cancel_workers(); cancel_workers();
} }
@ -331,6 +332,7 @@ namespace smt {
SASSERT(p.ctx.m_unsat_core.empty()); SASSERT(p.ctx.m_unsat_core.empty());
for (expr* e : unsat_core) for (expr* e : unsat_core)
p.ctx.m_unsat_core.push_back(l2g(e)); p.ctx.m_unsat_core.push_back(l2g(e));
cv.notify_all();
cancel_workers(); cancel_workers();
} }
@ -341,6 +343,7 @@ namespace smt {
return; return;
m_state = state::is_exception_code; m_state = state::is_exception_code;
m_exception_code = error_code; m_exception_code = error_code;
cv.notify_all();
cancel_workers(); cancel_workers();
} }
@ -351,6 +354,7 @@ namespace smt {
return; return;
m_state = state::is_exception_msg; m_state = state::is_exception_msg;
m_exception_msg = msg; m_exception_msg = msg;
cv.notify_all();
cancel_workers(); cancel_workers();
} }
@ -400,6 +404,11 @@ namespace smt {
cv.notify_all(); cv.notify_all();
return false; return false;
} }
if (m_state != state::is_running) {
IF_VERBOSE(1, verbose_stream() << "aborting get_cube\n";);
cv.notify_all();
return false;
}
cv.wait(lock); cv.wait(lock);
} }
IF_VERBOSE(1, m_search_tree.display(verbose_stream()); verbose_stream() << "\n";); IF_VERBOSE(1, m_search_tree.display(verbose_stream()); verbose_stream() << "\n";);