https://github.com/Z3Prover/z3/pull/10284 changed the UNREACHABLE macro
in debug.h to use __builtin_unreachable() to indicate to the compiler
that the
code leading it should be considered unreachable.
In https://github.com/Z3Prover/z3/pull/10295 Copilot figured out that
this was wrong: the unreachable macro makes calls, which shouldn't be
elided, and whose arguments should be evaluated. It partially fixed the
problem by declaring invoke_exit_action to be `[[noreturn]]`. This
eliminated warnings in non-debug builds, but when Z3_DEBUG is enabled,
`UNREACHABLE` ends with an invocation of `INVOKE_DEBUGER()`. This can
call `invoke_debugger()`, which *can* actually return (so it can't be
given the `[[noreturn]]` attribute. So we still get warnings in debug
builds.
This PR fixes those, creating a Z3_unreachable_case macro, which is just
a combination of `UNREACHABLE()` and `Z3_fallthrough`. It uses that in
the places that give warnings.
It seemed better to me to still have these cases have a single macro,
rather than `UNREACHABLE` followed by an explicit `Z3_fallthrough`; this
seemed to me like it would confuse people -- "how can you fall through
if this code is unreachable?" But I'm open to alternative suggestions!
Remove the seq_split (regex sigma-splitting / factorization) module and all
code that uses it:
- delete src/ast/rewriter/seq_split.{h,cpp} and src/test/seq_split.cpp
- drop the m_split member, include, and split/simplify_split/split_membership
wrappers from seq_rewriter
- remove the regex factorization propagation block from seq_regex.cpp
- remove the seq.regex_factorization_enabled/threshold parameters and their
theory_seq_params fields
- drop the files from the rewriter/test CMake lists and the test registry
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
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 building the model value of a sequence, an unresolved element such as
(seq.nth_i k!0 0) over an internal sequence constant could be emitted
verbatim, exposing internal skolem symbols (e.g. k!0) in the user-visible
model returned by get-model / get-value.
Such a term is not a proper value and is unconstrained at model-construction
time, so replace it with a concrete fresh value from the sequence factory.
This only affects model values that were already non-concrete (i.e. leaking
internal terms); genuine concrete sequence values satisfy m.is_value and are
left untouched, so sat/unsat verdicts and normal string/sequence models are
unaffected.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
`set.size` reported `sat` for `(= 1 (set.size (set.union (set.singleton
1) (set.singleton 2))))` — a soundness bug, not just a performance gap.
The returned model did not satisfy the constraint.
## Root cause
In `theory_finite_set_size::run_solver()`, the cardinality sub-solver
enumerates propositional models of the membership structure and sums
fresh "slack" variables to represent `set.size`. All slacks were bounded
only by `>= 0`, so the arithmetic solver could freely assign `size = 1`
even when two distinct concrete members were independently asserted:
- **Model M₁** (`{1}` active, `{2}` inactive) — element 1 is a concrete
witness → slack must be `≥ 1`
- **Model M₂** (`{1}` inactive, `{2}` active) — element 2 is a concrete
witness → slack must be `≥ 1`
Without this enforcement: `slack₁ = 1, slack₂ = 0` satisfied `size = 1`.
With it: `size ≥ 2`.
## Changes
- **`src/smt/theory_finite_set_size.cpp`** — In `run_solver()`, after
retrieving the propositional model, check if exactly one singleton
equivalence class is active *and* a positive `set.in` assertion exists
for that element in an active set. If so, assert `slack >= 1` instead of
`>= 0`. This is sound: the concrete member witnesses the slot contains
at least one element.
- **`src/ast/rewriter/finite_set_axioms.cpp`** — Add the missing
monotonicity lower bounds for union:
```
|A ∪ B| ≥ |A| and |A ∪ B| ≥ |B|
```
These complement the existing upper bound `|A ∪ B| ≤ |A| + |B|` and let
the arithmetic solver derive `|{1} ∪ {2}| ≥ 2` directly from the
singleton axiom `|{i}| = 1`.
## Verified cases
| Query | Before | After |
|---|---|---|
| `(= 1 (set.size (set.union (set.singleton 1) (set.singleton 2))))` |
`sat` ❌ | `unsat` ✓ |
| `(= 2 (set.size (set.union (set.singleton 1) (set.singleton 2))))` |
`sat` ✓ | `sat` ✓ |
| `set.in 1 s ∧ set.in 2 s ∧ (= 1 (set.size s))` | `sat` ❌ | `unsat` ✓ |
| `¬(>= (set.size (set.union ...)) 2)` | `sat` ❌ | `unsat` ✓ |
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10232
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
PR #10180 moved nonlinear bound propagation to final_check only, removing
the eager propagate_nla() from the search-time propagation path. This left
E-matching without nla-implied bound facts during search, causing an
instantiation blowup on number-theory goals (e.g. FStar.Math.Euclid),
which exhausted rlimit and returned unknown on queries previously proved.
Re-run propagate_nla() before propagate_bounds_with_lp_solver() in the
l_true case of propagate_core so tightened nonlinear bounds are surfaced
to the SMT core during search. Recovers FStar.Math.Euclid-1/-2.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
With `(set-option :smtlib2_compliant true)`, Z3 disables implicit
Int→Real coercions. When the LP solver generates Gomory cuts/bounds over
expressions that mix Int and Real LP variables (as happens when
`to_real(n)` is internalized — both `to_real(n)` as Real and `n` as Int
are registered as LP vars), `coeffs2app` was constructing
`mk_mul(Real_numeral, Int_expr)`. Without implicit coercions,
`check_args` throws an `ast_exception` that bubbles up through
`cmd_context::check_sat()` as `l_undef`, producing a spurious `unknown`
instead of `unsat`.
## Changes
- **`src/smt/theory_lra.cpp` — `coeffs2app`**: Before building each
product term, coerce `o` to Real via `a.mk_to_real(o)` when `!is_int &&
a.is_int(o)`. This makes the sort explicit rather than relying on
implicit coercions.
- **`src/test/smt2print_parse.cpp`**: Regression test for the exact
formula from the issue — verifies the result is `unsat` (not `unknown`)
when `smtlib2_compliant` is set.
```smt2
(set-option :smtlib2_compliant true)
(set-logic ALL)
(declare-datatype SBVRational ((SBV.Rational (sbv.rat.numerator Int) (sbv.rat.denominator Int))))
; ... mixed Int/Real via to_real ...
(check-sat)
; was: unknown (:reason-unknown "Sort mismatch at argument #2 for function * (Real Real) Real supplied sort is Int")
; now: unsat
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10166
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
…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).
With `parallel.enable=true`, Z3 could return a SAT model for a QF_BV
instance that violates its own assertions. The bug traces to solver
translation: named assertions were re-registered with swapped
formula/indicator arguments, corrupting the translated solver's
assertion state.
## Bug
`m_name2assertion` stores `indicator → formula`. In
`smt_solver::translate()`, the structured binding `[k, v]` gives `k =
indicator`, `v = formula`, but `assert_expr(t, a)` expects `(formula,
indicator)`:
```cpp
// Before — args reversed
for (auto& [k, v] : m_name2assertion) {
expr* val = translator(k); // indicator
expr* key = translator(v); // formula
result->assert_expr(val, key); // assert_expr(indicator, formula) ← wrong
}
```
## Fix
```cpp
// After — correct order
for (auto& [k, v] : m_name2assertion) {
expr* fml = translator(v); // formula
expr* ind = translator(k); // indicator
result->assert_expr(fml, ind); // assert_expr(formula, indicator) ✓
}
```
This affects any code path that calls `smt_solver::translate()` and uses
named assertions (`assert_and_track` / `Z3_solver_assert_and_track`),
including all parallel solving modes.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
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
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>
`seq.foldl` could produce a concrete sequence model while related
`seq.nth` constraints were still validated against stale or
underconstrained length information, leading to invalid models. In the
reported case, `all` was modeled as `(seq.++ (seq.unit 7) (seq.unit 0))`
while `final = (seq.nth all 0)` remained inconsistent with `final = 6`.
- **Root cause**
- Sequence solutions were propagated as equalities, but parent `seq.len`
terms were not updated when a sequence term was solved.
- As a result, `seq.nth` guard reasoning could miss that a solved
sequence had known in-bounds length.
- **Solver change**
- Extend `theory_seq::add_solution` to collect parent `seq.len`
expressions of a solved term when the solved result is sequence-typed.
- After propagating the solved sequence equality, also propagate the
rewritten length equality for those parent length terms.
- Keep this propagation guarded to sequence results so scalar
`seq.foldl`/`seq.foldli` solutions do not regress from `sat` to
`unknown` under model validation.
- **Regression coverage**
- Add a focused test for the reported SMT-LIB pattern:
- `all = seq.foldl(...)`
- `final = seq.nth all 0`
- `initial = 0`
- `final = 6`
- Add focused scalar `seq.foldl`/`seq.foldli` model-validation coverage
for the existing benchmark shapes that must continue returning `sat`.
- The regressions check both that model validation no longer reports an
invalid model for the `seq.nth` case and that scalar fold/foldi cases do
not regress to `unknown`.
- **Effect**
- Solved sequence terms now push enough derived length information for
dependent `seq.nth` constraints to validate against the actual modeled
sequence.
- Existing scalar fold/foldi solving behavior is preserved.
```smt2
(define-fun all_sums ((prev_sums (Seq Int)) (elem Int)) (Seq Int)
(seq.++ (seq.unit (+ (seq.nth prev_sums 0) elem)) prev_sums)
)
(assert (= all (seq.foldl all_sums (seq.unit initial) elements)))
(assert (= final (seq.nth all 0)))
(assert (= initial 0))
(assert (= final 6))
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The reported case showed expensive reasoning for lexicographic string
comparisons under the default sequence solver, and incorrect handling
expectations with `z3str3` (which does not interpret these comparisons).
This change targets the default solver path by short-circuiting
contradictory constant-bound `<` constraints earlier.
- **Theory shortcut for constant lexical bounds**
- In `theory_seq::assign_eh`, detect asserted `str.<` constraints of the
form `c < x` or `x < c` where `c` is a string constant.
- When a complementary bound on the same equivalence class is already
true, check bound consistency immediately.
- If bounds are contradictory (`!(lower < upper)`), emit a direct theory
conflict from the two active literals instead of waiting for deeper
axiom propagation.
- **Preserve existing comparison reasoning**
- Existing `check_lts` transitivity/axiom flow is retained.
- The new logic is a narrow fast path for contradictory constant bounds
and does not alter general string-order semantics.
- **Regression coverage**
- Added a solver-level regression in `src/test/seq_rewriter.cpp` for
contradictory date-like lexical bounds to ensure this class of
constraints is rejected as `unsat`.
```cpp
ctx.assert_expr(su.str.mk_lex_lt(su.str.mk_string("2024-01-01"), x));
ctx.assert_expr(su.str.mk_lex_lt(x, su.str.mk_string("2024-12-31")));
ctx.assert_expr(su.str.mk_lex_lt(x, su.str.mk_string("2023-01-01")));
ENSURE(ctx.check() == l_false);
```
---------
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>
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>
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>
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>
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>
Root-caused and fixed 261 debug-assertion crashes found by running Z3
across the TPTP benchmarks (-tptp -T:5 model_validate=true):
1. theory_polymorphism::final_check_eh returned FC_DONE after assigning
the negation of its (already-true) theory assumption, which creates a
conflict. Returning FC_DONE reported l_true while the context was
inconsistent, tripping SASSERT(status != l_true || !inconsistent())
in context::restart. Return FC_CONTINUE so conflict resolution turns
it into l_false and the normal research loop runs.
2. model_evaluator::get_macro, polymorphic branch: def = subst(def)
assigned an expr_ref temporary to a raw expr*&; the temporary freed
the freshly substituted term, leaving def dangling (use-after-free
during model evaluation). Pin the substituted def in m_pinned, as the
as-array path already does.
3. smt_model_checker::add_instance: relax stale
SASSERT(!m.is_model_value(sk_term)); get_inv may legitimately return a
model value in polymorphic settings, already handled downstream by
get_type_compatible_term.
Unit tests: 92 passed, 0 failed. All 261 assertion crashes resolved;
the 3 remaining files are controlled ERR_PARSER (exit 103) rejections.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The polymorphism theory routed polymorphic (\) problems through
theory_polymorphism, which instantiated axioms during search. Two leaks:
1. In inst::instantiate, insert_ref_map was constructed with an expr_ref
argument, so its template parameter D deduced to expr_ref instead of
expr*. Trail objects are region-allocated and freed without running
destructors, so the embedded expr_ref never released its reference,
leaking one AST subtree per instantiation. Pass e_inst.get() so D is
expr*, matching the raw hashtable + manual inc_ref/dec_ref pattern.
2. trail_stack's destructor does not call reset(), so level-0 trail items
(including the inc_ref balancing entries for m_from_instantiation) were
never undone when the theory was destroyed. Added a ~theory_polymorphism
destructor that calls m_trail.reset().
Also keeps a defensive alias check in util::unify and a fresh per-iteration
substitution in inst::instantiate.
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.)
