From 46a45dee04c6fc380cff927192f1d9e0f736bea5 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Fri, 3 Jul 2026 05:52:36 -0700
Subject: [PATCH] smt_parallel: keep preprocessing for quantified formulas so
 MBQI can solve

The parallel SMT worker contexts disable preprocessing
(`m_preprocess = false`) so that units/clauses exchanged between workers
refer to a stable, shared atom set. This is fine for the quantifier-free
cubing the parallel solver was designed for, but it breaks quantifier
reasoning: MBQI relies on preprocessing (macro/quantifier simplification
and trigger setup). With preprocessing disabled, a worker running MBQI on
a satisfiable quantified formula can spin indefinitely and never find a
model that the sequential solver dispatches immediately.

Concretely, on `iss-3268/bug-1.smt2` (a satisfiable quantified array
formula that sets `smt.threads 4`) the sequential solver returns `sat` in
0.04s (64 conflicts), while every parallel worker fails to find a model
even with an effectively unbounded per-cube conflict budget, so the run
hits the wall-clock timeout.

Gate preprocessing on `ctx->has_quantifiers()` in the three worker
constructors (CDCL worker, core-minimizer worker, backbones worker):
keep it disabled for quantifier-free problems (unchanged behavior for the
cubing use case) and enable it when quantifiers are present so MBQI works.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/smt/smt_parallel.cpp | 21 ++++++++++++++++++---
 1 file changed, 18 insertions(+), 3 deletions(-)

diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 5096d23144..fab3092047 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -626,7 +626,12 @@ namespace smt {
         ctx->set_logic(p.ctx.m_setup.get_logic());
         context::copy(p.ctx, *ctx, true);
         ctx->pop_to_base_lvl();
-        ctx->get_fparams().m_preprocess = false;  // avoid preprocessing lemmas that are exchanged
+        // Disable preprocessing so units/clauses exchanged between workers refer to a
+        // stable shared atom set, but keep it enabled for quantified formulas: MBQI
+        // relies on preprocessing (macro/quantifier simplification, trigger setup) and
+        // without it a satisfiable quantified formula can spin without ever finding a
+        // model the sequential solver dispatches immediately.
+        ctx->get_fparams().m_preprocess = ctx->has_quantifiers();
     }
 
     void parallel::core_minimizer_worker::cancel() {
@@ -866,7 +871,12 @@ namespace smt {
         ctx->pop_to_base_lvl();
         m_shared_units_prefix = ctx->assigned_literals().size();
         m_num_initial_atoms = ctx->get_num_bool_vars();
-        ctx->get_fparams().m_preprocess = false;  // avoid preprocessing lemmas that are exchanged
+        // Disable preprocessing so units/clauses exchanged between workers refer to a
+        // stable shared atom set, but keep it enabled for quantified formulas: MBQI
+        // relies on preprocessing (macro/quantifier simplification, trigger setup) and
+        // without it a satisfiable quantified formula can spin without ever finding a
+        // model the sequential solver dispatches immediately.
+        ctx->get_fparams().m_preprocess = ctx->has_quantifiers();
 
         parallel_params pp(p.ctx.m_params);
         m_config.m_inprocessing = false;
@@ -901,7 +911,12 @@ namespace smt {
         ctx->pop_to_base_lvl();
         m_shared_units_prefix = ctx->assigned_literals().size();
         m_num_initial_atoms = ctx->get_num_bool_vars();
-        ctx->get_fparams().m_preprocess = false;  // avoid preprocessing lemmas that are exchanged
+        // Disable preprocessing so units/clauses exchanged between workers refer to a
+        // stable shared atom set, but keep it enabled for quantified formulas: MBQI
+        // relies on preprocessing (macro/quantifier simplification, trigger setup) and
+        // without it a satisfiable quantified formula can spin without ever finding a
+        // model the sequential solver dispatches immediately.
+        ctx->get_fparams().m_preprocess = ctx->has_quantifiers();
 
         m_use_failed_literal_test = false;
     }