From ea4bec9d039a2b61ad7102c7b62038a4178a1ba8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Sep 2025 17:40:41 -0700 Subject: [PATCH] internalize assertions during simplify Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel2.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/smt/smt_parallel2.cpp b/src/smt/smt_parallel2.cpp index 7a9253bed..d72a8014e 100644 --- a/src/smt/smt_parallel2.cpp +++ b/src/smt/smt_parallel2.cpp @@ -255,6 +255,8 @@ namespace smt { void parallel2::worker::simplify() { + if (!m.inc()) + return; // first attempt: one-shot simplification of the context. // a precise schedule of repeated simplification is TBD. // also, the in-processing simplifier should be applied to @@ -309,6 +311,14 @@ namespace smt { } ctx = new_ctx.detach(); + ctx->internalize_assertions(); + + auto old_atoms = m_num_initial_atoms; + m_num_shared_units = ctx->assigned_literals().size(); + m_num_initial_atoms = ctx->get_num_bool_vars(); + + + LOG_WORKER(1, " inprocess " << old_atoms << " -> " << m_num_initial_atoms << "\n"); // TODO: copy user-propagators similar to context::copy. }