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

address deadlock in cancellation path

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-13 08:32:34 -07:00
parent 864c6a3f34
commit bcbfeec6c0
1 changed files with 12 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/solver/parallel_tactical2.cpp
View file

@ -480,6 +480,11 @@ class parallel_solver {
cancel_workers_unlocked(); cancel_workers_unlocked();
} }
void set_cancel() {
std::scoped_lock lock(mux);
cancel_workers_unlocked();
}
void set_unsat(ast_translation& l2g, void set_unsat(ast_translation& l2g,
expr_ref_vector const& core) { expr_ref_vector const& core) {
std::scoped_lock lock(mux); std::scoped_lock lock(mux);
@ -1130,8 +1135,10 @@ class parallel_solver {
if (m_config.m_global_backbones) { if (m_config.m_global_backbones) {
bb_candidates local_candidates = find_backbone_candidates(cube); bb_candidates local_candidates = find_backbone_candidates(cube);
b.collect_backbone_candidates(m_l2g, local_candidates); b.collect_backbone_candidates(m_l2g, local_candidates);
if (!m.inc()) if (!m.inc()) {
b.set_cancel();
return; return;
}
} }
lbool r = check_cube(cube); lbool r = check_cube(cube);
@ -1142,7 +1149,10 @@ class parallel_solver {
continue; continue;
} }
if (!m.inc()) return; if (!m.inc()) {
b.set_cancel();
return;
}
switch (r) { switch (r) {