From dec2f2ec9953182d57d1c6a8a776c713e3b64bf2 Mon Sep 17 00:00:00 2001
From: Ilana Shapiro <ilanashapiro@Mac.lan1>
Date: Mon, 13 Apr 2026 14:15:18 -0700
Subject: [PATCH] fix bug about backtracking condition being too strict: The
 epoch guard should not block backtrack(...) the same way it blocks
 try_split(...). A stale worker that proves UNSAT for n should still be able
 to   close n, and that closure should then cancel the other workers on n and
 its subtree.

  I changed smt/smt_parallel.cpp accordingly:

  - try_split(...) still uses epoch to reject stale structural splits
  - backtrack(...) no longer requires is_lease_valid(..., epoch); it only requires that the lease is not already canceled

  So the intended asymmetry is now restored:

  - stale split: reject
  - stale unsat/backtrack: allow closure, then cancel affected workers
---
 src/smt/smt_parallel.cpp |  6 ++----
 src/util/search_tree.h   | 13 +++----------
 2 files changed, 5 insertions(+), 14 deletions(-)

diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 2c155ba29..f87e6944c 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -332,7 +332,7 @@ namespace smt {
         auto &lease = m_worker_leases[worker_id];
         if (!lease.node || lease.node != n || lease.epoch != epoch)
             return;
-        m_search_tree.release_worker(lease.node);
+        m_search_tree.dec_active_workers(lease.node);
         lease = {};
     }
 
@@ -358,9 +358,7 @@ namespace smt {
             g_core.push_back(expr_ref(l2g(c), m));
         }
         release_lease_unlocked(worker_id, lease.node, lease.epoch);
-        if (lease.node &&
-            m_search_tree.is_lease_valid(lease.node, lease.epoch) &&
-            !m_search_tree.is_lease_canceled(lease.node, lease.cancel_epoch))
+        if (lease.node && !m_search_tree.is_lease_canceled(lease.node, lease.cancel_epoch))
             m_search_tree.backtrack(lease.node, g_core);
 
         cancel_closed_leases_unlocked(worker_id);
diff --git a/src/util/search_tree.h b/src/util/search_tree.h
index 9d93c77e7..56a9bac77 100644
--- a/src/util/search_tree.h
+++ b/src/util/search_tree.h
@@ -143,13 +143,10 @@ namespace search_tree {
             ++m_num_activations;
             ++m_active_workers;
         }
-        void release_worker() {
+        void dec_active_workers() {
             if (m_active_workers > 0)
                 --m_active_workers;
         }
-        unsigned active_workers() const {
-            return m_active_workers;
-        }
         bool has_active_workers() const {
             return m_active_workers > 0;
         }
@@ -554,14 +551,10 @@ namespace search_tree {
             return activate_best_node();
         }
 
-        void release_worker(node<Config>* n) {
+        void dec_active_workers(node<Config>* n) {
             if (!n)
                 return;
-            n->release_worker();
-        }
-
-        bool is_lease_valid(node<Config>* n, unsigned epoch) const {
-            return n && n->get_status() != status::closed && n->epoch() == epoch;
+            n->dec_active_workers();
         }
 
         bool is_lease_canceled(node<Config>* n, unsigned cancel_epoch) const {