mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-29 02:39:24 +00:00
Code Activity

fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-08 15:35:18 -07:00
parent 63b4503c15
commit 99e3089f9f
2 changed files with 2 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/smt_parallel2.cpp
View file

@ -53,8 +53,7 @@ namespace smt {
void parallel2::worker::run() {
search_tree::node<cube_config>* node = nullptr;
expr_ref_vector cube(m);
while (m.inc()) {
while (true) {
collect_shared_clauses(m_g2l);
if (!b.get_cube(m_g2l, id, cube, node)) {
@ -208,7 +207,6 @@ namespace smt {
m_search_tree.backtrack(node, g_core);
if (m_search_tree.is_closed()) {
m_state = state::is_unsat;
cv.notify_all();
cancel_workers();
}
}
@ -315,7 +313,6 @@ namespace smt {
return;
m_state = state::is_sat;
p.ctx.set_model(m.translate(l2g));
cv.notify_all();
cancel_workers();
}
@ -332,7 +329,6 @@ namespace smt {
SASSERT(p.ctx.m_unsat_core.empty());
for (expr* e : unsat_core)
p.ctx.m_unsat_core.push_back(l2g(e));
cv.notify_all();
cancel_workers();
}
@ -343,7 +339,6 @@ namespace smt {
return;
m_state = state::is_exception_code;
m_exception_code = error_code;
cv.notify_all();
cancel_workers();
}
@ -354,7 +349,6 @@ namespace smt {
return;
m_state = state::is_exception_msg;
m_exception_msg = msg;
cv.notify_all();
cancel_workers();
}

1
src/smt/smt_parallel2.h
View file

@ -83,6 +83,7 @@ namespace smt {
IF_VERBOSE(1, verbose_stream() << "Canceling workers\n");
for (auto& w : p.m_workers)
w->cancel();
cv.notify_all();
}
void init_parameters_state();