### Problem
The order of evaluation of function arguments is unspecified in C++
(arguments are indeterminately sequenced since C++17). Compilers use
this freedom differently:
```c++
static int f(int i) { printf("%d ", i); return i; }
static void g(int, int, int) { printf("\n"); }
int main() { g(f(1), f(2), f(3)); }
```
| compiler/target | output |
|---|---|
| gcc 13, x86_64 | `3 2 1` |
| gcc 13, aarch64 | `1 2 3` |
| clang 18, x86_64 | `1 2 3` |
Z3 has many call sites where **two or more arguments each create AST
nodes**, e.g. (before this PR, `bv_rewriter.cpp:876`):
```c++
result = m.mk_ite(c, m_mk_extract(high, low, t), m_mk_extract(high, low, e));
```
The two extract nodes are hash-consed and receive their AST ids in
evaluation order, so the id assignment differs between
compilers/targets. AST ids feed heuristic tie-breaking throughout the
solver (`bool_rewriter`'s `m_order_eq` equality-operand ordering,
id-based sorts in `array_rewriter`, case-split ordering, ...), so
**byte-identical input takes different solver paths depending on the
compiler and architecture z3 was built with**.
### Evidence
Investigated while chasing cross-platform proof-time instability in
CBMC/mldsa-native CI (diffblue/cbmc#8991), on byte-identical ~12 MB SMT2
instances (bit-vectors + arrays + quantifiers), with the `string_hash`
fix from #10163 applied to isolate this effect. Z3 4.15.3, gcc 13 on
x86_64 Linux and aarch64 Linux (Graviton):
* one instance: **17 s on x86_64 vs 1633 s on aarch64** (both `unsat`; a
sibling instance shows the reverse direction). Run-to-run within one
host: ±1 %.
* Instrumenting `ast_manager::register_node_core` with an order
fingerprint (running hash over `(node hash, node id)`) shows both
architectures construct **identical AST sequences up to registration
#41,789**, where x86_64 creates `(extract[0:0] #xFFFFFFFF)` before
`(extract[0:0] #xFFFFFFFE)` and aarch64 the other way around — from
identical call stacks at the `mk_ite`-over-two-`mk_extract` site quoted
above. All divergence between the two hosts flows from such events
(pointer/ASLR effects experimentally excluded: fingerprints are
invariant under `setarch -R` and across repeated runs).
* Sequencing that one site by hand moved the first divergence to
#248,118 — the analogous `mk_ite(c, mk_select(...), mk_select(...))`
site in `array_rewriter.cpp`. Sequencing that one, too, moved it to
#248,411, inside `nnf:👿:process_iff_xor` — i.e. the next layer of
the same onion.
* With the whole `ast/rewriter` layer swept (this PR), the instrumented
builds produce **identical AST construction traces on both architectures
throughout the entire rewriter phase** of this 546k-line industrial
instance; the first divergence left is the NNF one.
### Fix
Following the precedent of 37904b9e8, e113d39aa, 360193098, 93ff8c76d,
9b88aaf13 ("parameter evaluation order", `bool_rewriter`/`seq_rewriter`)
and the existing comments in `seq_rewriter.cpp` ("introduce temporaries
to ensure deterministic evaluation order..."), this PR hoists
AST-creating arguments into named temporaries with a defined evaluation
order, across `src/ast/rewriter/` — 126 call sites in 17 files. The
transformation is purely sequencing: it selects one of the two valid C++
evaluation orders and makes it the same everywhere. (Temporaries are raw
pointers in rewriter-local scope, matching the precedent commits;
nothing can trigger GC between creation and consumption.)
The sites were found with a small AST-argument scanner (statement-level
call sites whose argument list contains ≥ 2 top-level arguments that
each contain an AST-creating call); I am happy to share/contribute the
script. Known remaining work, deliberately out of scope here to keep the
diff reviewable:
* 41 sites in `src/ast/rewriter/` that need manual treatment (inside
`if` conditions, ternaries, or multi-statement expressions) — list
available on request;
* `src/ast/normal_forms/nnf.cpp` (`process_iff_xor`, proven divergent by
the trace above), ~7 sites in `src/ast/simplifiers/`, ~3 in
`src/ast/converters/`, ~9 in `src/ast/`;
* other theory/solver layers (`src/smt/`, `src/sat/`, ...) — divergences
there only matter after search starts, where paths have usually already
split, but a full sweep would be needed for bit-reproducibility across
compilers.
Together with #10163, this is a step towards z3 builds whose behaviour
does not depend on the compiler or target architecture — which matters
for verification CI that runs identical proofs on heterogeneous
platforms and expects comparable runtimes.
---------
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
## Summary
Fixes a completeness regression where `elim_uncnstr` was silently
disabled for ordinary (non-polymorphic) goals, detected by the
`snapshot-regression` corpus.
- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/3054
- **Benchmark:** `iss-6260/small-2.smt2` (corpus `Z3Prover/bench`,
`inputs/issues/iss-6260/`)
- **Divergence:** recorded oracle `sat` → current z3 produces `unknown`
### Divergence diff
```diff
--- small-2.expected.out (expected)
+++ produced (current z3)
@@ -1,3 +1,3 @@
-sat
+unknown
(error "line 17 column 0: unexpected character")
(error "line 17 column 1: unexpected character")
```
(The `(error ...)` lines are expected: the benchmark contains a stray
```` ``` ```` fence on line 17. Only the `sat` → `unknown` change is the
regression.)
## Root cause
`git bisect` over the regression window pins the flip to commit
`208cc5686` ("fix build"), which added `|| m().has_type_vars()` to the
`elim_uncnstr_tactic` guard and an equivalent `if (m.has_type_vars())
return;` to the `elim_unconstrained` simplifier.
`ast_manager::has_type_vars()` is a **manager-wide, sticky** flag: it is
set to `true` as soon as *any* type variable is created, and is never
reset. In particular `finite_set_decl_plugin::init()` creates type
variables `A`/`B` to define its polymorphic signatures. Those type
variables never occur in the user's assertions, but once the finite_set
plugin is initialized — which happens while processing this benchmark —
the flag is globally `true` (confirmed by instrumenting `mk_type_var`:
the only type vars created for this benchmark are the finite_set
signature vars `A` and `B`).
As a result `elim_uncnstr` bails out for goals that contain **no**
polymorphic terms at all, i.e. it is effectively disabled. Unconstrained
subterms that used to be eliminated now reach the theory solvers.
For this benchmark the (single) assertion is `(not (xor (>= x 0) (>= x1
0) (>= x 0) x4 (str.contains ...)))`. The duplicated `(>= x 0)` cancels
(`a xor a = false`), and the free Boolean `x4` can fix the parity
regardless of the value of the `str.contains` term, so the goal is
trivially `sat`. That `str.contains`/`str.replace_re` subterm is
unconstrained and was previously removed by `elim_uncnstr`; without that
elimination it reaches `theory_seq`, which marks `str.replace_re` as
unhandled and gives up in `final_check` → `unknown` (`incomplete (theory
seq)`).
## Fix
Make the guard precise. Keep `has_type_vars()` as a cheap pre-filter
(matching existing usage in `ast_translation.cpp` and
`ast_manager::has_type_var`), but only bail out when the goal / asserted
formulas **actually** contain type-variable typed terms, using the
existing `polymorphism::util::has_type_vars(expr*)`.
This preserves the polymorphism crash-protection (goals with genuine
type-variable terms still skip `elim_uncnstr`) while restoring
`elim_uncnstr` for the vast majority of goals that merely triggered a
polymorphic-plugin initialization. Both twin guards (the `elim_uncnstr`
tactic and the `elim_unconstrained` simplifier) are fixed consistently.
## Validation
Built this checkout and re-ran the benchmark (step 5 of the fixer
workflow):
- `./configure && make -C build -j$(nproc)` — Z3 version 4.17.0.
- Unpatched master reproduced the divergence: `z3 -T:20
iss-6260/small-2.smt2` → `unknown`.
- After the fix, `z3 -T:20 inputs/issues/iss-6260/small-2.smt2` produces
**exactly** the recorded oracle:
```
sat
(error "line 17 column 0: unexpected character")
(error "line 17 column 1: unexpected character")
(error "line 17 column 2: unexpected character")
```
- Regression sanity checks: sibling `iss-6260/small.smt2` unchanged
(`sat`); plain arithmetic unconstrained goals unchanged; polymorphic
goals with genuine type-variable terms (including `declare-type-var` and
forcing `(check-sat-using (then elim-uncnstr smt))`) still solve without
crashing — the guard still fires for those.
Opened as a **draft** for human review.
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28844840657)
· 861.2 AIC · ⌖ 45.8 AIC · ⊞ 8.9K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests)
<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.63, model: claude-opus-4.8, id:
28844840657, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28844840657 -->
<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->
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 is a second version of https://github.com/Z3Prover/z3/pull/9957. I
address @NikolajBjorner 's comments about not changing the semicolons
after macro invocations, because some editors work better with them
present. It now, to the best of my ability, only deletes semis:
* after the closing brace of namespace decl.
* after the closing brace of an extern "C" decl.
* after a function definition.
This PR is very large, but it consists entirely of deletions of
semicolons in these situations.
(If there was a way to update the previous PR, which had been closed,
and that is preferable, please let me know. I couldn't figure it out.)
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>
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.
`sat.smt=true` could return `sat` with an invalid model for QF_UFBV
formulas combining Bool-valued UFs and BV range constraints. The failure
came from broken model-trail reconstruction in `elim_unconstrained`,
where `ADD` entries were effectively turned into identity substitutions.
- **Root-cause fix: restore model-trail substitution composition**
- In `elim_unconstrained::update_model_trail`,
`generic_model_converter::ADD` entries now use `entry.m_def` (rewritten
through accumulated substitutions) instead of creating self-referential
const-to-const mappings.
- This re-enables correct back-substitution for eliminated unconstrained
terms during witness reconstruction.
- **Regression coverage: QF_UFBV + `sat.smt=true` + model validation**
- Added a focused unit test in `src/test/simplifier.cpp` for:
- Bool-valued UF predicate over BV vars
- split BV range constraints (`bvuge` / `bvult`)
- `:sat.smt true` and `:model_validate true`
- The test asserts the solver returns `sat` without emitting an
invalid-model error.
```cpp
// before (effectively no-op back-mapping)
new_def = m.mk_const(entry.m_f);
sub->insert(new_def, new_def, nullptr, nullptr);
// after (compose and apply recorded definition)
new_def = entry.m_def;
(*rp)(new_def);
sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr);
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Recent GCC builds report two warning classes in core codepaths: a
possible uninitialized read in `bound_propagator::relevant_bound`, and
repeated `-Warray-bounds` diagnostics in `mpz_manager::get_sign_cell`
when materializing small integers into a reserved `mpz_cell`.
- **Warning cleanup in bound propagation**
- Initialize `interval_size` at declaration in
`src/ast/simplifiers/bound_propagator.cpp` so the compiler can prove
safety across templated `LOWER/UPPER` instantiations using `std::clamp`.
- Preserves existing control flow and refinement heuristics (`bounded`
remains the gate for interval-based logic).
- **Warning cleanup in mpz small-value cell materialization**
- In `src/util/mpz.h`, replace direct writes through `cell->m_digits[0]`
with writes via a derived digits pointer
(`reinterpret_cast<digit_t*>(cell + 1)`), avoiding zero-length
trailing-array indexing diagnostics.
- Keeps memory layout and semantics unchanged for the stack-reserved
`sign_cell` buffer.
- **Representative change**
```cpp
cell = reserve;
cell->m_size = 1;
digit_t* cell_digits = reinterpret_cast<digit_t*>(cell + 1);
cell_digits[0] = a.value() < 0 ? -a.value() : a.value();
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
