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>
With `parallel.enable=true`, Z3 could return a SAT model for a QF_BV
instance that violates its own assertions. The bug traces to solver
translation: named assertions were re-registered with swapped
formula/indicator arguments, corrupting the translated solver's
assertion state.
## Bug
`m_name2assertion` stores `indicator → formula`. In
`smt_solver::translate()`, the structured binding `[k, v]` gives `k =
indicator`, `v = formula`, but `assert_expr(t, a)` expects `(formula,
indicator)`:
```cpp
// Before — args reversed
for (auto& [k, v] : m_name2assertion) {
expr* val = translator(k); // indicator
expr* key = translator(v); // formula
result->assert_expr(val, key); // assert_expr(indicator, formula) ← wrong
}
```
## Fix
```cpp
// After — correct order
for (auto& [k, v] : m_name2assertion) {
expr* fml = translator(v); // formula
expr* ind = translator(k); // indicator
result->assert_expr(fml, ind); // assert_expr(formula, indicator) ✓
}
```
This affects any code path that calls `smt_solver::translate()` and uses
named assertions (`assert_and_track` / `Z3_solver_assert_and_track`),
including all parallel solving modes.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Problem
Fixes#10133. For `QF_BV` with `parallel.enable=true`, the solver could
return `sat` with a model that violates its own assertions.
`mk_qfbv_tactic` routes SAT solving to `mk_psat_tactic`, which built the
solver via `mk_inc_sat_solver(m, p, false)` (non-incremental). The
parallel cube-and-conquer engine **reuses this single solver** across
many `check_sat(cube)` calls, but SAT variable/blocked-clause
elimination ran because the simplifier's incremental gate was disabled.
Elimination model reconstruction is only sound for a single one-shot
solve; under repeated cube assumptions it produces models where
eliminated Tseitin variables get values contradicting the original
clauses.
## Root cause (two coupled defects)
1. **Stale simplifier cache.** `inc_sat_solver`'s constructor called
`m_solver.set_incremental()` *after* `updt_params()`. The SAT simplifier
caches `m_incremental_mode` from the SAT config *during* `updt_params`,
so setting the incremental flag afterwards left a stale non-incremental
mode and elimination stayed enabled. (This is why simply passing
`incremental_mode=true` had no effect on its own.)
2. **Non-incremental parallel solver.** `mk_psat_tactic` created the
reused solver as non-incremental.
## Fix
- Move `set_incremental()` **before** `updt_params()` in the
`inc_sat_solver` constructor so the simplifier caches the correct mode.
- Create the parallel solver with `incremental_mode=true` in
`mk_psat_tactic`.
## Validation
- Variable elimination on the QF_BV parallel path drops to zero
(`sat-elim-bool-vars-res` 21664 -> 0); remaining `elim-clauses/literals`
are sound cleaner/subsumption steps.
- Consistent with ground truth: on 4.16.0, `sat.elim_vars=false` removed
all 7 `failed to verify` errors; this change disables exactly that
unsound elimination, scoped to the reused/parallel solver.
- A solvable QF_BV instance returns a **valid** model under
`parallel.enable=true model_validate=true`.
- All 92 unit tests pass (`test-z3 /a`).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Automated workflow self-test
This PR is an **automated workflow self-test** of the `fixer-selftest` /
`snapshot-regression-fixer` pipeline running on the self-hosted
`rise-runner-1` pool. Its purpose is to verify that Copilot inference
runs and that the `create-pull-request` safe output can open a real
**draft** pull request on `Z3Prover/z3`.
### The fix
- **File:** `src/ast/euf/euf_ac_plugin.cpp` (line 995)
- **Before:** `// add difference betwen dst.l and src.l to both src.l,
src.r`
- **After:** `// add difference between dst.l and src.l to both src.l,
src.r`
A single spelling mistake (`betwen` → `between`) in a `//` code comment.
### Why no rebuild is needed
The change is **comment-only** — no code, string literals, identifiers,
or build files were touched — so it cannot affect z3's behaviour and
requires no compilation or testing.
### For maintainers
This is a genuine, correct fix, so feel free to **merge** it. Equally,
you may simply **close** it — the success of the self-test does not
depend on this PR being merged.
> Generated by [Self-test the agentic PR pipeline with a tiny z3 comment
fix](https://github.com/Z3Prover/bench/actions/runs/29523479037) · 54.5
AIC · ⌖ 18.9 AIC · ⊞ 8K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+fixer-selftest%22&type=pullrequests)
<!-- gh-aw-agentic-workflow: Self-test the agentic PR pipeline with a
tiny z3 comment fix, engine: copilot, version: 1.0.65, model:
claude-opus-4.8, id: 29523479037, workflow_id: fixer-selftest, run:
https://github.com/Z3Prover/bench/actions/runs/29523479037 -->
<!-- gh-aw-workflow-id: fixer-selftest -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/fixer-selftest -->
Co-authored-by: z3prover-ci-bot[bot] <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When a term column x - y is fixed to 0 (e.g. from t <= ca and t >= ca),
theory_lra previously discovered the implied equality x = y only lazily via
assume_eqs() during final_check. On the FP fuel-recursive axiom in issue #10065
this discovery is starved by E-matching, which unfolds the recursion and
bit-blasts an exploding FP subproblem before the branch closes.
Add propagate_offset_eq() to detect a fixed 2-variable offset term with opposite
unit-scaled coefficients and propagate the operand equality x = y directly to the
core, so congruence closure merges dependent terms immediately. This mirrors the
offset-row propagation performed by theory_arith (propagate_cheap_eq) and matches
its behavior on this benchmark (timeout -> unsat 0.06s, 2 quant-instantiations).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e
## Problem
A QF_NIA benchmark (`From_T2__ex16.t2__p22243_terminationG_0.smt2`, run
with `-T:200 model_validate=true`) crashes with SIGSEGV inside nlsat.
## Root cause
In `algebraic_numbers::manager:👿:compare_core`, the
interval-separation workaround computed the isolating intervals of `a`
and `b` with:
```cpp
if (get_interval(a, la, ua, precision) &&
get_interval(b, lb, ub, precision)) { ... }
```
`&&` short-circuits: when `a` is **rational**, `get_interval(a, ...)`
finds the exact root and returns `false`, so `get_interval(b, ...)`
never runs and `b`'s bounds `lb`/`ub` stay **0**. Those bounds are used
*unconditionally* below the `if` (in the `compare(cell_a, u_b)` /
`compare(cell_b, l_a)` checks), so `a` was effectively compared against
`0`, producing an incorrect and self-inconsistent sign (`compare`
returned `+1` while `<`, `=`, `>` were all false).
Concretely, comparing `c = 39017/131072` (rational) with `d ≈
0.297676176` (root of a quadratic) returned `c > d`, though `c < d`.
Downstream, this made nlsat's `interval_set::is_full` miss full coverage
of ℝ, so `pick_in_complement` was invoked on an empty complement and
read `s->m_intervals[UINT_MAX]` — a crash guarded only by a
release-stripped `SASSERT` (`nlsat_interval_set.cpp`).
## Fix
Compute both intervals unconditionally so `b`'s bounds are always valid
before they are used.
## Validation
- The crashing benchmark now returns `unsat` (verified on both macOS and
a Linux `RelWithDebInfo` build where the SIGSEGV was originally
reproduced under gdb).
- Unit tests pass: `algebraic`, `upolynomial`, `polynomial`, `nlsat`.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
reduce_core looped with while (true) and read p = todo.back() with no
empty check, exiting only when it reached a hypothesis-free sub-proof of
false. When hypothesis reduction cannot close all hypotheses on the root
proof, todo drains and todo.back() reads past the end of the vector,
producing a heap-use-after-free (SIGSEGV in Fixedpoint.query with
spacer.keep_proxy=false). Whether the root closes depends on search order,
making the crash nondeterministic / seed-dependent.
Bound the loop by todo emptiness, track the reduced root across cache-hit
pops, and return it if the loop drains without hitting the false-subproof
early return.
Verified on the issue #10123 benchmark: the UAF is eliminated across
spacer.random_seed 0/3/7/13/42/99, all returning unsat.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e
## Summary
Optimizes `lp::static_matrix<..>::remove_element`, reported as a hotspot
in
[Z3Prover/bench#3143](https://github.com/Z3Prover/bench/discussions/3143)
(the #1 exclusive-time function, ~19.6%, on
`inputs/issues/iss-5131/bug-1.smt2`).
`remove_element` uses swap-remove but **deep-copied** the relocated tail
coefficient:
```cpp
auto & rc = row_vals[row_offset] = row_vals.back(); // copy from the tail
```
In namespace `lp`, `mpq` is a typedef for the copyable `rational`, so
this copy-assign allocates a fresh bignum whenever the **source (the
tail)** is big — matching the `malloc`/`_int_malloc` entries in the
reported profile. The tail element is `pop_back`'d immediately
afterwards, so the allocation is wasteful.
## Change
A copy-assign allocates only when the **source** is big
(`mpz_manager::set` → `big_set`). So relocate the tail coefficient by
**swapping** exactly in that case — stealing its already-allocated
storage, zero `malloc`. When the tail is small, a plain copy never
allocates and is cheaper than swapping the `mpz` internals; the
destination's size is irrelevant. The column-cell relocation is
unchanged (a `column_cell` carries no coefficient).
Single-file change; no new parameters.
## Benchmarks
A/B produced by toggling the new code path against the original
deep-copy (via a temporary parameter, not included here).
- **rise-runner-2** (initial `is_big()||is_big()` variant): QF_LIA_small
neutral; certora identical outcomes, −1.5% paired solve-time.
- **128-core Linux box**, `run_on_dir.py`, `-max_workers 32` (final
tail-only variant):
| Set | Files | `-T` | Solved (new = orig) | Avg-time ratio new/orig |
Correctness |
|---|---|---|---|---|---|
| QF_LIA (SMT-LIB) | 6947 | 20s | 5817 ≈ 5815 | 1.00000 | identical (±2
timeout-edge) |
| certora | 308 | 120s | 186 = 186 | 0.9977 | identical, 0 unique
timeouts |
| QF_LRA (SMT-LIB 2025) | 1753 | 120s | 1552 = 1552 | 0.9985–0.9991 |
identical, 0 real regressions |
Consistently **correctness-neutral and marginally faster** (~0.1–0.5%)
on large-coefficient LP sets, flat on small-coefficient inputs. The
per-`remove_element` allocation saved is small relative to total solve
time, so the whole-solver delta is a fraction of a percent — a clean
micro-optimization with no downside.
## Validation
- `make`/`ninja` build clean; `test-z3 /a` — 92/92 pass.
- Baseline vs patched output byte-identical on the reported benchmark;
identical solve sets across all three benchmark suites above.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Implement check_mod_congruence in nla_divisions: for two mod-atoms
sharing a (possibly symbolic) divisor y, emit the model-guided tautology
div(x,y) - div(s,y) = delta => mod(x,y) - mod(s,y) = (x - s) - delta*y.
This discharges linear congruences over a symbolic modulus that the
nonlinear core did not otherwise isolate. Thread the div(x,y) variable
through add_divisibility (nla_core/nla_solver/nla_divisions) and
register it in theory_lra for symbolic-divisor mod terms.
Solves FStar.BitVector-1 (0.7s) and FStar.Matrix-1 (1.6s), previously
300s timeouts; all 92 unit tests pass.
Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Large Python bitvector workloads were hitting a sharp performance cliff
during `Solver.add(...)`, consistent with severe hash-table clustering
in expression-heavy assertion paths. The issue was sensitive to input
size/alignment, indicating weak low-bit dispersion in hash combination.
- **Hash mixing update (`src/util/hash.h`)**
- Replaced the old `combine_hash(h1, h2)` arithmetic/xor sequence with
stronger mixing:
- boost-style combine step
- `hash_u(...)` finalization
- Goal: improve low-bit entropy used by chained hash-table bucket
selection under aligned/high-volume AST patterns.
- **Regression guard and A/B comparison (`src/test/chashtable.cpp`)**
- Added `tst_combine_hash_low_bits()` and invoked it from
`tst_chashtable()`.
- The test stresses aligned first components (`i << 12`) combined with a
fixed seed.
- Added an in-test comparison between the **old** and **new** pairwise
hash combiners and validates:
- reduced collision counts for low-bit projections (8-bit and 16-bit
suffixes),
- improved low-bit uniformity for 8-bit and 16-bit suffixes,
- reported prefix/suffix uniformity metrics (high/low 8 and 16 bits) for
visibility in test output.
```cpp
static inline unsigned combine_hash(unsigned h1, unsigned h2) {
h1 ^= h2 + 0x9e3779b9 + (h1 << 6) + (h1 >> 2);
return hash_u(h1);
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Sound by array extensionality when a is independent of the bound
variables. Implemented as array_rewriter::mk_lambda_core and wired into
th_rewriter::reduce_quantifier alongside the ground-lambda case.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
rules_foreign_cc expects libraries under its default lib output
directory. GNUInstallDirs may instead select lib64, causing Bazel to
reject an otherwise successful CMake build because its declared output
is missing.
Share the default CMake arguments between the static and dynamic targets
and set CMAKE_INSTALL_LIBDIR to lib.
The nightly workflow’s `Publish to test.PyPI` job fails because
test.PyPI rejects uploaded macOS wheels tagged `macosx_13_3_*`. This
change keeps the validation publish path working by rewriting
unsupported macOS wheel tags to a supported form during that specific
upload step.
- **Root cause reflected in workflow behavior**
- `publish-test-pypi` currently uploads all artifacts from
`PythonPackages`, including macOS wheels that test.PyPI does not accept.
- **Workflow change (surgical)**
- In `.github/workflows/nightly.yml`, added a pre-upload rewrite step in
`publish-test-pypi` to rename wheel tags from `macosx_13_3_*` to
`macosx_13_*` in `dist/`.
- Left artifact production unchanged; only the filenames used for the
test.PyPI upload are adjusted.
- **Effect on release flow**
- test.PyPI upload continues for sdist + Linux/Windows wheels and now
includes rewritten macOS wheels.
- Nightly macOS artifacts remain built and available through existing
artifact/release paths.
```yaml
- name: Rewrite macOS wheel tags unsupported by test.PyPI
run: |
for whl in dist/*-macosx_13_3_*.whl; do
[ -e "$whl" ] || continue
mv "$whl" "${whl/macosx_13_3_/macosx_13_}"
done
ls -l dist
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `Release Build` workflow still targeted macOS 13.0 for the x64/arm64
packaging jobs, while the codebase now relies on libc++ functionality
that is only available with a 13.3 deployment target. This updates the
release workflow to use the same macOS target configuration already
applied in `nightly.yml`.
- **Release workflow**
- Raise `MACOSX_DEPLOYMENT_TARGET` from `13.0` to `13.3` for both
`mac-build-x64` and `mac-build-arm64`
- Update the packaging target passed to `mk_unix_dist.py` from
`--os=osx-13.0` to `--os=osx-13.3`
- **Config alignment**
- Bring `release.yml` in sync with the existing nightly macOS fix so
both workflows build against the same minimum macOS version
```yaml
env:
MACOSX_DEPLOYMENT_TARGET: "13.3"
run: python scripts/mk_unix_dist.py --arch=x64 --os=osx-13.3
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`seq.foldl` could produce a concrete sequence model while related
`seq.nth` constraints were still validated against stale or
underconstrained length information, leading to invalid models. In the
reported case, `all` was modeled as `(seq.++ (seq.unit 7) (seq.unit 0))`
while `final = (seq.nth all 0)` remained inconsistent with `final = 6`.
- **Root cause**
- Sequence solutions were propagated as equalities, but parent `seq.len`
terms were not updated when a sequence term was solved.
- As a result, `seq.nth` guard reasoning could miss that a solved
sequence had known in-bounds length.
- **Solver change**
- Extend `theory_seq::add_solution` to collect parent `seq.len`
expressions of a solved term when the solved result is sequence-typed.
- After propagating the solved sequence equality, also propagate the
rewritten length equality for those parent length terms.
- Keep this propagation guarded to sequence results so scalar
`seq.foldl`/`seq.foldli` solutions do not regress from `sat` to
`unknown` under model validation.
- **Regression coverage**
- Add a focused test for the reported SMT-LIB pattern:
- `all = seq.foldl(...)`
- `final = seq.nth all 0`
- `initial = 0`
- `final = 6`
- Add focused scalar `seq.foldl`/`seq.foldli` model-validation coverage
for the existing benchmark shapes that must continue returning `sat`.
- The regressions check both that model validation no longer reports an
invalid model for the `seq.nth` case and that scalar fold/foldi cases do
not regress to `unknown`.
- **Effect**
- Solved sequence terms now push enough derived length information for
dependent `seq.nth` constraints to validate against the actual modeled
sequence.
- Existing scalar fold/foldi solving behavior is preserved.
```smt2
(define-fun all_sums ((prev_sums (Seq Int)) (elem Int)) (Seq Int)
(seq.++ (seq.unit (+ (seq.nth prev_sums 0) elem)) prev_sums)
)
(assert (= all (seq.foldl all_sums (seq.unit initial) elements)))
(assert (= final (seq.nth all 0)))
(assert (= initial 0))
(assert (= final 6))
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `release-notes-updater` agent job was failing with HTTP 401 on every
Copilot API inference request because the GitHub Actions token lacked
`copilot-requests: write`.
## Changes
- **`release-notes-updater.md`**: Replace `permissions: read-all`
shorthand with an explicit permissions object that includes
`copilot-requests: write`
- **`release-notes-updater.lock.yml`**: Recompiled via `gh aw compile`
```yaml
# Before
permissions: read-all
# After
permissions:
contents: read
issues: read
pull-requests: read
discussions: read
copilot-requests: write
```
`read-all` expands all scopes to read but does not grant
`copilot-requests: write`, which is the permission required for the
GitHub Actions token to authenticate with the Copilot API proxy.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The reported case showed expensive reasoning for lexicographic string
comparisons under the default sequence solver, and incorrect handling
expectations with `z3str3` (which does not interpret these comparisons).
This change targets the default solver path by short-circuiting
contradictory constant-bound `<` constraints earlier.
- **Theory shortcut for constant lexical bounds**
- In `theory_seq::assign_eh`, detect asserted `str.<` constraints of the
form `c < x` or `x < c` where `c` is a string constant.
- When a complementary bound on the same equivalence class is already
true, check bound consistency immediately.
- If bounds are contradictory (`!(lower < upper)`), emit a direct theory
conflict from the two active literals instead of waiting for deeper
axiom propagation.
- **Preserve existing comparison reasoning**
- Existing `check_lts` transitivity/axiom flow is retained.
- The new logic is a narrow fast path for contradictory constant bounds
and does not alter general string-order semantics.
- **Regression coverage**
- Added a solver-level regression in `src/test/seq_rewriter.cpp` for
contradictory date-like lexical bounds to ensure this class of
constraints is rejected as `unsat`.
```cpp
ctx.assert_expr(su.str.mk_lex_lt(su.str.mk_string("2024-01-01"), x));
ctx.assert_expr(su.str.mk_lex_lt(x, su.str.mk_string("2024-12-31")));
ctx.assert_expr(su.str.mk_lex_lt(x, su.str.mk_string("2023-01-01")));
ENSURE(ctx.check() == l_false);
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Combining `mod0`/`div0` quantifier axioms with a mod-idempotency
quantifier caused Z3 to loop forever. The core issue was that
`mk_mod_core` in `arith_rewriter.cpp` only handled rewrite rules for
*numeral* moduli, leaving two gaps for symbolic `y`:
1. `mod(a + k*y, y)` was not reduced to `mod(a, y)`, so `(not (= (mod (+
a b) b) (mod a b)))` stayed unreduced and caused the nlsat solver to
spin.
2. The E-matching pattern `(mod (mod x y) y)` fired on every new term it
produced, creating an unbounded chain of nested `mod` expressions.
```lisp
; Previously non-terminating, now returns unsat immediately
(assert (forall ((x Int)) (! (= (mod0 x 0) 0) :pattern ((mod0 x 0)))))
(assert (forall ((x Int)) (! (= (div0 x 0) 0) :pattern ((div0 x 0)))))
(assert (forall ((x Int) (y Int))
(! (= (mod (mod x y) y) (mod x y)) :pattern ((mod (mod x y) y)))))
(assert (not (= (mod (+ a b) b) (mod a b))))
(check-sat)
```
## Changes
- **`src/ast/rewriter/arith_rewriter.cpp` — symbolic summand
elimination**: In `mk_mod_core`, when the modulus is a non-numeral
integer and the dividend is an `add`, strip any summand equal to the
modulus or an integer multiple of it. Soundness: `k*0 = 0` for all `k`,
so the rule holds even at `y = 0`. This immediately collapses the
reported formula to `false`.
- **`src/ast/rewriter/arith_rewriter.cpp` — symbolic idempotency via
ite**: Extend the existing `mod(mod(x,y), y) → mod(x,y)` rule
(previously numeral-only) to symbolic `y` by rewriting to `ite(y=0,
mod(mod(x,0),0), mod(x,y))`. The `y=0` branch uses a numeral divisor,
which is excluded by the `!v2.is_zero()` guard, halting the E-matching
chain.
- **`src/test/arith_rewriter.cpp`**: Regression tests for `mod(a+y, y) =
mod(a,y)`, `mod(a+2y, y) = mod(a,y)`, and `mod(mod(a,3),3) = mod(a,3)`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`ASSERTION VIOLATION` at `bv2int_translator.h:72` when using
`smt.bv.solver=2` with formulas containing `abs` (or other arith
expressions that rewrite to ITE with arith predicates).
**Root cause**
`ensure_translated` skips adding sub-expressions of boolean non-BV nodes
to the `todo` list — correct, since the base theory owns them in plugin
mode. However, `translate_expr`'s early-return only covered
`basic_family_id` booleans, not non-basic ones (e.g.,
`arith_family_id`).
When `(abs f)` is rewritten by the arith rewriter to `(ite (>= f 0) f (-
f))`, the predicate `(>= f 0)` ends up in `todo` (as a child of the
ITE), but its own children (e.g., the integer literal `0`) are not
added. `translate_expr` then calls `translated(0)` on an unmapped
expression, firing `SASSERT(r)`.
Reproducer:
```smt2
(declare-const f Int)
(assert (= 0 (mod 0 (bv2nat ((_ int_to_bv 1) (abs f))))))
(check-sat)
; z3 test.smt2 smt.bv.solver=2 → ASSERTION VIOLATION (before fix)
```
**Fix**
Extend the early-return in `translate_expr` to match
`ensure_translated`'s skip condition — all boolean non-BV expressions in
plugin mode map to themselves:
```cpp
// before
if (m_is_plugin && ap->get_family_id() == basic_family_id && m.is_bool(ap)) {
// after
if (m_is_plugin && m.is_bool(ap) && ap->get_family_id() != bv.get_family_id()) {
```
BV boolean predicates (`bvule`, etc.) are unaffected — they still route
through `translate_bv`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`Expr.getSort()` on a constant with an `EnumSort` sort returns a
`DatatypeSort`, causing `ClassCastException` when enum-specific methods
are called.
```java
Context ctx = new Context();
EnumSort<Foo> enumSort = ctx.mkEnumSort("my-enum", "e1", "e2");
Expr<EnumSort<Foo>> c = ctx.mkConst("my-const", enumSort);
c.getSort().getName(); // ClassCastException — getSort() returns DatatypeSort, not EnumSort
```
### Changes
- **`Sort.java`**: In `Sort.create()`, detect enum sorts at the
`Z3_DATATYPE_SORT` case by checking whether all constructors have arity
0 — matching Z3's own `util::is_enum_sort` logic in
`datatype_decl_plugin.cpp`. Return `EnumSort<>` when true,
`DatatypeSort<>` otherwise.
- **`EnumSort.java`**: Add package-private `EnumSort(Context ctx, long
obj)` constructor so an `EnumSort` can be instantiated from an existing
native sort handle (analogous to `DatatypeSort(Context ctx, long obj)`).
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Fixes the divergence in issue #7464: formulas involving `mod`/`div` by a
**variable** divisor could send `smt.arith.solver=6` into a
non-terminating nonlinear search.
Minimal reproducer (UNSAT, previously timed out; now solved in <0.5s):
```smt2
(declare-fun V () Int)
(declare-fun n () Int)
(declare-fun l () Int)
(assert (and (> V 0) (= 0 (mod n 2)) (= (div n 2) (div n l)) (= 0 (mod (div n l) V))))
(assert (distinct 0 (mod n V)))
(check-sat)
```
## Root cause
A variable-divisor `mod n V` is axiomatized by the Euclidean identity
`n = V*(n div V) + (n mod V)`. The `V*(n div V)` term is nonlinear, so
arith.solver=6
hands the problem to the nlsat/Gröbner branch, which branches on values
of `V` with no
termination bound and diverges.
## Fix
Add a **linear divisibility closure** lemma in `nla_divisions`:
> `mod(a, y) = 0 & x = c*a` (c an integer constant) ⟹ `mod(x, y) = 0`.
The emitted clause
```
(x - c*a != 0) \/ (mod(a, y) != 0) \/ (mod(x, y) = 0)
```
is a **tautology for every integer `c`**, so mining a candidate `c =
val(x)/val(a)` from
the current model can never be unsound. It is only emitted when all
three literals are
false in the current model, so the clause is a genuine
conflict/propagation and always
makes progress. This lets the theory refute the instance directly
instead of entering the
divergent nonlinear branch.
Variable-divisor `mod` terms were previously **not registered** in nla
at all; they are now
registered into a new `m_divisibility` list in `theory_lra`, so the
reasoner can pair a
violated `mod(x, y)` with a satisfied `mod(a, y)` of the same divisor.
## Changes
- `src/math/lp/nla_divisions.{h,cpp}` — new `m_divisibility` list
`{r=mod, x=dividend, y=divisor}`, `add_divisibility(...)`, and
`check_linear_divisibility()`; invoked from `divisions::check()`.
- `src/math/lp/nla_core.h`, `src/math/lp/nla_solver.{h,cpp}` —
forwarding of `add_divisibility`.
- `src/smt/theory_lra.cpp` — register variable-divisor `mod` into the
divisibility list.
## Validation
- `min.smt2` → `unsat` in 0.46s, minimized core → 0.15s (were timeouts).
- Soundness: 350 differential fuzz formulas (arith.solver=6 vs
arith.solver=2), **0 mismatches**.
- Spot checks correct (divisor-3 variant → unsat; non-divisible variants
→ sat).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
`decl_collector::visit_sort` did not collect sorts with `poly_family_id`
(type variables created via `mk_type_var` / `declare-type-var`), so
`solver::display` and `ast_pp_util::display_decls` never emitted type
variable declarations before referencing them — producing invalid
SMT-LIB2 output.
## Changes
- **`src/ast/decl_collector.h`**: added a dedicated `lim_svector<sort*>
m_type_vars` field (separate from `m_sorts`) with a `get_type_vars()`
getter; `reset()` clears it; `push()`/`pop()` maintain its scope.
- **`src/ast/decl_collector.cpp` — `visit_sort`**: sorts with
`poly_family_id` are now pushed to `m_type_vars` instead of `m_sorts`,
keeping type variables distinct from uninterpreted sorts:
```cpp
if (m.is_uninterp(n))
m_sorts.push_back(n);
else if (fid == poly_family_id)
m_type_vars.push_back(n);
```
- **`src/ast/ast_pp_util.h`**: added a `stacked_value<unsigned>
m_type_vars` cursor to track which type variables have already been
printed.
- **`src/ast/ast_pp_util.cpp` — `display_decls`**: emits
`(declare-type-var <name>)` for each collected type variable before
other sort declarations; `reset()`/`push()`/`pop()` maintain the new
cursor.
**Example** — given `(declare-type-var A)(declare-fun f (A) A)`, the
dump now correctly produces:
```smt2
(declare-type-var A)
(declare-fun f (A) A)
(assert ...)
```
The output round-trips cleanly through the Z3 parser.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `api_datalog` unit test was failing in CI with `"the logic has
already been set"`. Two consecutive regression tests shared a single
`Z3_context`, but both called `Z3_eval_smtlib2_string` with `(set-logic
HORN)` — the second call always fails because context logic state is
permanent.
## Changes
- **`src/test/api_datalog.cpp`**: Give each
`Z3_eval_smtlib2_string`-based regression test its own
`Z3_config`/`Z3_context`, destroyed immediately after the test block.
The outer context is retained only for the two tests that don't invoke
the SMT-LIB evaluator.
```cpp
// Before: both blocks shared `ctx`, second (set-logic HORN) always errored
Z3_string response = Z3_eval_smtlib2_string(ctx, chc1); // sets HORN logic
Z3_string response = Z3_eval_smtlib2_string(ctx, chc2); // ERROR: logic already set
// After: each block owns its context
Z3_config cfg2 = Z3_mk_config();
Z3_context ctx2 = Z3_mk_context(cfg2);
Z3_del_config(cfg2);
Z3_string response = Z3_eval_smtlib2_string(ctx2, chc2);
Z3_del_context(ctx2);
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`z3_add_install_tactic_rule` unconditionally called `file(WRITE)` during
CMake configure, updating `install_tactic.deps`'s mtime on every
reconfiguration — even when the content was identical. Since
`install_tactic.cpp` lists `install_tactic.deps` as a dependency, any
CMake reconfigure (e.g. touching `src/api/ml/CMakeLists.txt`) caused a
full rebuild of the tactic installation target.
## Change
- **`cmake/z3_add_component.cmake` — `z3_add_install_tactic_rule`**:
Replace unconditional `file(WRITE)` with a read-and-compare guard; the
deps file is only rewritten when its content actually changes.
```cmake
# Before
file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps" ${_tactic_header_files})
# After
set(_install_tactic_deps_file "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps")
if (EXISTS "${_install_tactic_deps_file}")
file(READ "${_install_tactic_deps_file}" _install_tactic_deps_old)
else()
set(_install_tactic_deps_old "")
endif()
if (NOT _install_tactic_deps_old STREQUAL "${_tactic_header_files}")
file(WRITE "${_install_tactic_deps_file}" "${_tactic_header_files}")
endif()
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
