From 3ba08bd3c5ad910d91b761eaae8b959a07887520 Mon Sep 17 00:00:00 2001
From: Ilana Shapiro <ishapiro00@gmail.com>
Date: Thu, 14 Aug 2025 12:35:00 -0700
Subject: [PATCH] Revert "resolve bug about not popping local ctx to base level
 before collecting shared lits"

This reverts commit bba1111e1b11cd14c0e266af6c5b0bd549f081a6.
---
 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 66e4ee28d..5a7615f4b 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -124,7 +124,6 @@ namespace smt {
 
     void parallel::worker::share_units(ast_translation& l2g) {
         // 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
             literal lit = ctx->assigned_literals()[j];