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>
This updates the compare-stats anomaly reporter to retrieve benchmark
data from `http://mtzguido.tplinkdns.com:8081/z3/` instead of the old
`compare_stats.html` endpoint. The workflow prompt and generated lock
file now consistently reference the root benchmark stats URL.
- **Workflow source**
- Repoint the benchmark source URL from `.../compare_stats.html` to
`.../z3/`
- Update prompt text to describe the source as benchmark statistics
rather than a specific HTML file
- Rename the temporary fetched artifact from `compare_stats.html` to
`benchmark_stats.html` for consistency
- **Generated workflow**
- Regenerate `compare-stats-anomaly-reporter.lock.yml` so the compiled
workflow matches the markdown source
- Refresh the embedded workflow description and prompt payload to
reference the new endpoint
- **Report output**
- Update the discussion template’s source link to point at the root
benchmark stats page
```md
Source URL:
`http://mtzguido.tplinkdns.com:8081/z3/`
curl -fsSL --max-time 60 "http://mtzguido.tplinkdns.com:8081/z3/" \
-o /tmp/gh-aw/agent/benchmark_stats.html
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This updates a formatting regression introduced in the `pop_app_frame`
non-`expr_head` path, where block indentation made control flow harder
to read. The patch is whitespace-only and keeps parser behavior
unchanged.
- **What changed**
- Reindented the `else` body in
`src/parsers/smt2/smt2parser.cpp::pop_app_frame` so nested `if/else`
structure is visually unambiguous.
- Removed trailing spaces on the `m_ctx.mk_app(symbol("select"), ...)`
lines in the same block.
- **Scope**
- No control-flow, data-flow, or API changes.
- No changes outside `pop_app_frame`.
```cpp
// Before
else {
local l;
if (m_env.find(fr->m_f, l)) {
...
}
else {
...
}
}
// After
else {
local l;
if (m_env.find(fr->m_f, l)) {
...
}
else {
...
}
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This adds an agentic workflow that analyzes `compare_stats.html` over a
rolling 30-hour window and publishes a GitHub Discussion summarizing
bugs, crashes, and anomalies. It explicitly captures unknown-outlier
patterns where a benchmark is `unknown` while peers in the same set are
mostly `sat`/`unsat`/`timeout`.
- **Workflow added**
- Introduces `.github/workflows/compare-stats-anomaly-reporter.md` (plus
compiled `.lock.yml`).
- Supports `workflow_dispatch` and scheduled execution.
- Uses safe discussion output with auto-close of older reports for the
same stream.
- **Data acquisition + robustness**
- Fetches `http://mtzguido.tplinkdns.com:8081/z3/compare_stats.html`
with `curl` and `wget` fallback.
- Adds integrity checks (non-empty HTML/table presence) and explicit
incomplete-report behavior on fetch/parse failures.
- **30-hour analysis semantics**
- Filters rows by timestamp candidates (`time`, `timestamp`, `date`,
`run`, etc.) using UTC.
- Falls back to full-table analysis when timestamps are unavailable, and
marks the report accordingly.
- **Classification logic**
- Detects bug/crash signals from status/details (`crash`, `segfault`,
`assert`, `abort`, `exception`, `error`, `failed`, `bug`).
- Detects:
- unknown-outlier anomalies (thresholded minority `unknown` in otherwise
decisive SAT-family outcomes),
- status divergences (conflicting non-timeout outcomes for same
benchmark),
- repeated hard-failure anomalies.
- **Discussion output shape**
- Produces a compact report with executive counts, bug/crash table,
anomaly subsections, and raw extraction summary/limitations.
```yaml
safe-outputs:
create-discussion:
title-prefix: "[Compare Stats] "
category: "agentic workflows"
close-older-discussions: true
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
So far, `algebraic_numbers compare_core ` handles an edge case
incorrectly:
- If the two compared numbers (`a`, `b`) are different,
- the intervals still overlap after refinements, and
- both a and b are a root of the second polynomial (`cell_b->m_p`), e.g.
they are the first and second root
then the method would return `sign_zero` (i.e. "equal"). This behavior
can be replicated with the provided test case (before the fix). This
requires `algebraic.factor=false`, though i first encountered it during
solver runs on QF_NRA instances with the default
`algebraic.factor=true`, which apparently means that the polynomials for
anums are still not always factored.
The fix is to compare the interval bounds of b to a and vice versa. Then
the Sturm-Tarski check is only run if `a` and `b` both lie in the
intersection of the intervals, because only then is it guaranteed to be
correct.
