diff --git a/src/smt/smt_parallel2.cpp b/src/smt/smt_parallel2.cpp
index 8b2aec7a2..2844949d2 100644
--- a/src/smt/smt_parallel2.cpp
+++ b/src/smt/smt_parallel2.cpp
@@ -220,6 +220,10 @@ namespace smt {
         IF_VERBOSE(1, verbose_stream() << "Batch manager splitting on literal: " << mk_bounded_pp(lit, m, 3) << "\n");
         if (m_state != state::is_running)
             return;
+        // optional heuristic:
+        // node->get_status() == status::active
+        // and depth is 'high' enough
+        // then ignore split, and instead set the status of node to open.
         m_search_tree.split(node, lit, nlit);
         cv.notify_all();
     }
diff --git a/src/util/search_tree.h b/src/util/search_tree.h
index b7a833cd2..778315fab 100644
--- a/src/util/search_tree.h
+++ b/src/util/search_tree.h
@@ -80,6 +80,8 @@ namespace search_tree {
                 if (res)
                     return res;
             }
+            if (m_left->get_status() == status::closed && m_right->get_status() == status::closed)
+                m_status = status::closed;
             return nullptr;
         }
 
@@ -137,6 +139,19 @@ namespace search_tree {
             n->set_status(status::closed);
             close_node(n->left());
             close_node(n->right());
+            while (n) {
+                auto p = n->parent();
+                if (!p)
+                    return;
+                if (p->get_status() != status::open)
+                    return;
+                if (p->left()->get_status() != status::closed)
+                    return;
+                if (p->right()->get_status() != status::closed)
+                    return;
+                p->set_status(status::closed);
+                n = p;
+            }
         }
 
     public: