Route all forall/exists creation in the TPTP frontend through a
with_weight1() helper so quantifiers use weight 1 instead of the
default 0. Improves smt.ho_matching on higher-order TPTP problems
(+26 net solved, fewer timeouts over the ^ benchmark set).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
`build-pyodide` failed because Python packaging assumed the wasm shell
artifact is always emitted as `build/z3.wasm`. In the failing run, the
expected file was absent, causing wheel build to abort during binary
copy.
- **Root cause handling in `setup.py`**
- In the emscripten path, add executable fallbacks (`z3.js.wasm`, `z3`)
alongside the canonical `z3.wasm`.
- During packaging, probe known output names in order and copy the first
match.
- **Stable wheel layout**
- Keep packaged artifact name stable as `bin/z3.wasm` regardless of
which build output variant exists.
- **Failure diagnostics**
- If no candidate exists, raise a `FileNotFoundError` listing all
attempted paths to make CI failures immediately actionable.
```python
executable_names = (EXECUTABLE_FILE,) + tuple(EXECUTABLE_FILE_FALLBACKS)
for executable_name in executable_names:
candidate = os.path.join(BUILD_DIR, executable_name)
if os.path.exists(candidate):
shutil.copy(candidate, os.path.join(BINS_DIR, EXECUTABLE_FILE))
break
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `WebAssembly Publish` workflow was failing in the `Publish` step
after a successful build/test pass. The failure was isolated to npm
publication, indicating the job was not running with the intended
release-scoped publish configuration.
- **Workflow wiring**
- Attach the `publish` job in `.github/workflows/wasm-release.yml` to
the existing `release` environment.
- Align the wasm npm publish path with the repository’s other release
publishing jobs that already rely on environment-scoped release
configuration.
- **Effect**
- Ensures the final `npm publish` step executes in the same release
context as other artifact publication jobs.
- Avoids publishing with default job context when release-specific
configuration is required.
```yaml
jobs:
publish:
name: Publish
runs-on: ubuntu-latest
environment: release
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`actions/setup-node` with `node-version: "lts/*"` requires fetching a
version manifest from GitHub's servers to resolve the alias. This
manifest request was returning a GitHub 500 error, causing the `Check`
job to fail at setup.
## Changes
- **`wasm.yml`, `wasm-release.yml`**: Replace `node-version: "lts/*"`
with `node-version: "22"` (current Active LTS), eliminating the remote
manifest lookup entirely.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@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>
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>
