The eight remaining README-listed agentic workflows (tptp-benchmark, qf-s-benchmark, smtlib-benchmark-finder, memory-safety-report, issue-backlog-processor, workflow-suggestion-agent, academic-citation-tracker, specbot-crash-analyzer) were failing with HTTP 401 because their agent/detection jobs depended on the missing/expired COPILOT_GITHUB_TOKEN repository secret.
Switch the agent and detection 'Execute Copilot CLI' steps from secrets.COPILOT_GITHUB_TOKEN to the S2STOKENS mechanism (github.token) and grant the required copilot-requests: write permission, matching the fix already applied to api-coherence-checker (#10223), code-simplifier (#10222), and release-notes-updater.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 8abbf1d4-fc99-4c10-ac89-3f0276ec8751
The `build-pyodide` CI job was failing because cibuildwheel's
`{project}` placeholder resolves to the **repository root**, not the
`package-dir` (`src/api/python`). The `test-command` in `pyproject.toml`
referenced `{project}/z3test.py`, which doesn't exist at the repo root.
## Change
**`src/api/python/pyproject.toml`**
```diff
-test-command = "python {project}/z3test.py z3"
+test-command = "python {project}/src/api/python/z3test.py z3"
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`set.size` reported `sat` for `(= 1 (set.size (set.union (set.singleton
1) (set.singleton 2))))` — a soundness bug, not just a performance gap.
The returned model did not satisfy the constraint.
## Root cause
In `theory_finite_set_size::run_solver()`, the cardinality sub-solver
enumerates propositional models of the membership structure and sums
fresh "slack" variables to represent `set.size`. All slacks were bounded
only by `>= 0`, so the arithmetic solver could freely assign `size = 1`
even when two distinct concrete members were independently asserted:
- **Model M₁** (`{1}` active, `{2}` inactive) — element 1 is a concrete
witness → slack must be `≥ 1`
- **Model M₂** (`{1}` inactive, `{2}` active) — element 2 is a concrete
witness → slack must be `≥ 1`
Without this enforcement: `slack₁ = 1, slack₂ = 0` satisfied `size = 1`.
With it: `size ≥ 2`.
## Changes
- **`src/smt/theory_finite_set_size.cpp`** — In `run_solver()`, after
retrieving the propositional model, check if exactly one singleton
equivalence class is active *and* a positive `set.in` assertion exists
for that element in an active set. If so, assert `slack >= 1` instead of
`>= 0`. This is sound: the concrete member witnesses the slot contains
at least one element.
- **`src/ast/rewriter/finite_set_axioms.cpp`** — Add the missing
monotonicity lower bounds for union:
```
|A ∪ B| ≥ |A| and |A ∪ B| ≥ |B|
```
These complement the existing upper bound `|A ∪ B| ≤ |A| + |B|` and let
the arithmetic solver derive `|{1} ∪ {2}| ≥ 2` directly from the
singleton axiom `|{i}| = 1`.
## Verified cases
| Query | Before | After |
|---|---|---|
| `(= 1 (set.size (set.union (set.singleton 1) (set.singleton 2))))` |
`sat` ❌ | `unsat` ✓ |
| `(= 2 (set.size (set.union (set.singleton 1) (set.singleton 2))))` |
`sat` ✓ | `sat` ✓ |
| `set.in 1 s ∧ set.in 2 s ∧ (= 1 (set.size s))` | `sat` ❌ | `unsat` ✓ |
| `¬(>= (set.size (set.union ...)) 2)` | `sat` ❌ | `unsat` ✓ |
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10232
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Fixes#10241
Among columns with a large value, the branching selection now prefers
the one whose absolute value is smallest. This avoids branching on ever
larger integers when better (smaller) options are available.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 1b264f0c-4bcc-4790-a3b8-5f038cc71f89
`memory_max_size` OOMs were recoverable at `check_sat` time
(`Z3_L_UNDEF` + error handler), but `Z3_solver_reset` could still
terminate the process with an uncaught `out_of_memory_error`. This
change keeps reset on the C API error-reporting path instead of letting
teardown allocations trip the same hard limit.
- **Reset path hardening**
- `Z3_solver_reset` now performs solver teardown under a temporary
suspension of the global memory cap, then restores the previous cap
afterward.
- This avoids aborts when allocator accounting is still above
`memory_max_size` at reset time.
- **Memory manager support**
- Added `memory::get_max_size()` to snapshot/restore the active cap
precisely.
- **Regression coverage**
- Extended `src/test/memory.cpp` with a focused scenario that trips
`Z3_MEMOUT_FAIL` and then calls `Z3_solver_reset` under a non-throwing
error handler, covering the previously aborting recovery path.
```cpp
struct scoped_memory_limit_reset {
size_t m_prev_max;
scoped_memory_limit_reset(): m_prev_max(memory::get_max_size()) {
memory::set_max_size(0);
}
~scoped_memory_limit_reset() {
memory::set_max_size(m_prev_max);
}
} scoped_max_memory;
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10250
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
On scheduled runs, `github.event.inputs.*` is empty, so the `||
fallback` values in the `env` block are what actually get used — but two
of them diverged from the declared `workflow_dispatch` input defaults.
## Changes
- `Z3_RUNTIME_ARGS`: scheduled fallback was `smt.ho_matching=true`;
corrected to `smt.ho_matching=false` to match the input default
- `FSTAR_OTHERFLAGS`: scheduled fallback was `''`; corrected to
`--split_queries on_failure --log_failing_queries --ext higher_order_smt
--proof_recovery` to match the input default
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
There are no `global`s in browser context. `globalThis` applied to both
browser and node.
---------
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
The `elim-term-ite` **simplifier** (via `set-simplifier` /
`addSimplifier`) was unsound: it reported `sat` with a spurious model on
trivially unsat inputs by replacing term-ITEs with fresh auxiliary
variables but never asserting their defining constraints, leaving them
unconstrained.
```smt2
(declare-const x Real)
(declare-const b Bool)
(set-simplifier elim-term-ite)
(assert (and (> x 10.0) (< x (ite b 1.0 2.0))))
(check-sat)
; was: sat (x=11 — spurious)
; now: unsat
```
## Changes
- **`src/ast/normal_forms/elim_term_ite.cpp` — `reduce_app`**: When
`defined_names::mk_name` returns `false` (name already cached for a
given ITE), the old code returned `BR_FAILED`, leaving the ITE
unreplaced in subsequent formulas. Now unconditionally sets `result =
new_r` and returns `BR_DONE`, mirroring the tactic version's behavior.
- **`src/ast/simplifiers/elim_term_ite.h` — `reduce()`**: After
rewriting each formula, the newly created definitions accumulated in
`m_rewriter.new_defs()` are now added to `m_fmls`. Previously these were
silently discarded, making auxiliary variables completely unconstrained.
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10239
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `build-pyodide` CI job has been failing consistently because
`_copy_bins()` cannot find the z3 executable after a successful cmake
build.
**Root cause**: `pyproject.toml`'s `[tool.pyodide.build]` sets `ldflags
= "... -sSIDE_MODULE=1"`. pyodide-build injects this into the
environment `LDFLAGS`, which cmake propagates to
`CMAKE_EXE_LINKER_FLAGS`. The z3 shell target is therefore linked as a
WASM side-module — emscripten emits a `.wasm` file whose name doesn't
match any of the expected paths (`z3.wasm`, `z3.js.wasm`, `z3`):
```
error: Could not find any executable in build directory. Tried:
- .../build/z3.wasm
- .../build/z3.js.wasm
- .../build/z3
```
**Fix** — `src/api/python/setup.py`:
- **`_configure_z3()`**: pass `Z3_BUILD_EXECUTABLE=FALSE` to cmake when
`IS_PYODIDE`, so the shell target is never built
- **`_copy_bins()`**: guard BINS_DIR creation and executable copy behind
`if not IS_PYODIDE`
- **`setup()`**: set `data_files=[]` for Pyodide builds (no executable
to package)
The z3 CLI isn't usable in a Pyodide environment anyway — Python users
only need `libz3.so` via ctypes, which continues to be built and
packaged correctly. Non-Pyodide builds (Linux/macOS/Windows) are
unaffected.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`euf-completion` crashed with an assertion violation on any unary
negation of a nonlinear product (e.g. `(= (- (* a a)) a)`), because
`register_node` hit `NOT_IMPLEMENTED_YET()` in the `is_uminus` branch.
## Changes
- **`src/ast/euf/euf_arith_plugin.cpp`**: Replace
`NOT_IMPLEMENTED_YET()` with the natural rewrite `-x ↦ (-1) * x`,
consistent with how subtraction is already handled (`x - y ↦ x + (-1 *
y)`). Creates the `-1` numeral of the correct sort, builds the
multiplication enode, and merges via `push_merge`.
- **`src/test/euf_arith_plugin.cpp`**: Add `test4` exercising the exact
repro shape — negation of a nonlinear product merged with a variable.
```smt2
(declare-const a Real)
(set-simplifier euf-completion)
(assert (= (- (* a a)) a))
(check-sat) ; previously: ASSERTION VIOLATION — now: sat
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10240
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Refactors the constraint/monic verification loops in `nra_solver.cpp`
introduced by #10230 to reduce nesting and improve readability. No
functional change.
### Changes
- **Early-continue guards**: Replace `if (!check_X(ci)) { if
(coi.contains(ci)) { ... } return l_undef; }` with `if (check_X(ci))
continue;` so the failure path reads linearly
- **Explicit braces**: Add braces to the constraint loop (monic loop
already had them), making both loops consistent
- **Condensed comment**: Collapse 6-line COI explanation to one line
```cpp
// Before
for (lp::constraint_index ci : lra.constraints().indices())
if (!check_constraint(ci)) {
// nlsat only solves over the cone-of-influence (COI) subset
// of constraints, so constraints outside the COI may be
// legitimately violated by the nlsat model. Only a violation
// of a COI constraint indicates a genuine nlsat bug; a
// non-COI violation is benign, so fall back to l_undef
// quietly without emitting diagnostics.
if (m_coi.constraints().contains(ci)) { ...; UNREACHABLE(); }
return l_undef;
}
// After
for (lp::constraint_index ci : lra.constraints().indices()) {
if (check_constraint(ci)) continue;
// Non-COI constraint violations are benign; only COI violations indicate a bug.
if (m_coi.constraints().contains(ci)) { ...; UNREACHABLE(); }
return l_undef;
}
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10235
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Fixes a snapshot-regression divergence reported in [Z3Prover/bench
discussion #3421](https://github.com/Z3Prover/bench/discussions/3421).
- **Benchmark:** `iss-6061/delta.smt2` (from
https://github.com/Z3Prover/z3/issues/6061)
- **Recorded oracle:** `sat`
- **Current (buggy) z3 output:** a large `constraint 19 violated` /
`number of constraints = 602` diagnostic dump (and, in an
assertion-enabled build, an `UNEXPECTED CODE WAS REACHED` abort at
`nra_solver.cpp:245`).
### Divergence diff
```diff
--- delta.expected.out (expected)
+++ produced (current z3)
@@ -1 +1,334 @@
-sat
+constraint 19 violated
+number of constraints = 602
+(0) j0 >= 1
+(1) j0 <= 1
...
+(19) j8 + j10 > 0
+(20) j8 + j10 >= 0
... (160 more diff line(s))
```
## Root cause
`nra_solver:👿:check()` runs nlsat over only the **cone-of-influence
(COI)** subset of the LRA constraints. When nlsat returns `l_true`, the
resulting model is validated against **all** LRA constraints/monics.
Constraints outside the COI can be *legitimately* violated by that
partial model — nlsat never assigned the variables that only occur
outside the COI.
This was previously handled by commit `8a146a92e` ("replace UNREACHABLE
with VERIFY for non-COI constraint/monic violations", fixes#8883). The
Nl2lin rewrite (`6fb68ac01`) reintroduced an **unconditional**
`UNREACHABLE()` plus an `IF_VERBOSE(0, ...)` diagnostic dump for *any*
violated constraint/monic, reverting that fix.
For `delta.smt2`, constraint 19 (`j8 + j10 > 0`) is **not** in the COI
(confirmed by instrumentation: `in_coi=0`). In a release build the
reintroduced `UNREACHABLE()` is a no-op, so z3 correctly falls back to
`l_undef` and ultimately answers `sat` — but the `IF_VERBOSE(0, ...)`
dump still leaks to stderr, and the snapshot capture merges stderr into
stdout, breaking the recorded oracle. In an assertion-enabled build the
`UNREACHABLE()` aborts outright.
## Fix
Only treat a violated constraint/monic as a genuine nlsat bug (verbose
dump + `UNREACHABLE()`) when it is actually in the COI. A non-COI
violation is benign, so return `l_undef` quietly without emitting any
diagnostics. This restores the intent of `8a146a92e` and additionally
stops the verbose dump from leaking for the benign case.
```cpp
if (!check_constraint(ci)) {
if (m_coi.constraints().contains(ci)) {
IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
}
return l_undef;
}
```
(analogous change for the monic check).
## Validation
Rebuilt z3 from this branch (`make -j`) and re-ran the benchmark exactly
as the snapshot capture does (combined stdout+stderr, `-T:20`):
```
$ z3 -T:20 inputs/issues/iss-6061/delta.smt2 2>&1
sat
```
The combined output is now exactly `sat`, byte-for-byte matching the
recorded `delta.expected.out` oracle. Basic SMT solving sanity-checked
and unaffected.
Closes the divergence in Z3Prover/bench discussion #3421.
> [!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/30150856651)
· 239.4 AIC · ⌖ 20.1 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:
30150856651, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/30150856651 -->
<!-- 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>
The `agent` job in the API Coherence Checker workflow was failing every
run with HTTP 401 because it depended on a `COPILOT_GITHUB_TOKEN`
repository secret that was missing/expired.
## Changes
- **`api-coherence-checker.lock.yml`**: Switch `agent` and `detection`
jobs from legacy `secrets.COPILOT_GITHUB_TOKEN` to the S2STOKENS
mechanism (service-to-service token exchange via the standard
`github.token`):
```yaml
# Before (agent and detection Execute Copilot CLI steps)
COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
# no S2STOKENS
# After
COPILOT_GITHUB_TOKEN: ${{ github.token }}
S2STOKENS: true
```
- **Permissions**: Replace broad `permissions: read-all` on the `agent`
job (and add to `detection`) with minimal explicit scopes required for
S2STOKENS:
```yaml
permissions:
contents: read
copilot-requests: write # required for S2STOKENS token exchange
```
This brings `api-coherence-checker` in line with the pattern already
used by `code-simplifier` and `release-notes-updater`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Problem
egressions/smt2/10220.smt2 (datatype + nonlinear integer arithmetic over
`SBVRational`, expected `unsat`) crashes with an ACCESS_VIOLATION (issue
#10220). The crash only occurs with the default `theory_lra`
(`arith.solver=6`) and is independent of `arith.nl`.
## Root cause
Debug build gives a clean stack: a `SASSERT(n)` violation / null
dereference in `smt::relevancy_propagator_imp::is_relevant_core` reached
from `theory_lra::set_conflict_or_lemma ->
ctx().mark_as_relevant(literal)`. The literal's boolean variable has
`bool_var2expr(v) == nullptr`.
Tracing showed the same nla lemma core being processed twice — first at
scope 6, then, after a backtrack, again at scope 3 — where the bound
atoms internalized to build the lemma had their boolean variables
deleted by the pop:
\\\
SCOL scope=6 core=[32 27 35 30 6 14 ]
SCOL scope=3 core=[32*NULL* 27 35*NULL* 30 6 14 ]
\\\
Commit d60d6a066 (*add incremental propagate for nla to retain some
propagation lemmas*) removed the `clear()` call from `core::propagate()`
(the final-check path) while adding a symmetric
`incremental_propagate()` that keeps it. Consequently `m_lemmas`
generated at a deep scope survived a backtrack and were replayed at a
shallower scope, referencing deleted bool vars.
## Fix
Restore `clear()` at the start of `core::propagate()`. Both
`propagate()` and `incremental_propagate()` consume their lemmas
immediately via `add_lemmas()`, so lemmas never need to survive across
calls; starting each final-check propagation from a fresh lemma set
removes the stale replay.
## Validation
- `regressions/smt2/10220.smt2` -> `unsat` (was ACCESS_VIOLATION)
- `FStar.Math.Euclid-1` still `unsat`
- `FStar.Math.Euclid-2/-3` unchanged (already `unknown` on master,
verified against the pre-fix binary)
Fixes#10220.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
The `Code Simplifier` workflow’s `agent` job was failing before any
analysis ran because Copilot requests were not authorized in the
workflow context. The generated lock workflow therefore executed against
a stale auth model and consistently hit `HTTP 401` during agent startup.
- **Root cause**
- The workflow frontmatter did not grant `copilot-requests: write`,
which is required for Copilot-backed agent execution in Actions.
- **Workflow change**
- Added `copilot-requests: write` to
`.github/workflows/code-simplifier.md`.
- **Generated workflow update**
- Recompiled `code-simplifier.lock.yml` so the executable workflow
matches the new permission model.
- This updates the Copilot invocation path from the old secret-based
flow to the GitHub Actions token-based flow used by current gh-aw
compilation.
- **Effective delta**
```yaml
permissions:
contents: read
issues: read
pull-requests: read
copilot-requests: write
```
- **Lockfile effect**
```yaml
# before
COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
# after
COPILOT_GITHUB_TOKEN: ${{ github.token }}
S2STOKENS: true
```
This keeps the change scoped to the failing workflow while aligning the
checked-in lock file with the auth mechanism expected by the current
Agentic Workflows toolchain.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
MinGW silently ignores `#pragma comment(lib, ...)` (MSVC-only), so
linker errors like missing `dbghelp` symbols go undetected until a
downstream user hits them. No CI coverage existed for MinGW on Windows.
## Changes
- **`.github/workflows/Windows.yml`**: New `mingw-build` job using MSYS2
UCRT64 (`mingw-w64-ucrt-x86_64-gcc`) that builds Z3 via `cmake -G Ninja`
and runs `test-z3 /a`, exercising the full link step under MinGW on
every push/PR to master.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
`lp::lar_solver::init_model()` (`src/math/lp/lar_solver.cpp`) picks an
infinitesimal `delta` that maps every distinct rational-pair column
value `(x, y)` to a *distinct* scalar `x + delta*y`, halving `delta`
whenever a collision is detected. The previous implementation rebuilt
**both** the set of distinct pairs and the set of scalars from a full
O(n) pass over all columns on *every* halving, and the pair set is
entirely independent of `delta`.
## Change
- Build the delta-invariant set of distinct column pairs
(`m_set_of_different_pairs`) **once**, before the halving loop.
- On each halving, only rebuild the scalar set by iterating over the
**distinct pairs** rather than rescanning all `n` columns (including
duplicates).
The collision test and the selected `delta` are unchanged: the loop
still halves `delta` whenever the number of distinct scalars is less
than the number of distinct pairs, and terminates when the scalar map is
injective. The early-`break` versus end-of-pass check produce the same
`delta` sequence because a size discrepancy on a full pass is exactly
the injectivity-failure condition.
## Cost argument
Let `n` = column count and `D` = number of *distinct* column pairs (`D ≤
n`), and `H` = number of halvings.
- Before: `O(H · n · log D)` — every halving re-inserts all `n` columns
into both sets.
- After: `O(n · log D + H · D · log D)` — the pair set is built once;
each halving touches only the `D` distinct pairs.
This removes the repeated full rescan from the halving loop and skips
redundant work for duplicate columns, turning a per-halving O(n) rebuild
into a one-time cost plus O(D) per halving.
## Evidence
Profiled under callgrind (deterministic instruction counts),
differential correctness preserved, static-analysis hygiene clean:
- Target function self-instructions: **2,695,433,533 → 2,084,074,808**
(−22.7%).
- Total program instructions ratio: **0.904** (−9.6%).
- Wall-time speedup: **~6.1%**.
- Differential correctness: identical results (no mismatches).
Logic class exercised: **QF_LRA / linear real arithmetic** model
construction.
<!-- gh-aw-workflow-id: coz3-deepperf-fix -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/coz3-deepperf-fix -->
---------
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>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`EXECUTABLE_FILE_FALLBACKS` was referenced on all platforms in
`_copy_bins()` but only defined in the `emscripten` and `else` (Linux)
branches — causing a `NameError` crash on Windows and macOS wheel
builds.
## Change
Add `EXECUTABLE_FILE_FALLBACKS = []` to the missing platform branches in
`src/api/python/setup.py`:
```python
if BUILD_PLATFORM in ('sequoia','darwin', 'osx'):
LIBRARY_FILE = "libz3.dylib"
EXECUTABLE_FILE = "z3"
EXECUTABLE_FILE_FALLBACKS = [] # added
elif BUILD_PLATFORM in ('win32', 'cygwin', 'win'):
LIBRARY_FILE = "libz3.dll"
EXECUTABLE_FILE = "z3.exe"
EXECUTABLE_FILE_FALLBACKS = [] # added
elif BUILD_PLATFORM in ('emscripten',):
...
EXECUTABLE_FILE_FALLBACKS = ["z3.js.wasm", "z3"]
else:
...
EXECUTABLE_FILE_FALLBACKS = []
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
The `Ubuntu build - python make - MT` job was failing in unit test
`max_reg` under debug configuration due to a shape-sensitive internal
NLA assertion. This PR updates the test’s nonlinear expressions to an
equivalent construction that avoids the failing path.
- **Root issue in CI path**
- `test_max_reg` built BNH objective/constraints with subtraction forms
that triggered a debug-only monic-check assertion in NLA internals.
- **Targeted test-only normalization**
- In `src/test/api.cpp` (`test_max_reg`), rewrote squared-difference
terms to constant-first subtraction forms (mathematically equivalent).
- Updated:
- `f2` construction
- circle/offset constraints in `mk_max_reg()`
- **No solver behavior change**
- This is a unit-test expression-shape change only; production solver
code is untouched.
```cpp
// before
Z3_ast f2 = mk_add(mk_sq(mk_sub(x1, mk_real(5))), mk_sq(mk_sub(x2, mk_real(5))));
Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx,
mk_add(mk_sq(mk_sub(x1, mk_real(5))), mk_sq(x2)), mk_real(25)));
// after
Z3_ast f2 = mk_add(mk_sq(mk_sub(mk_real(5), x2)), mk_sq(mk_sub(mk_real(5), x1)));
Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx,
mk_add(mk_sq(mk_sub(mk_real(5), x1)), mk_sq(x2)), mk_real(25)));
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
PR #10180 moved nonlinear bound propagation to final_check only, removing
the eager propagate_nla() from the search-time propagation path. This left
E-matching without nla-implied bound facts during search, causing an
instantiation blowup on number-theory goals (e.g. FStar.Math.Euclid),
which exhausted rlimit and returned unknown on queries previously proved.
Re-run propagate_nla() before propagate_bounds_with_lp_solver() in the
l_true case of propagate_core so tightened nonlinear bounds are surfaced
to the SMT core during search. Recovers FStar.Math.Euclid-1/-2.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
With `(set-option :smtlib2_compliant true)`, Z3 disables implicit
Int→Real coercions. When the LP solver generates Gomory cuts/bounds over
expressions that mix Int and Real LP variables (as happens when
`to_real(n)` is internalized — both `to_real(n)` as Real and `n` as Int
are registered as LP vars), `coeffs2app` was constructing
`mk_mul(Real_numeral, Int_expr)`. Without implicit coercions,
`check_args` throws an `ast_exception` that bubbles up through
`cmd_context::check_sat()` as `l_undef`, producing a spurious `unknown`
instead of `unsat`.
## Changes
- **`src/smt/theory_lra.cpp` — `coeffs2app`**: Before building each
product term, coerce `o` to Real via `a.mk_to_real(o)` when `!is_int &&
a.is_int(o)`. This makes the sort explicit rather than relying on
implicit coercions.
- **`src/test/smt2print_parse.cpp`**: Regression test for the exact
formula from the issue — verifies the result is `unsat` (not `unknown`)
when `smtlib2_compliant` is set.
```smt2
(set-option :smtlib2_compliant true)
(set-logic ALL)
(declare-datatype SBVRational ((SBV.Rational (sbv.rat.numerator Int) (sbv.rat.denominator Int))))
; ... mixed Int/Real via to_real ...
(check-sat)
; was: unknown (:reason-unknown "Sort mismatch at argument #2 for function * (Real Real) Real supplied sort is Int")
; now: unsat
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10166
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
spacer_qel could report a bound variable as eliminated (removing it from
vars) while do_qel/qel_project simplifications still left an occurrence of
it in the formula. The variable then surfaced in the qe2 result as a
fresh, undeclared constant (e.g. X!0), so asserting the result failed with
"unknown constant".
After qel_project, scan the formula for any originally-to-eliminate
variable that was dropped from vars yet still occurs in fml, and route it
through other_vars so the existing model-based projection/substitution
replaces it with its model value. The result is logically equivalent and
mentions only declared symbols.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
The drain_backtrack destructor added in d247df72a called
m_backtrack.pop(), which does not exist on ptr_vector (breaking the
build) and, even as pop_back(), would only drop the work item without
popping the backtracking trail scope it owns - reintroducing the
trail-scope leak that #10196 fixed. Use backtrack(), which pops the trail
scope for in_scope items and then removes the item.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
Building Z3 on Windows with MinGW (`mingw-w64-ucrt-x86_64-gcc`) fails
with undefined references to `SymSetOptions`, `SymInitialize`,
`SymFromAddr`, and `SymGetLineFromAddr64` from the DbgHelp library used
in `src/util/debug.cpp` for stack backtraces.
The existing `#pragma comment(lib, "dbghelp.lib")` in `debug.cpp` is an
MSVC-only extension — MinGW silently ignores it, so `dbghelp` is never
passed to the linker.
## Changes
- **`CMakeLists.txt`**: Append `dbghelp` to `Z3_DEPENDENT_LIBS` in the
`WIN32` platform block. This feeds the library to both the `libz3` and
`shell` link steps regardless of compiler.
- **`src/util/debug.cpp`**: Guard the `#pragma comment` with `#ifdef
_MSC_VER` to make the MSVC-only intent explicit.
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10171
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The higher-order matcher shares the solver's trail stack. On early-exit
paths (resource/rlimit reached via m.inc(), or search budget exhausted)
work items were left on m_backtrack with their pushed scopes never popped,
leaking a trail scope. This desynchronized the trail scope count from the
solver scope level and later tripped SASSERT(ilvl <= m_scope_lvl) /
unsound backtracking in smt::context::reinit_clauses.
Restore the trail before exit on every path using an RAII guard
(scoped_trail_level) and drain the backtrack stack after the main search
loop so m_backtrack is left empty for the next call. This avoids wrapping
large blocks in try/catch (which would mask underlying bugs such as
creating non-well-sorted expressions) while still guaranteeing the trail
is restored on both normal and exceptional exits. The sort-mismatch check
and UNREACHABLE() in refine_ho_match are preserved so ill-sorted terms
remain surfaced rather than silently discarded.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
These tests fed a fixed SMTLIB2 string to Z3_eval_smtlib2_string and checked
a sat/unsat verdict. They are now data-driven regression files under
z3test regressions/smt2 (with .expected.out ground truth), so remove them
from the C++ test suite:
- fpa.cpp: removed entirely (all tests transferred)
- seq_rewriter.cpp: removed the two seq.foldl model-validation tests
- simplifier.cpp: removed the sat.smt QF_UFBV predicate model-validation test
- mod_factor.cpp: removed the const-array store-chain unsat test
The API-constructed mod/idiv internalization-order tests remain in mod_factor.cpp.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
Remove unused m_fixed_val member variable from undo_fixed_column.
undo_fixed_column is allocated in a region/trail allocator where C++
destructors are not invoked when objects are popped/reclaimed. Storing
an mpq instance (which can allocate heap memory for multi-precision
numbers) inside a region-allocated object causes a memory leak that is
flagged by ASAN.
m_fixed_val was never used in undo() or elsewhere in the struct.
Removing it completely eliminates the ASAN finding, avoids unnecessary
mpq copies, and is entirely safe.
…icts
Add core::optimize_nl_bounds() (gated by arith.nl.optimize_bounds) which
runs LP max/min over monomial leaf variables inside core::propagate(),
analogous to solver=2's max_min_nl_vars, so nla (arith.solver=6) can
detect cross-nested conflicts previously missed. Collect improved bounds
first, then apply them and re-establish feasibility once; reconcile the
core solver via find_feasible_solution before the raw maximize solves to
preserve inf_heap_is_correct(). Skip null witnesses in
get_dependencies_of_maximum for implied/unconditional bounds.
On FStar-UInt128-divergence solver=6 this yields unsat in 2
final-checks, seed-insensitive (seeds 1-10).
Copilot-Session: ac36bb84-de91-4e6c-86df-6008c7396ceb
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: ac36bb84-de91-4e6c-86df-6008c7396ceb
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
## Summary
Include the equal-width case in symbolic unsigned BV-to-FP exponent
saturation,
preventing positive exponents from being interpreted as negative by the
rounder.
Adds regression coverage for overflow and in-range values.
Fixes#7135.
## Testing
- `./build-review/test-z3 fpa`
- `./build-review/test-z3 /a` (92 passed)
- Symbolic-versus-numeral differential matrix (50 cases across five
width boundaries and all rounding modes)
- Exact-head fork `CI` and `OCaml Binding CI` workflows (passed)
`qe2` could produce a nonlinear term (e.g. `(* x x1)`) when eliminating
quantifiers from a purely linear LIA formula. The result was logically
equivalent but broke downstream consumers expecting QF_LIA output.
**Root cause**
In `term_graph::term_lt`, numeric values were unconditionally ranked
*lower* than uninterpreted constants when selecting equivalence class
representatives. During model-based projection, ITE processing adds the
model literal `(= x1 2)` to the term graph, merging `x1` and `2` into
one equivalence class with `x1` elected as representative. Any
expression containing the coefficient `2` — e.g. `(* 2 x)` from `x + x`
— then gets rewritten as `(* x1 x)`, a nonlinear product of two free
variables.
**Fix** (`src/qe/mbp/mbp_term_graph.cpp` — `term_lt`)
When both terms are 0-argument and differ in value-ness, prefer the
*value* as class representative **unless** the non-value is a variable
slated for elimination (where `refine_repr_class` will later replace it
with a value anyway). This prevents free variables from displacing
numeric coefficients.
```smt2
; Before fix
(apply qe2)
; => (or (not (= x1 2)) (not (= (+ y (* (- 1) x x1)) 0)) (not (= y 0)))
; ^^^^^^^^^^^ nonlinear
; After fix
; => (or (not (= x1 2)) (not (= x 0)) (not (= y 0))) ; fully linear
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
This PR completes the job started by
https://github.com/Z3Prover/z3/pull/10169. It adds `-Wextra-semi` to the
set of CLANG_ONLY_WARNINGS, and adds
```
START_DISABLE_EXTRA_SEMI_WARNING;
...macro invocations with trailing semis...
END_DISABLE_WARNING;
```
around all the blocks of macro invocations that provoked warnings.
(Additionally, in realclosure.h, there was one block of macro
invocations that did *not* follow the trailing-semi pattern; changed
that to look like all the others).
Bumps [shell-quote](https://github.com/ljharb/shell-quote) from 1.8.4 to
1.10.0.
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a
href="https://github.com/ljharb/shell-quote/blob/main/CHANGELOG.md">shell-quote's
changelog</a>.</em></p>
<blockquote>
<h2><a
href="https://github.com/ljharb/shell-quote/compare/v1.9.0...v1.10.0">v1.10.0</a>
- 2026-07-10</h2>
<h3>Merged</h3>
<ul>
<li>[New] <code>parse</code>: add opt-in <code>splitUnquoted</code>
option for shell field-splitting of unquoted expansions <a
href="https://redirect.github.com/ljharb/shell-quote/pull/1"><code>[#1](https://github.com/ljharb/shell-quote/issues/1)</code></a></li>
</ul>
<h3>Commits</h3>
<ul>
<li>[Fix] <code>parse</code>: match nested <code>${...}</code> braces so
nested parameter expansion is consumed as one substitution <a
href="c0842c8a7a"><code>c0842c8</code></a></li>
<li>[Tests] <code>parse</code>: pin single-quote literalness and
unmatched-quote handling <a
href="a0d03e35c8"><code>a0d03e3</code></a></li>
<li>[readme] remove the space in js code fences so evalmd evaluates them
<a
href="2116fa36ae"><code>2116fa3</code></a></li>
<li>[Tests] <code>quote</code>: pin conservative escaping of
<code>=</code>, <code>@</code>, <code>^</code>, <code>,</code>,
<code>:</code>, <code>!</code> (<a
href="https://redirect.github.com/ljharb/shell-quote/issues/11">#11</a>)
<a
href="1c36f3ff77"><code>1c36f3f</code></a></li>
<li>[readme] document that <code>quote</code> outputs POSIX quoting, not
<code>cmd.exe</code>/PowerShell <a
href="100e96e0ff"><code>100e96e</code></a></li>
<li>[readme] document <code>parse</code>'s supported parameter-expansion
subset <a
href="e1c75cd6e4"><code>e1c75cd</code></a></li>
<li>[Fix] <code>parse</code>: a backslash inside single quotes must not
escape the closing quote <a
href="5d460a332b"><code>5d460a3</code></a></li>
<li>[readme] fix stale example outputs <a
href="2de86f5d44"><code>2de86f5</code></a></li>
<li>[Tests] <code>quote</code>: pin that a backslash with whitespace is
not doubled in single quotes (<a
href="https://redirect.github.com/ljharb/shell-quote/issues/14">#14</a>)
<a
href="190e236bcf"><code>190e236</code></a></li>
<li>[readme] <code>quote</code>: use output verbatim; do not re-quote it
(<a
href="https://redirect.github.com/ljharb/shell-quote/issues/11">#11</a>)
<a
href="1b364683b1"><code>1b36468</code></a></li>
<li>[Refactor] <code>parse</code>: fix swapped
<code>SINGLE_QUOTE</code>/<code>DOUBLE_QUOTE</code> variable names <a
href="801af5c935"><code>801af5c</code></a></li>
<li>[types] fix an error TS v6 ignores but v7 fails on <a
href="59bbf8b81b"><code>59bbf8b</code></a></li>
<li>[Dev Deps] update <code>@arethetypeswrong/cli</code>,
<code>evalmd</code> <a
href="a04d47516e"><code>a04d475</code></a></li>
<li>[Dev Deps] update <code>@arethetypeswrong/ci</code>,
<code>eslint</code> <a
href="d390f9a92b"><code>d390f9a</code></a></li>
<li>[Tests] <code>quote</code>: the tilde test escapes every
<code>~</code>, not just a leading one (<a
href="https://redirect.github.com/ljharb/shell-quote/issues/9">#9</a>)
<a
href="617d119795"><code>617d119</code></a></li>
</ul>
<h2><a
href="https://github.com/ljharb/shell-quote/compare/v1.8.4...v1.9.0">v1.9.0</a>
- 2026-06-24</h2>
<h3>Commits</h3>
<ul>
<li>[New] add types <a
href="dca6e21a02"><code>dca6e21</code></a></li>
<li>[Dev Deps] update <code>eslint</code> <a
href="9aa9e8f609"><code>9aa9e8f</code></a></li>
<li>[Fix] <code>parse</code>: finalize tokens in linear time
(GHSA-395f-4hp3-45gv) <a
href="7ff5488599"><code>7ff5488</code></a></li>
<li>[actions] update workflows <a
href="75e849741f"><code>75e8497</code></a></li>
<li>[actions] Windows + node 4/6/7: pin eslint to 9 before install,
since npm 2/3 cannot stage eslint 10<code>@types/esrecurse</code> <a
href="3fb739de44"><code>3fb739d</code></a></li>
<li>[actions] retry <code>npm install</code> on Windows to survive npm
2/3 staging-rename flake <a
href="abe0163293"><code>abe0163</code></a></li>
<li>[actions] Windows + node 5/7: install deps with a modern node <a
href="b4bafa2e7e"><code>b4bafa2</code></a></li>
<li>[Fix] <code>quote</code>: escape leading <code>~</code> to prevent
shell tilde-expansion <a
href="7a76c1a12d"><code>7a76c1a</code></a></li>
<li>[Dev Deps] update <code>auto-changelog</code>, <code>tape</code> <a
href="7184b4458b"><code>7184b44</code></a></li>
<li>[Dev Deps] apparently <code>jackspeak</code> is no longer in the
graph <a
href="9ba368a405"><code>9ba368a</code></a></li>
</ul>
</blockquote>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="64988d9a0e"><code>64988d9</code></a>
v1.10.0</li>
<li><a
href="617d119795"><code>617d119</code></a>
[Tests] <code>quote</code>: the tilde test escapes every <code>~</code>,
not just a leading one (<a
href="https://redirect.github.com/ljharb/shell-quote/issues/9">#9</a>)</li>
<li><a
href="59bbf8b81b"><code>59bbf8b</code></a>
[types] fix an error TS v6 ignores but v7 fails on</li>
<li><a
href="190e236bcf"><code>190e236</code></a>
[Tests] <code>quote</code>: pin that a backslash with whitespace is not
doubled in singl...</li>
<li><a
href="a04d47516e"><code>a04d475</code></a>
[Dev Deps] update <code>@arethetypeswrong/cli</code>,
<code>evalmd</code></li>
<li><a
href="b9545b39f4"><code>b9545b3</code></a>
[New] <code>parse</code>: add opt-in <code>splitUnquoted</code> option
for shell field-splitting of...</li>
<li><a
href="1b364683b1"><code>1b36468</code></a>
[readme] <code>quote</code>: use output verbatim; do not re-quote it (<a
href="https://redirect.github.com/ljharb/shell-quote/issues/11">#11</a>)</li>
<li><a
href="1c36f3ff77"><code>1c36f3f</code></a>
[Tests] <code>quote</code>: pin conservative escaping of <code>=</code>,
<code>@</code>, <code>^</code>, <code>,</code>, <code>:</code>,
<code>!</code> (<a
href="https://redirect.github.com/ljharb/shell-quote/issues/11">#11</a>)</li>
<li><a
href="e1c75cd6e4"><code>e1c75cd</code></a>
[readme] document <code>parse</code>'s supported parameter-expansion
subset</li>
<li><a
href="c0842c8a7a"><code>c0842c8</code></a>
[Fix] <code>parse</code>: match nested <code>${...}</code> braces so
nested parameter expansion is ...</li>
<li>Additional commits viewable in <a
href="https://github.com/ljharb/shell-quote/compare/v1.8.4...v1.10.0">compare
view</a></li>
</ul>
</details>
<br />
[](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores)
Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.
[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)
---
<details>
<summary>Dependabot commands and options</summary>
<br />
You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)
You can disable automated security fix PRs for this repo from the
[Security Alerts page](https://github.com/Z3Prover/z3/network/alerts).
</details>
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Bumps [linkify-it](https://github.com/markdown-it/linkify-it) from 5.0.1
to 5.0.2.
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a
href="https://github.com/markdown-it/linkify-it/blob/master/CHANGELOG.md">linkify-it's
changelog</a>.</em></p>
<blockquote>
<h2>5.0.2 / 2026-07-02</h2>
<ul>
<li>Fixed DoS in <code>mailto:</code> links (restrict user name to 64
chars).</li>
<li>Restricted user/pass part length in links.</li>
</ul>
</blockquote>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="50a0c914f8"><code>50a0c91</code></a>
5.0.2 released</li>
<li><a
href="de3b88554b"><code>de3b885</code></a>
Update package hooks</li>
<li><a
href="13effaaa46"><code>13effaa</code></a>
Add package lock</li>
<li><a
href="39d748dbfc"><code>39d748d</code></a>
Bump c8</li>
<li><a
href="00ce8771ac"><code>00ce877</code></a>
Drop tlds deps</li>
<li><a
href="ecde82341a"><code>ecde823</code></a>
Update benchmark to mitata</li>
<li><a
href="23c62cdd14"><code>23c62cd</code></a>
Refactor demo / doc build and publish</li>
<li><a
href="fd63f3b4ab"><code>fd63f3b</code></a>
CI config update</li>
<li><a
href="f4ea5afaa6"><code>f4ea5af</code></a>
demo: update bootstrap & layout</li>
<li><a
href="1454fb645f"><code>1454fb6</code></a>
lint: dim warnings</li>
<li>Additional commits viewable in <a
href="https://github.com/markdown-it/linkify-it/compare/5.0.1...5.0.2">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)
You can disable automated security fix PRs for this repo from the
[Security Alerts page](https://github.com/Z3Prover/z3/network/alerts).
</details>
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
z3-rs correctly used Or. I accidentally forgot that enclosing function
call, and had what resulted in And.
Test case:
```python
s = Solver()
x, y, z = Ints("x y z")
s.add(x >= 0, x <= 2, y >= 0, y <= 2, z >= 0, z <= 2, x + y + z == 2)
# I didn't test multivariable constraints last time fearing nondeterminism
# Sorting avoids that
print(sorted(map(lambda x: list(map(lambda x: x.as_long(), x)), s.solutions([x, y, z]))))
```
**Before**: `[[0, 1, 1], [2, 0, 0]]`
**After**: `[[0, 0, 2], [0, 1, 1], [0, 2, 0], [1, 0, 1], [1, 1, 0], [2,
0, 0]]`
Fixes: #8633
---------
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
With `smt.bv.solver=2`, `int_to_bv(x)` was translated to the raw integer
`x` without normalizing it to `[0, 2^N)`. Bitwise operations like
`bvxor(A, B)` are translated as `A + B - 2·band(A, B)`, which is only
valid when both operands are in `[0, 2^N)`. When `x` was negative or ≥
2^N, the LP solver could assign a band value inconsistent with bit
semantics, producing a model that fails validation.
## Changes
- **`OP_INT2BV` translation** (`translate_bv`): Apply `umod(e, 0)`
instead of passing the raw integer argument through. This normalizes the
value to `[0, 2^N)` before it participates in any bitwise arithmetic.
```cpp
// Before
case OP_INT2BV:
r = arg(0); // raw integer, may be negative or ≥ 2^N
// After
case OP_INT2BV:
r = umod(e, 0); // normalized to [0, 2^N)
```
- **`amod` shortcut**: Add a fast-path for `mod(t, N)` when the divisor
already equals `N` — the result is already in `[0, N)`, so wrapping it
again with another `mod(_, N)` is unnecessary and avoids expression
bloat.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Symbolic `re.range` nested under `re.++` caused Z3 to loop indefinitely,
ignoring timeouts. Direct symbolic range membership was fixed
previously, but the nested case reaches a different code path — the
Brzozowski derivative engine in `derive_range`.
## Root cause
`derive_range` in `seq_derive.cpp` only handled concrete unit-string
bounds. For symbolic bounds it returned a stuck `re.derivative(ele,
re.range(lo, hi))` term. When nested under concatenation, this stuck
term cycled infinitely:
1. `is_nullable` of the stuck term → `is_nullable_symbolic_regex` →
emits `re.in_re("", re.derivative(...))`
2. That `in_re` triggers `propagate_in_re` → new `accept` predicate
3. New `accept` computes another derivative → another stuck term →
repeat
## Fix
Replace the stuck fallback with a proper symbolic ITE. By SMT-LIB
semantics, `re.range(lo, hi)` accepts character `c` iff both bounds are
single-character strings and `lo[0] ≤ c ≤ hi[0]`. The derivative with
respect to `ele` becomes:
```
ite(len(lo)=1 ∧ len(hi)=1 ∧ lo[0] ≤ ele ∧ ele ≤ hi[0], ε, ∅)
```
Length conditions are omitted for bounds already known to be concrete
single-character strings.
```smt2
(set-logic ALL)
(declare-const s String)
(assert (str.in_re "a" (re.++ re.all (re.range s "c"))))
(check-sat)
; Previously hung indefinitely; now returns sat in ~10ms
```
## Changes
- **`src/ast/rewriter/seq_derive.cpp`** — `derive_range`: replace stuck
`re.derivative` fallback with symbolic ITE using `str.nth_i` and length
guards for non-concrete bounds
- **`src/test/seq_rewriter.cpp`** — add solver-level regression test
(case 21) for nested symbolic `re.range` under `re.++`
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
https://github.com/Z3Prover/z3/pull/10020 deleted a number of
unnecessary (and, by a strict interpretation, illegal) semicolons. These
were detected by adding -Wextra-semi to CLANG_ONLY_WARNINGS during
testing. The PR did not eliminate all such unnecessary/illegal
semi-colons; Nikolaj Bjorner argued that some IDEs would be confused by
doing so for macro invocations, which otherwise look like function
calls. So it left those, and did not include adding -Wextra-semi to
CLANG_ONLY_WARNINGS in the PR.
I'm worried that not having -Wextra-semi will allow instances of the
semis we'd like to eliminate to creep back in. This PR introduces a
mechanism to disable the warnings for regions with such macro
invocations, and uses that mechanism for one file. If accepted, a
subsequent PR would use this mechanism in all the remaining places, so
that there is a clean clang build with -Wextra-semi.
I verified that:
* It compiles cleanly for if the enable/disable macros have null
definitions, as they would for non-clang compilations.
* It compiles cleanly for a clang build without -Wextra-semis.
* It compiles successfully, albeit with *many* warnings, for a clang
build with-Wextra-semis -- but none of those errors are for the regions
in ast.h where the warning is disabled.
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
