diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index f87e6944c..07a29d777 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -358,7 +358,13 @@ 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_canceled(lease.node, lease.cancel_epoch))
+
+        // only backtrack if the lease is still valid (i.e., the worker has not been given a new node to work on or the lease has not been canceled by another worker)
+        // this means we can potentially delay backtracking for some unsat cubes until another worker (whose lease is valid) determines it UNSAT. 
+        // Empirically, this is better than aggressively backtracking on every unsat cube, for now.
+        if (lease.node &&
+            m_search_tree.is_lease_valid(lease.node, lease.epoch) &&
+            !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 56a9bac77..15f86eafa 100644
--- a/src/util/search_tree.h
+++ b/src/util/search_tree.h
@@ -557,6 +557,10 @@ namespace search_tree {
             n->dec_active_workers();
         }
 
+        bool is_lease_valid(node<Config>* n, unsigned epoch) const {
+            return n && n->get_status() != status::closed && n->epoch() == epoch;
+        }
+        
         bool is_lease_canceled(node<Config>* n, unsigned cancel_epoch) const {
             return !n || n->get_status() == status::closed || n->get_cancel_epoch() != cancel_epoch;
         }