From c36cb2f516d18ed2b56373705f517da747da5aeb Mon Sep 17 00:00:00 2001
From: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Date: Sat, 20 Dec 2025 09:36:30 -0800
Subject: [PATCH] dont collect clauses twice

---
 src/smt/smt_parallel.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index b8629fb50..5f20c623c 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -236,7 +236,6 @@ 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];