mirror of
https://github.com/Z3Prover/z3
synced 2026-06-05 08:30:50 +00:00
400fe313d9
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> |
||
|---|---|---|
| .. | ||
| shared | ||
| a3-python.lock.yml | ||
| a3-python.md | ||
| academic-citation-tracker.lock.yml | ||
| academic-citation-tracker.md | ||
| agentics-maintenance.yml | ||
| android-build.yml | ||
| api-coherence-checker.lock.yml | ||
| api-coherence-checker.md | ||
| build-warning-fixer.lock.yml | ||
| build-warning-fixer.md | ||
| build-z3-cache.yml | ||
| ci.yml | ||
| code-conventions-analyzer.lock.yml | ||
| code-conventions-analyzer.md | ||
| code-simplifier.lock.yml | ||
| code-simplifier.md | ||
| compare-stats-anomaly-reporter.lock.yml | ||
| compare-stats-anomaly-reporter.md | ||
| copilot-setup-steps.yml | ||
| coverage.yml | ||
| cross-build.yml | ||
| csa-analysis.lock.yml | ||
| csa-analysis.md | ||
| docs.yml | ||
| issue-backlog-processor.lock.yml | ||
| issue-backlog-processor.md | ||
| mark-prs-ready-for-review.yml | ||
| memory-safety-report.lock.yml | ||
| memory-safety-report.md | ||
| memory-safety.yml | ||
| msvc-static-build-clang-cl.yml | ||
| msvc-static-build.yml | ||
| nightly-validation.yml | ||
| nightly.yml | ||
| nuget-build.yml | ||
| ocaml.yaml | ||
| ostrich-benchmark.lock.yml | ||
| ostrich-benchmark.md | ||
| pyodide.yml | ||
| qf-s-benchmark.lock.yml | ||
| qf-s-benchmark.md | ||
| release-notes-updater.lock.yml | ||
| release-notes-updater.md | ||
| release.yml | ||
| smtlib-benchmark-finder.lock.yml | ||
| smtlib-benchmark-finder.md | ||
| specbot-crash-analyzer.lock.yml | ||
| specbot-crash-analyzer.md | ||
| tactic-to-simplifier.lock.yml | ||
| tactic-to-simplifier.md | ||
| tptp-benchmark.lock.yml | ||
| tptp-benchmark.md | ||
| wasm-release.yml | ||
| wasm.yml | ||
| Windows.yml | ||
| wip.yml | ||
| workflow-suggestion-agent.lock.yml | ||
| workflow-suggestion-agent.md | ||
| zipt-code-reviewer.lock.yml | ||
| zipt-code-reviewer.md | ||