The nightly release failed because the default `GITHUB_TOKEN` is a
GitHub Actions App installation token without permission to create a tag
that includes workflow changes.
- Mint a short-lived installation token for `z3prover-ci-bot`.
- Request only `contents: write` and `workflows: write`.
- Use the App token for checkout credentials, tag deletion/push, and
release deletion/creation.
- Do not use `GH_AW_GITHUB_TOKEN`, a PAT, or another classic token.
Repository setup:
- `Z3_CI_APP_CLIENT_ID` is configured on `Z3Prover/z3`.
- Add `Z3_CI_APP_PRIVATE_KEY` as an Actions repository secret.
- Grant `z3prover-ci-bot` **Workflows: Read and write**, then approve
the updated installation permissions for the Z3Prover organization.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
`re.loop` has two accepted AST forms: bounds as decl parameters, `((_
re.loop lo hi) r)` (1 argument, 2 parameters), and bounds as arguments,
`(re.loop r lo hi)` (3 arguments, 0 parameters). The plugin accepts
arities 1, 2 and 3, and `is_loop` has separate overloads for each form.
Only the parameter form was recognized downstream.
### The soundness bug
`mk_info_rec`'s `OP_RE_LOOP` case read the bounds solely from
`get_decl()->get_num_parameters()`, which is 0 for the argument form, so
it silently fell back to the locals `lower_bound = 0, upper_bound =
UINT_MAX`. `info::loop` computes
```cpp
loop_nullable = (nullable == l_true || lower == 0) ? l_true : nullable;
```
so `lower == 0` forces nullability, and `min_length` collapses to
`min_length * 0 = 0`.
Net effect: `(re.loop (str.to_re "ab") 1 3)` was reported as `nullable =
l_true, min_length = 0`. At the SMT level
```smt2
(declare-const x String)
(assert (str.in_re x (re.loop (str.to_re "ab") 1 3)))
(assert (= (str.len x) 0))
(check-sat)
```
answered **sat** rather than unsat. The indexed form of the same regex
correctly answers unsat.
`seq_rewriter::mk_re_loop` already normalizes the argument form to
`mk_loop_proper`, which is why this was never observable on the usual
paths — it only surfaces where the rewriter is bypassed, as in
`seq_monadic`. The `info.nullable` fast path added in #10366 didn't
create the bug but widened the path that reaches it.
### The performance bug
`derive_core` had no case for the argument form either, so the
derivative got stuck as an uninterpreted `re.derivative` term.
Instrumenting all three sites that can emit a symbolic `re.derivative`
showed that **every one of the 4171 stuck terms** in the regex corpus
came from this fall-through (the 512-deep recursion cap and the
unnormalizable `re.reverse` site never fired), and 4096 of them came
from a single legacy-form loop, whose search then burned its full budget
before giving up.
### The fix
* `mk_info_rec` branches on `get_num_args()`; for the argument form it
reads the bounds from `get_arg(1)`/`get_arg(2)` when they are unsigned
numerals, and returns `unknown_info` when they are not.
* `derive_core` normalizes the numeral argument forms to
`mk_loop_proper`/`mk_loop` and recurses. The block is gated on the cheap
`re().is_loop(r)` kind check so that regexes falling through to the
later cases don't pay for the `rational` locals.
Arguably the right long-term place to normalize is the parser, so the
legacy form never reaches the AST at all. Keeping the `mk_info_rec` half
is still worthwhile as a guard for API-constructed terms, and the
regression test builds the term directly via `mk_app`, so it stays
meaningful either way.
### Regression test
`src/test/seq_rewriter.cpp` gains a case asserting that `get_info`
agrees on the two forms (`nullable == l_false`, `min_length == 2`).
Verified to actually catch the bug: reverting `seq_decl_plugin.cpp` and
rebuilding gives `ASSERTION VIOLATION` with `nullable=l_true
min_length=0`.
### Evaluation
Full run over 1545 regex benchmarks with declared statuses, in both
transition modes:
| | light-ant | brz |
|---|---|---|
| decided (before → after) | 1462 → **1463** | 1464 → **1465** |
| soundness mismatches | 0 → 0 | 0 → 0 |
| verdict changes | 1 | 1 (same file) |
The one changed file is `L4-01-loop-sat.smt2`: **undef @ 8625 ms → sat @
0.20 ms**. The corpus contains 1 legacy-form file and 236 indexed-form
files, which share the modified `OP_RE_LOOP` path, hence the full A/B
rather than a spot check.
Timing is neutral. Measured with an interleaved base/fix/base/fix
protocol over two saved binaries, since same-binary run-to-run variance
(±8%) turned out to exceed the effect: paired best-of-2 over the 315
files taking >1 ms gives a **median ratio of 0.998** (p25/p75 =
0.889/1.075), overall 0.976.
`tst_seq_rewriter` passes, `seq_monadic` is ALL PASS in both modes, and
the 22172-file QF_S corpus shows no verdict changes and no mismatches.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
Follow-up cleanup requested in review of the seq_monadic work. Based
directly on master, independent of #10370.
`light_ant_derivative_cofactors` was implemented in `seq_rewriter`, even
though it is purely a derivative operation: it post-processes the output
of `derive::derivative_cofactors` and uses no rewriter state beyond the
shared `bool_rewriter`. The two sibling entry points, `get_cofactors`
and `brz_derivative_cofactors`, were already thin forwarders into
`seq::derive`, so this one was the odd one out.
### Change
The body moves to `seq::derive`, next to `get_cofactors` and
`derivative_cofactors`, so all three cofactor entry points live in one
place. `seq_rewriter` keeps `light_ant_derivative_cofactors` as an
inline forwarder in the header, matching how the other two are exposed —
no caller changes anywhere (`seq_monadic`, `smt/seq_regex`,
`seq_range_collapse`, `seq_regex_bisim`, and the unit tests all keep
calling it through the rewriter).
| file | |
|---|---|
| `seq_derive.h` | declaration + doc comment |
| `seq_derive.cpp` | +61, the body |
| `seq_rewriter.cpp` | −61, the body |
| `seq_rewriter.h` | forwarder becomes inline, like its two siblings |
The one non-mechanical detail: the splitting step builds its
concatenation with `seq_rewriter::mk_regex_concat`, which stays in the
rewriter because other rewriter code uses it. `derive` already holds the
`m_re` back-reference and calls through it for `mk_inter`, `mk_xor0` and
`is_subset`, so the moved code does the same rather than duplicating the
constructor. The terms produced are identical.
### Verification
Pure refactoring, so this was checked for exact equivalence rather than
for improvement.
* **0 verdict differences** against master over 1545 regex benchmarks,
in light-ant (the mode that exercises this path) and in brz. Decided
counts unchanged at 1462 / 1464.
* `seq_monadic` ALL PASS in both transition modes; `seq_rewriter`,
`seq_regex_bisim` and `regex_range_collapse` all pass.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
## Summary
Two related changes:
1. Rewrite `(Σ*·S)*` to the flat form `() | Σ*·S` in
`seq_rewriter::mk_re_star`.
2. Make `seq_monadic_bench` normalize its inputs, so that rewriter-level
changes are
observable at all.
## The rewrite
`Σ*·S` is idempotent under concatenation. Any word of `(Σ*·S)·(Σ*·S)`
factors as
`(Σ*·S·Σ*)·S`, and the leading `Σ*·S·Σ*` is absorbed by `Σ*`, so the
word is again in
`Σ*·S`. Hence `L·L ⊆ L`, and therefore `L* = () | L`.
This is the same absorption argument the subset checker already
implements — see the
"prefix absorption" rule `P·R' ⊆ Σ*·R'` in `seq_subset.cpp`. It was
simply never applied
to the star.
The two forms denote the same language but are not equally cheap to
determinize. Under
the star, every residual carries a trailing `(Σ*·S)*` factor, so the
derivative automaton
keeps a separate copy of the `S`-tracking states for each unfolding. The
flat form drops
that factor and the copies collapse.
Measured live-state counts of the derivative automaton:
| regex | star form | flat form |
|---|---|---|
| `nonA ∩ (Σ*·b·Σ^5)*` | 904 | **65** |
| `core ∩ (Σ*·b·Σ^5)*` | 1807 | **129** |
roughly a 14x reduction.
The shape is not exotic: it is what a "contains" pattern under a star
looks like, and it
occurs in 27 of the 1545 regex benchmarks I track.
## The bench change
`seq_monadic_bench` handed `seq_monadic` the raw parsed regex, whereas
in the solver
`seq_regex` only ever sees terms that `asserted_formulas` has already
rewritten. The
bench therefore could not observe a rewriter-level change at all — the
rewrite above
measured as *exactly zero* difference across all 1545 benchmarks in both
modes until the
bench was made to normalize.
Each `str.in_re` regex argument now goes through `th_rewriter` before
reaching
`seq_monadic`, placed ahead of the multi-membership merge so that
`mk_regex_inter_normalize` also receives normalized operands.
This is closer to production but not identical to it:
`asserted_formulas` rewrites whole
assertions and can propagate across them, while this rewrites each
membership's regex in
isolation.
## Measurements
Combined effect over 1545 regex benchmarks, against master:
| mode | decided | gained | lost | mismatches | status conflicts |
|---|---|---|---|---|---|
| light-ant | 1464 → **1467** | 4 | 1 | 0 | 0 |
| brz | 1466 → **1469** | 4 | 1 | 0 | 0 |
Gained in both modes:
- `MargusRegex/levels/L4-01-loop-sat`
- `ClemensRegex/generated/split_membership_medium_sat_0012`
- `ClemensRegex/generated/split_membership_medium_sat_0000`
- `ClemensRegex/generated_easy/split_membership_easy_unsat_0009`
The single loss per mode comes from the normalization, not the rewrite,
and is marginal in
both cases: `easy_unsat_0006` (light-ant) took 5.5 s and
`medium_sat_0036` (brz) took
3.9 s on master, and both now trip a cap slightly earlier. Each is
mode-specific —
`easy_unsat_0006` is still decided in `brz`, and `medium_sat_0036` was
already undecided in
`light-ant` on master.
Runtime, paired best-of-2 over two interleaved rounds:
| | outside `ClemensRegex/generated` | `ClemensRegex/generated` |
|---|---|---|
| light-ant | +2.2% | +12.0% |
| brz | −0.2% | +11.3% |
Outside the `generated` family this is inside the ±8% run-to-run noise
of the measurement
machine. Within that family the increase is expected and is what buys
the extra
decisions: those files previously tripped the `state_cap` bail early,
and with the smaller
automaton the search gets further before exhausting the budget. The cost
stays bounded by
the existing budget.
The rule fires only on the `Σ*·S` shape:
```
(simplify (re.* (re.++ re.all (str.to_re "b"))))
→ (re.union (re.++ re.all (str.to_re "b")) (str.to_re ""))
(simplify (re.* (re.++ (str.to_re "a") (str.to_re "b"))))
→ (re.* (str.to_re "ab"))
```
## Tests
Adds case 22 to `src/test/seq_rewriter.cpp`: checks that `(Σ*·b)*` is no
longer a star
after rewriting, and pins the semantics with three solver queries —
`"ab"` and `""` are
members, `"ba"` is not.
`seq_rewriter`, `seq_monadic`, `seq_regex_bisim` and
`regex_range_collapse` all pass in
both `light-ant` and `brz` modes.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
Materializing the monadic decomposition as a DNF is the dominant cost in
the
solver. The product over per-position split degrees (and, for a
conjunction of
memberships, over memberships) is exponential, and the `DNF_CAP` of 2^14
disjuncts meant the solver mostly gave up *structurally* rather than
because the
problem was hard — it paid the full product cost before testing
anything.
This decides the same disjunction by depth-first search, without ever
materializing it.
## How it works
`decide()` -> `prepare()` -> `dfs_membership(0)`.
`prepare()` parses each membership into atoms and records every
variable's
**last occurrence** as a packed `(membership_idx << 32) | atom_idx`.
Positions
compare lexicographically in exactly the order the search visits them,
so
"have I seen this variable for the last time?" is an integer equality.
`dfs_atoms(mi, i, R)` walks one membership:
- end of atoms: the remainder is epsilon, so the branch survives iff `R`
is
nullable (an undecidable nullability propagates as `l_undef` rather than
being
guessed);
- constant element: consumed by a derivative, `re.empty` prunes
immediately;
- variable: the last atom is a plain membership, otherwise the variable
drives
the derivative automaton from `R` to some live state `q`, one child per
target.
Components are accumulated per variable in `m_groups[vi]` along the
current
branch — pushed on entry, popped on backtracking. The per-variable
emptiness
test runs as soon as the group is complete (the search just passed the
variable's last occurrence) or holds more than one component, which is
the
earliest point an inconsistency can exist. That test has to happen
anyway;
running it there prunes the whole remaining subtree instead of after the
product
has been built. The search stops at the first satisfying leaf.
A variable shared by several memberships accumulates several components
in the
same branch and they are intersected, so the joint solve falls out of
the search
rather than needing the DNF multiplication.
## Supporting changes
- `group_nonempty` memoizes on the sorted, deduplicated `(state,
target)`
signature of the group, and collapses duplicated components before the
product
search (which is exponential in component count);
- memoize live split states per regex, and `der_elem` per `(regex,
element)`;
- memoize nullability locally — `seq_rewriter`'s own cache is capped at
10000 and
`cleanup()` flushes the entire table;
- hoist the cofactor vectors out of the product loop and reference them
instead
of re-materializing `expr_ref` pairs on every pop;
- `m_budget` becomes a global node budget, and `m_giveup` unwinds the
whole
search instead of letting sibling branches keep expanding.
Removed: `build_membership_dnf`, `decide_dnf`, `simplify_dnf`, the
`disjunct`
type and `DNF_CAP`. The persistent cofactor cache and the separate
`guard_set::cache` are kept as-is; both own their pins, so they survive
the
per-`decide` `m_pin` reset.
## Results
Measured against master (4b2e69c66), same bench harness.
**regexes (1545 files), light-antimirov:** 41 benchmarks newly decided
(22 sat, 19 unsat), **no verdict regressions**, and 8.8s -> 2.2s on the
1421
files both versions decide. Unchanged: 2 timeouts, 0 crashes, 0
mismatches
against declared status. Brzozowski mode agrees: 0 mismatches, 0
disagreements
with light-antimirov.
**QF_S (22172 files):** 0 crashes, 0 timeouts, 0 mismatches on the 4089
benchmarks that are complete and have a declared status. Verdicts are
identical
to master.
Unit tests pass in both transition modes.
## Caveat
On the 81 files neither version decides, DFS costs more (62s -> 149s):
it
explores until the 200000-node budget is exhausted, whereas the DNF path
bailed
immediately at its structural 2^14 cap. `m_budget` has not been retuned
since
the per-node cost dropped, so there is likely room to recover most of
that
without losing the 41 newly decided benchmarks.
---------
Co-authored-by: Margus Veanes <margus@microsoft.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
When smt.seq.regex_monadic is on, keep contains-style memberships
(s in .*P.*) as regex memberships routed to the monadic solver instead
of rewriting them into a word equation s = f1 ++ P ++ f2. The word
equation blows up theory_seq on long concatenations before final_check
(hence monadic) is ever reached.
Evaluated on 1476 regex benchmarks (10s timeout): solved 1160 -> 1341
vs legacy, +193 newly solved, 0 sat<->unsat soundness disagreements.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Follow-up to the feedback that `seq_monadic_bench` silently drops
non-membership
constraints and therefore reports results that don't correspond to the
benchmark
it claims to be solving. In particular the ipv6 benchmarks are guarded
by
`str.len` bounds, which the monadic solver *can* already express.
Test-only change (`src/test/`), no solver code touched.
## 1. Model length bounds via the existing API
`seq_monadic` already exposes `add_lo` / `add_hi` / `add_len`, which
encode
`t in Σ^lo Σ*`, `t in Σ^{0,hi}` and `t in Σ^{len,len}`. The harness now
extracts
constant length bounds from assertions and feeds them through:
- handles `<=`, `<`, `>=`, `>`, `=` in either argument order, under
arbitrary
`not` nesting;
- applies to any term the solver accepts (a variable, or a
concatenation), so
`(> (str.len x) 0)` alongside `(str.in_re (str.++ x y x) R)` works;
- intersects multiple bounds on the same term, and encodes an
unsatisfiable
bound (`|t| < 0`, or crossing bounds) as `lo=1, hi=0`;
- rejects rather than approximates anything not representable — an
out-of-range
constant, a relational bound `(= (str.len x) (str.len y))`, or a
semilinear
one `(= (str.len x) (* 2 k))` is counted as dropped, not silently
weakened.
`ipv6-exactly-one-cc-sat.smt2` now reports `complete=yes, dropped=0,
verdict=sat`,
matching its declared status.
## 2. Report incompleteness
Dropping conjuncts only weakens the problem, so on an incomplete
benchmark
`unsat` transfers to the original but `sat` says nothing. That was
previously
invisible. Now:
- a `dropped` column counts unmodellable **conjuncts** (not top-level
assertions), so it is a precise "how much of the benchmark is missing";
- single-file mode prints an `INCOMPLETE: ...` warning to stderr;
- the summary line gained `incomplete_sat=`, the count of results that
must not
be trusted;
- the file header documents the semantics.
`collect` also no longer short-circuits on the first unsupported
conjunct of an
`and`, which was discarding modellable siblings. On QF_S this alone
moves 456
files from `undef` to a decided verdict.
## 3. Unit tests
11 tests in a new *length bounds on compound terms* section of
`seq_monadic.cpp`: bounds on concatenations (`x.y.x`, `x.a.x`), several
bounded
variables under one membership, a case where the bound is the only cause
of
unsat, crossing `lo`/`hi`, and two ipv6-shaped tests reconstructing
`R = has_cc ∩ ¬two_cc ∩ hexcol`. All pass in both `brz` and `light-ant`.
## Validation
Both corpora, both transition modes, against master at c9a480cb3.
**regexes (1545 files):** complete 1448 → 1453. Two verdicts change,
both from
`sat` to `unsat` — these were previously *wrong*, caused by dropped
length
constraints; one of the two is declared `unsat` upstream. 0 crashes, 2
timeouts
(unchanged), 0 mismatches against declared status on complete benchmarks
in
either mode, and 0 disagreements between `brz` and `light-ant`.
**QF_S (22172 files):** 0 crashes, 0 timeouts. Of the 4089 files that
are both
complete and have a declared status, 0 mismatches. Of the 4366
incomplete files
that returned `unsat`, 4097 are declared `unsat` and **none** is
declared `sat`,
which is the invariant that matters for the weakening argument above.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
The cofactor cache is a pure function of the regex (and the fixed transition
mode), independent of the membership set, so tearing it down on every solve()/
decide() call forced it to be recomputed n+1 times during minimize_core()'s n
deletion trials. Keep it instead, resetting only when it grows past a size cap.
Encapsulate the cofactor memo, its pinned-key trail, and the coupled range-
predicate (guard_set_cache) into a self-contained cofactor_cache class with
find/insert/reset/maybe_reset, so the three reset in lockstep (the range
predicates' guards are owned by the cofactor vectors).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Addresses code review feedback on PR #10361: the raw `obj_map` typedef +
static `dealloc_cache` helper is replaced by a proper `guard_set_cache`
class that owns its memory and adds a recycling optimization.
## Changes
- **New `guard_set_cache` class** (`guard_set.h` / `.cpp`):
- `m_cache` — `obj_map<expr, seq::range_predicate*>` (null value =
unsupported guard, avoids retranslation)
- `m_fresh` — pre-allocated `range_predicate*` recycled across failed
translations; when `guard_to_range_predicate` rejects a guard, the heap
object is retained in `m_fresh` instead of deallocated, so the next miss
reuses it without an alloc/dealloc round-trip
- Public API: `reset()`, `find(expr*, seq::range_predicate*&) → bool`,
`fresh(unsigned max_char) → seq::range_predicate*`, `insert(expr*,
seq::range_predicate*)`
- **`guard_set`**: removed `rp_cache` typedef and `dealloc_cache`
static; constructor parameter updated to `guard_set_cache*`; `conjoin`
updated to use `fresh()` + `insert()` for the recycling path
- **`seq_monadic`**: field type `guard_set::rp_cache` →
`guard_set_cache`; reset call updated to `m_rp_cache.reset()`
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
`guard_set::conjoin` re-translated its guard expression into a
`seq::range_predicate` on every call. It sits in the innermost loop of
`seq_monadic::product_nonempty`'s product-transition enumeration, where
the same handful of cofactor guards recurs on every branch of the
product search — a single regex benchmark was measured at **4.4M
translations of a few dozen distinct guards**.
## Change
Add an optional `guard -> range_predicate` cache to `guard_set`. It is
owned by the caller so its lifetime can be tied to the lifetime of the
guard expressions themselves; `seq_monadic` keys it off
`m_cofactor_cache` (which owns the guards) and resets both together. A
null cache entry records an unsupported guard, preserving the `m_ok =
false` behaviour without retranslating.
The cache is used only on the character-sort path, and is valid only
while every `guard_set` sharing it uses the same element variable `v0`.
That holds in `seq_monadic`: `v0` is `m.mk_var(0, m_elem_sort)`, which
is hash-consed, and the element sort is fixed for the duration of a
solve. The parameter defaults to `nullptr`, so any other caller keeps
the previous behaviour unchanged.
No behavioural change.
## Validation
`test-z3 seq_monadic`: ALL PASS (0 fail) in both `brz` and `light-ant`
modes.
1545-file regex corpus (`light-ant`, 20s timeout per file):
| | master | this PR |
|---|---|---|
| sat / unsat / undef | 1166 / 255 / 121 | 1166 / 255 / 121 |
| timeouts | 3 | 2 |
| solve time, 1421 files decided by both | 74.7 s | **8.4 s (~9x)** |
Verdicts are identical to master on every file; one benchmark that
previously hit the 20s timeout now terminates.
Full QF_S corpus (22,172 files) on the follow-up branch that builds on
this one: 0 crashes, 0 timeouts, and on the 4,089 benchmarks where the
monadic solver is complete and the expected status is known, 0
mismatches against the declared status.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
- Fix angle-bracket include for expr_safe_replace.h to use quotes
(consistent with all other local includes in this file)
- Rewrite block_unfolding using early-return guard clauses instead of a
single boolean expression with a comma-operator side effect, which was
difficult to read and reason about
- Replace while (size() > 0) with idiomatic while (!empty()) in
mk_deriv_accept DFS loop
- Expand nested ternary chains in mk_deriv_accept into explicit if/else
chains for readability (ite-branch and union-branch cases)
No functional change.
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Feed arithmetic length lower/upper/exact bounds (via theory_seq
lower_bound/upper_bound) into the monadic regex end-game solver using the
existing add_lo/add_hi/add_len helpers, so proposed witnesses respect length
constraints and length-driven cases resolve directly instead of backtracking
over the model.
Dependencies handed to the monadic solver now encode a union of sorts:
2*lit.index() for membership literals (even) and 2*bound_index+1 for length
bounds (odd). On unsat, the core is decoded back into conflict literals,
materializing the justifying arithmetic bound literals (len>=lo, len<=hi) at
that point. Bounds are recorded in m_monadic_bounds and undone via push_trail.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
The clang-tidy warning report surfaced a small set of high-confidence
analyzer findings with straightforward fixes: intentional null
dereference in debug-only crash paths, undefined oversized shifts in
`mpff`, uninitialized state in sorting-network setup, and `% 0` in a
unit test edge case.
- **Debug crash path**
- Replaced intentional null writes in `src/util/debug.cpp` with an
explicit crash helper based on `SIGSEGV`/`abort`.
- Keeps the failure mode intentional without relying on undefined
pointer dereference.
```c++
[[noreturn]] static void force_segfault() {
std::raise(SIGSEGV);
std::abort();
}
```
- **`mpff` integer extraction**
- Hardened `get_uint64` / `get_int64` against analyzer-reported
oversized right shifts.
- Computes the shift count in `int64_t`, asserts the valid range, and
guards the shift site.
- **Sorting-network initialization**
- Initialized `psort_nw::m_t` in the constructor to avoid
uninitialized-object diagnostics on construction paths that inspect
state before later assignment.
- **Test-only edge cases**
- Added an early return in `src/test/total_order.cpp` for `sz == 0` to
avoid `% 0` in randomized loops.
- Removed the extra trailing semicolon pattern around the `find_q`
namespace in `src/test/var_subst.cpp`.
- **Scope**
- Focused only on localized, semantics-preserving fixes from the warning
artifact.
- Left broader architectural warnings (for example,
constructor/destructor virtual-call diagnostics) out of this change.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The clang-tidy warning fixer depended on
`download_workflow_run_artifact` to fetch the warning report from the
producer workflow. That path is blocked here, so the fixer could
discover the run but not access the warning contents it needs to
analyze.
- **Fixer input path**
- Update
`/home/runner/work/z3/z3/.github/workflows/build-warning-fixer.md` to
consume the triggering run via `list_workflow_jobs` + `get_job_logs`
- Remove the artifact-download flow from the workflow instructions
- Parse warning and status data from the build job log, with a grep
fallback if the structured summary is missing
- **Producer log contract**
- Update
`/home/runner/work/z3/z3/.github/workflows/clang-tidy-warning-report.yml`
to emit a stable, marker-delimited summary block at the end of the build
job log
- Include both build status and the extracted warning subset in that
block
- Leave artifact upload in place as optional output rather than a
required dependency
- **Workflow behavior**
- Make the fixer operate entirely from Actions logs, avoiding cross-run
artifact retrieval as part of its primary path
- Preserve the existing warning extraction model while shifting the
producer/consumer contract to log output
Example of the emitted log shape:
```text
CLANG_TIDY_WARNING_REPORT_BEGIN
CLANG_TIDY_STATUS_BEGIN
configure_status=0
build_status=0
CLANG_TIDY_STATUS_END
CLANG_TIDY_WARNINGS_BEGIN
123: warning: ...
CLANG_TIDY_WARNINGS_END
CLANG_TIDY_WARNING_REPORT_END
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This updates the Clang-Tidy Warning Fixer to run after
`clang-tidy-warning-report.yml` completes, consume that run’s warning
artifacts, and produce assignment-ready fix proposals as GitHub issues.
It replaces the previous self-build/PR-creation flow with
artifact-driven analysis and diff-first issue output.
- **Trigger + execution model**
- Switched workflow trigger from scheduled standalone runs to
`workflow_run` on **Clang-Tidy Warning Report** completion (with manual
dispatch retained).
- Keeps fixer analysis scoped to diagnostics from the originating report
run.
- **Artifact-driven diagnostics input**
- Removed in-fixer prebuild/clang-tidy compilation step.
- Updated agent instructions to resolve source run ID, list/download the
warning artifact, extract logs, and analyze
`warnings.txt`/`combined.log` from that artifact.
- **Output contract: PR → Issue**
- Replaced safe output target from `create-pull-request` to
`create-issue`.
- Issue content now requires:
- warning summary,
- skipped-warning rationale,
- proposed fixes as full unified diffs,
- assignment-ready checklist entries.
- **Workflow/runtime alignment**
- Regenerated lockfile to match source workflow changes.
- Added Actions toolset/permissions needed for run/artifact retrieval in
the agent runtime.
```yaml
on:
workflow_run:
workflows: ["Clang-Tidy Warning Report"]
types: [completed]
branches: [master]
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `Build Z3 with clang-tidy warnings` job was failing before
compilation due to an invalid `cmake --build` invocation. The workflow
passed a Ninja-only flag directly to CMake, so the job exited with
`Unknown argument -k` instead of producing the intended warning report.
- **Root cause**
- The workflow invoked:
```bash
cmake --build build --target shell test-z3 -k 0
```
- `-k 0` is a native Ninja argument and must be forwarded through CMake
after `--`.
- **Change**
- Update the clang-tidy warning workflow to pass native build-tool
arguments correctly:
```bash
cmake --build build --target shell test-z3 -- -k 0
```
- **Effect**
- The job can now reach the actual Ninja build instead of failing in
CMake argument parsing.
- This restores the intended behavior of collecting clang-tidy/build
diagnostics in the workflow artifact.
- **Files**
- `.github/workflows/clang-tidy-warning-report.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. (1 more flag after this!)
This one adds the flag -Wgnu-anonymous-struct. Z3 uses this anonymous
struct idiom, usually when using a struct as one of the members of a
union, as in:
```
union {
justification * m_js;
unsigned m_lidx;
struct {
enode * m_lhs;
enode * m_rhs;
};
};
```
This is not, strictly speaking, legal C++ (at least according to
Google's AI summary -- and the existence of this flag in Clang implies
that it is a GNU extension). You need to give the struct a member name
in the outer union to prevent the warning.
I'm of two minds on this. On the one hand it's not hurting anything, and
all the major compilers seem to support the idiom. On the other hand,
well, why do we have standards if we're going to ignore them in favor of
de-facto standards?
I submit this PR to show the size of the changes necessary to eliminate
the use of the extension. Personally, I'd do it, but I would gladly
withdraw the PR in favor of one that just silences the warning, if that
was the reviewer's preference.
Adds a scheduled workflow to build Z3 with the clang-tidy warning
configuration being tracked in detlefs' PRs, including the latest
`-Wgnu-anonymous-struct` flag from #10345. The workflow persists all
emitted warnings as an artifact so warning regressions can be reviewed
from each run.
- **Workflow**
- Adds `.github/workflows/clang-tidy-warning-report.yml`
- Runs daily and on manual dispatch
- Uses Ubuntu + CMake/Ninja with `clang` and `clang-tidy`
- **Warning coverage**
- Reuses the repository's existing Clang warning setup
- Layers in the current pending detlefs warning flag:
- `-Wgnu-anonymous-struct`
- **Artifacts**
- Captures:
- `configure.log`
- `build.log`
- `combined.log`
- `warnings.txt`
- `status.txt`
- Uploads them as a per-run artifact for inspection
- **Failure behavior**
- Still uploads logs on failure
- Marks the workflow failed if configure or build fails, so broken
clang-tidy runs are visible in Actions
```yaml
CC=clang CXX=clang++ cmake -GNinja -S . -B build \
-DCMAKE_BUILD_TYPE=Debug \
-DCMAKE_EXPORT_COMPILE_COMMANDS=ON \
-DCMAKE_CXX_CLANG_TIDY=clang-tidy \
-DCMAKE_CXX_FLAGS="-Wgnu-anonymous-struct"
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
An F* proof build failed to discharge a proof obligation because z3
returned `unknown` instead of the expected `unsat`. This PR fixes an
attributed nonlinear-arithmetic performance/completeness **regression**
in z3 that caused the failure.
- Originating F* build run:
https://github.com/Z3Prover/z3/actions/runs/30685489878
- Failing query:
`inputs/fstar-build-failures/run-30685489878/pulse/failedQueries-Pulse.Lib.PriorityQueue-3.smt2`
(`Z3Prover/bench`)
- Query label: `failedQueries-Pulse.Lib.PriorityQueue-3`
- z3 ref under test: `1ba30df028`
- **Expected result:** `unsat` — **Observed on ref under test:**
`unknown` (`:reason-unknown "canceled"`, i.e. the embedded `(set-option
:rlimit 5000000)` budget was exhausted).
The query embeds its own options (`smt.arith.solver=6`,
`smt.mbqi=false`, `auto_config=false`, `rlimit=5000000`, ...); all runs
below honor those embedded options.
## Root cause and attribution
Bisecting `./z3` between a known-good baseline
(`a05be8a291`, which returns `unsat`) and
the ref under test identified the first bad commit as:
> **`90fe0aa0f32d4cf66f3503c249d1878a39c0cf3c` — "Imp fix (#10304)"**
That commit adds `monomial_bounds::propagate_fixed_rows()` and calls it
from `nla::core::propagate()`, gated by the new parameter
`smt.arith.nl.propagate_fixed_rows` (default **true**). The routine
scans **all** LP rows on **every** nonlinear-propagation call, and calls
`lra.find_feasible_solution()` whenever anything is propagated. On this
obligation that extra work consumes the `rlimit` budget before a proof
is found, so a query that was previously `unsat` becomes `unknown`
(`canceled`). This is a pure performance/completeness regression from a
newly-added, parameter-gated heuristic — not a soundness issue in the
query.
## Fix
Default `smt.arith.nl.propagate_fixed_rows` to **false**, restoring the
pre-#10304 behaviour. The heuristic and its code are left intact and
remain available as opt-in via `smt.arith.nl.propagate_fixed_rows=true`,
pending a more efficient implementation (e.g. not re-scanning every row
on every propagation call).
This is a one-line change in `src/params/smt_params_helper.pyg`; no
solver check is weakened and the failing behaviour is not masked — the
regressing heuristic is simply returned to being opt-in.
## Reproduction and validation
All builds via `python3 scripts/mk_make.py && make -C build -j8`
(CMake/Ninja unavailable in this environment; the Makefile build
produces an equivalent binary).
| z3 | `smt.arith.nl.propagate_fixed_rows` | Result |
|---|---|---|
| baseline `a05be8a` | (n/a, pre-feature) | `unsat` |
| ref under test `1ba30df` | true (default) | `unknown` (canceled) |
| ref under test `1ba30df` | false (override) | `unsat` |
| **patched `1ba30df` (this PR)** | false (new default) | **`unsat`** |
Before the fix the query reproduced the `unknown`/`canceled` failure;
after the fix the patched binary returns the expected `unsat` with the
query's embedded options unchanged.
## Notes / uncertainty
This change restores correctness-preserving behaviour by disabling an
optional heuristic by default rather than reworking its cost model. A
follow-up could re-enable the heuristic once its per-propagation cost is
bounded (e.g. only scanning rows touched since the last call). Created
as a **draft** for maintainer review.
> [!WARNING]
> <details>
> <summary>Firewall blocked 1 domain</summary>
>
> The following domain was blocked by the firewall during workflow
execution:
>
> - `pypi.org`
>> To allow these domains, add them to the `network.allowed` list in
your workflow frontmatter:
>
> ```yaml
> network:
> allowed:
> - defaults
> - "pypi.org"
> ```
>
> See [Network
Configuration](https://github.github.com/gh-aw/reference/network/) for
more information.
>
> </details>
> Generated by [Fix a Z3 failure on an F* proof
obligation](https://github.com/Z3Prover/bench/actions/runs/30692520945)
· 398.4 AIC · ⌖ 21.5 AIC · ⊞ 9.4K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+fstar-build-fixer%22&type=pullrequests)
<!-- gh-aw-agentic-workflow: Fix a Z3 failure on an F* proof obligation,
engine: copilot, version: 1.0.65, model: claude-opus-4.8, id:
30692520945, workflow_id: fstar-build-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/30692520945 -->
<!-- gh-aw-workflow-id: fstar-build-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/fstar-build-fixer -->
Co-authored-by: z3prover-ci-bot[bot] <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
check() now records the dependencies of an unsat subset in m_core, exposed via
ptr_vector<u_dependency> const& core(). On l_false it calls minimize_core:
with the new m_min_core flag (set_min_core, default true) it deletion-minimizes
to a minimal unsat subset containing only constraints that participate in the
contradiction; with the flag off it returns all membership dependencies.
Add unit tests asserting the core omits irrelevant constraints (e.g. x in a*,
x in ~a*, y in b* has core {x-constraints} only), exercising both flag states.
The test harness runs with minimization disabled by default.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Replace the batch solve_and(mems) with an incremental interface:
void add(expr* term, expr* regex, u_dependency* d);
lbool check();
add() stores each (term, regex, dependency) triple in
m_memberships (vector<tuple<expr_ref, expr_ref, u_dependency*>>); the
dependency is retained for future unsat-core tracking and may be nullptr.
check() decides the accumulated conjunction (the former solve_and body) and
consumes the memberships; an empty conjunction is sat. Update the unit tests
and benchmark to the add()/check() API.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
