3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-28 19:38:51 +00:00
z3/src/solver
Lev Nachmanson f07acb459f
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>
2026-06-27 18:25:04 -07:00
..
assertions Use "override" keyword where needed. (#9892) 2026-06-18 13:36:14 -06:00
check_logic.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
check_logic.h debug arith/mbi 2020-11-02 12:13:19 -08:00
check_sat_result.cpp refactor solver to include settable stats 2026-06-07 14:17:38 -07:00
check_sat_result.h refactor solver to include settable stats 2026-06-07 14:17:38 -07:00
CMakeLists.txt Parallel tactic (#9824) (#9825) 2026-06-26 10:36:15 -06:00
combined_solver.cpp refactor solver to include settable stats 2026-06-07 14:17:38 -07:00
combined_solver.h booyah 2020-07-04 15:56:30 -07:00
combined_solver_params.pyg solver factories, cleanup solver API, simplified strategic solver, added combined solver 2012-12-11 17:47:27 -08:00
mus.cpp Remove copies (#8583) 2026-02-18 21:02:22 -08:00
mus.h booyah 2020-07-04 15:56:30 -07:00
parallel_params.pyg Parallel tactic (#9824) (#9825) 2026-06-26 10:36:15 -06:00
parallel_tactical.cpp Fix WASM build: remove duplicate mk_parallel_tactic definition (#9979) 2026-06-27 18:25:04 -07:00
parallel_tactical.h Parallel tactic (#9824) (#9825) 2026-06-26 10:36:15 -06:00
preferred_value_propagator.h Remove redundant non-virtual destructors with = default (#8462) 2026-02-18 20:58:01 -08:00
progress_callback.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
simplifier_solver.cpp refactor solver to include settable stats 2026-06-07 14:17:38 -07:00
simplifier_solver.h Add simplification customization for SMTLIB2 2023-01-30 22:38:51 -08:00
slice_solver.cpp refactor solver to include settable stats 2026-06-07 14:17:38 -07:00
slice_solver.h A slice solver option for interactive use case 2024-10-08 09:24:52 -07:00
smt_logics.cpp benchmark patching 2026-05-20 13:32:23 -07:00
smt_logics.h SMT2 front-end: accept HO_ALL and normalize curried expression-head applications (#9636) 2026-05-26 18:39:38 -07:00
solver.cpp #7468 - add option (get-info :parameters) to display solver parameters that were updated globally and distinct from defaults 2025-02-10 11:57:14 -08:00
solver.h Parallel tactic (#9824) (#9825) 2026-06-26 10:36:15 -06:00
solver2tactic.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
solver2tactic.h move model and proof converters to self-contained module 2022-11-03 05:23:01 -07:00
solver_na2as.cpp display assumptions used 2025-09-11 10:20:55 -07:00
solver_na2as.h remove default destructors & some default constructors 2024-09-04 22:30:23 +01:00
solver_pool.cpp refactor solver to include settable stats 2026-06-07 14:17:38 -07:00
solver_pool.h booyah 2020-07-04 15:56:30 -07:00
solver_preprocess.cpp move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
solver_preprocess.h add unconstrained elimination for sequences 2023-03-20 17:07:04 +01:00
tactic2solver.cpp refactor solver to include settable stats 2026-06-07 14:17:38 -07:00
tactic2solver.h booyah 2020-07-04 15:56:30 -07:00