remove_element uses swap-remove but deep-copied the relocated tail coefficient.
In namespace lp the coefficient type is rational (copyable), so this allocates
on the heap for large coefficients. Since the tail element is popped right after,
relocate large coefficients by swapping instead, avoiding the allocation; small
coefficients still use a plain copy (cheaper than swapping mpz internals).
Reported in Z3Prover/bench#3143 (remove_element was the top hotspot). Verified
correctness-neutral (identical results, 92/92 unit tests); ~1.5% faster on the
certora large-coefficient set, neutral on small-coefficient inputs.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: fd5693e4-3b1d-4dac-b3be-2942ae6f31f8
`ASSERTION VIOLATION` at `bv2int_translator.h:72` when using
`smt.bv.solver=2` with formulas containing `abs` (or other arith
expressions that rewrite to ITE with arith predicates).
**Root cause**
`ensure_translated` skips adding sub-expressions of boolean non-BV nodes
to the `todo` list — correct, since the base theory owns them in plugin
mode. However, `translate_expr`'s early-return only covered
`basic_family_id` booleans, not non-basic ones (e.g.,
`arith_family_id`).
When `(abs f)` is rewritten by the arith rewriter to `(ite (>= f 0) f (-
f))`, the predicate `(>= f 0)` ends up in `todo` (as a child of the
ITE), but its own children (e.g., the integer literal `0`) are not
added. `translate_expr` then calls `translated(0)` on an unmapped
expression, firing `SASSERT(r)`.
Reproducer:
```smt2
(declare-const f Int)
(assert (= 0 (mod 0 (bv2nat ((_ int_to_bv 1) (abs f))))))
(check-sat)
; z3 test.smt2 smt.bv.solver=2 → ASSERTION VIOLATION (before fix)
```
**Fix**
Extend the early-return in `translate_expr` to match
`ensure_translated`'s skip condition — all boolean non-BV expressions in
plugin mode map to themselves:
```cpp
// before
if (m_is_plugin && ap->get_family_id() == basic_family_id && m.is_bool(ap)) {
// after
if (m_is_plugin && m.is_bool(ap) && ap->get_family_id() != bv.get_family_id()) {
```
BV boolean predicates (`bvule`, etc.) are unaffected — they still route
through `translate_bv`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`Expr.getSort()` on a constant with an `EnumSort` sort returns a
`DatatypeSort`, causing `ClassCastException` when enum-specific methods
are called.
```java
Context ctx = new Context();
EnumSort<Foo> enumSort = ctx.mkEnumSort("my-enum", "e1", "e2");
Expr<EnumSort<Foo>> c = ctx.mkConst("my-const", enumSort);
c.getSort().getName(); // ClassCastException — getSort() returns DatatypeSort, not EnumSort
```
### Changes
- **`Sort.java`**: In `Sort.create()`, detect enum sorts at the
`Z3_DATATYPE_SORT` case by checking whether all constructors have arity
0 — matching Z3's own `util::is_enum_sort` logic in
`datatype_decl_plugin.cpp`. Return `EnumSort<>` when true,
`DatatypeSort<>` otherwise.
- **`EnumSort.java`**: Add package-private `EnumSort(Context ctx, long
obj)` constructor so an `EnumSort` can be instantiated from an existing
native sort handle (analogous to `DatatypeSort(Context ctx, long obj)`).
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Fixes the divergence in issue #7464: formulas involving `mod`/`div` by a
**variable** divisor could send `smt.arith.solver=6` into a
non-terminating nonlinear search.
Minimal reproducer (UNSAT, previously timed out; now solved in <0.5s):
```smt2
(declare-fun V () Int)
(declare-fun n () Int)
(declare-fun l () Int)
(assert (and (> V 0) (= 0 (mod n 2)) (= (div n 2) (div n l)) (= 0 (mod (div n l) V))))
(assert (distinct 0 (mod n V)))
(check-sat)
```
## Root cause
A variable-divisor `mod n V` is axiomatized by the Euclidean identity
`n = V*(n div V) + (n mod V)`. The `V*(n div V)` term is nonlinear, so
arith.solver=6
hands the problem to the nlsat/Gröbner branch, which branches on values
of `V` with no
termination bound and diverges.
## Fix
Add a **linear divisibility closure** lemma in `nla_divisions`:
> `mod(a, y) = 0 & x = c*a` (c an integer constant) ⟹ `mod(x, y) = 0`.
The emitted clause
```
(x - c*a != 0) \/ (mod(a, y) != 0) \/ (mod(x, y) = 0)
```
is a **tautology for every integer `c`**, so mining a candidate `c =
val(x)/val(a)` from
the current model can never be unsound. It is only emitted when all
three literals are
false in the current model, so the clause is a genuine
conflict/propagation and always
makes progress. This lets the theory refute the instance directly
instead of entering the
divergent nonlinear branch.
Variable-divisor `mod` terms were previously **not registered** in nla
at all; they are now
registered into a new `m_divisibility` list in `theory_lra`, so the
reasoner can pair a
violated `mod(x, y)` with a satisfied `mod(a, y)` of the same divisor.
## Changes
- `src/math/lp/nla_divisions.{h,cpp}` — new `m_divisibility` list
`{r=mod, x=dividend, y=divisor}`, `add_divisibility(...)`, and
`check_linear_divisibility()`; invoked from `divisions::check()`.
- `src/math/lp/nla_core.h`, `src/math/lp/nla_solver.{h,cpp}` —
forwarding of `add_divisibility`.
- `src/smt/theory_lra.cpp` — register variable-divisor `mod` into the
divisibility list.
## Validation
- `min.smt2` → `unsat` in 0.46s, minimized core → 0.15s (were timeouts).
- Soundness: 350 differential fuzz formulas (arith.solver=6 vs
arith.solver=2), **0 mismatches**.
- Spot checks correct (divisor-3 variant → unsat; non-divisible variants
→ sat).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
`decl_collector::visit_sort` did not collect sorts with `poly_family_id`
(type variables created via `mk_type_var` / `declare-type-var`), so
`solver::display` and `ast_pp_util::display_decls` never emitted type
variable declarations before referencing them — producing invalid
SMT-LIB2 output.
## Changes
- **`src/ast/decl_collector.h`**: added a dedicated `lim_svector<sort*>
m_type_vars` field (separate from `m_sorts`) with a `get_type_vars()`
getter; `reset()` clears it; `push()`/`pop()` maintain its scope.
- **`src/ast/decl_collector.cpp` — `visit_sort`**: sorts with
`poly_family_id` are now pushed to `m_type_vars` instead of `m_sorts`,
keeping type variables distinct from uninterpreted sorts:
```cpp
if (m.is_uninterp(n))
m_sorts.push_back(n);
else if (fid == poly_family_id)
m_type_vars.push_back(n);
```
- **`src/ast/ast_pp_util.h`**: added a `stacked_value<unsigned>
m_type_vars` cursor to track which type variables have already been
printed.
- **`src/ast/ast_pp_util.cpp` — `display_decls`**: emits
`(declare-type-var <name>)` for each collected type variable before
other sort declarations; `reset()`/`push()`/`pop()` maintain the new
cursor.
**Example** — given `(declare-type-var A)(declare-fun f (A) A)`, the
dump now correctly produces:
```smt2
(declare-type-var A)
(declare-fun f (A) A)
(assert ...)
```
The output round-trips cleanly through the Z3 parser.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `api_datalog` unit test was failing in CI with `"the logic has
already been set"`. Two consecutive regression tests shared a single
`Z3_context`, but both called `Z3_eval_smtlib2_string` with `(set-logic
HORN)` — the second call always fails because context logic state is
permanent.
## Changes
- **`src/test/api_datalog.cpp`**: Give each
`Z3_eval_smtlib2_string`-based regression test its own
`Z3_config`/`Z3_context`, destroyed immediately after the test block.
The outer context is retained only for the two tests that don't invoke
the SMT-LIB evaluator.
```cpp
// Before: both blocks shared `ctx`, second (set-logic HORN) always errored
Z3_string response = Z3_eval_smtlib2_string(ctx, chc1); // sets HORN logic
Z3_string response = Z3_eval_smtlib2_string(ctx, chc2); // ERROR: logic already set
// After: each block owns its context
Z3_config cfg2 = Z3_mk_config();
Z3_context ctx2 = Z3_mk_context(cfg2);
Z3_del_config(cfg2);
Z3_string response = Z3_eval_smtlib2_string(ctx2, chc2);
Z3_del_context(ctx2);
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The TPTP frontend was not forcing `pi.avoid_skolems=false`, so TPTP
problems could be solved with the default pattern-inference behavior
instead of the intended frontend-specific setting. This change applies
the override directly to the solver used by TPTP runs.
- **What changed**
- After constructing the TPTP solver, the frontend now sets
`pi.avoid_skolems=false` via solver parameters before `check_sat`.
- The override is scoped to the TPTP solver instance instead of mutating
process-global parameter state.
- **Why this shape**
- Keeps the TPTP behavior explicit at the point where the solver is
created.
- Avoids leaking the parameter change into unrelated solver contexts.
- **Code sketch**
```c++
ctx.set_solver_factory(mk_smt_strategic_solver_factory());
params_ref solver_params;
solver_params.set_bool("pi.avoid_skolems", false);
ctx.get_solver()->updt_params(solver_params);
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`check-sat-using qe` was reported to return `unsat` on a satisfiable
quantified-real formula, while a subsequent `check-sat` on the same
assertion returned `sat`. This PR adds focused regression coverage for
that shape to prevent reintroduction.
- **Regression coverage for the reported formula**
- Added `test_qe_regression_4175()` in `src/test/quant_solve.cpp`.
- Parses and quantifier-eliminates:
```smt2
(forall ((b Real)) (= (= r1 b) (= b 0)))
```
- **Behavioral oracle encoded in the test**
- Verifies the QE result is satisfiable under `r1 = 0`.
- Verifies the QE result is unsatisfiable under `r1 != 0`.
- This captures the intended semantics of the original formula and
guards against the unsound `unsat` outcome from the QE path.
- **Integration**
- Wires the new regression into `tst_quant_solve()` so it runs with
existing quantifier-solver test coverage.
Example snippet from the new test logic:
```cpp
solver.assert_expr(result);
solver.assert_expr(m.mk_eq(r1, zero));
VERIFY(l_true == solver.check());
solver.assert_expr(result);
solver.assert_expr(m.mk_not(m.mk_eq(r1, zero)));
VERIFY(l_false == solver.check());
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Spacer crashed in quantifier-elimination projection on certain HORN
inputs when model evaluation produced arithmetic expressions that were
not plain numerals. The failure was an assertion in
`spacer_qe_project.cpp` during sign/offset computation for projected
literals.
- **Projection robustness in Spacer arithmetic QE**
- Updated numeral extraction in `src/muz/spacer/spacer_qe_project.cpp`
from `is_numeral` to `is_extended_numeral` at all model-evaluation sites
used by projection.
- This covers evaluated arithmetic forms (e.g., normalized arithmetic
expressions) that are semantically numeric but not syntactic numerals,
preventing assertion failures in disequality/equality handling and bound
selection.
- **Regression coverage for the crashing HORN shape**
- Added a focused regression in `src/test/api_datalog.cpp` that
evaluates the reported Spacer/HORN input pattern through
`Z3_eval_smtlib2_string`.
- The test exercises the exact QE/projection path that previously
triggered the assertion.
```cpp
// Before
VERIFY(a.is_numeral(val, r));
// After
VERIFY(a.is_extended_numeral(val, r));
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This PR adds a first-class Python API helper for expressing regex
constraints in familiar Python regex syntax and translating them into Z3
regex terms. The translator is implemented as a separate module
(`z3regex.py`) as requested, keeping regex conversion logic isolated
from core API files.
- **New Python regex translator module**
- Adds `src/api/python/z3/z3regex.py`.
- Introduces `regex_to_re(pattern, flags=0, ctx=None)` to convert parsed
Python regex constructs into Z3 regex expressions.
- Supports core regular constructs (literals, classes/ranges,
alternation, grouping, quantifiers, categories, wildcard).
- Raises `NotImplementedError` for unsupported non-regular constructs
(e.g., features outside regular languages).
- **API/package integration**
- Exposes the module via `src/api/python/z3/__init__.py`.
- Includes `z3/z3regex.py` in Python binding file copy/install flow in
`src/api/python/CMakeLists.txt`.
- **Doctest entrypoint support**
- Extends `src/api/python/z3test.py` with `z3regex` mode so translator
doctests can be run consistently with existing Python API doctest flows.
```python
from z3 import *
from z3.z3regex import regex_to_re
x = String("x")
r = regex_to_re(r"(ab|cd)+\d{2}")
s = Solver()
s.add(InRe(x, r))
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
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>
…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>
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>
## 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>
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>
