From e11bf4b9b16d3f83f7f2227f6b7df13873b25e82 Mon Sep 17 00:00:00 2001
From: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Date: Fri, 19 Dec 2025 17:15:39 -0800
Subject: [PATCH] collect shared clauses inside share units after pop to base
 level (might help NIA)

---
 src/smt/smt_parallel.cpp | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 49e03c8e2..b8629fb50 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -154,6 +154,10 @@ namespace smt {
                     goto check_cube_start;
                 b.split(m_l2g, id, node, atom);
                 simplify();
+                if (m_config.m_share_units) {
+                    IF_VERBOSE(1, verbose_stream() << " Sharing units\n");
+                    share_units();
+                }
                 break;
             }
             case l_true: {
@@ -203,10 +207,6 @@ namespace smt {
                 break;
             }
             }
-            if (m_config.m_share_units) {
-                IF_VERBOSE(1, verbose_stream() << " Sharing units\n");
-                share_units();
-            }
         }
     }
 
@@ -236,6 +236,7 @@ namespace smt {
         // Collect new units learned locally by this worker and send to batch manager
         
         ctx->pop_to_base_lvl();
+        collect_shared_clauses(); // collect shared clauses from other workers while we're ALREADY POPPED TO BASE LEVEL
         unsigned sz = ctx->assigned_literals().size();
         for (unsigned j = m_num_shared_units; j < sz; ++j) {  // iterate only over new literals since last sync
             literal lit = ctx->assigned_literals()[j];