README build ribbons had drifted from current workflow reality (e.g.,
removed `pyodide.yml`, disabled workflows still shown). This updates the
badge matrix to reflect active workflows only.
- **Scheduled workflows**
- Replaced deprecated `pyodide.yml` badge with active `pyodide-pypi.yml`
(`Pyodide Wheel (PyPI)`).
- **Disabled workflow cleanup**
- Removed badges for disabled workflows, including `coverage.yml` and
disabled agentic workflows (`a3-python`, `build-warning-fixer`,
`code-conventions-analyzer`, `csa-analysis`, `ostrich-benchmark`,
`tactic-to-simplifier`, `zipt-code-reviewer`).
- **Agentic workflows alignment**
- Kept active lock workflows and refreshed the section to include
currently active entries such as `specbot-crash-analyzer`,
`smtlib-benchmark-finder`, and `tptp-benchmark`.
```md
- | [](.../pyodide.yml) |
+ | [](.../pyodide-pypi.yml) |
```
Co-authored-by: copilot-swe-agent[bot] <198982749+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 PR adds
```
"-Wcast-qual"
```
to the set of warnings enabled in the build. This gives warnings like:
```
/Users/daviddetlefs/z3/src/ast/ast.cpp:2897:38: warning: cast from 'app *const *' to 'expr **' drops const qualifier [-Wcast-qual]
```
I fixed these by inserting consts. In some cases, a "const_cast<T>(...)"
was necessary.
Nightly and release workflows were still building Pyodide wheels inline,
despite Pyodide now being handled by a dedicated workflow. This change
removes duplicate Pyodide build work from those pipelines and aligns
artifact assembly with the new split.
- **Workflow graph cleanup**
- Removed the `pyodide-python` job from:
- `.github/workflows/nightly.yml`
- `.github/workflows/release.yml`
- **Packaging dependency updates**
- Updated `python-package.needs` in both workflows to drop
`pyodide-python`, so packaging no longer waits on an in-workflow Pyodide
build.
- **Artifact collection updates**
- Removed `Download Pyodide Build` steps from both `python-package`
jobs, eliminating references to `PyodidePythonBuild`.
```yaml
python-package:
needs:
- mac-build-x64
- mac-build-arm64
- windows-build-x64
- windows-build-x86
- windows-build-arm64
- manylinux-python-amd64
- manylinux-python-arm64
- manylinux-python-riscv64
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The "Python bindings (Pyodide)" CI job fails at CMake configure time
because Emscripten's cross-compiler cannot pass the `std::atomic` link
tests in `check_link_atomic.cmake`, resulting in a fatal error even
though Pyodide builds are single-threaded and never need `libatomic`.
## Change
- **`cmake/check_link_atomic.cmake`**: guard the entire atomic check
behind `if (NOT (EMSCRIPTEN OR Z3_SINGLE_THREADED))`. Emscripten sets
`EMSCRIPTEN` automatically via `emcmake`; Pyodide builds also pass
`-DZ3_SINGLE_THREADED=TRUE`, so either condition is sufficient to bypass
the check safely.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+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 fixes warnings about "missing field initializers" -- struct
initializers that leave some field uninitialized.
In https://github.com/Z3Prover/z3/pull/9904, I tried to do this in the
code. @nunoplopes pointed out flaws with this approach. He outlined a
more ambitious approach to fix the actual problem (use of an "entry"
type when just a "key" type should be sufficient in some places). For
now, though, I think it's doesn't lose anything to just disable the
warning.
This is an **automated workflow self-test** of the `fixer-selftest` /
`snapshot-regression-fixer` pipeline running on the self-hosted
**`rise-runner-1`** runner pool. Its sole purpose is to prove the
end-to-end agentic pipeline works: Copilot inference runs, and the
`create-pull-request` safe output can open a real **draft** pull request
on `Z3Prover/z3` using the configured PAT. It is intentionally
build-free.
### Change
- **File:** `src/ast/simplifiers/elim_unconstrained.cpp` (module-header
`/*++ ... */` comment)
- **Before:** ` - it does not accomodate side constraints.`
- **After:** ` - it does not accommodate side constraints.`
A plain spelling correction in a comment: `accomodate` → `accommodate`.
The diff is a single line.
### Why this is safe
The change is **comment-only** — it touches no code, identifiers, string
literals, build files, or tests, and therefore **cannot affect z3's
behaviour or output**. Because of that, no compilation or testing was
performed and **no rebuild is needed** to be confident it is correct.
### For maintainers
This is a genuine, correct fix, so you are welcome to **merge** it.
Equally, you may simply **close** it — the success of this self-test
does not depend on the PR being merged.
> Generated by [Self-test the agentic PR pipeline with a tiny z3 comment
fix](https://github.com/Z3Prover/bench/actions/runs/27987685681) · 299.1
AIC · ⌖ 53.6 AIC · ⊞ 35.5K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+fixer-selftest%22&type=pullrequests)
<!-- gh-aw-agentic-workflow: Self-test the agentic PR pipeline with a
tiny z3 comment fix, engine: copilot, version: 1.0.60, model:
claude-opus-4.8, id: 27987685681, workflow_id: fixer-selftest, run:
https://github.com/Z3Prover/bench/actions/runs/27987685681 -->
<!-- gh-aw-workflow-id: fixer-selftest -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/fixer-selftest -->
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Automated workflow self-test
This is an **automated workflow self-test** of the `fixer-selftest` /
`snapshot-regression-fixer` pipeline running on the self-hosted
**`rise-runner-1`** pool. Its sole purpose is to verify the end-to-end
agentic pipeline: that Copilot inference runs and that the
`create-pull-request` safe output can open a real **draft** PR on
`Z3Prover/z3` using the configured PAT.
## The fix
A single, objectively-correct spelling fix in a **code comment** (the
header comment block of the file — not code, identifiers, or string
literals).
- **File:** `src/ast/simplifiers/solve_eqs.cpp` (line 23, inside the
`/*++ ... --*/` header comment)
- **Before:** `... where bitset reprsents set of free variables.`
- **After:** `... where bitset represents set of free variables.`
The diff is a single line:
```diff
-1. maintain map FV: term -> bit-set where bitset reprsents set of free variables. Assume the number of variables is bounded.
+1. maintain map FV: term -> bit-set where bitset represents set of free variables. Assume the number of variables is bounded.
```
## Why this is safe
The change is **comment-only** and therefore **cannot affect z3's
behaviour or output** — so it needs **no rebuild and no testing** to be
confident it is correct. Nothing outside the comment text was touched
(no code, no string literals, no identifiers, no whitespace elsewhere).
## For maintainers
This is a genuine, correct fix, so feel free to **merge** it — but you
may also simply **close** it. The self-test's success does not depend on
this PR being merged; it only depends on the PR having been opened.
> Generated by [Self-test the agentic PR pipeline with a tiny z3 comment
fix](https://github.com/Z3Prover/bench/actions/runs/27986232656) · 208.5
AIC · ⌖ 75.1 AIC · ⊞ 35.5K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+fixer-selftest%22&type=pullrequests)
<!-- gh-aw-agentic-workflow: Self-test the agentic PR pipeline with a
tiny z3 comment fix, engine: copilot, version: 1.0.60, model:
claude-opus-4.8, id: 27986232656, workflow_id: fixer-selftest, run:
https://github.com/Z3Prover/bench/actions/runs/27986232656 -->
<!-- gh-aw-workflow-id: fixer-selftest -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/fixer-selftest -->
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The `Issue Backlog Processor` workflow’s `agent` job was failing at
runtime because the generated lock workflow referenced a non-existent
gh-aw helper (`merge_awf_model_multipliers.cjs`). This PR updates the
lock file to align with current gh-aw output and eliminate that stale
invocation.
- **Root cause addressed**
- `issue-backlog-processor.lock.yml` contained an outdated step that
executed:
- `node "${RUNNER_TEMP}/gh-aw/actions/merge_awf_model_multipliers.cjs"`
- That module is not present in the runner-provisioned gh-aw action set,
causing `MODULE_NOT_FOUND` and failing the `agent` job.
- **Change made**
- Recompiled the source workflow (`issue-backlog-processor.md`) and
committed the regenerated lock file:
- `.github/workflows/issue-backlog-processor.lock.yml`
- The regenerated lock no longer includes the stale
`merge_awf_model_multipliers.cjs` call and updates associated gh-aw
metadata/version pins accordingly.
- **Illustrative diff (relevant line)**
```yaml
- GH_AW_MODEL_MULTIPLIERS_PATH="/tmp/gh-aw/model_multipliers.json" node "${RUNNER_TEMP}/gh-aw/actions/merge_awf_model_multipliers.cjs"
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `build` job in the Pyodide workflow was failing at wheel smoke-test
import time because `libz3.so` was not produced as a proper wasm side
module (`need the dylink section to be first`, missing exported
symbols). This PR restores the required Pyodide linker mode.
- **Root cause**
- Recent Pyodide linker flag changes enabled wasm EH/longjmp but omitted
`-sSIDE_MODULE=1`, so the generated `libz3.so` was not loadable by
Pyodide’s dynamic loader.
- **Changes**
- **`src/api/python/pyproject.toml`**
- Added `-sSIDE_MODULE=1` to `[tool.pyodide.build].ldflags`.
- **`src/api/python/setup.py`**
- Added `-sSIDE_MODULE=1` to the Pyodide `LDFLAGS` path to keep direct
`setup.py`-driven builds aligned with `pyproject.toml` behavior.
- **Flag delta (core fix)**
```toml
# src/api/python/pyproject.toml
[tool.pyodide.build]
ldflags = "-fwasm-exceptions -sSUPPORT_LONGJMP=wasm -sWASM_BIGINT -sSIDE_MODULE=1"
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The Pyodide `build` job was passing legacy Emscripten exception flags
that conflict with the wasm-exception ABI now used by the Python
packaging configuration. This caused the wheel build to fail before
compilation completed.
- **Align Pyodide workflow flags**
- Remove per-workflow `CFLAGS` / `CXXFLAGS` / `LDFLAGS` overrides from
the Pyodide build step.
- Let the build inherit the canonical wasm-exception / longjmp / bigint
flags from `src/api/python/pyproject.toml`.
- **Apply the fix consistently**
- Update the standalone Pyodide workflow.
- Update the matching Pyodide build steps in `nightly.yml` and
`release.yml` to avoid the same regression in scheduled and release
builds.
- **Why this fixes the failure**
- The broken path mixed JS-exception and wasm-exception settings:
```yaml
CFLAGS: "-fexceptions -s DISABLE_EXCEPTION_CATCHING=0 -g2"
CXXFLAGS: "-fexceptions -s DISABLE_EXCEPTION_CATCHING=0"
```
- The updated workflows now invoke:
```yaml
~/env/bin/pyodide build --exports whole_archive
```
and rely on the packaging config’s wasm-exception settings instead.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `API Coherence Checker` workflow’s `agent` job was failing in
Actions (`82289334242`) due to a lockfile/runtime mismatch that invoked
a non-existent gh-aw script (`merge_awf_model_multipliers.cjs`). This PR
refreshes the generated lockfile so the compiled workflow and gh-aw
runtime are aligned.
- **Root cause surfaced in generated workflow**
- The existing `.lock.yml` referenced an outdated gh-aw runtime
path/script combination that no longer exists in the installed action
payload.
- **Lockfile regeneration (single-file, surgical)**
- Updated only:
- `.github/workflows/api-coherence-checker.lock.yml`
- Regenerated with strict gh-aw compile output so metadata, setup action
refs, and generated agent-step wiring are internally consistent.
- **Effect on `agent` job behavior**
- Removes the stale generated invocation path to
`merge_awf_model_multipliers.cjs`.
- Aligns generated runtime variables/steps with the currently resolved
gh-aw setup version.
```yaml
# before (generated agent step)
GH_AW_MODEL_MULTIPLIERS_PATH="/tmp/gh-aw/model_multipliers.json" \
node "${RUNNER_TEMP}/gh-aw/actions/merge_awf_model_multipliers.cjs"
# after
# stale merge step no longer emitted in this lockfile
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The "agent" job was failing immediately because the lock file (compiled
by `gh-aw v0.79.6`) generated a step calling
`merge_awf_model_multipliers.cjs`, but the pinned
`github/gh-aw-actions/setup@v0.80.4` did not ship that script — causing
a `MODULE_NOT_FOUND` crash before the Copilot CLI ever ran.
## Changes
- **`.github/workflows/academic-citation-tracker.lock.yml`** —
recompiled with `gh aw compile --strict` using v0.79.8; setup action is
now pinned to the matching `@v0.79.8` release which includes all
expected scripts
- **`.github/dependabot.yml`** — compiler updated ignore entries to
cover both `github/gh-aw-actions/**` (subdirectory refs like `setup`)
and `github/gh-aw-actions` (base ref), preventing Dependabot from
bumping the setup pin out of sync again
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Z3 incorrectly returns SAT for formulas like `store(store(const(x), i0,
e0), i1, e1) = store(store(const(y), i0, e0), i1, e1) ∧ x ≠ y` when the
index sort has a small finite domain (e.g. `(_ BitVec 2)` = 4 elements).
The quantifier-based encoding of the same constraint correctly returns
UNSAT.
## Changes
### `src/sat/smt/array_solver.cpp` — `add_parent_lambda()`
When a store is added to an array's `m_parent_lambdas` after that array
already has `m_has_default = true` (i.e., a `default(array)` term
already exists in the e-graph), the default axiom for the new store was
silently dropped. This breaks the propagation chain:
```
default(const(x)) = x
↓ [via store default axiom]
default(store(const(x), i, v)) = x
↓ [via store default axiom]
default(store(store(const(x), ...), ...)) = x
↓ [EUF congruence from store equality]
x = y → contradiction
```
Fix: push `default_axiom(lambda)` in `add_parent_lambda` when
`m_has_default` is already set, so late-arriving stores still get their
default axioms instantiated.
```cpp
void solver::add_parent_lambda(theory_var v_child, euf::enode* lambda) {
auto& d = get_var_data(find(v_child));
ctx.push_vec(d.m_parent_lambdas, lambda);
if (should_prop_upward(d))
propagate_select_axioms(d, lambda);
if (d.m_has_default) // new: fire default axiom retroactively
push_axiom(default_axiom(lambda));
}
```
### Known remaining gap
`mk_eq_core` in `array_rewriter.cpp` also has a related issue: the
unconditional store-chain expansion fires only when `domain_size >
num_lhs + num_rhs` (line 893), but the correct threshold is `domain_size
> max(num_lhs, num_rhs)`. With 4-element domain and 2 stores per side,
`2+2 = 4` equals the domain size so the expansion is skipped. The
variant gated by `m_expand_store_eq` already uses `max()` correctly
(line 911); the unconditional path needs the same fix.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
## Summary
Fix a use-after-free in `func_interp::compress()`.
When a function interpretation had previously grown large enough to
allocate `m_entry_table`, `compress()` could deallocate entries whose
result matched the else-case but leave the hash table intact. Later
`get_entry()` lookups could then return freed `func_entry*` values,
which showed up during model checking as a corrupted expression result
from `model_evaluator`.
## Root cause
`func_interp::compress()` compacted `m_entries` and freed removed
entries, but it did not rebuild or clear `m_entry_table`.
This left stale pointers in the lookup table whenever:
- the table had already been allocated on a larger interpretation, and
- compression removed some entries.
In the reported case, model evaluation rewrote `stack_s!1041` through
`BR_REWRITE1`, fetched a freed `func_entry` result from the stale table,
and then tripped an assertion in `expr::get_sort()` during quantifier
model checking.
## Fix
After compression removes entries, rebuild `m_entry_table` from the
surviving `m_entries`, or clear it when the surviving interpretation is
small.
## Regression coverage
Added a unit regression in `src/test/model_evaluator.cpp` that:
- creates a `func_interp` large enough to allocate `m_entry_table`,
- compresses away almost all entries,
- checks that removed keys no longer resolve, and
- checks that the surviving key still resolves to the correct result.
## Validation
- `../build/z3 ebso-115.smt2` previously hit an assertion in
`rewriter_def.h` / `ast.cpp`; after the fix it no longer asserts.
- `./test-z3 model_evaluator` passes with the new regression.
## Reproducer
I did not produce a smaller SMT2 benchmark in this change. The original
reproducer I used was `ebso-115.smt2`, and the new unit regression
directly exercises the stale-entry-table path in-process.
Co-authored-by: Can Cebeci <t-cancebeci@microsoft.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.
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.
