https://github.com/Z3Prover/z3/pull/10284 changed the UNREACHABLE macro
in debug.h to use __builtin_unreachable() to indicate to the compiler
that the
code leading it should be considered unreachable.
In https://github.com/Z3Prover/z3/pull/10295 Copilot figured out that
this was wrong: the unreachable macro makes calls, which shouldn't be
elided, and whose arguments should be evaluated. It partially fixed the
problem by declaring invoke_exit_action to be `[[noreturn]]`. This
eliminated warnings in non-debug builds, but when Z3_DEBUG is enabled,
`UNREACHABLE` ends with an invocation of `INVOKE_DEBUGER()`. This can
call `invoke_debugger()`, which *can* actually return (so it can't be
given the `[[noreturn]]` attribute. So we still get warnings in debug
builds.
This PR fixes those, creating a Z3_unreachable_case macro, which is just
a combination of `UNREACHABLE()` and `Z3_fallthrough`. It uses that in
the places that give warnings.
It seemed better to me to still have these cases have a single macro,
rather than `UNREACHABLE` followed by an explicit `Z3_fallthrough`; this
seemed to me like it would confuse people -- "how can you fall through
if this code is unreachable?" But I'm open to alternative suggestions!
For every row with only one non-fixed variable in nla_core.cpp,
core::propagate, fix this variable.
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Fixes#10303.
## Symptom
On the reported QF_NRA instance z3 answers `sat` for some values of
`smt.random_seed` and `unsat` for others, and every `sat` comes with a
model z3's own validator rejects. The correct answer is `unsat`.
`smt.arith.solver=2` is unaffected; `smt.arith.solver=6` (the default)
is not.
## Root cause
The simplex model is not rational — each column is a `numeric_pair<mpq>`
`(x, y)` denoting `x + δ·y`, where `δ` is a positive infinitesimal used
to represent *strict* bounds exactly (`v > 0` is stored as `(0, 1)`).
`δ` only becomes concrete at model-output time, in
`from_model_in_impq_to_mpq(v) = v.x + m_delta * v.y`.
But nla decides monomial consistency using **only the rational parts**:
```cpp
const rational& val(lpvar j) const { return lra.get_column_value(j).x; } // nla_core.h:165
r *= lra.get_column_value(j).x; // product_value
return product_value(m) == lra.get_column_value(m.var()).x; // check_monic
```
That is sound only on a δ-free model, and it cannot be repaired by also
tracking `y`: a **product** `(x₁+δy₁)(x₂+δy₂)` has a `δ²` term, which a
`numeric_pair` cannot represent. The delta encoding is inherently
linear, so nla structurally cannot reason on a δ-carrying model.
The code relies on this: `core::check()` calls
`lra.get_rid_of_inf_eps()` as its very first action to instantiate δ
before any monomial is inspected. The invariant is:
> `m_to_refine` must only ever be computed on a δ-free model.
`core::optimize_nl_bounds()` breaks it. It calls
`lra.find_feasible_solution()` in the middle of the nla check; the
simplex re-runs, parks columns back onto strict bounds and
**re-introduces non-zero `y`**. It then calls `init_to_refine()` on that
model — one full LP re-solve after the scrub in `core::check()`.
A wrong `m_to_refine` turns directly into a wrong answer:
```
find_feasible_solution() re-introduces δ
→ init_to_refine() mis-measures monomials (compares only .x)
→ m_to_refine wrongly empty
→ horner.cpp:117 set_nla_satisfied()
→ core::check() returns l_true
→ theory_lra FC_DONE → sat
→ model output instantiates δ (x + m_delta·y)
→ monomial equations violated → "an invalid model was generated"
```
Instrumenting model construction on the reported benchmark confirms it
exactly: `use_nra_model=0`, **87 columns still carrying infinitesimals,
44 monomials violated** once δ is instantiated — every one of them with
`to_refine = 0`.
## Fix
Enforce the invariant where it is actually depended upon, instead of
only at the entry to `core::check()`:
```cpp
void core::init_to_refine() {
if (lra.is_feasible())
lra.get_rid_of_inf_eps();
m_to_refine.reset();
...
}
```
Every caller — including the ones inside `optimize_nl_bounds()` that
follow an LP re-solve — now measures monomials on a δ-free model.
A second commit closes a related hole: the
`arith.nl.optimize_bounds_lp_max_vars` throttle exit returns *after*
`find_feasible_solution()` has already moved the model, and was the only
exit that never called `init_to_refine()` at all — leaving `m_to_refine`
stale rather than merely δ-contaminated.
## Validation
Reported benchmark, `tactic.default_tactic=smt` (deterministic — the
default QF_NRA portfolio uses wall-clock `try_for` budgets, so it is
timing-dependent): master fails on **9 of 20** seeds; with the fix
**20/20** answer `unsat`. Under the default configuration, seeds 1–10
all answer `unsat` (was `sat` + invalid model on 1, 3, 4, 10), matching
`smt.arith.solver=2`.
The bug was much broader than the single reported instance. On the
`QF_NRA_small` corpus (1147 instances, `-T:10`):
| | sat | unsat | unknown | invalid model |
|---|---|---|---|---|
| master | 460 | 597 | 77 | **13** |
| this PR | 466 | 602 | 79 | **0** |
**Zero sat/unsat conflicts.** Of the 13 instances where master emitted
an invalid model, **7 are genuinely `unsat`** — the same unsoundness as
the reported one.
## Performance
Net **faster**, on the 1054 instances answered identically before and
after:
| | total |
|---|---|
| master | 229.7 s |
| this PR | 146.4 s (**−36.3 %**) |
133 instances faster by >200 ms vs. 13 slower by >200 ms.
The added `get_rid_of_inf_eps()` is asymptotically free —
`init_to_refine()` already costs Θ(Σ|monic|) arbitrary-precision
*multiplications*, so adding Θ(#columns) `mpq::is_zero()` tests (which
early-exit when no deltas are present) does not change its complexity
class. The expensive path is also moved rather than added: deltas left
by `optimize_nl_bounds()` previously survived until the next
`core::check()`, which paid the full `find_delta_for_strict_bounds` +
rewrite cost anyway.
The speedup itself comes from correctness — a truthful `m_to_refine`
points grobner / basic_lemma / order / monotonicity / tangent / nra at
the monomials that are genuinely violated, instead of letting them chase
a model that was never consistent.
`test-z3 /a`: 93/93 pass.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Remove the seq_split (regex sigma-splitting / factorization) module and all
code that uses it:
- delete src/ast/rewriter/seq_split.{h,cpp} and src/test/seq_split.cpp
- drop the m_split member, include, and split/simplify_split/split_membership
wrappers from seq_rewriter
- remove the regex factorization propagation block from seq_regex.cpp
- remove the seq.regex_factorization_enabled/threshold parameters and their
theory_seq_params fields
- drop the files from the rewriter/test CMake lists and the test registry
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
## Summary
Adds `seq_monadic` (`src/ast/rewriter/seq_monadic.{h,cpp}`), a
self-contained,
rewriter-level decision procedure for regex membership of a term that is
a
concatenation of sequence variables and constant elements — e.g. `x·a·x
∈ R`,
including repeated and multiple variables. It uses a whole-language
*monadic
decomposition* plus automaton product-reachability; it is minterm-free
and does
**not** use Nielsen word-equation splitting or `seq_split`.
The component is **purely additive**: it is not wired into any solver
path, so
default behavior is unchanged. It ships with a unit test and an opt-in
benchmark
harness that is inert unless `Z3_SEQ_BENCH_DIR` is set.
## What it does
- `x·u ∈ R ⇔ ⋁_q ( x reaches q in A_R ∧ u ∈ q )` over the derivative
automaton; `reach(q)` is never materialized as a regex (avoids the
state-elimination blowup). A variable's constraint is decided by a lazy
product-reachability search over tuples of derivative states, with
transitions
= the product of `brz_derivative_cofactors` branches and
pairwise-conjoined
`seq::range_predicate` guards.
- **Generic in the element sort**: characters use the exact
`range_predicate`
algebra; any other element sort uses a candidate-basis over the element
values
the guards mention (sound and complete for the
`{true,false,=,<=,and,or,not}`
guard grammar the derivatives emit).
- **Concrete witnesses**: on sat it reconstructs a witness value (a
sequence of
concrete elements, not predicates) per variable from the accepting
product path.
- **Boolean combinations**: `solve_and` decides a conjunction of
memberships
jointly, so a variable shared across memberships is constrained
consistently.
This is the natural extension since `¬(t∈R) ≡ t∈~R`, `∨` = union of
DNFs, and
`∧` = product of DNFs.
Also de-duplicates the char-guard → `range_predicate` translator into a
single
public `seq::guard_to_range_predicate` in `seq_range_collapse` (it was
previously
duplicated there and in `seq_monadic`).
## Testing
- `tst_seq_monadic`: single / multiple / repeated variables, nested
complement,
bounded loops, per-variable constraints, a generic `(Seq Int)` section,
witness
verification (substitute the model back and re-decide membership), and
`solve_and` cases that are individually sat but jointly unsat.
- Full unit suite `test-z3 /a` passes (93/93).
## Evaluation (offline harness, not part of CI)
On a regex-membership benchmark corpus, restricted to files carrying a
genuine
`(set-info :status)`, the solver decides 318 and 316 are correct
(99.4%); the
only 2 disagreements are a length limitation (`|x|=2k`) that is outside
the
membership fragment.
## Known limitations / follow-ups
- Pathological deeply-nested, high-multiplicity regexes can overflow the
recursive derivative stack; a recursion-depth guard to degrade to
`unknown` is
a natural follow-up.
- Out-of-fragment constraints (word equations, length / Parikh) are not
handled,
by design — this decides regex membership only.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Copilot-Session: 916db256-43c6-4067-b6f4-fa8d2cf2f37f
## Summary
Fixes a Spacer regression where a satisfiable HORN benchmark that
previously returned `sat` now returns `unknown` with `(:reason-unknown
"Stuck on a lemma")`.
- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/3420
- **Benchmark:** `iss-5561/bug-2.smt2` (`inputs/issues/iss-5561/` in
`Z3Prover/bench`)
- **Kind:** `diff` (semantic answer changed)
### Divergence
```diff
--- bug-2.expected.out (expected)
+++ produced (current z3)
@@ -1,2 +1,2 @@
-sat
-(:reason-unknown "")
+unknown
+(:reason-unknown "Stuck on a lemma")
```
## Root cause
`git bisect` (clean per-commit builds, `-T:20`) identifies the first bad
commit as **df8d23960** — *"qe2: fix nonlinear term introduced by
term_graph representative selection in MBP (#10186)"* — which modified
`term_graph::term_lt` in `src/qe/mbp/mbp_term_graph.cpp`.
That change made concrete model **values** win over non-eliminated
uninterpreted **constants** when electing equivalence-class
representatives (previously the documented invariant was *"prefer
uninterpreted constants over values"*). It was intended to keep `qe2`'s
one-shot output linear (avoiding e.g. `(* 2 x)` becoming `(* x1 x)`).
Spacer, however, shares this same term_graph machinery for model-based
projection when generalizing lemmas. Preferring the value makes a
non-eliminated state constant get substituted by its concrete model
value everywhere in the projected lemma. This **over-grounds** the lemma
to the specific model, so Spacer keeps regenerating an over-specialized
lemma at infinity level; each regeneration bumps it until
`old_lemma->get_bumped() >= 100`, at which point `add_lemma_core` throws
`default_exception("Stuck on a lemma")`
(`src/muz/spacer/spacer_context.cpp`), surfacing as `unknown`.
`qe2`'s projection and Spacer's lemma generalization both funnel through
the same `spacer_qel`/`mbp_qel`/`qel` term_graph paths, so there is no
clean, separately-validatable client seam at which to gate the new
behavior without threading a new context flag through several layers.
## Fix
Revert the `term_lt` value-preference block, restoring the long-standing
invariant *"prefer uninterpreted constants over values"* that Spacer's
projection relies on. The change is confined to `term_lt` and adds an
explanatory comment referencing this regression.
## Validation
Built the patched `./z3` checkout (mk_make + `make`) and re-ran the
benchmark with the snapshot capture options (`-T:20`):
```
$ z3 -T:20 inputs/issues/iss-5561/bug-2.smt2
sat
(:reason-unknown "")
```
This matches the recorded `bug-2.expected.out` oracle exactly. The
sibling benchmark `iss-5561/bug-1.smt2` and basic solving were also
spot-checked and unaffected.
## Caveat for reviewers
This is a straight revert of the `term_lt` portion of #10186, so that
PR's cosmetic improvement — keeping `apply qe2` output in linear
`QF_LIA` form (avoiding logically-equivalent nonlinear terms) — is
reintroduced. #10186 added no regression test, so that behavior could
not be re-validated here. A non-regressing reimplementation should make
the representative preference **client-controlled** (as the `XXX`
comment above `term_lt` already suggests): enable value-preference only
for one-shot QE tactics (`qe2`) while keeping symbolic representatives
for Spacer's MBP generalization. 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/30191159770)
· 572.3 AIC · ⌖ 20.4 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:
30191159770, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/30191159770 -->
<!-- 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>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Fixes a **completeness regression** in `qe_mbp` uncovered by the
snapshot-regression corpus.
- Originating discussion:
https://github.com/Z3Prover/bench/discussions/3445
- Benchmark ref: `iss-5925/small.smt2` (`Z3Prover/bench`,
`inputs/issues/iss-5925/`)
### Divergence
```diff
--- small.expected.out (expected)
+++ produced (current z3)
@@ -1 +1 @@
-unsat
+unknown
```
The benchmark is `(check-sat-using qe2)` over a formula that eliminates
an array variable `r` used **directly** as a store index: `(store (store
a v true) r true)`.
### Root cause
Commit 5bd9e6a00 ("Fix #7259, #7036: unsound MBP array projection with
array var in select/store index") added `has_array_var_in_index`, which
routes `spacer_qel` to the classic model-based projection
(`spacer_qe_lite`) whenever an eliminated array variable occurs anywhere
in a select/store index position. That guard is **too broad**: it also
fires when the array variable is used *directly* as an index (e.g. `r`
in `(store base r val)`). For `iss-5925/small.smt2` the fallback path
cannot decide the goal and returns `unknown` instead of the correct
`unsat`.
Using an array variable *directly* as an index is sound under `mbp_qel`:
the index is exactly that variable, and its model value is substituted
soundly. The genuine unsoundness of #7259/#7036 arises only when the
variable is **nested inside a compound index term** that the
partial-array-equality class-merge can silently rewrite (e.g. `(select
va (= v va))` becoming `(select v true)`).
### Fix
Restrict `has_array_var_in_index` to the dangerous nested case by
skipping index arguments that are *exactly* the array variable (`v !=
idx && occurs(v, idx)`). This keeps the #7259/#7036 soundness fallback
intact while restoring `qe2` completeness for direct-index benchmarks.
### Validation
Built z3 from this checkout (`make -j`, Release) and re-ran with
`-T:20`:
- `inputs/issues/iss-5925/small.smt2`: `unknown` (before) -> **`unsat`**
(after), matching the recorded oracle.
- `inputs/issues/iss-5925/delta.smt2`: still `unknown`, matching its
oracle.
- Reconstructed #7259 case `(select va (= v va))` under `qe2`: still
**`unsat`** (fallback still triggers for the nested-index case) -
soundness preserved.
- Unit tests `test-z3 mbp_qel` and `test-z3 qe_arith`: **PASS**.
Opened as a draft for human review. Please double-check the soundness
argument against the exact #7036 reproducer, which was not available in
the checkout.
> [!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/30425630832)
· 287.3 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:
30425630832, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/30425630832 -->
<!-- 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>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
The generated Python bindings loaded `libz3.so` without a soversion,
which could bind to an ABI-incompatible shared library when multiple Z3
versions are present. This change makes Linux bindings prefer the
versioned soname while leaving other platforms on the existing lookup
path.
- **Python loader generation**
- Thread a `z3py_soversion` parameter through `scripts/update_api.py`.
- Generate `_lib_name` as `libz3.so.<major>.<minor>` on Linux, and keep
`libz3.<ext>` elsewhere.
- Reuse `_lib_name` consistently for directory probing, system fallback,
and error messages.
- **Build-system wiring**
- Pass the current `SOVERSION` from the CMake Python bindings build on
Linux.
- Pass the same value through the `mk_make`/`mk_util.py` generation path
so both build systems emit the same loader behavior.
- **In-tree Python bindings layout**
- Add the matching `libz3.so.<major>.<minor>` link in `build/python/` on
Linux so the generated bindings work directly from the build tree.
- **Regression coverage**
- Add a focused script-level test for the generated loader preamble to
check:
- Linux uses the versioned soname when provided.
- Non-versioned fallback remains available when no soversion is
supplied.
Example of the generated Linux loader behavior:
```python
_sover = '5.0'
_ext = 'so'
_lib_name = 'libz3.%s.%s' % (_ext, _sover) if sys.platform.startswith('linux') and _sover else 'libz3.%s' % _ext
_lib = ctypes.CDLL(_lib_name)
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#7518
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
`scanner::scan()` was returning `EOF_TOKEN` when the underlying stream
had `badbit` set, making a failed read (EIO, ENOSPC, etc.)
indistinguishable from a clean end-of-file. Z3 would silently produce no
output with exit code 0.
## Root cause
`std::istream::gcount()` returns 0 for both normal EOF and I/O failure.
`read_char()` returned -1 in both cases, and `scan()`'s `-1` handler
unconditionally set `EOF_TOKEN`.
## Fix
### `src/parsers/util/scanner.cpp`
Check `m_stream.bad()` in the `-1` case; emit an error message and
`ERROR_TOKEN` on failure:
```cpp
case static_cast<char>(-1):
if (m_stream.bad()) {
m_err << "ERROR: I/O failure while reading input stream.\n";
m_state = ERROR_TOKEN;
} else {
m_state = EOF_TOKEN;
}
break;
```
### `src/test/scanner_io.cpp` (new)
Regression test (ported from the `io_test` branch) verifying:
1. A good stream scans to completion (`n > 0` tokens).
2. A stream with `badbit` pre-set produces `ERROR_TOKEN` or a non-empty
error message rather than silent EOF.
### `src/test/main.cpp` + `src/test/CMakeLists.txt`
Register `tst_scanner_io` in the `FOR_EACH_ALL_TEST` macro and add
`scanner_io.cpp` to the build.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Commit d46fbad3 added `__builtin_unreachable()` to the `UNREACHABLE()`
macro in Clang builds to suppress `-Wimplicit-fallthrough` warnings. In
Release+Clang mode, this causes UB: Clang can legally eliminate the
`invoke_exit_action` call (since reaching `__builtin_unreachable()` is
UB, the compiler assumes the entire branch is dead), so when
`UNREACHABLE()` is actually hit, the function continues with
uninitialized state — producing the segfault observed in the FPA C
example.
## Changes
- **`src/util/debug.h`** — Declare `invoke_exit_action` as
`[[noreturn]]`. This is semantically accurate: the function always
terminates via `exit()` or `throw`, never returning normally. The
`[[noreturn]]` annotation naturally suppresses `-Wimplicit-fallthrough`
after `UNREACHABLE()` without any UB.
- **`src/util/debug.h`** — Remove `__compiler_unreachable` macro and its
use in `UNREACHABLE()`. With `[[noreturn]]` on `invoke_exit_action`, it
is redundant.
- **`src/util/debug.cpp`** — Add `[[noreturn]]` to the
`invoke_exit_action` definition to match.
```cpp
// Before (broken in Release+Clang: UB allows optimizer to eliminate invoke_exit_action)
# define UNREACHABLE() { notify_assertion_violation(...); invoke_exit_action(ERR_UNREACHABLE); }; __builtin_unreachable()
// After (invoke_exit_action is [[noreturn]], no UB)
# define UNREACHABLE() { notify_assertion_violation(...); invoke_exit_action(ERR_UNREACHABLE); } ((void) 0)
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This refines the recently added `has_array_var_in_index` helper in
`src/qe/qe_mbp.cpp` to match the surrounding style without changing
behavior. The array-index guard remains identical; the implementation is
just expressed more consistently.
- **What changed**
- Replaced the nested `for`/`if` occurrence check with the local
`any_of(...)` pattern already used nearby in `has_unsupported_th`.
- Added the missing blank line before `operator()` to align with spacing
used between other methods in the class.
- **Behavior**
- No functional change intended.
- The helper still returns `true` as soon as any array variable occurs
in a `select`/`store` index position.
- **Example**
```c++
for (unsigned i = 1; i < last; ++i)
if (any_of(arr_vars, [&](app* v) { return occurs(v, a->get_arg(i)); }))
return true;
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10282
---------
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.
This PR enable the "-Wimplicit-fallthrough" warning, then fix all the
warnings this gets
in the clang build, by:
* Augmenting UNREACHABLE to add __builtin_unreachable(), which
suppresses
warnings for fallthrough in that cse.
* Adding Z3_fallthrough in many cases, to make it clear that
fallthroughs are intentional.
* Adding [[noreturn]] to functions that throw, so the compiler knows
they don't fall through to the next case.
* In a couple of cases, there's a fall-through to a default case, which
does "break", or "return nullptr". In those cases, I duplicated the
action in the preceding case, to make it more self-contained, and robust
in the face of change.
In some cases, I am concerned about whether the warnings are identifying
real bugs. For example, the fall-throughs in these files seem at least a
little suspect:
nnf.cpp
seq_rewriter.cpp
lar_solver.cpp
while very probably correct, also seem at least a tiny bit suspect.
However, this PR does *not* attempt to change any behavior, only to
silence the warnings. It would be great if somebody with more knowledge
of the code could vet these cases. If vetted, the explicit presence of
the Z3_fallthrough would reassure future readers of the code that the
fall-through is intentional, not accidental.
Expose enum_tuples(sorts) which produces an iterator over vectors of
terms, one term per input sort, dovetailing the per-sort streams so all
combinations are enumerated even when individual streams are infinite.
Each sort is enumerated by a self-contained sort_stream owning its own
grammar and bottom_up_enumerator seeded from the user productions, so
array sorts (with their fresh select ops and bound vars) do not collide
across sorts.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: cb1e958b-f89b-4407-958d-8e7ecf172bbc
The array term-graph projection (mbp_qel) treats an array equality (= a b)
as an implicit partial array equality and eliminates it by merging the
array variable's congruence class. That rewrite is unsound when the array
variable being eliminated occurs inside a select/store index position,
because the index is a first-class term whose value must be preserved.
For example, (select va (= v va)) was rewritten to (select v true) after
merging va into v, turning a model-false literal into a model-true one and
triggering the qe_mbp validation assertions (qe_mbp.cpp:412 for #7259,
qe_mbp.cpp:622 for #7036), or a crash at qsat.cpp:579 in release builds.
Detect when an array variable to be eliminated occurs inside a select or
store index and fall back to the classic model-based projection
(spacer_qe_lite) for such formulas. Both reproducers now return the correct
unsat verdict with no assertion failure, and all unit tests pass.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
When building the model value of a sequence, an unresolved element such as
(seq.nth_i k!0 0) over an internal sequence constant could be emitted
verbatim, exposing internal skolem symbols (e.g. k!0) in the user-visible
model returned by get-model / get-value.
Such a term is not a proper value and is unconstrained at model-construction
time, so replace it with a concrete fresh value from the sequence factory.
This only affects model values that were already non-concrete (i.e. leaking
internal terms); genuine concrete sequence values satisfy m.is_value and are
left untouched, so sat/unsat verdicts and normal string/sequence models are
unaffected.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
When NLA interval arithmetic processes a linear term, a temporary
`interval` holding `mpq` numerals was stack-allocated but never freed,
leaking any heap-allocated big-number representations produced by
`mpq_manager`.
## Change
- **`src/math/lp/nla_intervals.cpp`** — In `interval_from_term`, replace
raw `interval bi` with `scoped_dep_interval bi(get_dep_intervals())`.
The scoped wrapper calls `m_manager.del()` on destruction, which frees
both `m_lower` and `m_upper` mpq values.
```cpp
// Before
interval bi;
m_dep_intervals.mul<wd>(a, i, bi);
// After
scoped_dep_interval bi(get_dep_intervals());
m_dep_intervals.mul<wd>(a, i, bi);
```
The leak was triggered on optimization problems with nonlinear
arithmetic (e.g. `opt.priority box` + `maximize` with NLA constraints),
where the interval multiplication produces mpq values large enough to
require heap allocation via `mpz_manager::set_big_i64`.
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10275
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
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>
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>
## 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
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
