The doctests for Statistics.__len__ and Statistics.__getitem__ in
src/api/python/z3/z3.py asserted a fixed counter count (len(st) == 7).
This is fragile because the ":time" entry is only added to statistics
when the elapsed wall-clock time of check() is non-zero (see
collect_timer_stats in src/solver/check_sat_result.h). On fast native
builds, ":time" rounds to 0 and is omitted; under slow environments
(e.g. riscv64 under qemu emulation), it becomes non-zero and is
included, changing len(st).
Fix this by checking the presence of statistics rather than an exact
count.
Signed-off-by: Julien Stephan <jstephan@baylibre.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>
The `Build FStar master with Z3 master` workflow was failing because
FStar's `karamel` submodule was not present after a shallow clone,
causing `make` to abort immediately.
## Change
- Added `--recurse-submodules` to the `git clone` call for FStar in
`.github/workflows/fstar-master-build.yml`
```diff
-git clone --depth=1 --branch "$FSTAR_REF" https://github.com/FStarLang/FStar.git /tmp/gh-aw/agent/FStar
+git clone --depth=1 --recurse-submodules --branch "$FSTAR_REF" https://github.com/FStarLang/FStar.git /tmp/gh-aw/agent/FStar
```
Failing run:
https://github.com/Z3Prover/z3/actions/runs/27072072789/job/79903014692
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This change replaces the existing agentic workflow with a standard
GitHub Actions workflow that builds Z3 and then builds FStar against
that Z3. The workflow remains parameterized for both toolchains and
supports exercising `smt.ho_matching` via configurable Z3 runtime args
and FStar `OTHERFLAGS`.
- **Workflow migration (agentic → standard)**
- Replaced `.github/workflows/fstar-master-build.md` + `.lock.yml` with
a single native workflow: `.github/workflows/fstar-master-build.yml`.
- Removed dependency on agentic frontmatter, safe-outputs, and
runtime-import flow.
- **Configurable build inputs**
- Added `workflow_dispatch` inputs for:
- `z3_ref`, `z3_cmake_args`, `z3_runtime_args`
- `fstar_ref`, `fstar_opam_switch`, `fstar_otherflags`
- `discussion_category`
- Defaults preserve the requested ho-matching exercise path:
- `z3_runtime_args: smt.ho_matching=true`
- `fstar_otherflags: --smt.ho_matching true`
- **Build and integration flow**
- Builds Z3 from configured ref in `build/release` with CMake+Ninja.
- Clones/builds FStar from configured ref, wiring it to the just-built
Z3 (including version override and PATH aliases expected by FStar).
- **Discussion reporting without agents**
- Adds an `actions/github-script` step that:
- resolves discussion category ID by name,
- posts a summary discussion with inputs, produced versions, commit, and
workflow run URL.
- **Failure diagnostics hardening**
- Added explicit failure messages for missing parsed Z3 version and
missing FStar executable.
- Added defensive handling when parsing generated version text.
```yaml
on:
workflow_dispatch:
inputs:
z3_runtime_args:
default: "smt.ho_matching=true"
fstar_otherflags:
default: "--smt.ho_matching true"
```
---------
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>
This change adds an agentic workflow that builds the latest `master` of
Z3, then builds the latest `master` of FStar using that exact Z3 binary.
It addresses the gap where cross-project compatibility on head revisions
was not automated.
- **Workflow added: Z3→FStar head build**
- Created `.github/workflows/fstar-master-build.md` with daily + manual
triggers.
- Keeps permissions minimal (`read-all`) and uses `network: defaults`.
- **Z3 build phase**
- Checks out Z3 `master`.
- Builds `build/release/z3` via CMake + Ninja.
- Captures and parses the built Z3 version for downstream use.
- **FStar build phase wired to built Z3**
- Clones `FStarLang/FStar` `master`.
- Sets up OPAM and FStar dependencies.
- Forces FStar build to use the newly built Z3 via PATH aliases and
`OTHERFLAGS="--z3version <built-version>"`.
- **Compiled workflow artifact**
- Added `.github/workflows/fstar-master-build.lock.yml` generated from
the new source workflow.
```yaml
# Key integration point used in the workflow
PATH="/tmp/gh-aw/agent/z3-bin:$PATH" \
OTHERFLAGS="--z3version $Z3_VERSION" \
make -j"$(nproc)"
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This introduces an agentic workflow that continuously validates Z3→F*
integration by building Z3 from this repository’s `master` and then
building `FStarLang/FStar` from its latest `master` using that exact Z3
binary.
- **Workflow added**
- New source workflow: `.github/workflows/fstar-master-build.md`
- New compiled workflow: `.github/workflows/fstar-master-build.lock.yml`
- Triggered on `daily` schedule and `workflow_dispatch`.
- **Build orchestration**
- Checks out Z3 `master` and builds/installs it with CMake + Ninja into
`/tmp/gh-aw/agent/z3-install`.
- Clones latest `FStarLang/FStar` `master` and records the exact commit
SHA used.
- Forces F* build to use the locally built Z3 via:
- `PATH=/tmp/gh-aw/agent/z3-install/bin:$PATH`
- `Z3_EXE=/tmp/gh-aw/agent/z3-install/bin/z3`
- **Reporting + failure handling**
- On success: posts a discussion with Z3 commit/version, F* commit, and
command summary.
- On failure: opens an issue with failing phase, error summary, and log
excerpts.
- Uses safe-outputs with bounded lifetime (`expires: 14d`) and explicit
failure labeling.
```yaml
safe-outputs:
create-discussion:
title-prefix: "[F* Build] "
close-older-discussions: true
expires: 14d
create-issue:
title-prefix: "[F* Build Failure] "
labels: ["build", "fstar"]
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Why
Removes the three issue-oracle steps from the Ubuntu nightly job. They
have been failing every nightly run since they landed in #9688 — see
[run
26927938635](https://github.com/Z3Prover/z3/actions/runs/26927938635/job/79441695358):
- **`Clone bench (for issue-oracle smoke test)`** → exit 128 with
`fatal: could not read Username for 'https://github.com'`, because
`Z3Prover/bench` is a private repo and the workflow had no credentials
for it.
- **`Run issue-oracle smoke test`** → exit 2 because
`bench/scripts/issues_check_oracle.py` was never downloaded.
- **`Upload issue-oracle report`** → warning because the JSON report was
never produced.
All three were absorbed by `continue-on-error: true`, so the job stayed
green, but every nightly emitted two stale red error annotations and
**the smoke test never actually ran**.
## What replaces it
The smoke test has been moved to a new workflow in `Z3Prover/bench`:
[`.github/workflows/issue-oracle.yml`](https://github.com/Z3Prover/bench/blob/ci/issue-oracle-pull-z3-nightly/.github/workflows/issue-oracle.yml)
— see **Z3Prover/bench PR #2504**.
The bench-side workflow:
- runs at 04:30 UTC daily (this repo's nightly runs at 02:00 UTC + DAG,
so ~2.5 h slack);
- pulls the `z3-*-x64-glibc-*.zip` asset from **this repo's public
`Nightly` release** via `gh release download` — unauthenticated for
`Z3Prover/z3` because z3 is public, so **no cross-repo PAT and no
`BENCH_REPO_TOKEN` secret** are required;
- checks the release's `publishedAt` is < 18 h old, so a skipped/failed
upstream nightly reds the workflow instead of silently re-testing
yesterday's binary;
- runs `issues_check_oracle.py` with the exact same smoke-test budget
the deleted step used (`--max 200 --timeout 5 --wallclock 20 --jobs 0`,
outer `timeout 90`);
- uploads `issue-oracle-report.json` as an artifact (7-day retention).
## Scope of this PR
Only the three dead steps are deleted; the downstream `Upload artifact`
(`UbuntuBuild`) step and everything that depends on it
(`deploy-nightly`, etc.) are unchanged. A short comment replaces the
deleted block to direct future readers to the new home.
## Merge order
This PR can land **before, after, or simultaneously with** the
bench-side PR. There is no functional regression either way:
- Today, the deleted steps produce zero useful output (just noisy
annotations). Removing them is strictly an improvement to nightly log
signal.
- The bench-side workflow stands on its own and produces output the
moment it lands (since it pulls from the already-existing `Nightly`
release).
## Validation
- `python -c "import yaml;
yaml.safe_load(open('.github/workflows/nightly.yml'))"` → OK.
- Search confirms no remaining live references to `bench/`,
`BENCH_REPO_TOKEN`, or `issue-oracle-report.json` in `nightly.yml` (only
the explanatory comment in the deletion block).
- Diff: -56 / +9, single file.
---
**Companion PR (do not merge before this one is reviewed):**
https://github.com/Z3Prover/bench/pull/2504
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Adds a tightly-bounded issue-oracle smoke test as a sibling of the
existing `test_benchmarks.py` step in the nightly's `ubuntu-build` job.
The step always runs as part of every nightly, can never fail the build,
and completes in ~2 min.
## Why
`Z3Prover/bench` ships a per-issue regression corpus
(`inputs/issues/iss-N/`) plus a runner
(`scripts/issues_check_oracle.py`) that diffs current z3 output against
captured `<stem>.expected.out` byte streams. Wiring that into the
nightly gives us a daily smoke signal that detects regressions on
benchmarks distilled from real z3 issues — without requiring any z3
contributor to ever touch the bench repo.
## What
A two-step block added right after the existing `Clone z3test` + `Test`
steps in `ubuntu-build`:
1. **Clone bench (sparse, ~800 MB of ~12 GB total)**
`git clone --depth 1 --filter=blob:none --sparse
https://github.com/Z3Prover/bench bench` then `sparse-checkout set
scripts inputs/issues`.
2. **Run issue-oracle smoke test (~2 min)**
```yaml
continue-on-error: true
run: |
timeout 90 python bench/scripts/issues_check_oracle.py \
--z3 build-dist/z3 \
--all bench/inputs/issues \
--max 200 --timeout 5 --wallclock 60 \
--jobs 0 --quiet \
--json-report issue-oracle-report.json
```
The JSON report is then uploaded as a workflow artifact
(`issue-oracle-report`, 7-day retention) for inspection.
### Wall-clock bounds (defense in depth)
| Bound | Where | Purpose |
|---|---|---|
| `--max 200` | issues_check_oracle CLI | walk only first 200 of ~2,700
`iss-*` dirs (alphabetic; stable across nightlies) |
| `--timeout 5` | issues_check_oracle CLI | per-file z3 cap |
| `--wallclock 60` | issues_check_oracle CLI | hard global cap inside
the script |
| `timeout 90` | shell wrapper | belt-and-braces backstop, leaves 30 s
headroom for the script to flush its JSON report before SIGTERM |
| `continue-on-error: true` | step gate | absorbs every failure mode
(missing z3, sparse-clone failure, outer timeout firing, etc.) so the
smoke test can **never** red the nightly build |
### Scope
Only `ubuntu-build` and only one place in `nightly.yml`. The push/PR
lanes (`ci.yml`, `Windows.yml`) and the other scheduled/dispatch lanes
(`coverage.yml`, `memory-safety.yml`, `nightly-validation.yml`,
`release.yml`, `wip.yml`, `daily-test-improver`) are intentionally left
untouched so this gate runs exactly once per night.
## Local verification
On Mac (16 cores, capped to 8 jobs by `--jobs 0` resolving to `min(jobs,
cores)`):
```
[issues_check_oracle] 368 file-check(s) | timeout=5s | wallclock=60s
=== summary ===
total: 368 ok: 286 DIFF: 4 (per-file timeouts) skipped: 78
elapsed: 8.3s / 60s
exit code: 0
```
GHA Ubuntu (4 cores → 4 jobs) extrapolation: ~17 s typical, well under
all wall-clock caps.
### Adversarial cases (all leave the workflow green via step-level
`continue-on-error: true`)
| Failure mode | Result |
|---|---|
| z3 binary missing | each per-file run records `exec-error`, script
summary-exits 0 → green |
| Sparse clone fails (previous step's continue-on-error absorbs it) |
oracle finds no `bench/` → script `sys.exit(1)` → step's
continue-on-error absorbs → green |
| Wallclock fires | script writes report with `wallclock_hit: true`,
exits 0 → green |
| Outer `timeout 90` fires | SIGTERM → bash exits 124 → step's
continue-on-error absorbs → green |
## Companion bench-repo PR
The data side of this (per-bench sidecar schema, `bug-K.json` +
`<stem>.expected.out`, oracle rewrite) lands in `Z3Prover/bench` as PR
[#2503](https://github.com/Z3Prover/bench/pull/2503). The nightly step
here depends on that PR's `scripts/issues_check_oracle.py` and the
migrated corpus. Both PRs should be merged together; bench can also
merge first (the script handles a missing corpus gracefully).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+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>
https://github.com/Z3Prover/z3/pull/9405 made the trace report
used_enodes incorrectly, since the previous code relied on
update_max_generation to maintain the relevant data structure. This
should fix it.
Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
Cleans up dead code left by the "remove side definitions" refactoring
(a0a3047).
- **`smt_model_checker.cpp`** — Remove `defined_names dn(m)` variable
that was declared but never used
- **`smt_model_checker.h`** — Drop the now-unnecessary `#include
"ast/normal_forms/defined_names.h"`
- **`fingerprints.cpp`** — Collapse redundant tail in
`fingerprint_set::contains`:
```cpp
// Before
if (m_set.contains(d))
return true;
return false;
// After
return m_set.contains(d);
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Z3's -T measures wall clock time, whereas `ulimit -t` measures CPU time.
Currently, an expired ulimit timeout crashes Z3 without printing
statistics; this patch makes it react cleanly (just as if it has
encountered a regular timeout) to SIGXCPU, the signal that ulimit sends
before sending SIGKILL.
Two fixes for mbp_dt_tg::apply() when encountering an accessor whose
argument has a different constructor in the model:
1. Don't call rm_accessor (which would assert a contradictory
recognizer, making the formula false). This prevents the original bug
where QEL returned 'false' for satisfiable formulas.
2. Branch on the model-assigned constructor for the accessor's argument.
The correct output should include the literal introduced in (2).
However, this fix does not produce it. Spacer is sound with this
over-approximation, as long as the counter example does not depend on
value of mismatched accessors (e.g. (tl nil)).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.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>
Bumps [github/gh-aw-actions](https://github.com/github/gh-aw-actions)
from 0.76.1 to 0.77.0.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/github/gh-aw-actions/releases">github/gh-aw-actions's
releases</a>.</em></p>
<blockquote>
<h2>v0.77.0</h2>
<p>Sync of actions from <a
href="https://github.com/github/gh-aw">gh-aw</a> at
<code>v0.77.0</code>.</p>
</blockquote>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="b11be78086"><code>b11be78</code></a>
chore: sync actions from gh-aw@v0.77.0 (<a
href="https://redirect.github.com/github/gh-aw-actions/issues/122">#122</a>)</li>
<li>See full diff in <a
href="https://github.com/github/gh-aw-actions/compare/v0.76.1...v0.77.0">compare
view</a></li>
</ul>
</details>
<br />
[](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores)
Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.
[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)
---
<details>
<summary>Dependabot commands and options</summary>
<br />
You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)
</details>
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
- only the internalizer performs closure conversion
- theory_array treats propagation of lambdas similar to stores
- ho_matcher treats top-level flex patterns as first-order
- pattern-inference fix to handle quantifiers (lambdas) in patterns that are computed
A `root-obj`-driven unsat case was exiting with a leaked `mpz_manager`
allocation even though solver output was correct. The leak came from
temporary rational bounds created during algebraic-number comparison and
not released before shutdown.
- **Root cause**
- `algebraic_numbers::compare_core()` materialized interval bounds as
raw `mpq` temporaries.
- Those temporaries could allocate backing `mpz` storage, but their
lifetime was not tied to the manager, so the allocator retained leaked
cells at process exit.
- **Change**
- Replace the raw `mpq` temporaries with `scoped_mpq` in
`/src/math/polynomial/algebraic_numbers.cpp`.
- This keeps the comparison logic unchanged while making temporary bound
conversion use RAII-managed cleanup.
- **Effect**
- `root-obj` comparisons no longer leave `mpz_manager` allocations
behind.
- Solver behavior is unchanged; the fix is limited to temporary numeral
lifetime management.
```c++
- mpq l_a, u_a, l_b, u_b;
+ scoped_mpq l_a(qm()), u_a(qm()), l_b(qm()), u_b(qm());
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This change wires SMT-LIB Hilbert choice parsing to a concrete
array-theory operator and ensures both array backends enforce the
expected semantic axiom. Previously, `(choice ((x T)) phi)` parsed as
NYI and had no solver-side instantiation path.
- **Parser: lower `choice_k` into array `OP_CHOICE`**
- `pop_quant_frame(choice_k)` now builds `(choice p)` instead of
throwing.
- Added parser include/use of array utilities to construct the term
directly from the generated lambda predicate.
- **Array decl plugin: add `OP_CHOICE` typing + surface syntax**
- Added declaration support for `choice` with signature:
- `(Array T Bool) -> T` (encoded as `('a -> Bool) -> 'a` in HO view).
- Added recognizer/util helpers (`is_choice`, `mk_choice`) and exposed
`"choice"` in op names.
- **SMT array theory (`theory_array_full`): instantiate choice axiom**
- Added instantiation for each encountered `choice(p)`:
- `forall x . p(x) => p(choice(p))`
- Integrated into internalization/relevancy paths and statistics.
- **SAT/SMT array backend (`sat/smt/array_*`): instantiate choice
axiom**
- Added new axiom record kind for choice, internalization hook,
assertion routine, and diagnostics/stat tracking.
- Uses the same quantified implication schema as above.
- **Regression coverage**
- Extended SMT2 parser regression with an HO `choice` example to ensure
parser/eval pipeline accepts and processes choice terms.
Example of the now-supported input:
```smt2
(set-logic HO_ALL)
(declare-sort U 0)
(declare-fun P () (-> U Bool))
(assert (exists ((x U)) (P x)))
(assert (= witness (choice ((x U)) (P x))))
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
