From f07acb459ff23c278adc890befe1cdc482ff432c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sat, 27 Jun 2026 18:25:04 -0700 Subject: [PATCH] Fix WASM build: remove duplicate mk_parallel_tactic definition (#9979) ## Problem The [master WebAssembly Build](https://github.com/Z3Prover/z3/actions/runs/28306680131) fails with: ``` ../src/solver/parallel_tactical.cpp:59:9: error: redefinition of 'mk_parallel_tactic' 59 | tactic* mk_parallel_tactic(solver* s, params_ref const& /* p */) { ../src/solver/parallel_tactical.cpp:55:9: note: previous definition is here ``` ## Cause Commit 7564ccc3f (an unrelated lar_solver change) accidentally renamed the dead `mk_parallel_tactic2` stub to `mk_parallel_tactic`, leaving two identical definitions inside the `#ifdef SINGLE_THREAD` block. The WASM build defines `SINGLE_THREAD`, so it hits the redefinition. ## Fix `mk_parallel_tactic2` and its `non_parallel_tactic2` class were never referenced anywhere. This removes the dead stub and orphaned class, keeping the single `mk_parallel_tactic` that degrades to `mk_solver2tactic(s)` in single-threaded mode (added in #9977). Verified both `SINGLE_THREAD` and multi-threaded paths pass `-fsyntax-only`. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/solver/parallel_tactical.cpp | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/src/solver/parallel_tactical.cpp b/src/solver/parallel_tactical.cpp index b2955ed5a2..c5f4949bee 100644 --- a/src/solver/parallel_tactical.cpp +++ b/src/solver/parallel_tactical.cpp @@ -35,27 +35,8 @@ Author: #include #include -/* ------------------------------------------------------------------ */ -/* Single-threaded stub */ -/* ------------------------------------------------------------------ */ - -class non_parallel_tactic2 : public tactic { -public: - non_parallel_tactic2(solver*, params_ref const&) {} - char const* name() const override { return "parallel_tactic2"; } - void operator()(const goal_ref&, goal_ref_buffer&) override { - throw default_exception("parallel_tactic2 is disabled in single-threaded mode"); - } - tactic* translate(ast_manager&) override { return nullptr; } - void cleanup() override {} -}; - #ifdef SINGLE_THREAD -tactic* mk_parallel_tactic(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); }