Creating and disposing `Context` instances causes unbounded native
memory growth (~12 GB for 100k contexts) because `NativeContext` had no
finalizer — if `Dispose()` was never called, the native Z3 context
leaked permanently. Additionally, both `Context` and `NativeContext` had
delegate lifetime and thread-safety issues in their disposal paths.
## `NativeContext.cs`
- **Add missing finalizer** `~NativeContext() { Dispose(); }` — the root
cause of permanent leaks when callers don't explicitly dispose
- **Atomic disposal** via `Interlocked.Exchange(ref m_ctx, IntPtr.Zero)`
— prevents double-free when `Dispose()` is called concurrently (e.g.
user code + finalizer race)
- **Delegate lifetime** — capture `errHandler` locally +
`GC.KeepAlive(errHandler)` after `Z3_del_context`; the GC could
otherwise collect the error handler callback before the native
destructor finishes
- **Remove dead code** — `GC.SuppressFinalize` in `InitContext()` and
`GC.ReRegisterForFinalize` in `Dispose()` were both no-ops (no finalizer
existed); the latter would have caused infinite finalization with the
new finalizer
- **GC memory pressure** — `GC.AddMemoryPressure(8MB)` on init /
`GC.RemoveMemoryPressure(8MB)` on dispose, guarded by
`m_memPressureAdded` flag, so the GC schedules finalizers promptly when
contexts accumulate
## `Context.cs`
- **Thread-safe disposal** — capture `ctx` and `errHandler` inside the
existing `lock(this)` block; previously both were read outside the lock,
allowing two concurrent callers to both capture the same non-zero `ctx`
and double-free it
- **Delegate lifetime** — same `errHandler` + `GC.KeepAlive` pattern as
`NativeContext`
- **`GC.SuppressFinalize` placement** — moved inside the `if (m_ctx !=
IntPtr.Zero)` block, before cleanup, per .NET best practice
- **GC memory pressure** — same add/remove pattern, conditioned on
`!is_external` via `m_memPressureAdded` flag
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Unit tests relied on `SASSERT()` which is a no-op in release builds
(`DEBUG_CODE` wrapper), silently skipping all assertions outside debug
mode. Several test files were also gated behind `#ifdef _WINDOWS`,
making them dead code on Linux/macOS CI.
## Changes
- **`SASSERT` → `ENSURE` in 20 test files (200 occurrences)**: `ENSURE`
maps to `VERIFY` and always executes regardless of build type, ensuring
test assertions are active in both debug and release builds.
- **`src/test/diff_logic.cpp`**: Removed `#ifdef _WINDOWS` wrapping the
entire file. No Windows-specific APIs were used; the guard only
prevented compilation on non-Windows platforms.
- **`src/test/dl_product_relation.cpp`**: Removed `#ifdef _WINDOWS`
guard around `tst_dl_product_relation()`. The function body has no
platform dependencies.
- **`src/test/sat_local_search.cpp`**: Replaced `sscanf_s`
(MSVC-specific) with portable `sscanf`; added return-value check to
detect malformed input. Previously, `build_instance()` unconditionally
returned `false` on non-Windows, making the SAT local search test a
no-op on Linux/macOS.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`Z3_API_LOG_SYNC` uses `std::mutex` to serialize API log writes across
threads. When combined with `Z3_SINGLE_THREADED`, all mutex operations
become no-ops (`SINGLE_THREAD` define strips them), silently defeating
the synchronization.
## Changes
- **`CMakeLists.txt`**: Emit `FATAL_ERROR` when both
`Z3_API_LOG_SYNC=ON` and `Z3_SINGLE_THREADED=ON` are set:
```
CMake Error: Z3_API_LOG_SYNC requires threading support and cannot be
combined with Z3_SINGLE_THREADED
```
- **`README-CMake.md`**: Expand `Z3_API_LOG_SYNC` description to clarify
its purpose and document the incompatibility with `Z3_SINGLE_THREADED`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
…158)
rule_manager::mk_query eliminates gaps in de Bruijn indices caused by
unused quantified variables via a substitution that renumbers the
remaining variables contiguously. This was done in a single pass, but
var_subst applies the rewriter, which can simplify away further variable
occurrences (e.g. collapsing ite terms such as (ite true a b) or (ite c
x x)), introducing new gaps. The leftover null sort was then
dereferenced, asserting in debug and segfaulting in release.
Iterate the gap-elimination until the free variables are contiguous.
Each iteration either compacts the indices or strictly reduces the set
of used variables, so it terminates.
Fixes the crash reported for:
(assert (forall ((a Bool)(b Bool)(d (_ BitVec 1))(e (_ BitVec 1))(f (_
BitVec 1))(g Bool))
(= (= f (ite a (_ bv0 1) (ite true (_ bv0 1) (ite b e e)))) g)))
(check-sat-using horn)
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
`std::format` (C++20 `<format>`) pulls in `std::to_chars` for
floating-point formatting, which is only available on macOS 13.3+. The
Mac x64 CI job was targeting macOS 13.0, causing build errors in
`src/ast/`.
## Changes
Updated `nightly.yml` to raise the macOS deployment target for the x64
build:
- **`MACOSX_DEPLOYMENT_TARGET`**: `"13.0"` → `"13.3"` in the
`mac-build-x64` job
- **`--os` flag**: `osx-13.0` → `osx-13.3` in the `mk_unix_dist.py`
invocation
This matches the existing `mac-build-arm64` job, which already targets
macOS 13.3, and allows `std::format` to be used freely in `src/ast/`
without workarounds.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Z3 4.16.0 introduced a cube-and-conquer parallel solver that regressed
easy QF_LIRA problems from <1s to hanging indefinitely. Workers start
with a 1000-conflict budget and multiply by 1.5× on each timeout, but
after ~38 escalations the `unsigned` cast overflows, causing the budget
to oscillate chaotically (e.g. 3.27B → 618M → 927M → … never reaching a
stable large value). For sub-cubes that require more conflicts than any
value in the oscillation window, the worker loops forever.
## Changes
- **`src/smt/smt_parallel.h`** – `update_max_thread_conflicts()`:
replace raw `(unsigned)(mul * val)` cast with saturating arithmetic that
caps at `UINT_MAX`, eliminating the UB and the oscillation:
```cpp
// Before – UB when product > UINT_MAX, budget oscillates after ~38
escalations
m_config.m_threads_max_conflicts =
(unsigned)(m_config.m_max_conflict_mul *
m_config.m_threads_max_conflicts);
// After – saturates at UINT_MAX
double next = m_config.m_max_conflict_mul *
m_config.m_threads_max_conflicts;
m_config.m_threads_max_conflicts = (next >= (double)UINT_MAX) ? UINT_MAX
: (unsigned)next;
```
- **`src/solver/parallel_tactical.cpp`** – Identical
saturating-arithmetic fix in the `parallel_tactical2` worker's
`update_max_thread_conflicts()`, which is the code path actually
exercised for QF_LIRA problems.
- **`src/smt/smt_parallel.cpp`** – Worker's initial per-cube conflict
budget is now sourced from `m_smt_params.m_threads_max_conflicts` (the
user-visible `smt.threads.max_conflicts` parameter) instead of being
hardcoded to 1000, so users who leave the parameter at its default get
an unlimited initial budget matching Z3 4.12.x portfolio behaviour.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
## Problem
Maximizing/minimizing under a **strict** inequality has a delta-rational
optimum. For
```smt2
(declare-const r Real)
(assert (< r 1))
(maximize r)
(check-sat)
(get-objectives)
```
the optimum is the supremum `1 - epsilon`, but z3 reported `r = 0`.
The same defect makes shared-symbol objectives report a value matching
**neither the model nor the true optimum** (issue #10028 follow-up).
Minimal reproducer — a 6-mark Golomb ruler (a `>32`-arg `distinct`, so
the objective is coupled to EUF) with a strict real objective `obj >
x5`, whose true optimum is `17 + epsilon`:
| case | before | after |
|---|---|---|
| `maximize r`, `r < 1` | `0` ❌ | `1 - epsilon` ✅ |
| `minimize r`, `r > 1` | `0` ❌ | `1 + epsilon` ✅ |
| Golomb `minimize obj`, `obj > x5` | `35/2` / `7+eps` ❌ | `17 +
epsilon` ✅ |
## Root cause
`check_bound` validates the LP hint by asserting `objective >= optimum`.
For a supremum `1 - epsilon` this is a **lower** bound whose value
carries a **negative** infinitesimal `(1, -1)`.
No `lconstraint_kind` can express that. The kind->infinitesimal map only
yields the *matching-sign* cases — `GT` -> lower `(r, +1)`, `LT` ->
upper `(r, -1)` — or zero (`GE`/`LE`). The opposite-sign lower bound
`(r, -1)` (i.e. `r >= r0 - delta`) is a *relaxation* that no strict
inequality produces. `opt_solver::mk_ge` therefore projected the
`-epsilon` away, turning `r >= 1 - epsilon` into the over-strong,
unsatisfiable `r >= 1`; validation failed and the strictly smaller
current model value was reported instead.
## Fix — carry the infinitesimal faithfully through the bound pipeline
- **`lp_api::bound`** gains an `eps` component so `get_value` returns
the true delta value (no spurious rational fixed-variable equality is
propagated to EUF).
- **`lar_base_constraint`** stores its right-hand side as a
delta-rational `impq` pair; `rhs()` returns the rational component,
`bound_eps()` the infinitesimal one.
- **`lar_solver`** bound activation/update threads the whole `impq`
bound, so a lower bound `(r, -1)` can be asserted. `constraint_holds`
accounts for it using the **same** strict-bounds delta that flattens the
model, computed **once per model**.
- **`theory_lra::mk_ge`** builds a *fresh* predicate for the `(r, -1)`
lower bound (to avoid colliding with an already-internalized `v >= r`
literal) and attaches `eps = -1`. **`opt_solver::mk_ge`** passes the
unprojected value to `theory_lra` / `theory_mi_arith` /
`theory_inf_arith` (whose bounds are already `inf_rational`).
The pair machinery is what makes the supremum both representable
(optimum `1 - epsilon`) and validatable; the reported witness model
remains the flattened rational (`find_delta_for_strict_bounds`),
consistent with the existing epsilon semantics.
## Validation
- Strict optima correct: `1-eps`, `1+eps`, bounded `2<r<5 -> 5-eps`, and
lex/box variants.
- Integer optima and the #10028 shared-symbol cases unchanged (Golomb
n=6/7/8 -> 17/25/34, consistent with the model).
- Unit tests **92/92** (release); no new debug-suite failures.
- Opt regression corpus (73 files, `model_validate=true`)
**byte-identical** to baseline.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
The Nightly **Mac ARM64 Build** job fails on current Xcode/libc++
because `std::format` pulls floating-point formatting paths that require
`std::to_chars` availability from macOS 13.3+. The job was still
compiling with a 13.0 deployment target.
- **Root cause**
- ARM64 nightly job used:
- `MACOSX_DEPLOYMENT_TARGET=13.0`
- `mk_unix_dist.py --os=osx-13.0`
- This mismatched the effective libc++ requirements in the runner
toolchain.
- **Workflow change**
- Updated only `.github/workflows/nightly.yml` for `mac-build-arm64`:
- `MACOSX_DEPLOYMENT_TARGET: "13.0" -> "13.3"`
- `--os=osx-13.0 -> --os=osx-13.3`
- **Resulting behavior**
- ARM64 nightly build target now aligns with the minimum OS level
required by the formatting code paths used by current compilation units.
```yaml
# .github/workflows/nightly.yml (mac-build-arm64)
env:
MACOSX_DEPLOYMENT_TARGET: "13.3"
- name: Build
run: python scripts/mk_unix_dist.py --dotnet-key=$GITHUB_WORKSPACE/resources/z3.snk --arch=arm64 --os=osx-13.3
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Hoists loop-invariant matrix reads out of the hot inner loop of
`pivot_column_non_fractional` in the Hermite Normal Form (HNF)
computation used by z3's linear-arithmetic integer solver. The
arithmetic is unchanged; the patch only removes repeated
permutation-indexed `mpq` accesses from an O(n2) elimination loop.
## Hotspot
`lp::hnf_calc::pivot_column_non_fractional<M>` (`src/math/lp/hnf.h:130`)
performs the Bareiss-style fraction-free Gaussian elimination step over
a matrix `m`:
```cpp
for (unsigned j = r + 1; j < m.column_count(); ++j)
for (unsigned i = r + 1; i < m.row_count(); ++i)
m[i][j] = (r > 0) ? (m[r][r]*m[i][j] - m[i][r]*m[r][j]) / m[r-1][r-1]
: (m[r][r]*m[i][j] - m[i][r]*m[r][j]);
```
For `general_matrix`, every `m[a][b]` builds a temporary `ref_row` and
performs two permutation-array indirections (row and column permutation
lookups in `src/math/lp/general_matrix.h`) before the underlying vector
access. Inside this double loop the terms `m[r][r]`, `m[r-1][r-1]` and
`m[r][j]` are re-read on every iteration even though they are invariant,
so those redundant indexed reads dominate the loop cost.
## Change and complexity argument
Rows `<= r` are never written by this loop — it only assigns `m[i][j]`
for `i > r`, `j > r` — so the three pivot entries in rows `<= r` are
loop-invariant:
- `m[r][r]` and `m[r-1][r-1]` are invariant across **both** loops → bind
`m[r][r]` to a reference and take a pointer to `m[r-1][r-1]` once before
the outer loop. The pointer is `nullptr` when `r == 0`, which also
encodes the existing "no division" case with a single branch.
- `m[r][j]` is invariant across the inner `i` loop → hoist it to a
reference at the top of the outer `j` loop.
- `m[i][j]` is bound to a reference so it is indexed once per iteration
instead of three times (two reads + one write).
This turns **O(n2)** repeated permutation-indexed `mpq` reads into
**O(1)/O(n)** hoisted reads. The operands, operation order, and division
are identical to the original, so the computed matrix is bit-for-bit the
same.
## Measurements
Profiled with callgrind (z3 built with the same configuration,
`model_validate=true`) on a representative integer-arithmetic problem
that exercises the HNF cut generator:
- Target function instructions: **6,793,150,548 → 6,241,093,226**
(0.9187×; its share of total drops 15.2% → 14.5%).
- Total program instructions: **44,727,385,309 → 43,036,726,143**
(0.9622×).
- Wall-clock: **5.53s → 4.89s (~11.6% faster)**.
- Differential correctness preserved: identical solver output before and
after the change.
## Logic class
Integer linear arithmetic — the HNF-based cut generation path in the
`lp` int-solver.
<!-- gh-aw-workflow-id: coz3-deepperf-fix -->
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Details in original PR: https://github.com/Z3Prover/z3/pull/10007
---------
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Can Cebeci <can.cebeci99@gmail.com>
Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
The Ubuntu `python make - MT` job was failing in unit tests because the
debug-time well-sorted check could invalidate freshly constructed
assertion expressions during solver entry. This surfaced as crashes in
`theory_dl` and `seq_rewriter`, not as logic bugs in those tests.
- **Root cause**
- `is_well_sorted` traversed the input through a temporary
`expr_ref`/`subterms` wrapper.
- For freshly built assertions passed directly into `assert_expr`, that
temporary ownership could drop the last refcount during validation and
free the AST before the solver used it.
- **Change**
- Reworked the traversal in `src/ast/well_sorted.cpp` to walk raw
`expr*` nodes explicitly.
- The checker now validates subterms without taking transient ownership
of the asserted expression.
- **Effect**
- Debug validation remains intact.
- Temporary formulas survive the well-sorted check, so assertion-time
validation no longer corrupts the caller’s AST.
- **Representative change**
```cpp
ptr_vector<expr> todo;
expr_mark visited;
todo.push_back(e);
while (!todo.empty()) {
expr* term = todo.back();
todo.pop_back();
if (visited.is_marked(term))
continue;
visited.mark(term, true);
if (is_app(term)) {
for (expr* arg : *to_app(term))
if (!visited.is_marked(arg))
todo.push_back(arg);
check_app(to_app(term));
}
else if (is_var(term)) {
check_var(to_var(term));
}
else if (is_quantifier(term)) {
check_quantifier(to_quantifier(term));
}
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Fixes a completeness regression where `elim_uncnstr` was silently
disabled for ordinary (non-polymorphic) goals, detected by the
`snapshot-regression` corpus.
- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/3054
- **Benchmark:** `iss-6260/small-2.smt2` (corpus `Z3Prover/bench`,
`inputs/issues/iss-6260/`)
- **Divergence:** recorded oracle `sat` → current z3 produces `unknown`
### Divergence diff
```diff
--- small-2.expected.out (expected)
+++ produced (current z3)
@@ -1,3 +1,3 @@
-sat
+unknown
(error "line 17 column 0: unexpected character")
(error "line 17 column 1: unexpected character")
```
(The `(error ...)` lines are expected: the benchmark contains a stray
```` ``` ```` fence on line 17. Only the `sat` → `unknown` change is the
regression.)
## Root cause
`git bisect` over the regression window pins the flip to commit
`208cc5686` ("fix build"), which added `|| m().has_type_vars()` to the
`elim_uncnstr_tactic` guard and an equivalent `if (m.has_type_vars())
return;` to the `elim_unconstrained` simplifier.
`ast_manager::has_type_vars()` is a **manager-wide, sticky** flag: it is
set to `true` as soon as *any* type variable is created, and is never
reset. In particular `finite_set_decl_plugin::init()` creates type
variables `A`/`B` to define its polymorphic signatures. Those type
variables never occur in the user's assertions, but once the finite_set
plugin is initialized — which happens while processing this benchmark —
the flag is globally `true` (confirmed by instrumenting `mk_type_var`:
the only type vars created for this benchmark are the finite_set
signature vars `A` and `B`).
As a result `elim_uncnstr` bails out for goals that contain **no**
polymorphic terms at all, i.e. it is effectively disabled. Unconstrained
subterms that used to be eliminated now reach the theory solvers.
For this benchmark the (single) assertion is `(not (xor (>= x 0) (>= x1
0) (>= x 0) x4 (str.contains ...)))`. The duplicated `(>= x 0)` cancels
(`a xor a = false`), and the free Boolean `x4` can fix the parity
regardless of the value of the `str.contains` term, so the goal is
trivially `sat`. That `str.contains`/`str.replace_re` subterm is
unconstrained and was previously removed by `elim_uncnstr`; without that
elimination it reaches `theory_seq`, which marks `str.replace_re` as
unhandled and gives up in `final_check` → `unknown` (`incomplete (theory
seq)`).
## Fix
Make the guard precise. Keep `has_type_vars()` as a cheap pre-filter
(matching existing usage in `ast_translation.cpp` and
`ast_manager::has_type_var`), but only bail out when the goal / asserted
formulas **actually** contain type-variable typed terms, using the
existing `polymorphism::util::has_type_vars(expr*)`.
This preserves the polymorphism crash-protection (goals with genuine
type-variable terms still skip `elim_uncnstr`) while restoring
`elim_uncnstr` for the vast majority of goals that merely triggered a
polymorphic-plugin initialization. Both twin guards (the `elim_uncnstr`
tactic and the `elim_unconstrained` simplifier) are fixed consistently.
## Validation
Built this checkout and re-ran the benchmark (step 5 of the fixer
workflow):
- `./configure && make -C build -j$(nproc)` — Z3 version 4.17.0.
- Unpatched master reproduced the divergence: `z3 -T:20
iss-6260/small-2.smt2` → `unknown`.
- After the fix, `z3 -T:20 inputs/issues/iss-6260/small-2.smt2` produces
**exactly** the recorded oracle:
```
sat
(error "line 17 column 0: unexpected character")
(error "line 17 column 1: unexpected character")
(error "line 17 column 2: unexpected character")
```
- Regression sanity checks: sibling `iss-6260/small.smt2` unchanged
(`sat`); plain arithmetic unconstrained goals unchanged; polymorphic
goals with genuine type-variable terms (including `declare-type-var` and
forcing `(check-sat-using (then elim-uncnstr smt))`) still solve without
crashing — the guard still fires for those.
Opened as a **draft** for human review.
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28844840657)
· 861.2 AIC · ⌖ 45.8 AIC · ⊞ 8.9K ·
[◷](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.63, model: claude-opus-4.8, id:
28844840657, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28844840657 -->
<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This patch fixes a corner case where quantifier conflicts can create
fresh terms that aren't marked as relevant.
I couldn't easily produce a minimal query that this patch turns stable,
nor did the patch stabilize the query I have been working on, but I
think the example below still illustrates the problem:
```
(set-option :auto_config false)
(set-option :type_check true)
(set-option :smt.case_split 3)
(set-option :smt.mbqi false)
(declare-fun R (Int) Bool)
(declare-fun S (Int) Bool)
(declare-fun dummy (Int) Bool)
(assert (or (R 0) (dummy 0)))
(assert (forall ((x Int)) (!
(and (not (R x)) (not (S x)))
:pattern ((R x))
:qid not_r_not_s
)))
(assert (forall ((x Int)) (!
(S x)
:pattern ((S x))
:qid s_true
)))
(check-sat)
```
The query is unstable (due to the same interaction between relevancy and
triggers in https://github.com/Z3Prover/z3/issues/7444): if the solver
assigns `(dummy 0)` first, it returns `unknown`.
If the solver assigns `(R 0)` first, we would expect an `unsat`. The
current implementation returns `unknown` because `not_r_not_s` leads to
a quantifier conflict, which creates `S(x)` without marking it (or any
of its ancestors) as relevant.
---------
Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This removes the temporary `lp.batch_explain_fixed_in_row` knob added
with the recent LP changes. The batched fixed-column explanation path is
kept as the only implementation, matching the follow-up review comments.
- **Problem**
- The new LP setting exposed a temporary fallback path that is no longer
needed.
- Keeping both paths added parameter surface area and settings plumbing
without a lasting behavioral distinction.
- **Changes**
- **Remove parameter definition**
- Delete `lp.batch_explain_fixed_in_row` from LP parameter generation.
- **Remove settings plumbing**
- Drop the stored field, accessor methods, and parameter update wiring
from `lp_settings`.
- **Keep batched explanation as default behavior**
- Remove the runtime branch in `lar_solver::explain_fixed_in_row`.
- Always linearize fixed-column witnesses together in a single
dependency pass.
- **Resulting simplification**
- The solver no longer carries a dead configuration toggle for fixed-row
explanation.
- The batched dependency-linearization path remains intact and is now
the sole code path.
```c++
void lar_solver::explain_fixed_in_row(unsigned row, explanation& ex) {
auto& witnesses = m_imp->m_tmp_witnesses;
witnesses.reset();
for (auto const& c : get_row(row)) {
if (!column_is_fixed(c.var()))
continue;
const column& ul = m_imp->m_columns[c.var()];
witnesses.push_back(ul.lower_bound_witness());
witnesses.push_back(ul.upper_bound_witness());
}
m_imp->m_tmp_dependencies.reset();
m_imp->m_dependencies.linearize(witnesses, m_imp->m_tmp_dependencies);
for (auto ci : m_imp->m_tmp_dependencies)
ex.push_back(ci);
}
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Wheels started inheriting `macosx_15_0` tags because macOS jobs run on
newer runners and no deployment target was pinned. That blocks wheel
installation on macOS 13/14 hosts and forces source builds.
- **macOS deployment target pinning**
- Added `MACOSX_DEPLOYMENT_TARGET: "13.0"` to both macOS build jobs
(`x64`, `arm64`) in:
- `.github/workflows/release.yml`
- `.github/workflows/nightly.yml`
- **Stable macOS artifact OS metadata**
- Updated macOS `mk_unix_dist.py` invocations to pass `--os=osx-13.0` in
both workflows, so artifact metadata stays aligned with the intended
minimum macOS compatibility used for Python wheel tagging.
```yaml
mac-build-x64:
runs-on: macos-15
env:
MACOSX_DEPLOYMENT_TARGET: "13.0"
steps:
- name: Build
run: python scripts/mk_unix_dist.py --dotnet-key=$GITHUB_WORKSPACE/resources/z3.snk --arch=x64 --os=osx-13.0
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Fixes a build error (C3694) from an illegal specifier in the structured
binding at pattern_inference.cpp:127, and removes the temporary
is_well_sorted SASSERTs (and well_sorted.h include) from rewriter_def.h
that were used during pattern-inference diagnosis.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The higher-order matcher produced ill-typed instantiations that aborted
the solve (sort-mismatch / unbound-variable exceptions), making
smt.ho_matching=true net-negative on the TPTP THF benchmarks.
Two root causes:
1. Imitation rule (ho_matcher.cpp): the select chain 'pats' is collected
outermost-first, i.e. in reverse application order. The imitating
lambda must curry arguments in application order (first-applied select
binds the outermost lambda). Reversing 'pats' before building the
domain/argument/body vectors and the lambda-wrapping loop makes the
constructed lambda's sort agree with the flex head variable. Fixes
unit-test ho_matcher test6c/test6d (previously asserted at
add_binding: v->get_sort() == t->get_sort()).
2. Instance assembly (smt_quantifier.cpp on_ho_match): the fixpoint
binding substitution used var_subst with the default std_order=true
while the binding vector is directly indexed (binding[k] = value for
var k). This resolved chained HO variable references against the wrong
slots and built ill-sorted terms (assertion at rewriter_def.h:52).
Use direct (std_order=false) substitution to match the binding layout.
Also adds defensive guards as belt-and-suspenders: subst_sorts_match
skips sort-inconsistent substitutions, an is_ground check skips bindings
with leftover de Bruijn variables, and on_ho_match catches z3_exception
to skip an unusable heuristic instance rather than aborting the solve
(re-raising only on cancellation/resource-limit).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add -st statistics counters:
- ho-matching refinements / instances (default_qm_plugin, gated on
smt.ho_matching)
- ho-var term-enum: terms produced by mf::ho_var::populate_inst_sets
in the model finder
Wired via a new quantifier_manager_plugin::collect_statistics virtual
forwarded from quantifier_manager::collect_statistics.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Summary
Reverts #10052, whose eager-commit of infinitesimal LP hints is
**unsound** for shared-symbol objectives.
#10052 added, in `opt_solver::maximize_objective`:
```cpp
if (val.is_finite() && !val.get_infinitesimal().is_zero() && val > m_objective_values[i])
m_objective_values[i] = val;
```
on the premise that *"a non-zero infinitesimal ⇒ an exact, unattainable
strict optimum, so the LP hint is authoritative."* That holds for a
**pure LP**, but is **false when the objective is a shared symbol** with
another theory (e.g. the auxiliary uninterpreted function used to encode
a `distinct` with > 32 arguments). There the LP relaxation only yields a
*hint* that can be a strict **over-estimate**, and #10052 commits it
without validation — exactly the class of bound that #10028's
`check_bound` exists to reject.
## Counterexample
A 6-mark Golomb ruler over integers `x0..x5`, with the `distinct` padded
to > 32 arguments so `x5` becomes a shared symbol; objective is a real
`obj` with `obj > x5` (full file attached to #5720):
- Ground truth: `minimize x5` (integer) ⇒ **17**; since `obj > x5`, the
true optimum is **`17 + ε`**.
- With #10052, z3 reports **`(obj (+ 5.0 epsilon))`** — wrong and
**infeasible** (`obj < 6` is `unsat`; the returned model itself has `x5
= 35, obj = 49.5`).
| benchmark | with #10052 (master) | after this revert |
| --- | --- | --- |
| Golomb `bug.smt2` (shared symbol) | `(obj (+ 5.0 epsilon))` ❌
infeasible | `(obj 18)` ✅ consistent |
| #5720 (`max r < 1`) | `1 - epsilon` ✅ | `0` ❌ (regression returns) |
## Tradeoff / follow-up
This revert restores soundness on the shared-symbol case but
**reintroduces the #5720 regression** (`max r<1` ⇒ `0`), which is why
**#5720 has been reopened**. A correct fix should preserve the strict
single-objective supremum **without** trusting an unvalidated
shared-symbol hint — e.g. gate the eager commit on `!has_shared` (pure
LP only), or validate the rational part of the hint while keeping the
infinitesimal. The same blind spot affects the alternative `check_bound`
guard proposed in #10051.
Re: #5720
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
### Summary
`lp_bound_propagator::explain_fixed_in_row` explained every fixed column
of a row
independently, calling `lar_solver::explain_fixed_column` once per fixed
column
(`src/math/lp/lar_solver.cpp`). Each such call linearizes the lower- and
upper-bound witnesses of a single column — a BFS over the `u_dependency`
DAG using
the dependency manager's mark bits — and inserts every reached leaf
constraint into
the `explanation`.
Fixed columns of the same row routinely share large portions of their
bound-witness
sub-DAGs (common ancestor constraints). The per-column scheme therefore
re-traverses
those shared sub-DAGs and re-inserts their leaves once for *every*
column, with an
independent mark/unmark cycle per column.
### Change
Add `lar_solver::explain_fixed_in_row(row, ex)`, which collects the
lower/upper
witnesses of all fixed columns in the row and linearizes them together
in a single
`u_dependency_manager::linearize` pass.
`lp_bound_propagator::explain_fixed_in_row`
and `explain_fixed_in_row_and_get_base` now delegate to it; the
base-column lookup in
the latter is unchanged. `explain_fixed_column` is kept for its
single-column caller.
### Why it is correct
`explanation` is a set — `push_back` deduplicates. Dependency
reachability is
monotone, so the union of the per-column leaf sets equals the leaf set
of the union
of all roots: the batched pass yields exactly the same explanation. The
manager's
mark bits guarantee each shared sub-DAG node is visited once, and the
`linearize(ptr_vector, ...)` overload already skips null/duplicate
roots.
### Complexity
For a row with `N` fixed columns:
- before: `O(Σ_j |witness-DAG(j)|)` traversal + `O(Σ_j leaves(j))` set
insertions, with `N` mark/unmark cycles;
- after: `O(|⋃_j witness-DAG(j)|)` traversal + `O(#distinct leaves)` set
insertions, with a single mark/unmark cycle.
Shared sub-DAGs are walked and their leaves inserted once instead of
once per column.
### Measured effect
Profiled with callgrind on a representative conflict-heavy `QF_SLIA`
input
(`model_validate=true`, bounded run), baseline vs. patched:
- `lp::lar_solver::explain_fixed_column` on the hot path:
`24,337,671,616 → 0`
retired instructions (59.2% → 0% of the run), replaced by the single
batched
traversal;
- total retired instructions: `41,113,093,210 → 35,983,363,256` (×0.875,
≈ 12.5%
fewer) — the net work removed by de-duplicating shared sub-DAGs;
- wall-clock: `6.428 s → 6.079 s` (≈ 5.4% faster);
- differential correctness preserved (identical results across the
validation inputs).
<!-- gh-aw-workflow-id: coz3-deepperf-fix -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/coz3-deepperf-fix -->
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Summary
Fixes a Z3 output regression detected by the `Z3Prover/bench`
snapshot-regression corpus.
- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/3050
- **Benchmark:** `iss-5134/small.smt2`
(`inputs/issues/iss-5134/small.smt2` in `Z3Prover/bench`)
- **Kind:** `diff` — recorded oracle vs. current nightly z3
(`z3-4.17.0-x64-glibc-2.39`)
## Divergence
The benchmark constrains a string `a` using a regex that contains
`(re.range "" <ite>)`:
```smt2
(declare-fun a () String)
(assert (str.in_re a (re.* (re.union (str.to_re "b") (str.to_re (ite
(str.in_re a (re.* (re.range "" (ite (str.in_re a (str.to_re "")) ""
a)))) "" "a"))))))
(assert (not (str.in_re a (re.* (str.to_re "")))))
(check-sat)
(get-model)
```
Recorded oracle (**expected**) vs. current z3 (**current**):
```diff
-sat
-(
- (define-fun a () String
- "a")
-)
+unknown
+(error "line 7 column 10: model is not available")
```
## Root cause
Per SMT-LIB, `re.range` over an argument that is **not a single
character** denotes the empty language, so `(re.range "" X)` is
`re.none` regardless of `X` (the lower bound `""` is the empty string).
Before the *"Derive with ranges"* refactor (#9963 / #9965),
`seq_rewriter::mk_re_range` recognised this through several emptiness
checks, including a concrete non-single-character test and a `max_length
== 0` test:
```cpp
if (str().is_string(lo, slo) && slo.length() != 1) is_empty = true;
if (max_length(lo) == std::make_pair(true, rational(0))) is_empty = true;
if (max_length(hi) == std::make_pair(true, rational(0))) is_empty = true;
```
The refactor rewrote `mk_re_range` and kept only the `min_length(..) >
1` emptiness test (a bound provably **≥ 2** characters). That misses a
bound of length **exactly 0**: an empty-string bound has `min_length ==
0`, so it is no longer detected as empty, and `mk_re_range` returns
`BR_FAILED`, leaving `(re.range "" X)` symbolic. The new range-aware
derivative engine (`seq_derive.cpp`) then produces a *stuck* derivative
for such a range (its `is_unit_string("")` test fails), so the sequence
theory can no longer decide membership and the solver answers `unknown`
/ "model is not available".
## Fix
Restore the sound emptiness check the refactor dropped — a bound whose
`max_length` is provably `0` can never be a single character, so the
range is empty:
```cpp
// A bound that is provably of length 0 (e.g. the empty string "") can
// likewise never be a single character, so the range is empty. Unlike a
// symbolic bound, max_length == 0 is a provable emptiness fact, so this is
// sound (it is never true for a model-dependent bound such as a variable).
if (max_length(lo) == std::make_pair(true, rational(0)))
is_empty = true;
if (max_length(hi) == std::make_pair(true, rational(0)))
is_empty = true;
```
This does **not** reintroduce the unsoundness the refactor guarded
against: `max_length == (true, 0)` is a *provable* emptiness fact and is
never true for a model-dependent (symbolic) bound, so `(re.range x x)`
is still correctly left symbolic (it denotes `{x}` whenever `x` is a
single character).
## Validation
Built the patched `./z3` checkout (`./configure && make -C build`) and
re-ran the benchmark with the option the snapshot capture uses
(`-T:20`):
- **Before the fix:** `z3 -T:20 small.smt2` → `unknown` + `(error "...
model is not available")` — reproduces the divergence.
- **After the fix:** `z3 -T:20 small.smt2` → `sat` + `(define-fun a ()
String "a")` — **exactly matches** the recorded oracle.
Additional checks with the rebuilt binary:
- Sibling benchmarks `iss-5134/bug.smt2` and `iss-5134/small-2.smt2`
still match their oracles.
- Symbolic bound not over-collapsed: `(str.in_re "a" (re.range x x))` →
`sat` (x = "a").
- `(re.range "" "a")` is the empty language: `(str.in_re "a" (re.range
"" "a"))` and `(str.in_re "" (re.range "" "a"))` → `unsat`.
- Ordinary ranges unaffected: `"b" ∈ (re.range "a" "c")` sat, `"d" ∈
(re.range "a" "c")` unsat, `(re.range "a" "a")` singleton.
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28731229299)
· 592.3 AIC · ⌖ 39.1 AIC · ⊞ 8.9K ·
[◷](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.63, model: claude-opus-4.8, id:
28731229299, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28731229299 -->
<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Summary
Fixes a Z3 optimization regression where maximizing a real objective
under a
**strict** inequality returned a plain feasible model value instead of
the
strict supremum.
Originating discussion:
https://github.com/Z3Prover/bench/discussions/3053
Benchmark: `iss-5720/bug-1.smt2` (in `Z3Prover/bench`)
```smt2
(declare-const r Real)
(assert (< r 1))
(maximize r)
(check-sat)
(get-objectives)
```
The optimum of `r` subject to `r < 1` is the strict supremum `1 -
epsilon`,
which the recorded oracle expects. Current z3 instead reports the
feasible
point `0`.
## Divergence
```diff
--- bug-1.expected.out (expected)
+++ produced (current z3)
@@ -1,4 +1,4 @@
sat
(objectives
- (r (+ 1.0 (* (- 1.0) epsilon)))
+ (r 0)
)
```
## Root cause
Regression from commit `fdc32d0e6` ("Fix inconsistent optimization
result with
unvalidated LP bound", #10028). That change stopped committing the LP
optimization hint `val` to `m_objective_values` up front in
`opt_solver::maximize_objective`, deferring the commit until
`check_bound()`
validates it. Its goal is to reject **plain-rational** over-estimates
produced
when the objective shares symbols with other theories (e.g. the
auxiliary
uninterpreted function used to encode large `distinct` constraints);
those
over-estimates have a **zero** infinitesimal.
For a strict real supremum/infimum the hint has a **non-zero**
infinitesimal
(here `val = 1 - epsilon`). `check_bound()` can never validate it,
because
`opt_solver::mk_ge` drops the negative infinitesimal (mathematically,
`r >= 1 - epsilon` is equivalent over the reals to `r >= 1`), turning
the
validation bound into the unsatisfiable `r >= 1` given `r < 1`.
Validation
therefore fails, `maximize_objective` returns `false`, and
`m_objective_values`
is left holding the strictly smaller current **model** value (`0`),
which
`optsmt::geometric_lex` then reports as the optimum.
## Fix
`src/opt/opt_solver.cpp`, `maximize_objective`: restore the pre-#10028
eager
commit of the hint, **scoped to finite values with a non-zero
infinitesimal**:
```cpp
if (val.is_finite() && !val.get_infinitesimal().is_zero() && val > m_objective_values[i])
m_objective_values[i] = val;
```
A finite value with a non-zero infinitesimal is a strict optimum that no
concrete model can attain and that `check_bound()` cannot validate, so
the
arithmetic hint is authoritative and must be preserved. Plain-rational
(zero-infinitesimal) values — including **all integer objectives** and
the
`#10028` shared-symbol over-estimates — do not enter this branch and
continue
through the deferred-commit validation path unchanged, so `#10028` is
structurally preserved. The change does not alter control flow or the
return
value, so the lex/box drivers behave as before.
## Validation
Built the patched `./z3` checkout (`./configure && make -C build
-j$(nproc)`)
and re-ran the benchmark with the same options the snapshot capture
uses:
```
$ ./build/z3 -T:20 inputs/issues/iss-5720/bug-1.smt2
sat
(objectives
(r (+ 1.0 (* (- 1.0) epsilon)))
)
```
This is a **byte-exact match** with the recorded `bug-1.expected.out`
oracle.
Additional before/after checks on the rebuilt binary (baseline = current
nightly, unpatched):
| case | baseline | patched |
| --- | --- | --- |
| single strict-real max `r<1` | `r=0` ❌ | `r=1-eps` ✅ (target) |
| single strict-real min `r>1` | `r=0` ❌ | `r=1+eps` ✅ |
| non-strict real max `r<=1` | `r=1` ✅ | `r=1` ✅ |
| integer max `x<10` | `x=9` ✅ | `x=9` ✅ |
| bounded strict `2<r<5` | — | `r=5-eps` ✅ |
| box: two strict reals | — | both `-eps` ✅ |
| lex: nonstrict-real then int | `r=1,x=9` ✅ | `r=1,x=9` ✅ |
| lex: int then nonstrict-real | `x=9,r=5` ✅ | `x=9,r=5` ✅ |
| lex: all integer | `x=9,y=9` ✅ | `x=9,y=9` ✅ |
| lex: int then strict-real (final) | `x=9,r=0` ❌ | `x=9,r=1-eps` ✅ |
All well-defined lex/box cases are preserved, and a strict-real
objective as
the **final** lex objective is now also correct.
## Known limitation (pre-existing, honest disclosure)
Lexicographic optimization where a **non-final** objective is a strict
real
supremum (e.g. `maximize r` with `r<1`, *then* `maximize x`) remains
ill-defined: the supremum `1-epsilon` is not attained by any model, so
`optsmt::commit_assignment` asserting `r >= 1-epsilon` (which `mk_ge`
reduces to
`r >= 1`) contradicts `r < 1`. This corner is already mishandled by the
current
nightly (it returns `r=0`) and is not what discussion #3053 reports;
this patch
does not attempt to redefine that semantics. It changes only how that
corner
manifests, while fixing the reported single-objective divergence and all
well-defined cases above.
Draft for human review.
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28733642068)
· 691.9 AIC · ⌖ 44.2 AIC · ⊞ 8.9K ·
[◷](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.63, model: claude-opus-4.8, id:
28733642068, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28733642068 -->
<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Small readability refactor in `opt_solver`, no behavioral change.
## Rename
- `m_models` → `m_objective_models`
- `m_last_model` → `m_model`
## Rationale
`m_models` is the per-objective vector of witnessing models, indexed by
the objective index `i` exactly like `m_objective_vars`,
`m_objective_values`, and `m_objective_terms`. It was the only member of
that parallel family not following the `m_objective_*` naming, so
`m_objective_models` makes the intent self-documenting.
`m_last_model` is the single, transient model most recently obtained
from the context and handed back to callers via `get_model_core`.
Renaming it to `m_model` reads more naturally, and the two now-distinct
names (`m_model` vs `m_objective_models`) avoid the previous one-letter
`m_model`/`m_models` clash hazard.
Both are private members of `opt_solver`, so the change is fully
self-contained within `opt_solver.{h,cpp}`. A stale TRACE label ("last
model") was updated to "current model" to match.
## Testing
- Builds clean (CMake/Ninja, Release).
- `test-z3 /a`: 92 passed, 0 failed.
- Spot-checked optimization behavior (single-objective minimize with
large `distinct`, box mode) — unchanged.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Fixes#10028.
## Problem
Minimizing an integer variable over a problem containing a large
`distinct` constraint returned an **inconsistent** result: the reported
optimum did not match the returned model, and it was not the true
optimum.
Reproducer from the issue (a Golomb-ruler problem, true optimum = 55):
```python
import z3
n, U = 10, 500
x = [z3.Int(f"x{i}") for i in range(n)]
o = z3.Optimize()
for xi in x: o.add(xi >= 0, xi <= U)
o.add(x[0] == 0)
for i in range(n - 1): o.add(x[i] < x[i + 1])
o.add(z3.Distinct([x[j] - x[i] for i in range(n) for j in range(i + 1, n)]))
h = o.minimize(x[n - 1])
print(o.check(), o.lower(h), o.upper(h), o.model()[x[n - 1]])
# sat 20 20 500 <-- objective 20, but model has x9 = 500 (and 20 is unsat)
```
## Root cause
A `distinct` with more than 32 arguments is encoded with a fresh
uninterpreted sort and function (`smt_internalizer.cpp`), so the
objective variable becomes a *shared symbol* whose feasible values
depend on EUF as well as arithmetic. The arithmetic relaxation therefore
only produces a **hint** for the optimum, which may over-estimate it and
be unachievable.
Two combined defects:
- `opt_solver::maximize_objective` committed the hint into
`m_objective_values` **before** validating it with `check_bound`, and
never rolled it back when validation failed. `update_objective` only
ever *raises* the stored value, so the real (achievable) model value was
discarded.
- `optsmt::geometric_lex` **ignored** the boolean return value and
asserted the blocker derived from the unachievable hint, so the very
next `check_sat` was UNSAT and the search terminated prematurely,
reporting the bogus bound together with a non-matching model.
## Fix
- `opt_solver.cpp`: do not commit the hint before it is validated. On
validation failure, `update_objective` now records the actual achievable
model value. The no-model early-return keeps its previous behavior.
- `optsmt.cpp`: `geometric_lex` now honors the validation result. When
the hint could not be validated, it discards the poisoned blocker and
tightens from the real model value, so the search keeps converging
toward the true optimum. When the hint is valid, the condition reduces
to the original expression and behavior is unchanged.
After the fix the same reproducer produces consistent,
monotonically-improving bounds (325 → 85 → … → 58 → … → 55), and the
reported objective always matches the returned model.
## Testing
Exact-optimum, fast-terminating checks (all correct): EUF-forced minimum
(= 5), `distinct(x, 0..32)` minimize (= 33), Golomb n=8 (= 34), plus
basic min/max, real objective, box, lex, pareto, and weighted
soft/maxsat.
Regression suites, rebuilt in **both Release and Debug**:
| Suite | Release | Debug |
|-------|---------|-------|
| `test-z3 /a` | 92 passed, 0 failed | 92 passed, 0 failed |
| z3test `regressions/smt2` (908 files, `model_validate=true`) | 0
failures | 0 failures |
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
