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 15:58:10 -07:00
parent 356d3a4de1
commit 49e4c2e9eb
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/smt_parallel2.cpp
View file

@ -343,7 +343,7 @@ namespace smt {
void parallel2::batch_manager::set_exception(std::string const& msg) { void parallel2::batch_manager::set_exception(std::string const& msg) {
std::scoped_lock lock(mux); std::scoped_lock lock(mux);
IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception msg: " << msg << ".\n"); IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception msg: " << msg << ".\n");
if (m_state != state::is_running || m.limit().is_canceled()) if (m_state != state::is_running)
return; return;
m_state = state::is_exception_msg; m_state = state::is_exception_msg;
m_exception_msg = msg; m_exception_msg = msg;
@ -390,7 +390,6 @@ namespace smt {
while ((t = m_search_tree.activate_node(n)) == nullptr) { while ((t = m_search_tree.activate_node(n)) == nullptr) {
// if all threads have reported they are done, then return false // if all threads have reported they are done, then return false
// otherwise wait for condition variable // otherwise wait for condition variable
IF_VERBOSE(1, verbose_stream() << "waiting... " << "\n";);
if (m_search_tree.is_closed()) { if (m_search_tree.is_closed()) {
IF_VERBOSE(1, verbose_stream() << "all done\n";); IF_VERBOSE(1, verbose_stream() << "all done\n";);
cv.notify_all(); cv.notify_all();
@ -401,7 +400,9 @@ namespace smt {
cv.notify_all(); cv.notify_all();
return false; return false;
} }
IF_VERBOSE(1, verbose_stream() << "waiting... " << id << "\n";);
cv.wait(lock); cv.wait(lock);
IF_VERBOSE(1, verbose_stream() << "release... " << id << "\n";);
} }
IF_VERBOSE(1, m_search_tree.display(verbose_stream()); verbose_stream() << "\n";); IF_VERBOSE(1, m_search_tree.display(verbose_stream()); verbose_stream() << "\n";);
n = t; n = t;