From bd2ead977e5548bb25359410aaaa11345e6f2526 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 15 Nov 2025 16:49:13 -0800
Subject: [PATCH] add back statistics to smt-parallel

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

diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 5d1f61586..46b883b1e 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -148,6 +148,7 @@ namespace smt {
 
     void parallel::worker::share_units() {
         // Collect new units learned locally by this worker and send to batch manager
+        
         ctx->pop_to_base_lvl();
         unsigned sz = ctx->assigned_literals().size();
         for (unsigned j = m_num_shared_units; j < sz; ++j) {  // iterate only over new literals since last sync
@@ -156,7 +157,7 @@ namespace smt {
                 continue;
 
             if (m_config.m_share_units_initial_only && lit.var() >= m_num_initial_atoms) {
-                LOG_WORKER(2, " Skipping non-initial unit: " << lit.var() << "\n");
+                LOG_WORKER(4, " Skipping non-initial unit: " << lit.var() << "\n");
                 continue;  // skip non-iniial atoms if configured to do so
             }
 
@@ -285,6 +286,8 @@ namespace smt {
         // node->get_status() == status::active
         // and depth is 'high' enough
         // then ignore split, and instead set the status of node to open.
+        ++m_stats.m_num_cubes;
+        m_stats.m_max_cube_depth = std::max(m_stats.m_max_cube_depth, node->depth() + 1);
         m_search_tree.split(node, lit, nlit);
     }
 
@@ -303,7 +306,7 @@ namespace smt {
         // iterate over new clauses and assert them in the local context
         for (expr *e : new_clauses) {
             ctx->assert_expr(e);
-            LOG_WORKER(2, " asserting shared clause: " << mk_bounded_pp(e, m, 3) << "\n");
+            LOG_WORKER(4, " asserting shared clause: " << mk_bounded_pp(e, m, 3) << "\n");
         }
     }
 
diff --git a/src/util/search_tree.h b/src/util/search_tree.h
index c2bae663c..29b021906 100644
--- a/src/util/search_tree.h
+++ b/src/util/search_tree.h
@@ -68,6 +68,15 @@ namespace search_tree {
         node* left() const { return m_left; }
         node* right() const { return m_right; }
         node* parent() const { return m_parent; }
+        unsigned depth() const {
+            unsigned d = 0;
+            node* p = m_parent;
+            while (p) {
+                ++d;
+                p = p->parent();
+            }
+            return d;
+        }
 
         node* find_active_node() {
             if (m_status == status::active)