## Summary
Fixes a Z3 output regression detected by the `Z3Prover/bench`
snapshot-regression corpus.
- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/3050
- **Benchmark:** `iss-5134/small.smt2`
(`inputs/issues/iss-5134/small.smt2` in `Z3Prover/bench`)
- **Kind:** `diff` — recorded oracle vs. current nightly z3
(`z3-4.17.0-x64-glibc-2.39`)
## Divergence
The benchmark constrains a string `a` using a regex that contains
`(re.range "" <ite>)`:
```smt2
(declare-fun a () String)
(assert (str.in_re a (re.* (re.union (str.to_re "b") (str.to_re (ite
(str.in_re a (re.* (re.range "" (ite (str.in_re a (str.to_re "")) ""
a)))) "" "a"))))))
(assert (not (str.in_re a (re.* (str.to_re "")))))
(check-sat)
(get-model)
```
Recorded oracle (**expected**) vs. current z3 (**current**):
```diff
-sat
-(
- (define-fun a () String
- "a")
-)
+unknown
+(error "line 7 column 10: model is not available")
```
## Root cause
Per SMT-LIB, `re.range` over an argument that is **not a single
character** denotes the empty language, so `(re.range "" X)` is
`re.none` regardless of `X` (the lower bound `""` is the empty string).
Before the *"Derive with ranges"* refactor (#9963 / #9965),
`seq_rewriter::mk_re_range` recognised this through several emptiness
checks, including a concrete non-single-character test and a `max_length
== 0` test:
```cpp
if (str().is_string(lo, slo) && slo.length() != 1) is_empty = true;
if (max_length(lo) == std::make_pair(true, rational(0))) is_empty = true;
if (max_length(hi) == std::make_pair(true, rational(0))) is_empty = true;
```
The refactor rewrote `mk_re_range` and kept only the `min_length(..) >
1` emptiness test (a bound provably **≥ 2** characters). That misses a
bound of length **exactly 0**: an empty-string bound has `min_length ==
0`, so it is no longer detected as empty, and `mk_re_range` returns
`BR_FAILED`, leaving `(re.range "" X)` symbolic. The new range-aware
derivative engine (`seq_derive.cpp`) then produces a *stuck* derivative
for such a range (its `is_unit_string("")` test fails), so the sequence
theory can no longer decide membership and the solver answers `unknown`
/ "model is not available".
## Fix
Restore the sound emptiness check the refactor dropped — a bound whose
`max_length` is provably `0` can never be a single character, so the
range is empty:
```cpp
// A bound that is provably of length 0 (e.g. the empty string "") can
// likewise never be a single character, so the range is empty. Unlike a
// symbolic bound, max_length == 0 is a provable emptiness fact, so this is
// sound (it is never true for a model-dependent bound such as a variable).
if (max_length(lo) == std::make_pair(true, rational(0)))
is_empty = true;
if (max_length(hi) == std::make_pair(true, rational(0)))
is_empty = true;
```
This does **not** reintroduce the unsoundness the refactor guarded
against: `max_length == (true, 0)` is a *provable* emptiness fact and is
never true for a model-dependent (symbolic) bound, so `(re.range x x)`
is still correctly left symbolic (it denotes `{x}` whenever `x` is a
single character).
## Validation
Built the patched `./z3` checkout (`./configure && make -C build`) and
re-ran the benchmark with the option the snapshot capture uses
(`-T:20`):
- **Before the fix:** `z3 -T:20 small.smt2` → `unknown` + `(error "...
model is not available")` — reproduces the divergence.
- **After the fix:** `z3 -T:20 small.smt2` → `sat` + `(define-fun a ()
String "a")` — **exactly matches** the recorded oracle.
Additional checks with the rebuilt binary:
- Sibling benchmarks `iss-5134/bug.smt2` and `iss-5134/small-2.smt2`
still match their oracles.
- Symbolic bound not over-collapsed: `(str.in_re "a" (re.range x x))` →
`sat` (x = "a").
- `(re.range "" "a")` is the empty language: `(str.in_re "a" (re.range
"" "a"))` and `(str.in_re "" (re.range "" "a"))` → `unsat`.
- Ordinary ranges unaffected: `"b" ∈ (re.range "a" "c")` sat, `"d" ∈
(re.range "a" "c")` unsat, `(re.range "a" "a")` singleton.
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28731229299)
· 592.3 AIC · ⌖ 39.1 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:
28731229299, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28731229299 -->
<!-- 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>
The polymorphism theory routed polymorphic (\) problems through
theory_polymorphism, which instantiated axioms during search. Two leaks:
1. In inst::instantiate, insert_ref_map was constructed with an expr_ref
argument, so its template parameter D deduced to expr_ref instead of
expr*. Trail objects are region-allocated and freed without running
destructors, so the embedded expr_ref never released its reference,
leaking one AST subtree per instantiation. Pass e_inst.get() so D is
expr*, matching the raw hashtable + manual inc_ref/dec_ref pattern.
2. trail_stack's destructor does not call reset(), so level-0 trail items
(including the inc_ref balancing entries for m_from_instantiation) were
never undone when the theory was destroyed. Added a ~theory_polymorphism
destructor that calls m_trail.reset().
Also keeps a defensive alias check in util::unify and a fresh per-iteration
substitution in inst::instantiate.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When merging two type substitutions, util::unify(substitution, substitution,
substitution) inserted bindings without an occurs-check. Merging maps such as
A |-> list(B) and B |-> list(A) produced a self-referential binding
B |-> list(list(B)), and applying that substitution recursed forever, causing
a stack overflow during the first polymorphic instantiation round.
This was exposed by encoding TPTP $tType quantification as polymorphism
(8ee8a3cda): mutually-recursive polymorphic types in THF problems (e.g.
COM/DAT/ITP Coq-derived files) triggered 60 stack-overflow crashes during
check_sat.
Add occurs-checks so a binding that would make the substitution cyclic causes
the merge to fail (the instantiation is soundly skipped). Values are resolved
against the current substitution before insertion, preserving the acyclic
invariant.
Verified: the 60 previously-crashing TPTP files now terminate cleanly;
92/92 unit tests pass.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
In polymorphism::substitution::operator()(sort*), each substituted
sub-sort was held only in a local sort_ref that was destroyed at the end
of the loop iteration, while its raw pointer was retained in the
parameter vector passed to mk_sort. When the sub-sort's refcount dropped
to zero, its memory was freed and then reused by the next allocation,
producing a self-referential sort. Structural sort traversals such as
has_type_var (which has no cycle detection) then recursed infinitely,
manifesting as a stack overflow.
Pin each intermediate sub-sort in a sort_ref_vector so it stays alive
until after mk_sort has taken its own references.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Summary
Fixes the snapshot-regression divergence reported in Z3Prover/bench
discussion
**#2977** — https://github.com/Z3Prover/bench/discussions/2977 — for
benchmark
**`iss-4525/bug-7.smt2`**.
## Divergence
The benchmark's second query
`(check-sat-using (then simplify ctx-solver-simplify))` regressed from
`sat` to
`unknown`:
```diff
--- bug-7.expected.out (expected)
+++ produced (current z3)
@@ -1,2 +1,2 @@
sat
-sat
+unknown
```
The input sets `:rewriter.split_concat_eq true` and `:smt.threads 3`,
and its
core assertion has the shape
`(not (forall ((q11 (_ BitVec 21)) ...) (not (= q11 q9 q11 (concat
#b01111000010 s)))))`.
## Root cause
With `split_concat_eq` enabled, `bv_rewriter::mk_eq_concat` rewrites an
equality
`(= x (concat ...))` into per-slice **extract** equalities, e.g.
`(= (extract 9 0 x) s) ∧ (= (extract 20 10 x) #b01111000010)`.
When `x` is a **bound (de Bruijn) variable**, this is harmful:
destructive
equality resolution (`der.cpp`) only recognises the pattern `(= VAR t)`
to
eliminate a bound variable. After the split, the variable only appears
under
`extract`, so DER can no longer eliminate it and a **residual
quantifier**
survives `simplify`. Discharging that residual quantifier is then left
to the
solver invoked inside `ctx-solver-simplify`.
That solver is where the observable regression actually lives: with
`smt.threads ≥ 2` the parallel solver (`smt_parallel.cpp`) now returns
`unknown`
on the quantified cube instead of solving it (the older, oracle-era
parallel
solver kept splitting and proved it), so `ctx-solver-simplify` can no
longer
reduce `(not (forall ...))` to `true` and reports `unknown`. Reproduced
with an
A/B comparison of an oracle-era build (`sat` / correct) vs. current tip
(`unknown`); the sequential path (`threads=1`) is unaffected.
Rather than touch the parallel solver — whose current early-exit
behaviour is a
deliberate termination fix and is risky to revert — this change removes
the
condition that *creates* the residual quantifier in the first place, so
the goal
is solved by `simplify` alone and no longer depends on the parallel
solver's
completeness.
## Fix
In `bv_rewriter::is_concat_split_target`, exclude a bare variable from
being a
split target:
```diff
- m_split_concat_eq ||
+ (m_split_concat_eq && !is_var(t)) ||
m_util.is_concat(t) ||
m_util.is_numeral(t) ||
m_util.is_bv_or(t);
```
`split_concat_eq` is only a bit-blasting heuristic, so skipping it for
`(= var concat)` is sound and restores DER-based variable elimination.
Ground
terms are `app` nodes (never `var` nodes), so **default behaviour**
(`split_concat_eq` is off by default) **and all ground uses are
completely
unchanged** — only the explicitly-enabled option with a bound-variable
operand
is affected.
## Validation
- Rebuilt the checkout (`./configure && make -C build`) with the fix.
- Re-ran the benchmark with the capture options
(`z3 -T:20 inputs/issues/iss-4525/bug-7.smt2`): output is now `sat` /
`sat`,
an **exact match** to the recorded `bug-7.expected.out` oracle,
deterministic
across repeated runs.
- Confirmed the mechanism: `(apply (then simplify))` with
`split_concat_eq`
enabled now empties the goal (DER eliminates the bound variable),
whereas
before it left a residual quantifier.
- Confirmed `split_concat_eq` still splits **ground** `(= (concat a b)
c)`
equalities into extract-equalities (intended behaviour preserved).
- Ran the relevant `test-z3` unit suites — all pass: `ast`,
`bit_vector`,
`fixed_bit_vector`, `simplifier`, `bit_blaster`, `var_subst`,
`arith_rewriter`,
`seq_rewriter`, `factor_rewriter`, `quant_solve`, `euf_bv_plugin`.
Opened as a **draft** for human review. Note the transparency caveat
above: the
deeper behavioural regression is in the parallel solver's handling of
quantified
cubes; this patch resolves the reported divergence robustly at the
rewriter/DER layer instead of altering that solver.
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28646063005)
· 989.2 AIC · ⌖ 40.3 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:
28646063005, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28646063005 -->
<!-- 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>
## Summary
Fixes a **soundness regression** in the sequence/regex rewriter: a
symbolic character range such as `(re.range x x)` was unsoundly
collapsed to `re.empty`, causing a satisfiable membership constraint to
be reported `unsat`.
This was surfaced by the `snapshot-regression` corpus in
`Z3Prover/bench`.
- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/2761
- **Benchmark:** `iss-5873/bug-2.smt2` (in `Z3Prover/bench`, under
`inputs/issues/iss-5873/`)
- **z3 under test at capture:** `z3-4.17.0-x64-glibc-2.39` (Nightly)
## Divergence
The recorded oracle expects `sat`; current z3 returns `unsat`:
```diff
--- bug-2.expected.out (expected)
+++ produced (current z3)
@@ -1,3 +1,4 @@
-sat
-((tmp_str0 "\u{0}"))
+unsat
+(error "line 12 column 10: check annotation that says sat")
+(error "line 14 column 22: model is not available")
(:reason-unknown "")
```
The benchmark asserts (simplified):
```smt2
(assert (= (str.in_re (str.replace tmp_str0 tmp_str0 tmp_str0)
(re.range tmp_str0 tmp_str0))
(str.contains tmp_str0 tmp_str0)))
```
`str.contains x x` is always true and `str.replace x x x = x`, so this
requires `str.in_re x (re.range x x)` to hold, which is satisfiable
exactly when `x` is a single character (`len(x) = 1`).
## Root cause
`seq_rewriter::mk_re_range` treated any bound that is not a concrete
single-character literal as making the whole range **empty**:
```cpp
if (str().is_string(lo, slo) && slo.length() == 1) clo = slo[0];
else if (str().is_unit(lo, lo1) && m_util.is_const_char(lo1, clo)) ;
else is_empty = true; // unsound for a symbolic bound
```
For a symbolic bound this is unsound: `(re.range x x)` denotes `{x}`
whenever `x` is a single character, not `∅`. Collapsing it to `re.empty`
makes `str.in_re x (re.range x x)` false, contradicting the (true)
`str.contains x x`, so the solver derives an unsound `unsat`.
`git blame` attributes this unsound collapse to z3 commit `15f33f458d`
("Derive with ranges (#9965)"), which post-dates the oracle capture.
## Fix
Two surgical changes in `src/ast/rewriter/seq_rewriter.cpp`:
1. **`mk_re_range`** no longer assumes emptiness for symbolic bounds. It
concludes `re.empty` only when it can *prove* emptiness — a bound whose
length can never be 1, or two concrete bounds with `lo > hi`. When a
bound is symbolic it returns `BR_FAILED` and keeps the range. Concrete
single-character ranges keep their existing handling (`lo == hi →
str.to_re`, inverted → `re.empty`).
2. **`mk_str_in_regexp`** reduces membership in a range that has a
symbolic bound to the equivalent length/order constraints, which are
sound and complete under SMT-LIB `re.range` semantics:
`str.in_re e (re.range lo hi)` ⟶ `len(lo)=1 ∧ len(hi)=1 ∧ len(e)=1 ∧ lo
≤ e ∧ e ≤ hi`
(using `str.<=`). The derivative engine only unfolds ranges whose bounds
are concrete characters, so without this reduction a symbolic-bound
range would otherwise be left unsolved.
## Validation
Rebuilt z3 from this branch on the workflow runner (`./configure && make
-C build -j$(nproc)`) and re-ran the failing benchmark with the same
option the snapshot capture uses (`-T:20`):
```
$ z3 -T:20 inputs/issues/iss-5873/bug-2.smt2
sat
((tmp_str0 "A"))
(:reason-unknown "")
```
The verdict is now **`sat`** (was `unsat`) — the soundness regression is
resolved. A correctness battery over concrete and symbolic ranges all
returns the expected results, e.g.:
- `(str.in_re "b" (re.range "a" "c"))` → `sat`, `(str.in_re "d"
(re.range "a" "c"))` → `unsat`
- `(str.in_re x (re.range x x))` → `sat`; with `(= (str.len x) 2)` →
`unsat`
- `(str.in_re "b" (re.range x y))` → `sat`; with `(str.< y x)` → `unsat`
- `(str.in_re "" (re.range x y))` → `unsat`; `(str.in_re "ab" (re.range
"a" "c"))` → `unsat`
The pre-existing concrete-range derivative fast path is unchanged.
### Note on the model value (benign, unrelated to this fix)
The model value differs from the recorded oracle: current z3 prints
`((tmp_str0 "A"))` whereas the oracle recorded `((tmp_str0 "\u{0}"))`.
Both are valid single-character models (the formula has many). This
difference is **pre-existing and unrelated to this fix**: even a bare
`(assert (= (str.len x) 1))` yields `"A"` on current z3. It stems from
the seq/char theory's default character assignment for
otherwise-unconstrained characters (`theory_char.cpp` assigns fresh
characters starting from `'A'`), not from range handling. I deliberately
did **not** force the character to `\u{0}` — adding `x = "\u{0}"` would
be unsound over-constraining, and changing the global default character
is out of scope for this soundness fix and would perturb unrelated
models. The output is therefore semantically equivalent to the oracle
(same `sat` verdict and reason-unknown) but not byte-identical.
---
*Draft for human review. Diagnosed and fixed by the
`snapshot-regression-fixer` maintenance workflow.*
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28502614658)
· 890.7 AIC · ⌖ 46.8 AIC · ⊞ 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:
28502614658, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28502614658 -->
<!-- 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>
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 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.)
Fixes a Z3 snapshot-regression divergence reported in `Z3Prover/bench`
discussion: https://github.com/Z3Prover/bench/discussions/2667
## Divergence
- **benchmark:** `iss-6615/original.smt2` (lives at
`inputs/issues/iss-6615/` in `Z3Prover/bench`)
- **kind:** `diff`
- **z3 under test:** `z3-4.17.0-x64-glibc-2.39` (Nightly)
- **budget:** per-file `20s` — the snapshot capture runs `z3 -T:20
original.smt2`
The recorded oracle is 13× `unknown` (one per `check-sat`, each preceded
by an in-file `(set-option :timeout 100)` soft timeout). Current z3
instead prints a single `timeout`:
```diff
--- original.expected.out (expected)
+++ produced (current z3)
@@ -1,13 +1 @@
-unknown
-unknown
-unknown
-unknown
-unknown
-unknown
-unknown
-unknown
-unknown
-unknown
-unknown
-unknown
-unknown
+timeout
```
## Root cause
The benchmark uses `(set-logic ALL)` with quantifiers over higher-order
(array / lambda) sorts, so MBQI drives `ho_var::populate_inst_sets`
(`src/smt/smt_model_finder.cpp`), which enumerates candidate ground
terms with the bottom-up term-enumeration engine added in #9908
(`src/ast/rewriter/term_enumeration.cpp`):
```cpp
unsigned max_count = 20;
for (auto t : tn.enum_terms(srt)) { // each ++ runs find_next()
if (max_count == 0)
break;
--max_count;
S->insert(t, generation);
}
```
`max_count = 20` bounds the number of **inserted** terms, but it does
**not** bound the work the generator performs to find the *next*
target-sort term. For sorts that admit few cheap target-sort terms but a
large intermediate term space (here `(Array enc_val Int)` and `(Array
String (option enc_val))`), a single advance of the iterator can explore
an explosive number of intermediate terms, each rewritten through
`th_rewriter`.
Crucially, the three driving loops of the engine —
`bottom_up_enumerator::find_next`,
`bottom_up_enumerator::enumerate_operators`, and
`children_iterator::has_next` — never check the resource limit /
cancellation flag. The per-query soft timeout (`:timeout 100`) *does*
fire and cancels `m.limit()` (via `cmd_context`'s `cancel_eh<reslimit>`
+ `scoped_timer`), but the enumeration never observes it, so the query
cannot be interrupted at 100 ms. It spins until the hard *process*
timeout `-T:20` fires, which prints `timeout` for the whole run and
aborts — instead of the solver returning `unknown` per query.
## Fix
Make the enumeration honor cancellation by checking
`m.limit().is_canceled()` at the head of each of the three unbounded
loops in `src/ast/rewriter/term_enumeration.cpp`. When a query is
cancelled (soft timeout / rlimit / Ctrl-C) the enumeration stops
promptly and the solver returns `unknown`, as it did before #9908. When
nothing is cancelled `is_canceled()` is `false`, so the set of
enumerated terms is unchanged — this only adds an interrupt point, it
does not alter which terms are produced.
```diff
bool has_next(unsigned cost) {
while (!m_done) {
+ if (m.limit().is_canceled())
+ return false;
if (has_child_at_cost(cost))
return true;
advance();
}
@@ find_next()
while (true) {
+ if (m.limit().is_canceled()) {
+ m_state = State::Done;
+ return nullptr;
+ }
switch (m_state) {
@@ enumerate_operators()
while (true) {
+ if (m.limit().is_canceled())
+ return nullptr;
```
## Validation
Built this branch in Release mode (base `6fd303c4b`) and ran the exact
snapshot-capture command:
```
$ z3 -T:20 inputs/issues/iss-6615/original.smt2
unknown
unknown
unknown
unknown
unknown
unknown
unknown
unknown
unknown
unknown
unknown
unknown
unknown
real 0m1.49s
```
- Output is **byte-identical** to the recorded
`inputs/issues/iss-6615/original.expected.out` oracle (13× `unknown`).
- The isolated first `check-sat` returns `unknown` in 0.14 s (previously
it did not terminate within 30 s under only the in-file `:timeout 100`).
- Trivial sanity check (`(assert (> x 0)) (check-sat)` → `sat`) is
unaffected.
Opened as a draft for human review.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28155155541)
· 3.5K AIC · ⌖ 85.5 AIC · ⊞ 41.2K ·
[◷](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.60, model: claude-opus-4.8, id:
28155155541, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28155155541 -->
<!-- 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 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.
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>
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 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>
Implements the algorithm of Eq(p,q) = Empty(p XOR q)' using a union-find
driven bisimulation closure (per the CAV'26 ERE paper).
### What's added
* **New primitive OP_RE_XOR (re.xor)** wired through seq_decl_plugin:
parser signature, info propagation (nullable, min_length), and
pretty-printer.
* **seq_rewriter**: structural XOR rewrites ( XOR r = empty, XOR empty =
r, ull XOR r = comp(r), comp/comp absorption, complement push, AC
normalisation), nullability (Null(p XOR q) = Null(p) != Null(q)),
derivative (D_a(p XOR q) = D_a(p) XOR D_a(q)), reverse, antimirov
derivative, and `check_deriv_normal_form` coverage.
* **New class seq::regex_bisim** in
`src/ast/rewriter/seq_regex_bisim.{h,cpp}` to keep the bisim logic out
of the already-large `seq_rewriter.cpp`. Uses `basic_union_find` from
`util/union_find.h`, an `obj_map` for the node assignment, and a
50000-step bound (returns `l_undef` on overrun).
* **Integration** in `seq_rewriter::reduce_re_eq` (with a re-entry
guard) and in `seq_regex::propagate_eq` / `propagate_ne` for ground
regexes; on `l_undef` we fall back to the existing axiomatisation.
* **`sls_seq_plugin`**: extend `OP_RE_DIFF` switch arms to also cover
`OP_RE_XOR`.
### Validation
* Full release build with MSVC + Ninja.
* `./test-z3 /a` -- 89/89 tests passing.
* `./test-z3 /seq smt2print_parse` -- PASS.
* Smoke tests with `(a|b)*` vs `(a*b*)*` (equal) and `a*` vs `(a|b)*`
(not equal) return the expected `sat`/`unsat` quickly.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
`seq_rewriter.cpp` was missing several regex-concat normalizations
around `re.all` (`Σ*`), causing avoidable growth and missed
simplifications. This update fills the four gaps: nullable absorption,
guarded union distribution, intersection suffix elimination, and
nested-star collapse.
- **Nullable/full-seq absorption (A1)**
- Generalizes `Σ*·R → Σ*` and `R·Σ* → Σ*` beyond `Σ*·Σ*`.
- Applies when `R` is interpreted, nullable, and has `min_length = 0`.
- **Guarded distribution over union (A2)**
- Adds `Σ*·(R1 ∪ R2)` distribution when at least one arm is already
`Σ*`-headed.
- Rebuilds via normalized union so the redundant arm collapses to `Σ*`.
- **Intersection + full-seq tail elimination (A3)**
- Adds `(R1 ∩ … ∩ Rn)·Σ* → (R1 ∩ … ∩ Rn)` when every intersection leaf
already ends in `Σ*`.
- **Nested star concat collapse (A4)**
- Adds `R*·(R*·X) → R*·X`, covering non-adjacent star patterns not
handled by the prior adjacent-only rewrite.
```cpp
if (re().is_full_seq(a) && accepts_empty_word(b)) result = a; // A1
if (re().is_full_seq(a) && re().is_union(b, u1, u2) && ...) ... // A2
if (re().is_intersection(a, u1, u2) && re().is_full_seq(b) && ...) result=a; // A3
if (re().is_star(a, a1) && re().is_concat(b, b1, b2) && re().is_star(b1,b3) && a1==b3) result=b; // A4
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`seq_plugin::edit_distance_with_updates` used the left-string DP index
when checking whether the right string could accept an insertion from
the `d[i][j - 1]` transition. This miscomputed updateable edit distance
and could suppress valid repair proposals when `i != j`.
- **Bug fix**
- Change the right-side insertion guard in
`src/ast/sls/sls_seq_plugin.cpp` from `b.can_add(i - 1)` to `b.can_add(j
- 1)`.
- This aligns the mutability check with the DP transition being
evaluated and with the existing update-generation logic below it.
- **Regression coverage**
- Add a focused test in `src/test/sls_seq_plugin.cpp` for an asymmetric
variable/value layout on the right-hand side.
- The test asserts that the repair logic admits the right-side add at `j
- 1`, which is the case that the previous index mixup could reject.
- **Reference**
- The updated condition now matches the intended transition semantics:
```cpp
if (d[i][j - 1] < u[i][j] && b.can_add(j - 1)) {
m_string_updates.reset();
u[i][j] = d[i][j - 1];
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`src/ast/sls/sls_seq_plugin.cpp::is_sat()` had two unconditional abort
paths (`VERIFY(false)` and `NOT_IMPLEMENTED_YET()`) reachable from valid
string formulas under SLS. This changes those paths to graceful
repair/fail behavior so SLS can continue search instead of terminating
the process.
- **Length coherence fallback no longer aborts**
- Replaced the terminal `VERIFY(false)` in the `str.len` coherence block
with a normal `return false` repair failure path.
- Effect: failed local repair is propagated to the outer SLS loop
instead of crashing.
- **Implemented `seq.last_indexof` coherence handling**
- Replaced `NOT_IMPLEMENTED_YET()` with concrete coherence logic:
- read current `x`, `y`, and `e`,
- compute `actual = sx.last_indexof(sy)`,
- update `e` when `e != actual`,
- otherwise continue.
- Effect: formulas containing `seq.last_indexof` are handled in SLS
coherence checks instead of aborting.
- **No new hard-abort behavior introduced**
- In the new `last_index` block, non-numeral `e` is handled by graceful
`return false` (repair failure), not assertion abort.
```cpp
if (seq.str.is_last_index(e, x, y) && seq.is_string(x->get_sort())) {
auto sx = strval0(x), sy = strval0(y);
rational val_e;
if (!a.is_numeral(ctx.get_value(e), val_e))
return false;
rational actual(sx.last_indexof(sy));
if (val_e == actual) continue;
update(e, actual);
return false;
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`add_substr_edit_updates` uses a `HashSet` to deduplicate substrings of
`val_other`, but on a duplicate hit it `break`s the inner loop instead
of skipping just that entry. This causes all longer substrings from the
same starting position to be silently dropped as repair candidates.
## Change
- **`src/ast/sls/sls_seq_plugin.cpp`** — replace `break` with `continue`
in the inner substring-enumeration loop.
```cpp
// Before — exits the inner loop on first duplicate, missing e.g. "ab" in "aab"
if (set.contains(sub))
break;
// After — skips only the duplicate, continues with longer substrings at same offset
if (set.contains(sub))
continue;
```
For `val_other = "aab"`, the old code never proposed `"ab"` (i=1, j=2)
as a repair candidate because the duplicate `"a"` (i=1, j=1) terminated
the inner loop prematurely.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`src/ast/ast_smt_pp.cpp` emitted a compiler warning on macOS because
`quantifier_kind::choice_k` was not handled in
`smt_printer::visit_quantifier`. This change makes the switch exhaustive
and preserves printer behavior for existing quantifier kinds.
- **Problem**
- `visit_quantifier` handled `forall_k`, `exists_k`, and `lambda_k`, but
omitted `choice_k`, triggering `-Wswitch`.
- **Change**
- Added an explicit `choice_k` branch in the quantifier-kind switch in
`/tmp/workspace/Z3Prover/z3/src/ast/ast_smt_pp.cpp`.
- The branch prints `choice` in SMT output, consistent with how other
quantifier headers are emitted.
- **Code snippet**
```cpp
switch (q->get_kind()) {
case forall_k: m_out << "forall "; break;
case exists_k: m_out << "exists "; break;
case lambda_k: m_out << "lambda "; break;
case choice_k: m_out << "choice "; break;
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
While working on https://github.com/Z3Prover/z3/pull/9405, I noticed
that euf_mam.cpp code was slightly out of sync with mam.cpp and did some
redundant work.
Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
This simplifies the recent `choice` axiom path in the SMT array solver
for consistency with the SAT-side implementation. The change is purely
structural: align local naming with the quantifier body it represents,
inline a single-use literal, and remove stray whitespace in the array
decl header.
- **Choice axiom cleanup**
- Rename the local implication term in
`theory_array_full::instantiate_choice_axiom` from `ax` to `body`
- Match the naming already used in
`sat/smt/array_axioms.cpp::assert_choice_axiom`
- **Single-use literal inlining**
- Replace the temporary `literal l = mk_literal(q); assert_axiom(l);`
with a direct call
- Reduce noise without changing behavior
- **Header whitespace cleanup**
- Remove trailing whitespace in `src/ast/array_decl_plugin.h`
```c++
expr_ref body(m.mk_implies(px, pc), m);
expr_ref q(m.mk_forall(1, &x_sort, &x_name, body), m);
ctx.get_rewriter()(q);
assert_axiom(mk_literal(q));
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
