From 189a03c94a10270c81cdf7692d33ec7a267707c3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 8 Sep 2025 16:10:16 -0700
Subject: [PATCH] work-coop

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_parallel2.cpp |  7 +++++++
 src/util/search_tree.h    | 18 ++++++++++++++++++
 2 files changed, 25 insertions(+)

diff --git a/src/smt/smt_parallel2.cpp b/src/smt/smt_parallel2.cpp
index 4549c0c75..8b2aec7a2 100644
--- a/src/smt/smt_parallel2.cpp
+++ b/src/smt/smt_parallel2.cpp
@@ -203,6 +203,8 @@ namespace smt {
             g_core.push_back(expr_ref(l2g(c), m));
         }
         m_search_tree.backtrack(node, g_core);
+
+        IF_VERBOSE(1, m_search_tree.display(verbose_stream() << core << "\n"););
         if (m_search_tree.is_closed()) {
             m_state = state::is_unsat;
             cancel_workers();
@@ -400,6 +402,11 @@ namespace smt {
                 cv.notify_all();
                 return false;
             }
+            t = m_search_tree.find_active_node();
+            if (t) {
+                IF_VERBOSE(1, verbose_stream() << "found active node\n";);
+                break;
+            }
             IF_VERBOSE(1, verbose_stream() << "waiting... " << id << "\n";);
             cv.wait(lock);
             IF_VERBOSE(1, verbose_stream() << "release... " << id << "\n";);
diff --git a/src/util/search_tree.h b/src/util/search_tree.h
index 5f3e6d239..b7a833cd2 100644
--- a/src/util/search_tree.h
+++ b/src/util/search_tree.h
@@ -69,6 +69,20 @@ namespace search_tree {
         node* right() const { return m_right; }
         node* parent() const { return m_parent; }
 
+        node* find_active_node() {
+            if (m_status == status::active)
+                return this;
+            if (m_status != status::open)
+                return nullptr;
+            node* nodes[2] = { m_left, m_right };
+            for (unsigned i = 0; i < 2; ++i) {
+                auto res = nodes[i] ? nodes[i]->find_active_node() : nullptr;
+                if (res)
+                    return res;
+            }
+            return nullptr;
+        }
+
         void display(std::ostream& out, unsigned indent) const {
             for (unsigned i = 0; i < indent; ++i)
                 out << " ";
@@ -218,6 +232,10 @@ namespace search_tree {
             return nullptr;
         }
 
+        node<Config>* find_active_node() {
+            return m_root->find_active_node();
+        }
+
         bool is_closed() const {
             return m_root->get_status() == status::closed;
         }