- Add makeCCSinglethreadWrapper() in make-cc-wrapper.ts that generates
synchronous async wrappers using EM_ASM instead of threads +
MAIN_THREAD_ASYNC_EM_ASM. Refactor shared error-handler code into a
SHARED_ERROR_HANDLERS constant used by both variants.
- Add build-wasm-singlethread.ts: new build script that compiles a
separate libz3.a (in build-singlethread/) and z3-built-singlethread.js
without -pthread / USE_PTHREADS=1. Uses -DSINGLE_THREAD -DPOLLING_TIMER
and ALLOW_MEMORY_GROWTH instead of a fixed 2 GB SharedArrayBuffer.
- Add src/node-singlethread.ts and src/browser-singlethread.ts entry
points. Browser variant reads initZ3SingleThread from global scope
(load z3-built-singlethread.js via importScripts in a Web Worker).
- Add tests for both new entry points (node-singlethread.test.ts,
browser-singlethread.test.ts).
- Update package.json: add build:wasm:singlethread script; add exports
map so users can do import { init } from 'z3-solver/singlethread'.
- Update PUBLISHED_README.md: document the single-threaded variant,
explain when to use it (no COOP/COEP headers), and provide a Web
Worker usage example.
- Update wasm.yml CI: add check-singlethread parallel job.
- Update wasm-release.yml: build single-threaded artifact before publish.
- Guard scoped_timer.cpp with #if defined(SINGLE_THREAD) &&
!defined(__EMSCRIPTEN_PTHREADS__) so that thread-based timer creation
is skipped in single-threaded Emscripten builds (POLLING_TIMER covers
the primary cancel_eh<reslimit> use-case).
Multiple agentic workflows were failing at runtime with
`MODULE_NOT_FOUND` for `merge_awf_model_multipliers.cjs` under
`${RUNNER_TEMP}/gh-aw/actions`. The lock workflows had stale generated
runtime steps that no longer matched the current `gh-aw` actions bundle.
- **Root cause**
- Generated `.lock.yml` workflows referenced a removed script:
- `node "${RUNNER_TEMP}/gh-aw/actions/merge_awf_model_multipliers.cjs"`
- **Change**
- Recompiled all agentic workflow sources (`.github/workflows/*.md`)
with current `gh aw` tooling.
- Checked in regenerated lock artifacts:
- `.github/workflows/*.lock.yml`
- `.github/aw/actions-lock.json`
- Result: stale `merge_awf_model_multipliers.cjs` invocations were
eliminated from generated workflows.
- **Representative diff shape**
```yaml
# removed from generated lock workflows
- GH_AW_MODEL_MULTIPLIERS_PATH="/tmp/gh-aw/model_multipliers.json" \
node "${RUNNER_TEMP}/gh-aw/actions/merge_awf_model_multipliers.cjs"
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
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>
## Problem
Maximizing/minimizing under a **strict** inequality has a delta-rational
optimum. For
```smt2
(declare-const r Real)
(assert (< r 1))
(maximize r)
(check-sat)
(get-objectives)
```
the optimum is the supremum `1 - epsilon`, but z3 reported `r = 0`.
The same defect makes shared-symbol objectives report a value matching
**neither the model nor the true optimum** (issue #10028 follow-up).
Minimal reproducer — a 6-mark Golomb ruler (a `>32`-arg `distinct`, so
the objective is coupled to EUF) with a strict real objective `obj >
x5`, whose true optimum is `17 + epsilon`:
| case | before | after |
|---|---|---|
| `maximize r`, `r < 1` | `0` ❌ | `1 - epsilon` ✅ |
| `minimize r`, `r > 1` | `0` ❌ | `1 + epsilon` ✅ |
| Golomb `minimize obj`, `obj > x5` | `35/2` / `7+eps` ❌ | `17 +
epsilon` ✅ |
## Root cause
`check_bound` validates the LP hint by asserting `objective >= optimum`.
For a supremum `1 - epsilon` this is a **lower** bound whose value
carries a **negative** infinitesimal `(1, -1)`.
No `lconstraint_kind` can express that. The kind->infinitesimal map only
yields the *matching-sign* cases — `GT` -> lower `(r, +1)`, `LT` ->
upper `(r, -1)` — or zero (`GE`/`LE`). The opposite-sign lower bound
`(r, -1)` (i.e. `r >= r0 - delta`) is a *relaxation* that no strict
inequality produces. `opt_solver::mk_ge` therefore projected the
`-epsilon` away, turning `r >= 1 - epsilon` into the over-strong,
unsatisfiable `r >= 1`; validation failed and the strictly smaller
current model value was reported instead.
## Fix — carry the infinitesimal faithfully through the bound pipeline
- **`lp_api::bound`** gains an `eps` component so `get_value` returns
the true delta value (no spurious rational fixed-variable equality is
propagated to EUF).
- **`lar_base_constraint`** stores its right-hand side as a
delta-rational `impq` pair; `rhs()` returns the rational component,
`bound_eps()` the infinitesimal one.
- **`lar_solver`** bound activation/update threads the whole `impq`
bound, so a lower bound `(r, -1)` can be asserted. `constraint_holds`
accounts for it using the **same** strict-bounds delta that flattens the
model, computed **once per model**.
- **`theory_lra::mk_ge`** builds a *fresh* predicate for the `(r, -1)`
lower bound (to avoid colliding with an already-internalized `v >= r`
literal) and attaches `eps = -1`. **`opt_solver::mk_ge`** passes the
unprojected value to `theory_lra` / `theory_mi_arith` /
`theory_inf_arith` (whose bounds are already `inf_rational`).
The pair machinery is what makes the supremum both representable
(optimum `1 - epsilon`) and validatable; the reported witness model
remains the flattened rational (`find_delta_for_strict_bounds`),
consistent with the existing epsilon semantics.
## Validation
- Strict optima correct: `1-eps`, `1+eps`, bounded `2<r<5 -> 5-eps`, and
lex/box variants.
- Integer optima and the #10028 shared-symbol cases unchanged (Golomb
n=6/7/8 -> 17/25/34, consistent with the model).
- Unit tests **92/92** (release); no new debug-suite failures.
- Opt regression corpus (73 files, `model_validate=true`)
**byte-identical** to baseline.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.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>
[//]: # (dependabot-start)
⚠️ **Dependabot is rebasing this PR** ⚠️
Rebasing might not happen immediately, so don't worry if this takes some
time.
Note: if you make any changes to this PR yourself, they will take
precedence over the rebase.
---
[//]: # (dependabot-end)
Bumps [actions/cache](https://github.com/actions/cache) from 6.0.0 to
6.1.0.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/releases">actions/cache's
releases</a>.</em></p>
<blockquote>
<h2>v6.1.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Bump <code>@actions/cache</code> to v6.1.0 - handle read-only cache
access by <a
href="https://github.com/jasongin"><code>@jasongin</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1768">actions/cache#1768</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v6...v6.1.0">https://github.com/actions/cache/compare/v6...v6.1.0</a></p>
</blockquote>
</details>
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/blob/main/RELEASES.md">actions/cache's
changelog</a>.</em></p>
<blockquote>
<h3>6.1.0</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v6.1.0 to pick up <a
href="https://redirect.github.com/actions/toolkit/pull/2435">actions/toolkit#2435
Handle cache write error due to read-only token</a></li>
<li>Switch redundant "Cache save failed" warning to debug log
in save-only</li>
</ul>
</blockquote>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="55cc834586"><code>55cc834</code></a>
Merge pull request <a
href="https://redirect.github.com/actions/cache/issues/1768">#1768</a>
from jasongin/readonly-cache</li>
<li><a
href="d8cd72f230"><code>d8cd72f</code></a>
Bump <code>@actions/cache</code> to v6.1.0 - handle cache write error
due to RO token</li>
<li>See full diff in <a
href="https://github.com/actions/cache/compare/v6.0.0...v6.1.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>
Bumps [actions/cache/save](https://github.com/actions/cache) from 5.0.5
to 6.1.0.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/releases">actions/cache/save's
releases</a>.</em></p>
<blockquote>
<h2>v6.1.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Bump <code>@actions/cache</code> to v6.1.0 - handle read-only cache
access by <a
href="https://github.com/jasongin"><code>@jasongin</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1768">actions/cache#1768</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v6...v6.1.0">https://github.com/actions/cache/compare/v6...v6.1.0</a></p>
<h2>v6.0.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Update packages, migrate to ESM by <a
href="https://github.com/Samirat"><code>@Samirat</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1760">actions/cache#1760</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v5...v6.0.0">https://github.com/actions/cache/compare/v5...v6.0.0</a></p>
<h2>v5.1.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Bump <code>@actions/cache</code> to v5.1.0 - handle read-only cache
access by <a
href="https://github.com/jasongin"><code>@jasongin</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1775">actions/cache#1775</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v5...v5.1.0">https://github.com/actions/cache/compare/v5...v5.1.0</a></p>
</blockquote>
</details>
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/blob/main/RELEASES.md">actions/cache/save's
changelog</a>.</em></p>
<blockquote>
<h1>Releases</h1>
<h2>How to prepare a release</h2>
<blockquote>
<p>[!NOTE]
Relevant for maintainers with write access only.</p>
</blockquote>
<ol>
<li>Switch to a new branch from <code>main</code>.</li>
<li>Run <code>npm test</code> to ensure all tests are passing.</li>
<li>Update the version in <a
href="https://github.com/actions/cache/blob/main/package.json"><code>https://github.com/actions/cache/blob/main/package.json</code></a>.</li>
<li>Run <code>npm run build</code> to update the compiled files.</li>
<li>Update this <a
href="https://github.com/actions/cache/blob/main/RELEASES.md"><code>https://github.com/actions/cache/blob/main/RELEASES.md</code></a>
with the new version and changes in the <code>## Changelog</code>
section.</li>
<li>Run <code>licensed cache</code> to update the license report.</li>
<li>Run <code>licensed status</code> and resolve any warnings by
updating the <a
href="https://github.com/actions/cache/blob/main/.licensed.yml"><code>https://github.com/actions/cache/blob/main/.licensed.yml</code></a>
file with the exceptions.</li>
<li>Commit your changes and push your branch upstream.</li>
<li>Open a pull request against <code>main</code> and get it reviewed
and merged.</li>
<li>Draft a new release <a
href="https://github.com/actions/cache/releases">https://github.com/actions/cache/releases</a>
use the same version number used in <code>package.json</code>
<ol>
<li>Create a new tag with the version number.</li>
<li>Auto generate release notes and update them to match the changes you
made in <code>RELEASES.md</code>.</li>
<li>Toggle the set as the latest release option.</li>
<li>Publish the release.</li>
</ol>
</li>
<li>Navigate to <a
href="https://github.com/actions/cache/actions/workflows/release-new-action-version.yml">https://github.com/actions/cache/actions/workflows/release-new-action-version.yml</a>
<ol>
<li>There should be a workflow run queued with the same version
number.</li>
<li>Approve the run to publish the new version and update the major tags
for this action.</li>
</ol>
</li>
</ol>
<h2>Changelog</h2>
<h3>6.1.0</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v6.1.0 to pick up <a
href="https://redirect.github.com/actions/toolkit/pull/2435">actions/toolkit#2435
Handle cache write error due to read-only token</a></li>
<li>Switch redundant "Cache save failed" warning to debug log
in save-only</li>
</ul>
<h3>6.0.0</h3>
<ul>
<li>Updated <code>@actions/cache</code> to ^6.0.1,
<code>@actions/core</code> to ^3.0.1, <code>@actions/exec</code> to
^3.0.0, <code>@actions/io</code> to ^3.0.2</li>
<li>Migrated to ESM module system</li>
<li>Upgraded Jest to v30 and test infrastructure to be ESM
compatible</li>
</ul>
<h3>5.0.4</h3>
<ul>
<li>Bump <code>minimatch</code> to v3.1.5 (fixes ReDoS via globstar
patterns)</li>
<li>Bump <code>undici</code> to v6.24.1 (WebSocket decompression bomb
protection, header validation fixes)</li>
<li>Bump <code>fast-xml-parser</code> to v5.5.6</li>
</ul>
<h3>5.0.3</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v5.0.5 (Resolves: <a
href="https://github.com/actions/cache/security/dependabot/33">https://github.com/actions/cache/security/dependabot/33</a>)</li>
<li>Bump <code>@actions/core</code> to v2.0.3</li>
</ul>
<h3>5.0.2</h3>
<!-- raw HTML omitted -->
</blockquote>
<p>... (truncated)</p>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="55cc834586"><code>55cc834</code></a>
Merge pull request <a
href="https://redirect.github.com/actions/cache/issues/1768">#1768</a>
from jasongin/readonly-cache</li>
<li><a
href="d8cd72f230"><code>d8cd72f</code></a>
Bump <code>@actions/cache</code> to v6.1.0 - handle cache write error
due to RO token</li>
<li><a
href="2c8a9bd745"><code>2c8a9bd</code></a>
Merge pull request <a
href="https://redirect.github.com/actions/cache/issues/1760">#1760</a>
from actions/samirat/esm_migration_and_package_update</li>
<li><a
href="e9b91fdc3f"><code>e9b91fd</code></a>
Prettier fixes</li>
<li><a
href="e4884b8ff7"><code>e4884b8</code></a>
Rebuild dist</li>
<li><a
href="10baf0191a"><code>10baf01</code></a>
Fixed licenses</li>
<li><a
href="e39b386c90"><code>e39b386</code></a>
Fix test mock return order</li>
<li><a
href="b692820337"><code>b692820</code></a>
PR feedback</li>
<li><a
href="60749128a4"><code>6074912</code></a>
Rebuild dist bundles as ESM to match type:module</li>
<li><a
href="5a912e8b4a"><code>5a912e8</code></a>
Fix lint and jest issues</li>
<li>Additional commits viewable in <a
href="27d5ce7f10...55cc834586">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>
The "Ubuntu with OCaml on z3-static" CI job intermittently fails with
`Fatal error: exception End_of_file` from the OCaml bytecode linker when
compiling `ml_example_static.byte`.
## Root cause
`ocamlfind install z3-static build/api/ml/* build/libz3-static.a`
auto-recognizes `dllz3ml-static.so` (starts with `dll`) as a C stub and
copies it to `stublibs`, but without an explicit `-dll` flag it **does
not update `ld.conf`**—confirmed by the CI warning:
```
ocamlfind: [WARNING] You have installed DLLs but the directory .../stublibs is not mentioned in ld.conf
```
`ocamlc` searches `ld.conf` for stub DLLs at bytecode link time; the
missing entry causes `End_of_file`. The non-static job is unaffected
because it passes `-dll build/libz3.*` explicitly, which triggers the
`ld.conf` update as a side-effect.
## Fix
After `ocamlfind install`, append the `stublibs` path to `ld.conf` if
absent:
```bash
STUBLIBS="$(dirname "$(ocamlfind printconf destdir)")/stublibs"
LDCONF="$(ocamlfind printconf ldconf)"
if [ -d "$STUBLIBS" ] && ! grep -qF "$STUBLIBS" "$LDCONF" 2>/dev/null; then
echo "$STUBLIBS" >> "$LDCONF"
fi
```
Idempotent; uses `ocamlfind printconf` to avoid hardcoded paths.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
Bumps [actions/cache/restore](https://github.com/actions/cache) from
5.0.5 to 6.0.0.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/releases">actions/cache/restore's
releases</a>.</em></p>
<blockquote>
<h2>v6.0.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Update packages, migrate to ESM by <a
href="https://github.com/Samirat"><code>@Samirat</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1760">actions/cache#1760</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v5...v6.0.0">https://github.com/actions/cache/compare/v5...v6.0.0</a></p>
</blockquote>
</details>
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/blob/main/RELEASES.md">actions/cache/restore's
changelog</a>.</em></p>
<blockquote>
<h1>Releases</h1>
<h2>How to prepare a release</h2>
<blockquote>
<p>[!NOTE]
Relevant for maintainers with write access only.</p>
</blockquote>
<ol>
<li>Switch to a new branch from <code>main</code>.</li>
<li>Run <code>npm test</code> to ensure all tests are passing.</li>
<li>Update the version in <a
href="https://github.com/actions/cache/blob/main/package.json"><code>https://github.com/actions/cache/blob/main/package.json</code></a>.</li>
<li>Run <code>npm run build</code> to update the compiled files.</li>
<li>Update this <a
href="https://github.com/actions/cache/blob/main/RELEASES.md"><code>https://github.com/actions/cache/blob/main/RELEASES.md</code></a>
with the new version and changes in the <code>## Changelog</code>
section.</li>
<li>Run <code>licensed cache</code> to update the license report.</li>
<li>Run <code>licensed status</code> and resolve any warnings by
updating the <a
href="https://github.com/actions/cache/blob/main/.licensed.yml"><code>https://github.com/actions/cache/blob/main/.licensed.yml</code></a>
file with the exceptions.</li>
<li>Commit your changes and push your branch upstream.</li>
<li>Open a pull request against <code>main</code> and get it reviewed
and merged.</li>
<li>Draft a new release <a
href="https://github.com/actions/cache/releases">https://github.com/actions/cache/releases</a>
use the same version number used in <code>package.json</code>
<ol>
<li>Create a new tag with the version number.</li>
<li>Auto generate release notes and update them to match the changes you
made in <code>RELEASES.md</code>.</li>
<li>Toggle the set as the latest release option.</li>
<li>Publish the release.</li>
</ol>
</li>
<li>Navigate to <a
href="https://github.com/actions/cache/actions/workflows/release-new-action-version.yml">https://github.com/actions/cache/actions/workflows/release-new-action-version.yml</a>
<ol>
<li>There should be a workflow run queued with the same version
number.</li>
<li>Approve the run to publish the new version and update the major tags
for this action.</li>
</ol>
</li>
</ol>
<h2>Changelog</h2>
<h3>6.1.0</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v6.1.0 to pick up <a
href="https://redirect.github.com/actions/toolkit/pull/2435">actions/toolkit#2435
Handle cache write error due to read-only token</a></li>
<li>Switch redundant "Cache save failed" warning to debug log
in save-only</li>
</ul>
<h3>6.0.0</h3>
<ul>
<li>Updated <code>@actions/cache</code> to ^6.0.1,
<code>@actions/core</code> to ^3.0.1, <code>@actions/exec</code> to
^3.0.0, <code>@actions/io</code> to ^3.0.2</li>
<li>Migrated to ESM module system</li>
<li>Upgraded Jest to v30 and test infrastructure to be ESM
compatible</li>
</ul>
<h3>5.0.4</h3>
<ul>
<li>Bump <code>minimatch</code> to v3.1.5 (fixes ReDoS via globstar
patterns)</li>
<li>Bump <code>undici</code> to v6.24.1 (WebSocket decompression bomb
protection, header validation fixes)</li>
<li>Bump <code>fast-xml-parser</code> to v5.5.6</li>
</ul>
<h3>5.0.3</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v5.0.5 (Resolves: <a
href="https://github.com/actions/cache/security/dependabot/33">https://github.com/actions/cache/security/dependabot/33</a>)</li>
<li>Bump <code>@actions/core</code> to v2.0.3</li>
</ul>
<h3>5.0.2</h3>
<!-- raw HTML omitted -->
</blockquote>
<p>... (truncated)</p>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="2c8a9bd745"><code>2c8a9bd</code></a>
Merge pull request <a
href="https://redirect.github.com/actions/cache/issues/1760">#1760</a>
from actions/samirat/esm_migration_and_package_update</li>
<li><a
href="e9b91fdc3f"><code>e9b91fd</code></a>
Prettier fixes</li>
<li><a
href="e4884b8ff7"><code>e4884b8</code></a>
Rebuild dist</li>
<li><a
href="10baf0191a"><code>10baf01</code></a>
Fixed licenses</li>
<li><a
href="e39b386c90"><code>e39b386</code></a>
Fix test mock return order</li>
<li><a
href="b692820337"><code>b692820</code></a>
PR feedback</li>
<li><a
href="60749128a4"><code>6074912</code></a>
Rebuild dist bundles as ESM to match type:module</li>
<li><a
href="5a912e8b4a"><code>5a912e8</code></a>
Fix lint and jest issues</li>
<li><a
href="b9bf592b98"><code>b9bf592</code></a>
Update documentation for v6 release</li>
<li><a
href="80f777761d"><code>80f7777</code></a>
Update packages, migrate to ESM</li>
<li>See full diff in <a
href="27d5ce7f10...2c8a9bd745">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>
Bumps [actions/cache](https://github.com/actions/cache) from 5.0.5 to
6.0.0.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/releases">actions/cache's
releases</a>.</em></p>
<blockquote>
<h2>v6.0.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Update packages, migrate to ESM by <a
href="https://github.com/Samirat"><code>@Samirat</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1760">actions/cache#1760</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v5...v6.0.0">https://github.com/actions/cache/compare/v5...v6.0.0</a></p>
</blockquote>
</details>
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/blob/main/RELEASES.md">actions/cache's
changelog</a>.</em></p>
<blockquote>
<h3>6.0.0</h3>
<ul>
<li>Updated <code>@actions/cache</code> to ^6.0.1,
<code>@actions/core</code> to ^3.0.1, <code>@actions/exec</code> to
^3.0.0, <code>@actions/io</code> to ^3.0.2</li>
<li>Migrated to ESM module system</li>
<li>Upgraded Jest to v30 and test infrastructure to be ESM
compatible</li>
</ul>
<h3>5.0.4</h3>
<ul>
<li>Bump <code>minimatch</code> to v3.1.5 (fixes ReDoS via globstar
patterns)</li>
<li>Bump <code>undici</code> to v6.24.1 (WebSocket decompression bomb
protection, header validation fixes)</li>
<li>Bump <code>fast-xml-parser</code> to v5.5.6</li>
</ul>
<h3>5.0.3</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v5.0.5 (Resolves: <a
href="https://github.com/actions/cache/security/dependabot/33">https://github.com/actions/cache/security/dependabot/33</a>)</li>
<li>Bump <code>@actions/core</code> to v2.0.3</li>
</ul>
<h3>5.0.2</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v5.0.3 <a
href="https://redirect.github.com/actions/cache/pull/1692">#1692</a></li>
</ul>
<h3>5.0.1</h3>
<ul>
<li>Update <code>@azure/storage-blob</code> to <code>^12.29.1</code> via
<code>@actions/cache@5.0.1</code> <a
href="https://redirect.github.com/actions/cache/pull/1685">#1685</a></li>
</ul>
<h3>5.0.0</h3>
<blockquote>
<p>[!IMPORTANT]
<code>actions/cache@v5</code> runs on the Node.js 24 runtime and
requires a minimum Actions Runner version of <code>2.327.1</code>.
If you are using self-hosted runners, ensure they are updated before
upgrading.</p>
</blockquote>
<h3>4.3.0</h3>
<ul>
<li>Bump <code>@actions/cache</code> to <a
href="https://redirect.github.com/actions/toolkit/pull/2132">v4.1.0</a></li>
</ul>
<h3>4.2.4</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v4.0.5</li>
</ul>
<h3>4.2.3</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v4.0.3 (obfuscates SAS token in
debug logs for cache entries)</li>
</ul>
<h3>4.2.2</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v4.0.2</li>
</ul>
<h3>4.2.1</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v4.0.1</li>
</ul>
<!-- raw HTML omitted -->
</blockquote>
<p>... (truncated)</p>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="2c8a9bd745"><code>2c8a9bd</code></a>
Merge pull request <a
href="https://redirect.github.com/actions/cache/issues/1760">#1760</a>
from actions/samirat/esm_migration_and_package_update</li>
<li><a
href="e9b91fdc3f"><code>e9b91fd</code></a>
Prettier fixes</li>
<li><a
href="e4884b8ff7"><code>e4884b8</code></a>
Rebuild dist</li>
<li><a
href="10baf0191a"><code>10baf01</code></a>
Fixed licenses</li>
<li><a
href="e39b386c90"><code>e39b386</code></a>
Fix test mock return order</li>
<li><a
href="b692820337"><code>b692820</code></a>
PR feedback</li>
<li><a
href="60749128a4"><code>6074912</code></a>
Rebuild dist bundles as ESM to match type:module</li>
<li><a
href="5a912e8b4a"><code>5a912e8</code></a>
Fix lint and jest issues</li>
<li><a
href="b9bf592b98"><code>b9bf592</code></a>
Update documentation for v6 release</li>
<li><a
href="80f777761d"><code>80f7777</code></a>
Update packages, migrate to ESM</li>
<li>See full diff in <a
href="https://github.com/actions/cache/compare/v5.0.5...v6.0.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>
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 `Issue Backlog Processor` workflow’s `agent` job was failing at
runtime because the generated lock workflow referenced a non-existent
gh-aw helper (`merge_awf_model_multipliers.cjs`). This PR updates the
lock file to align with current gh-aw output and eliminate that stale
invocation.
- **Root cause addressed**
- `issue-backlog-processor.lock.yml` contained an outdated step that
executed:
- `node "${RUNNER_TEMP}/gh-aw/actions/merge_awf_model_multipliers.cjs"`
- That module is not present in the runner-provisioned gh-aw action set,
causing `MODULE_NOT_FOUND` and failing the `agent` job.
- **Change made**
- Recompiled the source workflow (`issue-backlog-processor.md`) and
committed the regenerated lock file:
- `.github/workflows/issue-backlog-processor.lock.yml`
- The regenerated lock no longer includes the stale
`merge_awf_model_multipliers.cjs` call and updates associated gh-aw
metadata/version pins accordingly.
- **Illustrative diff (relevant line)**
```yaml
- GH_AW_MODEL_MULTIPLIERS_PATH="/tmp/gh-aw/model_multipliers.json" node "${RUNNER_TEMP}/gh-aw/actions/merge_awf_model_multipliers.cjs"
```
---------
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>
The `API Coherence Checker` workflow’s `agent` job was failing in
Actions (`82289334242`) due to a lockfile/runtime mismatch that invoked
a non-existent gh-aw script (`merge_awf_model_multipliers.cjs`). This PR
refreshes the generated lockfile so the compiled workflow and gh-aw
runtime are aligned.
- **Root cause surfaced in generated workflow**
- The existing `.lock.yml` referenced an outdated gh-aw runtime
path/script combination that no longer exists in the installed action
payload.
- **Lockfile regeneration (single-file, surgical)**
- Updated only:
- `.github/workflows/api-coherence-checker.lock.yml`
- Regenerated with strict gh-aw compile output so metadata, setup action
refs, and generated agent-step wiring are internally consistent.
- **Effect on `agent` job behavior**
- Removes the stale generated invocation path to
`merge_awf_model_multipliers.cjs`.
- Aligns generated runtime variables/steps with the currently resolved
gh-aw setup version.
```yaml
# before (generated agent step)
GH_AW_MODEL_MULTIPLIERS_PATH="/tmp/gh-aw/model_multipliers.json" \
node "${RUNNER_TEMP}/gh-aw/actions/merge_awf_model_multipliers.cjs"
# after
# stale merge step no longer emitted in this lockfile
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The "agent" job was failing immediately because the lock file (compiled
by `gh-aw v0.79.6`) generated a step calling
`merge_awf_model_multipliers.cjs`, but the pinned
`github/gh-aw-actions/setup@v0.80.4` did not ship that script — causing
a `MODULE_NOT_FOUND` crash before the Copilot CLI ever ran.
## Changes
- **`.github/workflows/academic-citation-tracker.lock.yml`** —
recompiled with `gh aw compile --strict` using v0.79.8; setup action is
now pinned to the matching `@v0.79.8` release which includes all
expected scripts
- **`.github/dependabot.yml`** — compiler updated ignore entries to
cover both `github/gh-aw-actions/**` (subdirectory refs like `setup`)
and `github/gh-aw-actions` (base ref), preventing Dependabot from
bumping the setup pin out of sync again
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
z3 already builds under Pyodide (there is a `pyodide.yml` workflow and
an
`IS_PYODIDE` path in `setup.py`), but that path uses `pyodide build` and
produces
a wheel tagged `emscripten_<pyodide-version>_wasm32`, which is pinned to
a single
Pyodide release and rejected by PyPI — so today it's only usable as a CI
artifact.
[PEP 783](https://peps.python.org/pep-0783/) introduced the portable
`pyemscripten_<date>_wasm32` platform tag that **PyPI accepts** and
`micropip` can
install at runtime. This makes `z3-solver` build that wheel via
`cibuildwheel --platform pyodide`.
## Changes
- **`setup.py`** — for the emscripten target, use the wheel platform tag
that
pyodide-build provides verbatim via `_PYTHON_HOST_PLATFORM` (e.g.
`pyemscripten_2026_0_wasm32`) instead of reconstructing an
`emscripten_*` tag.
Falls back to the previous behaviour when that env var is absent.
- **`setup.py` / `CMakeLists.txt` / `pyproject.toml`** — switch the
Pyodide build
from JS-based exceptions (`-fexceptions`,
`-sDISABLE_EXCEPTION_CATCHING=0`) to
**native wasm exception handling** (`-fwasm-exceptions
-sSUPPORT_LONGJMP=wasm`),
matching the ABI of the Pyodide 314 / emscripten 5 main module. With the
old
flags `libz3.so` imports `invoke_*` trampolines the runtime no longer
provides,
so the wheel builds but the first `Z3_mk_config` call fails at runtime
with
`Dynamic linking error: cannot resolve symbol invoke_vi`.
- **`pyproject.toml`** — add `[tool.cibuildwheel]` /
`[tool.pyodide.build]` so
`cibuildwheel --platform pyodide` builds and tests the wheel (`cp314`).
- **`.github/workflows/pyodide-pypi.yml`** (new) — build with
cibuildwheel and
publish to PyPI (trusted publishing) on tags. Existing `pyodide.yml`
unchanged.
## Verification
Built with `cibuildwheel 4.1.0` / `pyodide-build 0.35.0` / `emscripten
5.0.3`,
CPython 3.14 / Pyodide 314:
- Produces `z3_solver-4.17.0.0-py3-none-pyemscripten_2026_0_wasm32.whl`.
- `z3test.py` passes in the Pyodide runtime (node + wasm32).
- Installed via `micropip` and solves SMT problems both under node and
in a
browser (`sat` with a model, `unsat` for a contradiction).
🤖 Generated with [Claude Code](https://claude.com/claude-code)
🕵️♂️ Reviewed by [Alcides Fonseca](https://wiki.alcidesfonseca.com)
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
`Microsoft.Z3.dll` ships with PE `Machine=0x8664` (AMD64), causing the
CLR loader to reject it on arm64 .NET hosts (macOS/Linux/Windows ARM)
even though the assembly is pure IL (`CorFlags.ILONLY=True`) and arm64
native libraries are already bundled in the package.
## Changes
- **`.github/workflows/nightly-validation.yml`** — adds
`validate-dotnet-anycpu` job to the Nightly Build Validation workflow:
- Downloads the nightly NuGet package from the GitHub release
- Extracts `lib/netstandard2.0/Microsoft.Z3.dll` (NuGet packages are ZIP
archives)
- Reads the COFF `Machine` field from the PE header using Python
`struct`
- Fails with an actionable error if `Machine` is `0x8664` (AMD64) or
`0xAA64` (ARM64); passes for `0x014C` (i386/AnyCPU) or `0x0000`
The check catches any regression where the managed wrapper is compiled
architecture-specific, blocking non-x64 .NET hosts from loading it.
---------
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>
This change stops agentic workflows from opening GitHub issues when a
run fails due to workflow/tooling conditions such as missing-tool
reports or token-budget exhaustion. It applies the repository-wide
suppression suggested by the failure issue itself, so these runs can
still fail without creating issue noise.
- **What changed**
- Added `safe-outputs.report-failure-as-issue: false` to each top-level
agentic workflow source under `.github/workflows/*.md`
- Regenerated the corresponding compiled `.lock.yml` workflows so the
runtime configuration matches the source frontmatter
- **Effect**
- Agentic workflow runs continue to report failure in Actions
- Automatic `[aw] ... failed` issue creation is disabled for these
workflows
- Existing safe outputs such as `noop` and `missing-tool` remain
unchanged
- **Scope**
- Applied consistently across the repository’s top-level agentic
workflows, including `zipt-code-reviewer`, `build-warning-fixer`,
`code-conventions-analyzer`, `workflow-suggestion-agent`, and related
workflows
- **Configuration pattern**
```yaml
safe-outputs:
report-failure-as-issue: false
create-issue:
...
missing-tool:
create-issue: true
noop:
report-as-issue: false
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This updates `fstar-master-build.yml` so generated `.smt2` files are
preserved and discoverable from the build discussion. The discussion now
links the artifact and includes an inline preview of each generated SMT2
file (first 1000 lines).
- **SMT2 collection and packaging**
- Added an always-run step to recursively find generated `*.smt2` files
under the FStar checkout.
- Copies discovered files into a dedicated artifact staging directory
while preserving relative paths.
- **Artifact publication**
- Added artifact upload for collected SMT2 files
(`fstar-generated-smt2-${{ github.run_id }}`).
- Exposes uploaded artifact metadata to downstream steps for linking.
- **Discussion enrichment**
- Extended discussion body generation to include:
- direct artifact link (when SMT2 files exist),
- inline preview blocks with the first 1000 lines per file,
- fallback messaging when no SMT2 files are produced.
- Added size-aware truncation to keep discussion content within GitHub
body limits.
```yaml
- name: Upload generated SMT2 artifact
id: upload_smt2
if: always() && steps.collect_smt2.outputs.has_files == 'true'
uses: actions/upload-artifact@v4
with:
name: fstar-generated-smt2-${{ github.run_id }}
path: /tmp/gh-aw/agent/smt2-artifact
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The memory-safety scan workflow already runs ASan/UBSan, but its
reporting workflow was configured to post discussions rather than filing
actionable issues. This change aligns the reporter with the expected
outcome: sanitizer findings become trackable GitHub issues.
- **Reporting output switched to issues**
- Replaced `safe-outputs.create-discussion` with
`safe-outputs.create-issue` in `memory-safety-report.md`
- Added issue labels and issue cap for controlled issue creation
- Updated workflow description text to reflect issue-based reporting
- **Prompt behavior updated for clean/noisy runs**
- Updated agent instructions to generate issue reports for actionable
findings
- Changed zero-finding behavior to `noop` (no issue spam on clean runs)
- Updated wording for failure/edge-case paths to reference issue output
- **Compiled workflow updated**
- Regenerated `memory-safety-report.lock.yml` from the markdown source
so runtime behavior matches the new safe-output contract
```yaml
safe-outputs:
create-issue:
title-prefix: "[Memory Safety] "
labels: [bug, memory-safety, automated-analysis]
max: 1
noop:
report-as-issue: false
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This change simplifies recently touched skill scripts by removing
duplicated repo-root discovery code, promoting shared root lookup to a
public API, and tightening small readability issues without changing
behavior. It keeps script semantics intact while making cross-skill
reuse explicit.
- **Shared API cleanup (`.github/skills/shared/z3db.py`)**
- Promote `_find_repo_root` to public `find_repo_root`.
- Add `require_repo_root()` for scripts that should fail-fast when root
discovery fails.
- Update library usage docstring to expose both helpers.
- Replace adjacent SQL string literals in `log()` with a single literal.
- **Deduplicate memory-safety root lookup
(`.github/skills/memory-safety/scripts/memory_safety.py`)**
- Remove local `find_repo_root()` implementation.
- Import and use shared `require_repo_root()` from `z3db`.
- **Simplify static-analysis label selection
(`.github/skills/static-analysis/scripts/static_analysis.py`)**
- Replace two-step label assignment with a single expression:
- `label = f["type"] or f["category"]`
```python
# before
label = f["category"]
if f["type"]:
label = f["type"]
# after
label = f["type"] or f["category"]
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`build-and-report` was failing hard when the `Build FStar` step hit
prover regressions, preventing downstream reporting from running. This
change makes FStar failures non-blocking and ensures the reporting path
still executes with an explicit FStar outcome.
- **Workflow failure propagation**
- Marked `Build FStar` as non-blocking:
- added `id: build_fstar`
- added `continue-on-error: true`
- **Guaranteed reporting execution**
- Made the summary step unconditional with `if: always()` so it runs
even when FStar fails.
- **Robust summary generation**
- Passed step outcome into the script (`FSTAR_BUILD_OUTCOME`).
- Hardened file reads for missing FStar artifacts/version files.
- Report body now reflects actual FStar outcome (`success` vs
non-success) while preserving pipeline continuity.
```yaml
- name: Build FStar
id: build_fstar
continue-on-error: true
run: |
# existing FStar build commands
- name: Create discussion summary
if: always()
env:
FSTAR_BUILD_OUTCOME: ${{ steps.build_fstar.outcome }}
uses: actions/github-script@v9
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `build-and-report` workflow failed in `build-and-report` because
FStar was invoked with a default `OTHERFLAGS` value containing
`--smt.ho_matching true`, which current FStar no longer recognizes. This
change removes that default while keeping the input configurable for
manual runs.
- **Root cause**
- Workflow default `fstar_otherflags` was set to `--smt.ho_matching
true`.
- During `make`, FStar exited with `error: unrecognized option
'--smt.ho_matching'` (job `79905082893`).
- **Workflow changes**
- Updated `.github/workflows/fstar-master-build.yml`:
- `workflow_dispatch.inputs.fstar_otherflags.default` changed from
`--smt.ho_matching true` to `""`.
- Job env fallback `FSTAR_OTHERFLAGS` changed from `--smt.ho_matching
true` to `""`.
- Removed the outdated option example from the `fstar_otherflags` input
description.
- **Resulting behavior**
- Default scheduled/manual workflow runs no longer pass unsupported
FStar flags.
- Custom flags can still be provided via `fstar_otherflags` when needed.
```yaml
fstar_otherflags:
description: "Extra FStar OTHERFLAGS"
required: false
default: ""
# ...
FSTAR_OTHERFLAGS: ${{ github.event.inputs.fstar_otherflags || '' }}
```
---------
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>
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>
