From 39ea5ce8c03d13cdaa200a6edfe816751f6f6b89 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sat, 27 Jun 2026 10:20:11 -0600 Subject: [PATCH] Fix SINGLE_THREAD build: add `mk_parallel_tactic` stub to `parallel_tactical.cpp` (#9977) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `#ifdef SINGLE_THREAD` block in `parallel_tactical.cpp` only defined `mk_parallel_tactic2`, leaving `mk_parallel_tactic` (called by `smt_tactic_core.cpp`, `fd_solver.cpp`, and `inc_sat_solver.cpp`) undefined — causing linker failures in the ST CI job. ## Changes - **`src/solver/parallel_tactical.cpp`**: Add `mk_parallel_tactic` stub inside `#ifdef SINGLE_THREAD` that falls back to `mk_solver2tactic(s)`, consistent with how other parallel tactics degrade in single-threaded mode (`par()` → `or_else_tactical`, `par_and_then()` → `and_then_tactical`): ```cpp #ifdef SINGLE_THREAD tactic* mk_parallel_tactic2(solver* s, params_ref const& p) { return alloc(non_parallel_tactic2, s, p); } tactic* mk_parallel_tactic(solver* s, params_ref const& /* p */) { return mk_solver2tactic(s); } #else // ... full parallel implementation ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/solver/parallel_tactical.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/solver/parallel_tactical.cpp b/src/solver/parallel_tactical.cpp index 9c986f1866..eb6659bf0d 100644 --- a/src/solver/parallel_tactical.cpp +++ b/src/solver/parallel_tactical.cpp @@ -56,6 +56,10 @@ tactic* mk_parallel_tactic2(solver* s, params_ref const& p) { return alloc(non_parallel_tactic2, s, p); } +tactic* mk_parallel_tactic(solver* s, params_ref const& /* p */) { + return mk_solver2tactic(s); +} + #else #include