Under `parallel.enable=true`, QF_BV workers that exhaust their per-cube
conflict budget (1000) are misclassified as unrecoverably incomplete,
causing the portfolio to return `unknown` in ~1 second instead of
escalating the budget and continuing.
## Root cause
`parallel_tactical.cpp` only recognizes `"max-conflicts-reached"` (the
`smt::context` spelling) as a signal to escalate the conflict budget.
SAT-core-backed solvers — which QF_BV workers use — report the same
condition as `"sat.max.conflicts"` (from
`sat_solver::reached_max_conflicts()`). The mismatch causes every QF_BV
cube attempt to fall through to `b.set_unknown()` instead of
`update_max_thread_conflicts()`.
## Fix
```diff
- if (reason != "max-conflicts-reached") {
+ if (reason != "max-conflicts-reached" && reason != "sat.max.conflicts") {
```
Both spellings now correctly route to the budget-escalation path. The
parallel `smt_parallel.cpp` path is unaffected — it owns `smt::context`
workers, which can only produce `"max-conflicts-reached"`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`IF_VERBOSE(0, ...)` in the parallel tactic's `l_undef` handler caused
the raw reason string (e.g. `sat.max.conflicts`) to be written
unconditionally to stderr, polluting output for any application
embedding libz3 that hits the conflict-budget give-up path.
## Change
- **`src/solver/parallel_tactical.cpp:2186`** — raise verbosity
threshold from `0` to `1`:
```cpp
// Before: fires at default verbosity, writes bare string to stderr
IF_VERBOSE(0, verbose_stream() << reason << "\n");
// After: only fires under -v:1
IF_VERBOSE(1, verbose_stream() << reason << "\n");
```
The reason string remains fully accessible via `(get-info
:reason-unknown)` and `set_reason_unknown` regardless of verbosity.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Validate a polymorphic declaration's arity before matching argument
sorts. This prevents
`Z3_mk_app` from reading past the declaration domain and makes both
too-few and too-many
arguments return `Z3_INVALID_ARG`.
Adds C API regression coverage for valid, too-few, and too-many
applications.
Fixes#10177.
## Testing
- `./build-release/test-z3 api`
- `./build-release/test-z3 /a` (92 passed)
- Standalone #10177 reproducer against the patched shared library
`string_hash`'s tail-byte handling reads bytes through plain `char`,
whose signedness is implementation-defined. On signed-char platforms
(x86_64 Linux, macOS) bytes ≥ `0x80` are sign-extended before entering
the hash state (e.g. `c+=((unsigned)data[10]<<24);` becomes `c +=
0xFF80xxxx` instead of `c += 0x0080xxxx`); on unsigned-char platforms
(Linux aarch64) they are not. Hashes of byte strings containing such
bytes therefore differ across platforms.
This is not just cosmetic: `mpz_manager::hash` feeds the digit arrays of
large numerals through `string_hash`, so AST hashes of bit-vector
constants like `(_ bv36028797018963968 64)` (= 2^55, whose digit bytes
include `0x80`) differ between architectures. AST hashes determine hash
table layouts throughout the solver, so preprocessing and search take
platform-dependent paths for byte-identical input.
Observed impact (Z3 4.15.3 release binaries as well as local gcc-13
builds, identical `.smt2` input generated by CBMC from the
[mldsa-native](https://github.com/pq-code-package/mldsa-native)
verification suite — quantifiers + arrays + bit-vectors, ~120k lines):
| instance | x86_64 | aarch64 |
|---|---|---|
| instance A | 643 s | 11.7 s |
| instance B | 22.8 s | 1578 s |
Tracing AST construction on both hosts showed the first divergence at
the registration of the numeral `2^55`, whose node hash was `2587296535`
on x86_64 vs `808470355` on aarch64, with identical mpz digit arrays;
from that point on, hash table iteration orders (and consequently
`ctx-simplify` steps, quantifier instantiation order, and case-split
order) diverge. With this patch, instance A solves in ~21 s on x86_64
(down from 643 s), matching the aarch64 behaviour class.
The fix casts the tail bytes to `unsigned char`, matching the
4-byte-chunk path (which is already signedness-independent via `memcpy`
into `unsigned`). Note that hash values on signed-char platforms change
for inputs containing bytes ≥ `0x80` (pure-ASCII symbol names are
unaffected).
(Found while investigating cross-platform proof-time instability
reported in diffblue/cbmc#8991.)
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
### Problem
The order of evaluation of function arguments is unspecified in C++
(arguments are indeterminately sequenced since C++17). Compilers use
this freedom differently:
```c++
static int f(int i) { printf("%d ", i); return i; }
static void g(int, int, int) { printf("\n"); }
int main() { g(f(1), f(2), f(3)); }
```
| compiler/target | output |
|---|---|
| gcc 13, x86_64 | `3 2 1` |
| gcc 13, aarch64 | `1 2 3` |
| clang 18, x86_64 | `1 2 3` |
Z3 has many call sites where **two or more arguments each create AST
nodes**, e.g. (before this PR, `bv_rewriter.cpp:876`):
```c++
result = m.mk_ite(c, m_mk_extract(high, low, t), m_mk_extract(high, low, e));
```
The two extract nodes are hash-consed and receive their AST ids in
evaluation order, so the id assignment differs between
compilers/targets. AST ids feed heuristic tie-breaking throughout the
solver (`bool_rewriter`'s `m_order_eq` equality-operand ordering,
id-based sorts in `array_rewriter`, case-split ordering, ...), so
**byte-identical input takes different solver paths depending on the
compiler and architecture z3 was built with**.
### Evidence
Investigated while chasing cross-platform proof-time instability in
CBMC/mldsa-native CI (diffblue/cbmc#8991), on byte-identical ~12 MB SMT2
instances (bit-vectors + arrays + quantifiers), with the `string_hash`
fix from #10163 applied to isolate this effect. Z3 4.15.3, gcc 13 on
x86_64 Linux and aarch64 Linux (Graviton):
* one instance: **17 s on x86_64 vs 1633 s on aarch64** (both `unsat`; a
sibling instance shows the reverse direction). Run-to-run within one
host: ±1 %.
* Instrumenting `ast_manager::register_node_core` with an order
fingerprint (running hash over `(node hash, node id)`) shows both
architectures construct **identical AST sequences up to registration
#41,789**, where x86_64 creates `(extract[0:0] #xFFFFFFFF)` before
`(extract[0:0] #xFFFFFFFE)` and aarch64 the other way around — from
identical call stacks at the `mk_ite`-over-two-`mk_extract` site quoted
above. All divergence between the two hosts flows from such events
(pointer/ASLR effects experimentally excluded: fingerprints are
invariant under `setarch -R` and across repeated runs).
* Sequencing that one site by hand moved the first divergence to
#248,118 — the analogous `mk_ite(c, mk_select(...), mk_select(...))`
site in `array_rewriter.cpp`. Sequencing that one, too, moved it to
#248,411, inside `nnf:👿:process_iff_xor` — i.e. the next layer of
the same onion.
* With the whole `ast/rewriter` layer swept (this PR), the instrumented
builds produce **identical AST construction traces on both architectures
throughout the entire rewriter phase** of this 546k-line industrial
instance; the first divergence left is the NNF one.
### Fix
Following the precedent of 37904b9e8, e113d39aa, 360193098, 93ff8c76d,
9b88aaf13 ("parameter evaluation order", `bool_rewriter`/`seq_rewriter`)
and the existing comments in `seq_rewriter.cpp` ("introduce temporaries
to ensure deterministic evaluation order..."), this PR hoists
AST-creating arguments into named temporaries with a defined evaluation
order, across `src/ast/rewriter/` — 126 call sites in 17 files. The
transformation is purely sequencing: it selects one of the two valid C++
evaluation orders and makes it the same everywhere. (Temporaries are raw
pointers in rewriter-local scope, matching the precedent commits;
nothing can trigger GC between creation and consumption.)
The sites were found with a small AST-argument scanner (statement-level
call sites whose argument list contains ≥ 2 top-level arguments that
each contain an AST-creating call); I am happy to share/contribute the
script. Known remaining work, deliberately out of scope here to keep the
diff reviewable:
* 41 sites in `src/ast/rewriter/` that need manual treatment (inside
`if` conditions, ternaries, or multi-statement expressions) — list
available on request;
* `src/ast/normal_forms/nnf.cpp` (`process_iff_xor`, proven divergent by
the trace above), ~7 sites in `src/ast/simplifiers/`, ~3 in
`src/ast/converters/`, ~9 in `src/ast/`;
* other theory/solver layers (`src/smt/`, `src/sat/`, ...) — divergences
there only matter after search starts, where paths have usually already
split, but a full sweep would be needed for bit-reproducibility across
compilers.
Together with #10163, this is a step towards z3 builds whose behaviour
does not depend on the compiler or target architecture — which matters
for verification CI that runs identical proofs on heterogeneous
platforms and expects comparable runtimes.
---------
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
## Summary
Fixes a completeness regression where a **satisfiable** floating-point
problem is answered `unknown`.
- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/3232
- **Benchmark:** `iss-3199/bug-1.smt2` (from
https://github.com/Z3Prover/z3/issues/3199)
### Divergence
```diff
--- bug-1.expected.out (expected)
+++ produced (current z3)
@@ -1 +1 @@
-sat
+unknown
```
The benchmark:
```smt2
(declare-fun x () (_ FloatingPoint 40 60))
(declare-fun y () (_ BitVec 8))
(assert (= ((_ fp.to_ubv 8) RTP x) y #x00))
(check-sat)
```
`(get-info :reason-unknown)` reports `"exponents over 31 bits are not
supported"`.
### Root cause
The problem is clearly `sat` (e.g. `x = 0.0`, `y = #x00`; and for any
out-of-range `x`, `fp.to_ubv` is unspecified so `= #x00` is
satisfiable). z3 bit-blasts and finds a model that assigns `x` a value
with a very large binary exponent (the `FloatingPoint 40 60` sort has a
40-bit exponent field). During model reconstruction,
`fpa_util::is_considered_uninterpreted` performs a range check by
calling `mpf_manager::to_sbv_mpq`, which **throws** `"exponents over 31
bits are not supported"` when the unpacked exponent does not fit into an
`int` (guard added in `eacde16b` for #3199). The tactic framework
catches that exception and turns the whole result into `unknown`,
instead of treating the conversion as out-of-range/unspecified.
### Fix
A finite FP value whose (unbiased) binary exponent is at least the
target bitwidth `bv_sz` has magnitude `>= 2^bv_sz` and therefore cannot
fit into a `bv_sz`-bit signed or unsigned integer — the conversion is
unspecified. Short-circuit this case using the exponent, before reaching
`to_sbv_mpq`, in the two range-check paths:
- `src/ast/fpa_decl_plugin.cpp`
(`fpa_util::is_considered_uninterpreted`) — return `true` (considered
uninterpreted / out of range).
- `src/ast/rewriter/fpa_rewriter.cpp` (`fpa_rewriter::mk_to_bv`) —
return the unspecified result.
This is consistent with the existing precise logic for every exponent it
covers (those values are already classified out-of-range), and it avoids
materializing an astronomically large integer. It does not affect
in-range or boundary conversions.
### Validation
Built z3 from this checkout (Python/`make` build) and re-ran the
benchmark:
- `z3 -T:20 inputs/issues/iss-3199/bug-1.smt2` now prints `sat`,
matching the recorded `bug-1.expected.out` oracle.
Additional manual sanity checks (all correct, no regression):
- `fp.to_ubv 8` of `5.0` -> `#x05`
- `fp.to_sbv 8` of `-5.0` -> `#xfb` (-5)
- `fp.to_sbv 8` of `128.0` -> unspecified (`sat`, out of range)
- `fp.to_sbv 8` of `-128.0` -> `#x80` (-128, in-range boundary
preserved)
Opened as a **draft** for human review.
> [!WARNING]
> <details>
> <summary>Firewall blocked 1 domain</summary>
>
> The following domain was blocked by the firewall during workflow
execution:
>
> - `pypi.org`
>> To allow these domains, add them to the `network.allowed` list in
your workflow frontmatter:
>
> ```yaml
> network:
> allowed:
> - defaults
> - "pypi.org"
> ```
>
> See [Network
Configuration](https://github.github.com/gh-aw/reference/network/) for
more information.
>
> </details>
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/29804584327)
· 314.9 AIC · ⌖ 20.3 AIC · ⊞ 10.7K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests)
<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.65, model: claude-opus-4.8, id:
29804584327, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/29804584327 -->
<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->
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>
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>
