3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-28 03:18:49 +00:00

Fix SINGLE_THREAD build: add mk_parallel_tactic stub to parallel_tactical.cpp (#9977)

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>
This commit is contained in:
Copilot 2026-06-27 10:20:11 -06:00 committed by GitHub
parent 6a62a53181
commit 39ea5ce8c0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -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 <atomic>