The Nightly release occasionally exposed a mismatch between the commit
shown on the release page and the downloaded “Source code” archive. Root
cause was non-deterministic `Nightly` tag/release state during publish.
- **Deterministic Nightly tag lifecycle**
- Serialize Nightly workflow runs with a dedicated concurrency group to
prevent overlapping tag/release mutations.
- Replace best-effort cleanup with explicit release-exists checks and
failure-on-cleanup-error behavior.
- Remove orphan `Nightly` tags even when no release exists.
- **Pin release to the exact workflow commit**
- Force-update `Nightly` to `${{ github.sha }}` and push it before
release creation.
- Verify remote tag SHA (including annotated-tag dereference shape)
matches `${{ github.sha }}`.
- Create release with `--verify-tag` so source archives are generated
from the validated tag, not an implicit/stale target.
- **Workflow behavior change (deploy section)**
```yaml
concurrency:
group: nightly-release
cancel-in-progress: false
```
```bash
git tag -f Nightly "${{ github.sha }}"
git push --force origin refs/tags/Nightly
gh release create Nightly --verify-tag ...
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`std::format` (C++20 `<format>`) pulls in `std::to_chars` for
floating-point formatting, which is only available on macOS 13.3+. The
Mac x64 CI job was targeting macOS 13.0, causing build errors in
`src/ast/`.
## Changes
Updated `nightly.yml` to raise the macOS deployment target for the x64
build:
- **`MACOSX_DEPLOYMENT_TARGET`**: `"13.0"` → `"13.3"` in the
`mac-build-x64` job
- **`--os` flag**: `osx-13.0` → `osx-13.3` in the `mk_unix_dist.py`
invocation
This matches the existing `mac-build-arm64` job, which already targets
macOS 13.3, and allows `std::format` to be used freely in `src/ast/`
without workarounds.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The Nightly **Mac ARM64 Build** job fails on current Xcode/libc++
because `std::format` pulls floating-point formatting paths that require
`std::to_chars` availability from macOS 13.3+. The job was still
compiling with a 13.0 deployment target.
- **Root cause**
- ARM64 nightly job used:
- `MACOSX_DEPLOYMENT_TARGET=13.0`
- `mk_unix_dist.py --os=osx-13.0`
- This mismatched the effective libc++ requirements in the runner
toolchain.
- **Workflow change**
- Updated only `.github/workflows/nightly.yml` for `mac-build-arm64`:
- `MACOSX_DEPLOYMENT_TARGET: "13.0" -> "13.3"`
- `--os=osx-13.0 -> --os=osx-13.3`
- **Resulting behavior**
- ARM64 nightly build target now aligns with the minimum OS level
required by the formatting code paths used by current compilation units.
```yaml
# .github/workflows/nightly.yml (mac-build-arm64)
env:
MACOSX_DEPLOYMENT_TARGET: "13.3"
- name: Build
run: python scripts/mk_unix_dist.py --dotnet-key=$GITHUB_WORKSPACE/resources/z3.snk --arch=arm64 --os=osx-13.3
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Wheels started inheriting `macosx_15_0` tags because macOS jobs run on
newer runners and no deployment target was pinned. That blocks wheel
installation on macOS 13/14 hosts and forces source builds.
- **macOS deployment target pinning**
- Added `MACOSX_DEPLOYMENT_TARGET: "13.0"` to both macOS build jobs
(`x64`, `arm64`) in:
- `.github/workflows/release.yml`
- `.github/workflows/nightly.yml`
- **Stable macOS artifact OS metadata**
- Updated macOS `mk_unix_dist.py` invocations to pass `--os=osx-13.0` in
both workflows, so artifact metadata stays aligned with the intended
minimum macOS compatibility used for Python wheel tagging.
```yaml
mac-build-x64:
runs-on: macos-15
env:
MACOSX_DEPLOYMENT_TARGET: "13.0"
steps:
- name: Build
run: python scripts/mk_unix_dist.py --dotnet-key=$GITHUB_WORKSPACE/resources/z3.snk --arch=x64 --os=osx-13.0
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Nightly and release workflows were still building Pyodide wheels inline,
despite Pyodide now being handled by a dedicated workflow. This change
removes duplicate Pyodide build work from those pipelines and aligns
artifact assembly with the new split.
- **Workflow graph cleanup**
- Removed the `pyodide-python` job from:
- `.github/workflows/nightly.yml`
- `.github/workflows/release.yml`
- **Packaging dependency updates**
- Updated `python-package.needs` in both workflows to drop
`pyodide-python`, so packaging no longer waits on an in-workflow Pyodide
build.
- **Artifact collection updates**
- Removed `Download Pyodide Build` steps from both `python-package`
jobs, eliminating references to `PyodidePythonBuild`.
```yaml
python-package:
needs:
- mac-build-x64
- mac-build-arm64
- windows-build-x64
- windows-build-x86
- windows-build-arm64
- manylinux-python-amd64
- manylinux-python-arm64
- manylinux-python-riscv64
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The Pyodide `build` job was passing legacy Emscripten exception flags
that conflict with the wasm-exception ABI now used by the Python
packaging configuration. This caused the wheel build to fail before
compilation completed.
- **Align Pyodide workflow flags**
- Remove per-workflow `CFLAGS` / `CXXFLAGS` / `LDFLAGS` overrides from
the Pyodide build step.
- Let the build inherit the canonical wasm-exception / longjmp / bigint
flags from `src/api/python/pyproject.toml`.
- **Apply the fix consistently**
- Update the standalone Pyodide workflow.
- Update the matching Pyodide build steps in `nightly.yml` and
`release.yml` to avoid the same regression in scheduled and release
builds.
- **Why this fixes the failure**
- The broken path mixed JS-exception and wasm-exception settings:
```yaml
CFLAGS: "-fexceptions -s DISABLE_EXCEPTION_CATCHING=0 -g2"
CXXFLAGS: "-fexceptions -s DISABLE_EXCEPTION_CATCHING=0"
```
- The updated workflows now invoke:
```yaml
~/env/bin/pyodide build --exports whole_archive
```
and rely on the packaging config’s wasm-exception settings instead.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Implemented the largest cube heuristic from Bromberger and Weidenbach's
paper on cubes. Also fixes an overflow bug in mzp.
Use vswhere to find the visual studio version on windows in the build's ymls.
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Co-authored-by: Copilot <223556219+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>
This updates the release and nightly pipelines so the Pyodide wheel is
built alongside the existing Python wheels and carried through the
normal publication flow. As a result, Pyodide wheels are included in
nightly assets and in release-time Python package publishing without
introducing a separate publishing path.
- **Pyodide build in release/nightly**
- Added a `pyodide-python` job to both `release.yml` and `nightly.yml`
- Reused the existing Pyodide build flow: install
`pyodide-build`/`pyodide-cli`, provision the matching Emscripten
toolchain, build the wheel, and run `z3test.py` against the built
artifact
- **Artifact integration**
- Upload the built wheel as a dedicated workflow artifact:
`PyodidePythonBuild`
- Extend the existing `python-package` aggregation job in both workflows
to depend on and download that artifact
- **Publication path**
- No new publish logic was added
- The existing downstream steps already publish everything collected in
`src/api/python/dist`, so the Pyodide wheel now flows into:
- nightly GitHub release assets
- release GitHub assets
- release-time PyPI publishing when enabled
```yaml
pyodide-python:
name: "Python bindings (Pyodide)"
...
- name: Upload artifact
uses: actions/upload-artifact@v7.0.1
with:
name: PyodidePythonBuild
path: src/api/python/dist/*.whl
python-package:
needs: [..., pyodide-python]
...
- name: Download Pyodide Build
uses: actions/download-artifact@v8.0.1
with:
name: PyodidePythonBuild
path: artifacts
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Replace hardcoded -j3 with -j$(nproc) in ci.yml, nightly.yml, and
release.yml to utilize all available cores on GitHub Actions runners.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
