This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
The PR adds
```
"-Wsuggest-override"
"-Winconsistent-missing-override"
```
to the CLANG_ONLY_WARNINGS. This exposes a relatively small number of places where method overrides did not use the "override" keyword. The PR fixes those.
(In cmd_util.h, I also made the *_CMD macros be uniform in not ending the class they define with a semicolon; the invocation of the macro can add the semicolon.)
## Summary
z3 already builds under Pyodide (there is a `pyodide.yml` workflow and
an
`IS_PYODIDE` path in `setup.py`), but that path uses `pyodide build` and
produces
a wheel tagged `emscripten_<pyodide-version>_wasm32`, which is pinned to
a single
Pyodide release and rejected by PyPI — so today it's only usable as a CI
artifact.
[PEP 783](https://peps.python.org/pep-0783/) introduced the portable
`pyemscripten_<date>_wasm32` platform tag that **PyPI accepts** and
`micropip` can
install at runtime. This makes `z3-solver` build that wheel via
`cibuildwheel --platform pyodide`.
## Changes
- **`setup.py`** — for the emscripten target, use the wheel platform tag
that
pyodide-build provides verbatim via `_PYTHON_HOST_PLATFORM` (e.g.
`pyemscripten_2026_0_wasm32`) instead of reconstructing an
`emscripten_*` tag.
Falls back to the previous behaviour when that env var is absent.
- **`setup.py` / `CMakeLists.txt` / `pyproject.toml`** — switch the
Pyodide build
from JS-based exceptions (`-fexceptions`,
`-sDISABLE_EXCEPTION_CATCHING=0`) to
**native wasm exception handling** (`-fwasm-exceptions
-sSUPPORT_LONGJMP=wasm`),
matching the ABI of the Pyodide 314 / emscripten 5 main module. With the
old
flags `libz3.so` imports `invoke_*` trampolines the runtime no longer
provides,
so the wheel builds but the first `Z3_mk_config` call fails at runtime
with
`Dynamic linking error: cannot resolve symbol invoke_vi`.
- **`pyproject.toml`** — add `[tool.cibuildwheel]` /
`[tool.pyodide.build]` so
`cibuildwheel --platform pyodide` builds and tests the wheel (`cp314`).
- **`.github/workflows/pyodide-pypi.yml`** (new) — build with
cibuildwheel and
publish to PyPI (trusted publishing) on tags. Existing `pyodide.yml`
unchanged.
## Verification
Built with `cibuildwheel 4.1.0` / `pyodide-build 0.35.0` / `emscripten
5.0.3`,
CPython 3.14 / Pyodide 314:
- Produces `z3_solver-4.17.0.0-py3-none-pyemscripten_2026_0_wasm32.whl`.
- `z3test.py` passes in the Pyodide runtime (node + wasm32).
- Installed via `micropip` and solves SMT problems both under node and
in a
browser (`sat` with a model, `unsat` for a contradiction).
🤖 Generated with [Claude Code](https://claude.com/claude-code)
🕵️♂️ Reviewed by [Alcides Fonseca](https://wiki.alcidesfonseca.com)
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
This is another PR towards the goal of getting a clean build with clang,
using the compiler options used in building clang-tidy.
In https://github.com/Z3Prover/z3/pull/9800, we changed the build flags
to eliminate a warning for zero-length arrays. In that PR, I missed this
one: there was one instance of m_arr[] instead of m_arr[0]. In the
clang-tidy build, that gives warnings like:
```
/Users/daviddetlefs/llvm-project/build_dbg/_deps/z3-src/src/model/func_interp.h:43:12: warning: flexible array members are a C99 feature [-Wc99-extensions]
```
The PR fixes this, making it a zero-length array, the idiom used in all
the other similar cases. I also added the compiler flag that produced
this warning, so we can notice such changes in the future.
PR #9872 caused timeouts in QF_UFBV, QF_BV, and QF_FP regressions
(`t135`, `t136`, `nl53`, `3397`, `4841-1`, `fp-lt-gt`, `fp-rem-11`).
## Root cause
The `goal2sat` change skipped caching AST nodes with `ref_count ≤ 1`
under the assumption they're visited only once. This assumption is
wrong: EUF, BV, and FP theory extensions all call `internalize()` from
the theory solver side, outside the main DFS traversal. On the second
`internalize(n)` call, the missing cache entry causes the entire subtree
to be re-encoded with a fresh literal — inconsistent encoding and
exponential blowup.
## Changes
- **`goal2sat.cpp`**: revert the `ref_count ≤ 1` skip-caching
optimization entirely; it is unsafe whenever any theory extension is
active.
- **`bit_blaster_tpl_def.h`**: retain the `mk_eq` micro-optimization
from #9872 — pre-size with `resize(sz)` and use index assignment instead
of `push_back`. This is correct: `resize` null-initializes slots and
`element_ref::operator=` handles ref-counting via `inc_ref`/`dec_ref`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This tightens two historical `nlsat` regressions that were still
print-only.
Closes#9859.
In `tst_16`, the test already exercises the old `lws2380` shape, but it
only dumped the projected clause. On current `master`, both projection
paths still keep the `x7`-linked root constraints, so this change turns
that observation into an assertion and updates the stale comment to
describe the current invariant.
In `tst_22`, the test already computes whether the projected lemma is
falsified at the stored counterexample. It previously printed the result
and kept going. This change adds `ENSURE(!all_false)` so the test fails
if that historical unsoundness shape comes back.
Testing:
`cmake --build . --target test-z3 -j1`
`./test-z3 /seq nlsat`
`Microsoft.Z3.dll` ships with PE `Machine=0x8664` (AMD64), causing the
CLR loader to reject it on arm64 .NET hosts (macOS/Linux/Windows ARM)
even though the assembly is pure IL (`CorFlags.ILONLY=True`) and arm64
native libraries are already bundled in the package.
## Changes
- **`.github/workflows/nightly-validation.yml`** — adds
`validate-dotnet-anycpu` job to the Nightly Build Validation workflow:
- Downloads the nightly NuGet package from the GitHub release
- Extracts `lib/netstandard2.0/Microsoft.Z3.dll` (NuGet packages are ZIP
archives)
- Reads the COFF `Machine` field from the PE header using Python
`struct`
- Fails with an actionable error if `Machine` is `0x8664` (AMD64) or
`0xAA64` (ARM64); passes for `0x014C` (i386/AnyCPU) or `0x0000`
The check catches any regression where the managed wrapper is compiled
architecture-specific, blocking non-x64 .NET hosts from loading it.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`Microsoft.Z3.dll` was being emitted with PE `Machine=0x8664` (AMD64)
despite being pure IL, because the Windows x64 CI environment
(`vcvarsall.bat x64`) injects `Platform=x64` into MSBuild, which sets
the COFF machine type when `PlatformTarget` is not explicitly specified.
This causes `FS0193` / architecture mismatch errors on any arm64 .NET
host (macOS Apple Silicon, Linux aarch64, Windows on ARM).
## Changes
- **`scripts/mk_util.py`** — Add
`<PlatformTarget>AnyCPU</PlatformTarget>` to the in-memory `.csproj`
template generated by the Python build system (`mk_win_dist.py`,
`mk_unix_dist.py`)
- **`src/api/dotnet/Microsoft.Z3.csproj.in`** — Add
`<PlatformTarget>AnyCPU</PlatformTarget>` to the CMake build system
template
Both paths now produce `Machine=0x014C` (i386/AnyCPU) regardless of host
or CI environment, matching the assembly's actual nature (`ILONLY=True`,
`32BIT_REQUIRED=False`). The native side already ships six RIDs; no
changes needed there.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This is another PR towards the goal of getting a clean build with clang,
using the compiler options used in building clang-tidy.
By default, without any new -W flags, clang warns about unused local
variables and private class fields. This PR deletes the handful of these
that clang found.
I'm assuming that the class "enode" in smt_context.cpp is the one in
smt_enode.h, so that
```
parent->get_expr()
```
calls a const method with no side effects.
## Summary
egex_bisim::collect_leaves used to descend through `re.union` and
`re.antimirov_union` at the top of each leaf of the transition regex,
splitting a single bisimulation state into multiple states before they
were merged into the union-find. This contradicts the bisimulation
invariant: **each leaf of a t-regex represents one state, regardless of
its top-level shape**. The fix descends into `ite` only (which is the
actual structural splitter of guarded transitions).
## Why it matters
The split happens to be *sound* for the current algorithm when the goal
is asserting `L(union(A, B)) = empty` (since `L(A) = empty AND L(B) =
empty` is equivalent), but it:
1. Adds spurious merges to the union-find that distort state-class
identities.
2. Slows convergence on hard equivalence queries (and causes early
timeouts in practice).
3. Creates latent unsoundness risk for any extension that interprets
leaves more semantically (XOR pair handling, classical-flag propagation,
future antimirov re-enable, etc.).
## Empirical validation
Run on the 1523-file regex-equivalence corpus, 5s/file timeout, 8
workers:
| metric | pre-fix master | post-fix |
|---|---|---|
| sat | 1008 | 1014 |
| unsat | 368 | 368 |
| timeout | 145 | 139 |
| unknown | 2 | 2 |
| SAT↔UNSAT verdict flips | — | **0** |
| timeout→sat flips | — | 6 |
| commonly-solved wall ratio | 1.000x | **0.902x** |
The 6 `timeout` → `sat` cases all return the *same* `sat` under
pre-fix master if given 60s; they are previously-slow cases not
previously-wrong ones.
Z3 unit tests: 89/89 pass (`test-z3 /a`).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The single-ITE branch of hoist_ite was gated by 'm_path_stack.size() < 8'.
When the depth limit was reached, hoist_ite returned nullptr and callers
fell back to non-path-aware structural rewrites (mk_union0 / mk_xor0).
These rewrites simplify e.g. mk_union(empty, X) -> X and return X unchanged,
preserving inner ITE branches that were built at an earlier (less constrained)
path. Subsequent derivative computation never path-prunes those branches,
which can leak unreachable epsilon-leaves into the final t-regex and cause
the bisimulation algorithm to report inequivalence for equivalent regexes.
Concrete trigger: derivatives of unions/xors with >= 9 components produce
9-deep ITE chains; at depth 8 the inner ITE returns unprocessed, leaving an
unreachable epsilon-leaf that bisim mis-interprets as a distinguishing word.
Removing the guard restores soundness. The corpus run against
regex-equivalence (1523 files) fixes 22 triangulated soundness bugs
(mut_0013, mut_0241, mut_0257, mut_0301 among others) with zero regressions.
89/89 unit tests pass.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
`seq::derive::operator()(ele, r)` looks up `m_top_cache` keyed only by the
regex `r`, but on a miss it used to set `m_ele = ele` (a concrete char)
before calling `derive_rec(r)`. The resulting ITE-tree contained
constant-folded `(= ele c)` conditions, so the "symbolic" derivative
stored in the cache was actually specialized to that one ele. Subsequent
calls with the same `r` but a different ele hit the stale cached answer
and the substitution at the bottom was a no-op (no `v0` left to replace).
Simplest victim:
(str.in_re "aP" (re.++ (re.* "a") "P"))
returned `unsat`. The first call D_'a'(a*P) computed `a*P` and cached it
under key `a*P`; the next call D_'P'(a*P) hit that cache entry and
returned `a*P` instead of epsilon, so the membership check ended on a
non-nullable state.
Fix: set `m_ele = v` (the canonical fresh var) so the derivative is
genuinely symbolic. Concrete-ele callers go through the existing
substitution at the bottom of `operator()`.
Adds a regression test in src/test/seq_regex_bisim.cpp checking that
D_'a'(a*P) is not nullable while D_'P'(a*P) is.
Note: this is independent of the mut_0013 bisim-level unsoundness;
that case still fails and is being tracked separately.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The intersect_intervals routine in seq_derive.cpp maintains a path-tracking
disjoint union of character intervals. When intersecting the active suffix
with a new constraint [lo, hi], it iterated the suffix and, on encountering
the first interval disjoint from [lo, hi], reset the output cursor to the
end-marker and broke out of the loop. This both threw away the intervals it
had already kept and skipped every remaining interval, so e.g.
[(0, 96), (98, max)] intersected with [98, 98] became empty instead of
[(98, 98)].
Inside derive that silently killed valid branches of symbolic derivatives.
For example D(a|b) collapsed to ite(c='a', eps, empty) -- the 'b' branch
vanished -- which made the bisimulation procedure conclude bogus equalities
such as a* == (a|b)*. On the regex-equivalence corpus this single bug
accounted for ~510 false-unsat results vs master.
Fix: drop only the disjoint interval and continue scanning the rest of the
suffix. Add a small assertion-based regression test that builds D(a|b),
checks both branches survive, and runs bisim on a* vs (a|b)*.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Implemented the largest cube heuristic from Bromberger and Weidenbach's
paper on cubes. Also fixes an overflow bug in mzp.
Use vswhere to find the visual studio version on windows in the build's ymls.
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
This one concerns "-Wzero-length-array". Many classes in Z3 use the
"trailing array" idiom: the last field of the class C is a zero-length
array of some type T, and the allocation of an instance adds extra space
for some number of T's (usually the number is held in some other field
of C).
When the flag -Wzero-length-array is used, this gives warnings like:
```
warning: zero size arrays are an extension [-Wzero-length-array]
```
This PR first adds -Wzero-length-array to the CLANG_ONLY_WARNINGS
defined in compiler_warnings.cmake. This causes the warnings to occur in
a normal clang Z3 build. We then make a trailing_array.h, that defines a
TRAILING_ARRAY(type, field) macro. This is defined, on per-comnpiler
basis, to disable such warnings if they're enabled. I chose this route
because the use of the idiom is baked deeply into Z3, so it didn't seem
feasable to consider alternative patterns (like, for example, having the
trailing field be a pointer to a separately allocated array).
The rest of the changes in the PR are uses of this include file and
macro in place of "raw" zero-length arrays.
With these changes, all instances of this warning are removed.
Homebrew upgrade from Z3 4.15.4 to 4.16.0 failed on macOS 12 during
`src/ast/ast.cpp` compilation because `obj_map::key_data` was used with
`(key, value)` construction but only implicit constructors existed. This
surfaced at `m_poly_roots.insert(new_node, new_node)` and similar map
operations.
- **Root cause addressed**
- `obj_map<Key, Value>::key_data` relied on implicit constructors, which
are insufficient under stricter toolchains when `key_data(k, v)` /
`key_data(k)` are instantiated via `obj_map` helpers.
- **Code change (minimal, targeted)**
- Added explicit struct constructors in `src/util/obj_hashtable.h` for:
- default initialization
- key-only construction (`key_data(Key* k)`)
- key + lvalue value (`key_data(Key* k, Value const& v)`)
- key + rvalue value (`key_data(Key* k, Value&& v)`)
- No behavioral changes to map semantics; this only makes existing call
sites well-formed across compilers.
- **Example of the change**
```c++
struct key_data {
Key * m_key = nullptr;
Value m_value;
key_data() = default;
key_data(Key* k): m_key(k) {}
key_data(Key* k, Value const& v): m_key(k), m_value(v) {}
key_data(Key* k, Value&& v): m_key(k), m_value(std::move(v)) {}
// ...
};
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This change stops agentic workflows from opening GitHub issues when a
run fails due to workflow/tooling conditions such as missing-tool
reports or token-budget exhaustion. It applies the repository-wide
suppression suggested by the failure issue itself, so these runs can
still fail without creating issue noise.
- **What changed**
- Added `safe-outputs.report-failure-as-issue: false` to each top-level
agentic workflow source under `.github/workflows/*.md`
- Regenerated the corresponding compiled `.lock.yml` workflows so the
runtime configuration matches the source frontmatter
- **Effect**
- Agentic workflow runs continue to report failure in Actions
- Automatic `[aw] ... failed` issue creation is disabled for these
workflows
- Existing safe outputs such as `noop` and `missing-tool` remain
unchanged
- **Scope**
- Applied consistently across the repository’s top-level agentic
workflows, including `zipt-code-reviewer`, `build-warning-fixer`,
`code-conventions-analyzer`, `workflow-suggestion-agent`, and related
workflows
- **Configuration pattern**
```yaml
safe-outputs:
report-failure-as-issue: false
create-issue:
...
missing-tool:
create-issue: true
noop:
report-as-issue: false
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
