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];