From 5abf942c758ecd6c7ea89e261332483f6308c0a2 Mon Sep 17 00:00:00 2001
From: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Date: Sun, 21 Jun 2026 17:43:17 -0700
Subject: [PATCH] a couple more bugfixes about leases

---
 src/smt/smt_parallel.cpp          | 25 +++++++++++++++++--------
 src/solver/parallel_tactical2.cpp | 25 +++++++++++++++----------
 2 files changed, 32 insertions(+), 18 deletions(-)

diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index f26fb52bb..f02a39bc2 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -1409,14 +1409,21 @@ namespace smt {
         SASSERT(lease != nullptr || targets != nullptr);
         bool did_backtrack = false;
 
-        if (lease && !m_search_tree.is_lease_canceled(lease->leased_node)) {
-            // we close/backtrack regardless of whether this lease is stale or not, as long as the lease isn't canceled
-            // i.e. worker 1 splits this node, but then worker 2 determines UNSAT --> worker 2 is stale but we still close this node and backtrack
-            did_backtrack = true;
-            IF_VERBOSE(1, verbose_stream() << "Batch manager backtracking.\n");
-            node* leased_node = lease->leased_node;
-            release_worker_lease_unlocked(worker_id, *lease);
-            m_search_tree.backtrack(leased_node, g_core);
+        if (lease) {
+            if (!m_search_tree.is_lease_canceled(lease->leased_node)) {
+                // we close/backtrack regardless of whether this lease is stale or not, as long as the lease isn't canceled
+                // i.e. worker 1 splits this node, but then worker 2 determines UNSAT --> worker 2 is stale but we still close this node and backtrack
+                did_backtrack = true;
+                IF_VERBOSE(1, verbose_stream() << "Batch manager backtracking.\n");
+                node* leased_node = lease->leased_node;
+                release_worker_lease_unlocked(worker_id, *lease);
+                m_search_tree.backtrack(leased_node, g_core);
+            }
+            else { 
+                // the lease was canceled by another worker. don't backtrack on this node with whatever new core we just found with this thread
+                // however, we do proceed to external targets, since the new code may have exposed new external targets we can close/backtrack
+                attempt_release_canceled_lease_unlocked(worker_id, *lease);
+            }
         }
         if (targets) {
             for (auto const& target : *targets) {
@@ -1461,6 +1468,8 @@ namespace smt {
         lit = l2g(atom);
         nlit = mk_not(m, lit);
         node* leased_node = lease.leased_node;
+        VERIFY(!leased_node->path_contains_atom(lit));
+        VERIFY(!leased_node->path_contains_atom(nlit));
         bool did_split = m_search_tree.try_split(leased_node, lit, nlit, effort);
 
         release_worker_lease_unlocked(worker_id, lease);
diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp
index 1694a5461..c3a77149e 100644
--- a/src/solver/parallel_tactical2.cpp
+++ b/src/solver/parallel_tactical2.cpp
@@ -424,16 +424,21 @@ class parallel_solver {
             SASSERT(lease != nullptr || targets != nullptr);
             bool did_backtrack = false;
 
-            if (lease && !m_search_tree.is_lease_canceled(lease->leased_node)) {
-                // we close/backtrack regardless of whether this lease is stale or not, as long as the lease isn't canceled
-                // i.e. worker 1 splits this node, but then worker 2 determines UNSAT --> worker 2 is stale but we still close this node and backtrack
-                auto* leased_node = lease->leased_node;
-                did_backtrack = true;
-                release_worker_lease_unlocked(worker_id, *lease);
-                m_search_tree.backtrack(leased_node, g_core);
-            }
-            else if (lease) {
-                attempt_release_canceled_lease_unlocked(worker_id, *lease);
+            if (lease) {
+                if (!m_search_tree.is_lease_canceled(lease->leased_node)) {
+                    // we close/backtrack regardless of whether this lease is stale or not, as long as the lease isn't canceled
+                    // i.e. worker 1 splits this node, but then worker 2 determines UNSAT --> worker 2 is stale but we still close this node and backtrack
+                    did_backtrack = true;
+                    IF_VERBOSE(1, verbose_stream() << "Batch manager backtracking.\n");
+                    auto* leased_node = lease->leased_node;
+                    release_worker_lease_unlocked(worker_id, *lease);
+                    m_search_tree.backtrack(leased_node, g_core);
+                }
+                else { 
+                    // the lease was canceled by another worker. don't backtrack on this node with the new, arbitrary core we just found with this thread
+                    // however, we do proceed to external targets, since the new code may have exposed new external targets we can close/backtrack
+                    attempt_release_canceled_lease_unlocked(worker_id, *lease);
+                }
             }
             if (targets) {
                 for (auto const& target : *targets) {