Move the implementation and backtrackable state for \optimize_nl_bounds\
from \
la::core\ into \monomial_bounds\, alongside the LP bound optimization
helpers it orchestrates. Update Horner to invoke the component
directly.\n\nBuilt the CMake/Ninja \shell\ target successfully.
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings. (2 more flags after this!)
The first of these was -Wctad-maybe-unsupported. That has to do with
"class template argument deduction" -- the flag requires template
deduction guides to be explicitly provided if templated types are used
in situations that requires argument deduction. This fired for various
uses of templated types in the utils directory.
I decided that this should be a case of if it ain't broke, don't fix it,
and explicitly disabled the warning in the Z3 build (which will override
the setting if the flag is enabled in a larger build including Z3, like
clang).
-----
The second flag has to do with the C++ "rule of 3". Here is Google's AI
summary (inf_s_integer is a class in Z3 that triggered the warning):
_This warning means your inf_s_integer class defines a custom copy
assignment operator but lacks a user-defined copy constructor, which the
C++ standard deprecates to encourage the "Rule of Three". To fix this,
explicitly declare and = default the copy constructor in your class
definition._
_...example of how to fix..._
_This updates your code to modern C++ standards, cleanly silencing the
warning._
This seemed like a good standard to follow, and didn't require too many
changes, so I propose them.
Three `clang-analyzer-deadcode.DeadStores` warnings flagged by
clang-tidy: redundant bit-shifts in the log2 functions and an
unreachable assignment in `def::from_row()`.
## Changes
- **`src/util/util.cpp`** — `log2()` and `uint64_log2()`: Remove `v >>=
1` in the final `if (v & 0x2)` block. Only `r |= 1` matters; `v` is
never read after that point.
```cpp
// Before
if (v & 0x2) {
v >>= 1; // dead store
r |= 1;
}
// After
if (v & 0x2) {
r |= 1;
}
```
- **`src/math/simplex/model_based_opt.cpp`** — `def::from_row()`: Remove
`sign = true` assignment when `div < 0`. `sign` is only consumed earlier
in the function (`if (!sign)`) and is not read again after this point.
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10333
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings. (Only 4 more warnings after this one!)
This PR adds -Wignored-qualifiers. It detects only one violation: a
function whose by-value return type (unsigned) has a const qualifier.
Here is the error message:
```
/Users/daviddetlefs/z3/src/math/lp/dioph_eq.cpp:1518:9: warning: 'const' type qualifier on return type has no effect [-Wignored-qualifiers]
1518 | const unsigned sub_index(unsigned k) const {
| ^~~~~
```
Seems worth fixing.
### What it does
Fixes an inverted precondition assertion in `grobner::pop_scope`
(`src/math/grobner/grobner.cpp`).
```cpp
void grobner::pop_scope(unsigned num_scopes) {
SASSERT(num_scopes >= get_scope_level()); // was reversed
unsigned new_lvl = get_scope_level() - num_scopes; // requires num_scopes <= level
...
m_scopes.shrink(new_lvl);
}
```
`get_scope_level()` returns `m_scopes.size()` (grobner.h). The body
computes
`new_lvl = get_scope_level() - num_scopes` and calls
`m_scopes.shrink(new_lvl)`,
which is only well-defined when `num_scopes <= get_scope_level()`. The
assertion
stated the opposite (`>=`), so in debug builds it would fire on any
valid partial
pop (e.g. popping one of several scopes) while failing to catch the
unsigned
underflow it was meant to guard against. Changed to `<=`.
### Evidence
- `get_scope_level() const { return m_scopes.size(); }`
(`src/math/grobner/grobner.h`).
- Compiled the translation unit with MSVC and `Z3DEBUG` defined (so the
`SASSERT`
is active): builds cleanly.
### What we did not verify
This is a debug-only (`SASSERT`) correctness fix and has no effect on
release
builds. No behavioral test was added.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: ad2c295d-7523-48cf-b786-b435b833e3af
For every row with only one non-fixed variable in nla_core.cpp,
core::propagate, fix this variable.
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Fixes#10303.
## Symptom
On the reported QF_NRA instance z3 answers `sat` for some values of
`smt.random_seed` and `unsat` for others, and every `sat` comes with a
model z3's own validator rejects. The correct answer is `unsat`.
`smt.arith.solver=2` is unaffected; `smt.arith.solver=6` (the default)
is not.
## Root cause
The simplex model is not rational — each column is a `numeric_pair<mpq>`
`(x, y)` denoting `x + δ·y`, where `δ` is a positive infinitesimal used
to represent *strict* bounds exactly (`v > 0` is stored as `(0, 1)`).
`δ` only becomes concrete at model-output time, in
`from_model_in_impq_to_mpq(v) = v.x + m_delta * v.y`.
But nla decides monomial consistency using **only the rational parts**:
```cpp
const rational& val(lpvar j) const { return lra.get_column_value(j).x; } // nla_core.h:165
r *= lra.get_column_value(j).x; // product_value
return product_value(m) == lra.get_column_value(m.var()).x; // check_monic
```
That is sound only on a δ-free model, and it cannot be repaired by also
tracking `y`: a **product** `(x₁+δy₁)(x₂+δy₂)` has a `δ²` term, which a
`numeric_pair` cannot represent. The delta encoding is inherently
linear, so nla structurally cannot reason on a δ-carrying model.
The code relies on this: `core::check()` calls
`lra.get_rid_of_inf_eps()` as its very first action to instantiate δ
before any monomial is inspected. The invariant is:
> `m_to_refine` must only ever be computed on a δ-free model.
`core::optimize_nl_bounds()` breaks it. It calls
`lra.find_feasible_solution()` in the middle of the nla check; the
simplex re-runs, parks columns back onto strict bounds and
**re-introduces non-zero `y`**. It then calls `init_to_refine()` on that
model — one full LP re-solve after the scrub in `core::check()`.
A wrong `m_to_refine` turns directly into a wrong answer:
```
find_feasible_solution() re-introduces δ
→ init_to_refine() mis-measures monomials (compares only .x)
→ m_to_refine wrongly empty
→ horner.cpp:117 set_nla_satisfied()
→ core::check() returns l_true
→ theory_lra FC_DONE → sat
→ model output instantiates δ (x + m_delta·y)
→ monomial equations violated → "an invalid model was generated"
```
Instrumenting model construction on the reported benchmark confirms it
exactly: `use_nra_model=0`, **87 columns still carrying infinitesimals,
44 monomials violated** once δ is instantiated — every one of them with
`to_refine = 0`.
## Fix
Enforce the invariant where it is actually depended upon, instead of
only at the entry to `core::check()`:
```cpp
void core::init_to_refine() {
if (lra.is_feasible())
lra.get_rid_of_inf_eps();
m_to_refine.reset();
...
}
```
Every caller — including the ones inside `optimize_nl_bounds()` that
follow an LP re-solve — now measures monomials on a δ-free model.
A second commit closes a related hole: the
`arith.nl.optimize_bounds_lp_max_vars` throttle exit returns *after*
`find_feasible_solution()` has already moved the model, and was the only
exit that never called `init_to_refine()` at all — leaving `m_to_refine`
stale rather than merely δ-contaminated.
## Validation
Reported benchmark, `tactic.default_tactic=smt` (deterministic — the
default QF_NRA portfolio uses wall-clock `try_for` budgets, so it is
timing-dependent): master fails on **9 of 20** seeds; with the fix
**20/20** answer `unsat`. Under the default configuration, seeds 1–10
all answer `unsat` (was `sat` + invalid model on 1, 3, 4, 10), matching
`smt.arith.solver=2`.
The bug was much broader than the single reported instance. On the
`QF_NRA_small` corpus (1147 instances, `-T:10`):
| | sat | unsat | unknown | invalid model |
|---|---|---|---|---|
| master | 460 | 597 | 77 | **13** |
| this PR | 466 | 602 | 79 | **0** |
**Zero sat/unsat conflicts.** Of the 13 instances where master emitted
an invalid model, **7 are genuinely `unsat`** — the same unsoundness as
the reported one.
## Performance
Net **faster**, on the 1054 instances answered identically before and
after:
| | total |
|---|---|
| master | 229.7 s |
| this PR | 146.4 s (**−36.3 %**) |
133 instances faster by >200 ms vs. 13 slower by >200 ms.
The added `get_rid_of_inf_eps()` is asymptotically free —
`init_to_refine()` already costs Θ(Σ|monic|) arbitrary-precision
*multiplications*, so adding Θ(#columns) `mpq::is_zero()` tests (which
early-exit when no deltas are present) does not change its complexity
class. The expensive path is also moved rather than added: deltas left
by `optimize_nl_bounds()` previously survived until the next
`core::check()`, which paid the full `find_delta_for_strict_bounds` +
rewrite cost anyway.
The speedup itself comes from correctness — a truthful `m_to_refine`
points grobner / basic_lemma / order / monotonicity / tangent / nra at
the monomials that are genuinely violated, instead of letting them chase
a model that was never consistent.
`test-z3 /a`: 93/93 pass.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
This PR enable the "-Wimplicit-fallthrough" warning, then fix all the
warnings this gets
in the clang build, by:
* Augmenting UNREACHABLE to add __builtin_unreachable(), which
suppresses
warnings for fallthrough in that cse.
* Adding Z3_fallthrough in many cases, to make it clear that
fallthroughs are intentional.
* Adding [[noreturn]] to functions that throw, so the compiler knows
they don't fall through to the next case.
* In a couple of cases, there's a fall-through to a default case, which
does "break", or "return nullptr". In those cases, I duplicated the
action in the preceding case, to make it more self-contained, and robust
in the face of change.
In some cases, I am concerned about whether the warnings are identifying
real bugs. For example, the fall-throughs in these files seem at least a
little suspect:
nnf.cpp
seq_rewriter.cpp
lar_solver.cpp
while very probably correct, also seem at least a tiny bit suspect.
However, this PR does *not* attempt to change any behavior, only to
silence the warnings. It would be great if somebody with more knowledge
of the code could vet these cases. If vetted, the explicit presence of
the Z3_fallthrough would reassure future readers of the code that the
fall-through is intentional, not accidental.
When NLA interval arithmetic processes a linear term, a temporary
`interval` holding `mpq` numerals was stack-allocated but never freed,
leaking any heap-allocated big-number representations produced by
`mpq_manager`.
## Change
- **`src/math/lp/nla_intervals.cpp`** — In `interval_from_term`, replace
raw `interval bi` with `scoped_dep_interval bi(get_dep_intervals())`.
The scoped wrapper calls `m_manager.del()` on destruction, which frees
both `m_lower` and `m_upper` mpq values.
```cpp
// Before
interval bi;
m_dep_intervals.mul<wd>(a, i, bi);
// After
scoped_dep_interval bi(get_dep_intervals());
m_dep_intervals.mul<wd>(a, i, bi);
```
The leak was triggered on optimization problems with nonlinear
arithmetic (e.g. `opt.priority box` + `maximize` with NLA constraints),
where the interval multiplication produces mpq values large enough to
require heap allocation via `mpz_manager::set_big_i64`.
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10275
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Fixes#10241
Among columns with a large value, the branching selection now prefers
the one whose absolute value is smallest. This avoids branching on ever
larger integers when better (smaller) options are available.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 1b264f0c-4bcc-4790-a3b8-5f038cc71f89
Refactors the constraint/monic verification loops in `nra_solver.cpp`
introduced by #10230 to reduce nesting and improve readability. No
functional change.
### Changes
- **Early-continue guards**: Replace `if (!check_X(ci)) { if
(coi.contains(ci)) { ... } return l_undef; }` with `if (check_X(ci))
continue;` so the failure path reads linearly
- **Explicit braces**: Add braces to the constraint loop (monic loop
already had them), making both loops consistent
- **Condensed comment**: Collapse 6-line COI explanation to one line
```cpp
// Before
for (lp::constraint_index ci : lra.constraints().indices())
if (!check_constraint(ci)) {
// nlsat only solves over the cone-of-influence (COI) subset
// of constraints, so constraints outside the COI may be
// legitimately violated by the nlsat model. Only a violation
// of a COI constraint indicates a genuine nlsat bug; a
// non-COI violation is benign, so fall back to l_undef
// quietly without emitting diagnostics.
if (m_coi.constraints().contains(ci)) { ...; UNREACHABLE(); }
return l_undef;
}
// After
for (lp::constraint_index ci : lra.constraints().indices()) {
if (check_constraint(ci)) continue;
// Non-COI constraint violations are benign; only COI violations indicate a bug.
if (m_coi.constraints().contains(ci)) { ...; UNREACHABLE(); }
return l_undef;
}
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10235
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Fixes a snapshot-regression divergence reported in [Z3Prover/bench
discussion #3421](https://github.com/Z3Prover/bench/discussions/3421).
- **Benchmark:** `iss-6061/delta.smt2` (from
https://github.com/Z3Prover/z3/issues/6061)
- **Recorded oracle:** `sat`
- **Current (buggy) z3 output:** a large `constraint 19 violated` /
`number of constraints = 602` diagnostic dump (and, in an
assertion-enabled build, an `UNEXPECTED CODE WAS REACHED` abort at
`nra_solver.cpp:245`).
### Divergence diff
```diff
--- delta.expected.out (expected)
+++ produced (current z3)
@@ -1 +1,334 @@
-sat
+constraint 19 violated
+number of constraints = 602
+(0) j0 >= 1
+(1) j0 <= 1
...
+(19) j8 + j10 > 0
+(20) j8 + j10 >= 0
... (160 more diff line(s))
```
## Root cause
`nra_solver:👿:check()` runs nlsat over only the **cone-of-influence
(COI)** subset of the LRA constraints. When nlsat returns `l_true`, the
resulting model is validated against **all** LRA constraints/monics.
Constraints outside the COI can be *legitimately* violated by that
partial model — nlsat never assigned the variables that only occur
outside the COI.
This was previously handled by commit `8a146a92e` ("replace UNREACHABLE
with VERIFY for non-COI constraint/monic violations", fixes#8883). The
Nl2lin rewrite (`6fb68ac01`) reintroduced an **unconditional**
`UNREACHABLE()` plus an `IF_VERBOSE(0, ...)` diagnostic dump for *any*
violated constraint/monic, reverting that fix.
For `delta.smt2`, constraint 19 (`j8 + j10 > 0`) is **not** in the COI
(confirmed by instrumentation: `in_coi=0`). In a release build the
reintroduced `UNREACHABLE()` is a no-op, so z3 correctly falls back to
`l_undef` and ultimately answers `sat` — but the `IF_VERBOSE(0, ...)`
dump still leaks to stderr, and the snapshot capture merges stderr into
stdout, breaking the recorded oracle. In an assertion-enabled build the
`UNREACHABLE()` aborts outright.
## Fix
Only treat a violated constraint/monic as a genuine nlsat bug (verbose
dump + `UNREACHABLE()`) when it is actually in the COI. A non-COI
violation is benign, so return `l_undef` quietly without emitting any
diagnostics. This restores the intent of `8a146a92e` and additionally
stops the verbose dump from leaking for the benign case.
```cpp
if (!check_constraint(ci)) {
if (m_coi.constraints().contains(ci)) {
IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
}
return l_undef;
}
```
(analogous change for the monic check).
## Validation
Rebuilt z3 from this branch (`make -j`) and re-ran the benchmark exactly
as the snapshot capture does (combined stdout+stderr, `-T:20`):
```
$ z3 -T:20 inputs/issues/iss-6061/delta.smt2 2>&1
sat
```
The combined output is now exactly `sat`, byte-for-byte matching the
recorded `delta.expected.out` oracle. Basic SMT solving sanity-checked
and unaffected.
Closes the divergence in Z3Prover/bench discussion #3421.
> [!WARNING]
> <details>
> <summary>Firewall blocked 1 domain</summary>
>
> The following domain was blocked by the firewall during workflow
execution:
>
> - `pypi.org`
>> To allow these domains, add them to the `network.allowed` list in
your workflow frontmatter:
>
> ```yaml
> network:
> allowed:
> - defaults
> - "pypi.org"
> ```
>
> See [Network
Configuration](https://github.github.com/gh-aw/reference/network/) for
more information.
>
> </details>
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/30150856651)
· 239.4 AIC · ⌖ 20.1 AIC · ⊞ 10.7K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests)
<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.65, model: claude-opus-4.8, id:
30150856651, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/30150856651 -->
<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->
Co-authored-by: z3prover-ci-bot[bot] <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Problem
egressions/smt2/10220.smt2 (datatype + nonlinear integer arithmetic over
`SBVRational`, expected `unsat`) crashes with an ACCESS_VIOLATION (issue
#10220). The crash only occurs with the default `theory_lra`
(`arith.solver=6`) and is independent of `arith.nl`.
## Root cause
Debug build gives a clean stack: a `SASSERT(n)` violation / null
dereference in `smt::relevancy_propagator_imp::is_relevant_core` reached
from `theory_lra::set_conflict_or_lemma ->
ctx().mark_as_relevant(literal)`. The literal's boolean variable has
`bool_var2expr(v) == nullptr`.
Tracing showed the same nla lemma core being processed twice — first at
scope 6, then, after a backtrack, again at scope 3 — where the bound
atoms internalized to build the lemma had their boolean variables
deleted by the pop:
\\\
SCOL scope=6 core=[32 27 35 30 6 14 ]
SCOL scope=3 core=[32*NULL* 27 35*NULL* 30 6 14 ]
\\\
Commit d60d6a066 (*add incremental propagate for nla to retain some
propagation lemmas*) removed the `clear()` call from `core::propagate()`
(the final-check path) while adding a symmetric
`incremental_propagate()` that keeps it. Consequently `m_lemmas`
generated at a deep scope survived a backtrack and were replayed at a
shallower scope, referencing deleted bool vars.
## Fix
Restore `clear()` at the start of `core::propagate()`. Both
`propagate()` and `incremental_propagate()` consume their lemmas
immediately via `add_lemmas()`, so lemmas never need to survive across
calls; starting each final-check propagation from a fresh lemma set
removes the stale replay.
## Validation
- `regressions/smt2/10220.smt2` -> `unsat` (was ACCESS_VIOLATION)
- `FStar.Math.Euclid-1` still `unsat`
- `FStar.Math.Euclid-2/-3` unchanged (already `unknown` on master,
verified against the pre-fix binary)
Fixes#10220.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
## Summary
`lp::lar_solver::init_model()` (`src/math/lp/lar_solver.cpp`) picks an
infinitesimal `delta` that maps every distinct rational-pair column
value `(x, y)` to a *distinct* scalar `x + delta*y`, halving `delta`
whenever a collision is detected. The previous implementation rebuilt
**both** the set of distinct pairs and the set of scalars from a full
O(n) pass over all columns on *every* halving, and the pair set is
entirely independent of `delta`.
## Change
- Build the delta-invariant set of distinct column pairs
(`m_set_of_different_pairs`) **once**, before the halving loop.
- On each halving, only rebuild the scalar set by iterating over the
**distinct pairs** rather than rescanning all `n` columns (including
duplicates).
The collision test and the selected `delta` are unchanged: the loop
still halves `delta` whenever the number of distinct scalars is less
than the number of distinct pairs, and terminates when the scalar map is
injective. The early-`break` versus end-of-pass check produce the same
`delta` sequence because a size discrepancy on a full pass is exactly
the injectivity-failure condition.
## Cost argument
Let `n` = column count and `D` = number of *distinct* column pairs (`D ≤
n`), and `H` = number of halvings.
- Before: `O(H · n · log D)` — every halving re-inserts all `n` columns
into both sets.
- After: `O(n · log D + H · D · log D)` — the pair set is built once;
each halving touches only the `D` distinct pairs.
This removes the repeated full rescan from the halving loop and skips
redundant work for duplicate columns, turning a per-halving O(n) rebuild
into a one-time cost plus O(D) per halving.
## Evidence
Profiled under callgrind (deterministic instruction counts),
differential correctness preserved, static-analysis hygiene clean:
- Target function self-instructions: **2,695,433,533 → 2,084,074,808**
(−22.7%).
- Total program instructions ratio: **0.904** (−9.6%).
- Wall-time speedup: **~6.1%**.
- Differential correctness: identical results (no mismatches).
Logic class exercised: **QF_LRA / linear real arithmetic** model
construction.
<!-- gh-aw-workflow-id: coz3-deepperf-fix -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/coz3-deepperf-fix -->
---------
Co-authored-by: z3prover-ci-bot[bot] <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Remove unused m_fixed_val member variable from undo_fixed_column.
undo_fixed_column is allocated in a region/trail allocator where C++
destructors are not invoked when objects are popped/reclaimed. Storing
an mpq instance (which can allocate heap memory for multi-precision
numbers) inside a region-allocated object causes a memory leak that is
flagged by ASAN.
m_fixed_val was never used in undo() or elsewhere in the struct.
Removing it completely eliminates the ASAN finding, avoids unnecessary
mpq copies, and is entirely safe.
…icts
Add core::optimize_nl_bounds() (gated by arith.nl.optimize_bounds) which
runs LP max/min over monomial leaf variables inside core::propagate(),
analogous to solver=2's max_min_nl_vars, so nla (arith.solver=6) can
detect cross-nested conflicts previously missed. Collect improved bounds
first, then apply them and re-establish feasibility once; reconcile the
core solver via find_feasible_solution before the raw maximize solves to
preserve inf_heap_is_correct(). Skip null witnesses in
get_dependencies_of_maximum for implied/unconditional bounds.
On FStar-UInt128-divergence solver=6 this yields unsat in 2
final-checks, seed-insensitive (seeds 1-10).
Copilot-Session: ac36bb84-de91-4e6c-86df-6008c7396ceb
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: ac36bb84-de91-4e6c-86df-6008c7396ceb
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
This PR completes the job started by
https://github.com/Z3Prover/z3/pull/10169. It adds `-Wextra-semi` to the
set of CLANG_ONLY_WARNINGS, and adds
```
START_DISABLE_EXTRA_SEMI_WARNING;
...macro invocations with trailing semis...
END_DISABLE_WARNING;
```
around all the blocks of macro invocations that provoked warnings.
(Additionally, in realclosure.h, there was one block of macro
invocations that did *not* follow the trailing-semi pattern; changed
that to look like all the others).
When a term column x - y is fixed to 0 (e.g. from t <= ca and t >= ca),
theory_lra previously discovered the implied equality x = y only lazily via
assume_eqs() during final_check. On the FP fuel-recursive axiom in issue #10065
this discovery is starved by E-matching, which unfolds the recursion and
bit-blasts an exploding FP subproblem before the branch closes.
Add propagate_offset_eq() to detect a fixed 2-variable offset term with opposite
unit-scaled coefficients and propagate the operand equality x = y directly to the
core, so congruence closure merges dependent terms immediately. This mirrors the
offset-row propagation performed by theory_arith (propagate_cheap_eq) and matches
its behavior on this benchmark (timeout -> unsat 0.06s, 2 quant-instantiations).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e
## Problem
A QF_NIA benchmark (`From_T2__ex16.t2__p22243_terminationG_0.smt2`, run
with `-T:200 model_validate=true`) crashes with SIGSEGV inside nlsat.
## Root cause
In `algebraic_numbers::manager:👿:compare_core`, the
interval-separation workaround computed the isolating intervals of `a`
and `b` with:
```cpp
if (get_interval(a, la, ua, precision) &&
get_interval(b, lb, ub, precision)) { ... }
```
`&&` short-circuits: when `a` is **rational**, `get_interval(a, ...)`
finds the exact root and returns `false`, so `get_interval(b, ...)`
never runs and `b`'s bounds `lb`/`ub` stay **0**. Those bounds are used
*unconditionally* below the `if` (in the `compare(cell_a, u_b)` /
`compare(cell_b, l_a)` checks), so `a` was effectively compared against
`0`, producing an incorrect and self-inconsistent sign (`compare`
returned `+1` while `<`, `=`, `>` were all false).
Concretely, comparing `c = 39017/131072` (rational) with `d ≈
0.297676176` (root of a quadratic) returned `c > d`, though `c < d`.
Downstream, this made nlsat's `interval_set::is_full` miss full coverage
of ℝ, so `pick_in_complement` was invoked on an empty complement and
read `s->m_intervals[UINT_MAX]` — a crash guarded only by a
release-stripped `SASSERT` (`nlsat_interval_set.cpp`).
## Fix
Compute both intervals unconditionally so `b`'s bounds are always valid
before they are used.
## Validation
- The crashing benchmark now returns `unsat` (verified on both macOS and
a Linux `RelWithDebInfo` build where the SIGSEGV was originally
reproduced under gdb).
- Unit tests pass: `algebraic`, `upolynomial`, `polynomial`, `nlsat`.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Summary
Optimizes `lp::static_matrix<..>::remove_element`, reported as a hotspot
in
[Z3Prover/bench#3143](https://github.com/Z3Prover/bench/discussions/3143)
(the #1 exclusive-time function, ~19.6%, on
`inputs/issues/iss-5131/bug-1.smt2`).
`remove_element` uses swap-remove but **deep-copied** the relocated tail
coefficient:
```cpp
auto & rc = row_vals[row_offset] = row_vals.back(); // copy from the tail
```
In namespace `lp`, `mpq` is a typedef for the copyable `rational`, so
this copy-assign allocates a fresh bignum whenever the **source (the
tail)** is big — matching the `malloc`/`_int_malloc` entries in the
reported profile. The tail element is `pop_back`'d immediately
afterwards, so the allocation is wasteful.
## Change
A copy-assign allocates only when the **source** is big
(`mpz_manager::set` → `big_set`). So relocate the tail coefficient by
**swapping** exactly in that case — stealing its already-allocated
storage, zero `malloc`. When the tail is small, a plain copy never
allocates and is cheaper than swapping the `mpz` internals; the
destination's size is irrelevant. The column-cell relocation is
unchanged (a `column_cell` carries no coefficient).
Single-file change; no new parameters.
## Benchmarks
A/B produced by toggling the new code path against the original
deep-copy (via a temporary parameter, not included here).
- **rise-runner-2** (initial `is_big()||is_big()` variant): QF_LIA_small
neutral; certora identical outcomes, −1.5% paired solve-time.
- **128-core Linux box**, `run_on_dir.py`, `-max_workers 32` (final
tail-only variant):
| Set | Files | `-T` | Solved (new = orig) | Avg-time ratio new/orig |
Correctness |
|---|---|---|---|---|---|
| QF_LIA (SMT-LIB) | 6947 | 20s | 5817 ≈ 5815 | 1.00000 | identical (±2
timeout-edge) |
| certora | 308 | 120s | 186 = 186 | 0.9977 | identical, 0 unique
timeouts |
| QF_LRA (SMT-LIB 2025) | 1753 | 120s | 1552 = 1552 | 0.9985–0.9991 |
identical, 0 real regressions |
Consistently **correctness-neutral and marginally faster** (~0.1–0.5%)
on large-coefficient LP sets, flat on small-coefficient inputs. The
per-`remove_element` allocation saved is small relative to total solve
time, so the whole-solver delta is a fraction of a percent — a clean
micro-optimization with no downside.
## Validation
- `make`/`ninja` build clean; `test-z3 /a` — 92/92 pass.
- Baseline vs patched output byte-identical on the reported benchmark;
identical solve sets across all three benchmark suites above.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Implement check_mod_congruence in nla_divisions: for two mod-atoms
sharing a (possibly symbolic) divisor y, emit the model-guided tautology
div(x,y) - div(s,y) = delta => mod(x,y) - mod(s,y) = (x - s) - delta*y.
This discharges linear congruences over a symbolic modulus that the
nonlinear core did not otherwise isolate. Thread the div(x,y) variable
through add_divisibility (nla_core/nla_solver/nla_divisions) and
register it in theory_lra for symbolic-divisor mod terms.
Solves FStar.BitVector-1 (0.7s) and FStar.Matrix-1 (1.6s), previously
300s timeouts; all 92 unit tests pass.
Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## 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>
## 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>
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>
### 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>
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
This is a second version of https://github.com/Z3Prover/z3/pull/9957. I
address @NikolajBjorner 's comments about not changing the semicolons
after macro invocations, because some editors work better with them
present. It now, to the best of my ability, only deletes semis:
* after the closing brace of namespace decl.
* after the closing brace of an extern "C" decl.
* after a function definition.
This PR is very large, but it consists entirely of deletions of
semicolons in these situations.
(If there was a way to update the previous PR, which had been closed,
and that is preferable, please let me know. I couldn't figure it out.)
## Summary
Follow-up to #10001 addressing @NikolajBjorner's review comment:
> isn't this nearly identical AI generated code to the other file? There
has to be some modular approach to deal with sorting vectors?
#10001 introduced two nearly-identical copies of a bounds-safe,
mutation-aware index-permutation merge sort:
- `algebraic_numbers.cpp::merge_sort_roots_perm`
- `nlsat/levelwise.cpp::merge_sort_perm`
Both exist because the comparator (`anum_manager::compare`/`lt`) is
**not pure**: it mutates the algebraic numbers it compares (refining
isolating intervals) and may throw on the resource limit, which makes
`std::sort` undefined behavior (the original SIGSEGV).
## Change
Extract the algorithm into a single shared helper
`util/index_sort_with_mutations.h` (`stable_index_merge_sort`). The long
rationale for why `std::sort` is unsafe and merge sort is safe now lives
in exactly one place. Both call sites become thin wrappers that build
the scratch buffer and forward their local comparator.
No behavioral change: same stable O(n log n) merge sort over an index
permutation.
## Verification
CMake/Ninja Release build:
- `test-z3 /seq algebraic_numbers` — PASS
- `test-z3 /seq algebraic` — PASS
- NRA/NIA smoke solves with `nlsat.lws=true` return expected sat/unsat.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace goto-based control flow in get_cube_delta_for_term with an
all_ok flag for structured early-exit. Use aggregate initialization for
flip_candidate, constructor-based vector sizing for occs, brace
initialization for pairs in add_edge_rows_for_term.
No functional changes - all lcube tests pass.
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Summary
Alternative to #9991. Instead of disabling `nlsat.lws` by default, this
**fixes the underlying bug** so levelwise single-cell projection stays
enabled.
## Root cause
The crash was reproduced on the QF_NIA benchmark from #9991
(`20170427-VeryMax/ITS/From_AProVE_2014__Round3.jar-obl-8__p11898_terminationG_0.smt2`,
~40% SIGSEGV at `-T:20`). A core-dump backtrace points at:
```
mpbq_manager::le (mpbq.cpp:362)
algebraic_numbers::manager:👿:compare (algebraic_numbers.cpp:1913) c = 0xea24052d29f2d500 <- wild pointer
algebraic_numbers::manager:👿:compare (algebraic_numbers.cpp:2128)
nlsat::levelwise::impl::root_function_lt (levelwise.cpp:949)
... std::__unguarded_linear_insert ... <- OOB read
std::sort
nlsat::levelwise::impl::sort_root_function_partitions
```
The comparator (`root_function_lt` → `anum_manager::compare`, and
`anum_manager::lt`) **refines the isolating intervals of the algebraic
numbers it compares** and may **hit the resource limit (throwing)**
mid-comparison. Both make the order it induces non-deterministic / not a
strict weak ordering across a single `std::sort` — undefined behavior.
libstdc++'s *unguarded* insertion pass then walks past `begin()` and
dereferences a wild anum cell → SIGSEGV. This only fires when a timeout
interrupts levelwise, explaining the non-determinism (`signal-11`).
## Fix
Replace the two affected `std::sort` calls
(`sort_root_function_partitions` and `add_adjacent_root_resultants`)
with a **bounds-checked insertion sort over an index permutation**. A
fully guarded insertion sort can never read out of bounds regardless of
comparator consistency, and unwinds cleanly if `compare` throws on
cancellation. The partitions sorted here are small, so the O(n²) cost is
negligible.
`nlsat.lws` stays `true`.
## Verification
On the Linux repro box (Ubuntu 24.04, g++ 13), RelWithDebInfo:
- **Before:** ~40% SIGSEGV (e.g. 5/16 runs at `-T:20`).
- **After:** **0/30** SIGSEGV; results are `unsat`/`timeout`.
- Sanity batch over 25 QF_NIA/VeryMax/ITS files: no crashes, expected
sat/unsat/timeout mix.
- `model_validate=true` full solve still returns `unsat`.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Capture row as a pointer as lambda strips the reference and the vector was copied by value in lar_solver!
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The `Ubuntu build - cmake - debugGcc` job was failing because the solver
could emit an unexpected `check-assignment` line before normal
satisfiability output. This change removes that stray output so debug
GCC runs no longer contaminate expected CLI/results streams.
- **Root cause**
- `src/math/lp/nra_solver.cpp` printed `check-assignment` from
`solver::check_assignment()` via `IF_VERBOSE(0, ...)`.
- Verbosity level `0` made this effectively unconditional in the failing
path, so debug builds could leak internal diagnostics into user-visible
output.
- **Change**
- Remove the `check-assignment` print from the exception path in
`lp::solver::check_assignment()`.
- Preserve all existing control flow and error handling; only the
unintended output side effect is removed.
- **Effect**
- Debug GCC CMake builds keep their normal `sat`/`unsat` output shape.
- Internal solver diagnostics no longer interfere with output-sensitive
CI checks.
```c++
catch (z3_exception &) {
statistics &st = m_imp->m_nla_core.lp_settings().stats().m_st;
m_imp->m_nlsat->collect_statistics(st);
if (m_imp->m_limit.is_canceled()) {
return l_undef;
}
else {
throw;
}
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Improves the Diophantine (`dio`) integer-feasibility controller in
`int_solver`, and fixes a latent bug where the user's Gomory-cut
configuration could be silently overridden at runtime. Also includes the
earlier `lia_w` work: randomized hammer gates, the `int_hammer_period` /
`random_hammers` parameters, and the linear `dio_calls_period` recovery.
## Motivation
The controller used a **single field** both as the static
`lp.dio_cuts_enable_gomory` parameter and as the live "is Gomory
running" flag. It started running Gomory (and the gcd test) once
`dio_calls_period` crossed a hard-coded `16`. Because `dio_calls_period`
is also driven by the randomized hammer gate, on instances where `dio`
is only intermittently productive the period could be ratcheted past 16
*by chance*, turning on Gomory + gcd and thrashing — e.g. `dillig/20-14`
went from a 100s solve (deterministic) to a 600s timeout (randomized)
purely from this spurious activation.
## Changes
- **Separate config from runtime state.** Split the shared field into
`m_dio_cuts_enable_gomory` (static config, never mutated) and
`m_run_gomory_with_dio` (runtime flag). Toggling the runtime state can
no longer clobber the user's `dio_cuts_enable_gomory` parameter.
- **Trigger on genuine dio failures, not the period proxy.** Running
Gomory-with-dio now starts after a count of **consecutive `undef` dio
returns** (reset on a dio conflict) rather than when the
randomization-inflated period crosses a threshold — robust to
`random_hammers` gate variance.
- **Parameterize the threshold.** New `lp.dio_gomory_enable_period`
(default 16). Set it very large to never auto-start Gomory, so Gomory
follows `dio_cuts_enable_gomory` only.
- **Try `dio` before Gomory** in `check()` so a productive dio conflict
preempts Gomory on dio-dominated instances.
## Evaluation (QF_LIA, full set, 600s, seed 555 paired)
- Dio-before-Gomory: **+33** problems across the 6 `random_hammers x
int_hammer_period` cells (5/6 cells improve).
- New trigger (`dio_gomory_enable_period=32`, random): **6417** vs the
period-16 baseline **6409**; no short-cutoff regression.
- Linear `dio_calls_period` recovery: keeping it on is worth ~+20 vs
off; `decrease=1` slightly ahead of the default 2.
Default behavior (`dio_gomory_enable_period=16`) is byte-for-byte
equivalent to the previous threshold logic.
## Notes
Debug-only tracing used during analysis (the `dio_calls_period_trace`
parameter plus per-hammer / period-evolution verbose output) is **not**
included.
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
The PR adds
```
"-Wsuggest-override"
"-Winconsistent-missing-override"
```
to the CLANG_ONLY_WARNINGS. This exposes a relatively small number of places where method overrides did not use the "override" keyword. The PR fixes those.
(In cmd_util.h, I also made the *_CMD macros be uniform in not ending the class they define with a semicolon; the invocation of the macro can add the semicolon.)
Implemented the largest cube heuristic from Bromberger and Weidenbach's
paper on cubes. Also fixes an overflow bug in mzp.
Use vswhere to find the visual studio version on windows in the build's ymls.
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
MSVC ASan reports showed a container-overflow in LP tableau pivoting,
reproducible from both examples and solver tests (issue #9781). The
failure came from reading a `column_cell` through a reference after
pivoting removed that entry from the backing column.
- **Root cause**
- `pivot_column_tableau` and the analogous Diophantine elimination loop
both held `auto& c = column.back()` across a call
(`pivot_row_to_row_given_cell`) that immediately removes that very cell
from the column via `remove_element`.
- After the mutation, the subsequent read `c.var()` used for bookkeeping
observed invalid memory.
- **Change**
- Record the affected row in the bookkeeping set (`m_touched_rows` /
`m_changed_rows`) by reading `c.var()` **before** the pivot call, while
the back cell is still valid.
- Make `static_matrix::pivot_row_to_row_given_cell` return `void`
instead of `bool`. Its result (`!rowii.empty()`) was always `true`: both
callers keep the matrix at full row rank (the tableau basis columns form
an identity submatrix; the Diophantine `m_l_matrix` stays invertible),
so an elementary row operation can never empty a row. The dead `if
(!...) return false;` early-exit in `pivot_column_tableau` is removed
and replaced with a `SASSERT(!rowii.empty())` documenting the invariant.
- **Affected code paths**
- `src/math/lp/static_matrix.h`, `src/math/lp/static_matrix.cpp`,
`src/math/lp/static_matrix_def.h`
- `src/math/lp/lp_core_solver_base_def.h`
- `src/math/lp/dioph_eq.cpp`
- **Behavioral impact**
- No algorithmic change to pivoting.
- Removes the stale-reference hazard in the loops that repeatedly
eliminate entries from a column.
```c++
while (column.size() > 1) {
auto& c = column.back();
SASSERT(c.var() != piv_row_index);
if (m_touched_rows != nullptr)
m_touched_rows->insert(c.var());
m_A.pivot_row_to_row_given_cell(piv_row_index, c, j);
}
```
- **Verification**
- Reproduced the exact issue #9781 failure on a local ASan build
(`container-overflow` in `pivot_column_tableau`) using the pre-fix code,
and confirmed it is gone with this change.
- The 4 reported tests pass clean under ASan: `c_example`,
`cpp_example`, `test-z3 get_implied_equalities`, `test-z3 quant_solve`.
- Full `test-z3 /a` suite: 89 passed, 0 failed, 0 ASan errors.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
A `root-obj`-driven unsat case was exiting with a leaked `mpz_manager`
allocation even though solver output was correct. The leak came from
temporary rational bounds created during algebraic-number comparison and
not released before shutdown.
- **Root cause**
- `algebraic_numbers::compare_core()` materialized interval bounds as
raw `mpq` temporaries.
- Those temporaries could allocate backing `mpz` storage, but their
lifetime was not tied to the manager, so the allocator retained leaked
cells at process exit.
- **Change**
- Replace the raw `mpq` temporaries with `scoped_mpq` in
`/src/math/polynomial/algebraic_numbers.cpp`.
- This keeps the comparison logic unchanged while making temporary bound
conversion use RAII-managed cleanup.
- **Effect**
- `root-obj` comparisons no longer leave `mpz_manager` allocations
behind.
- Solver behavior is unchanged; the fix is limited to temporary numeral
lifetime management.
```c++
- mpq l_a, u_a, l_b, u_b;
+ scoped_mpq l_a(qm()), u_a(qm()), l_b(qm()), u_b(qm());
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
So far, `algebraic_numbers compare_core ` handles an edge case
incorrectly:
- If the two compared numbers (`a`, `b`) are different,
- the intervals still overlap after refinements, and
- both a and b are a root of the second polynomial (`cell_b->m_p`), e.g.
they are the first and second root
then the method would return `sign_zero` (i.e. "equal"). This behavior
can be replicated with the provided test case (before the fix). This
requires `algebraic.factor=false`, though i first encountered it during
solver runs on QF_NRA instances with the default
`algebraic.factor=true`, which apparently means that the polynomials for
anums are still not always factored.
The fix is to compare the interval bounds of b to a and vice versa. Then
the Sturm-Tarski check is only run if `a` and `b` both lie in the
intersection of the intervals, because only then is it guaranteed to be
correct.
