* Fix broken term_comparer in m_normalized_terms_to_columns lookup
The `m_normalized_terms_to_columns` map in `lar_solver` uses a
`term_comparer` that delegates to `lar_term::operator==`, which
intentionally returns `false` (with comment "take care not to create
identical terms"). This makes `fetch_normalized_term_column` unable to
find any term, rendering the Horner module's `interval_from_term`
bounds-recovery path dead code.
History: `lar_term::operator==` returning `false` has been present since
the original "merge LRA" commit (911b24784, 2018). The
`m_normalized_terms_to_columns` lookup was added later (dfe0e856,
c95f66e0, Aug 2019) as "toward fetching existing terms intervals from
lar_solver". The initial code had `lp_assert(find == end)` on
registration (always true with broken ==) and `lp_assert(find != end)`
on deregister (always false). The very next commit (207c1c50, one day
later) removed both asserts, replacing them with soft checks. The
`term_comparer` struct delegating to `operator==` was introduced during
a later PIMPL refactor (b375faa77).
Fix: Replace the `term_comparer` implementation with a structural
comparison that checks size and then verifies each coefficient-variable
pair via `coeffs().find_core()`. This is localized to the
`m_normalized_terms_to_columns` map and does not change
`lar_term::operator==`, preserving its intentional semantics elsewhere.
Validated: on a QF_UFNIA benchmark, `interval_from_term` lookups go
from 0/573 successful to 34/573 successful. Unit test added for the
`fetch_normalized_term_column` round-trip.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* Disable operator== for lar_term
The operator== for lar_term was never intended to be used.
This changes physically disables it to identify what happens to depend
on the operator.
* Work around missing lar_term==
Previous commit disabled lar_term==. This is the only use of the
operator that seems meaningful. Changed it to compare by references
instead.
Compiles, but not sure this is the best solution.
* replace with e
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Delete unused ineq::operator==
The operator is unused, so there is no need to figure what is
the best fix for it.
* Remove lp tests that use ineq::operator==
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix: address issues 1,2,4,5 and add Goal API to Go bindings
Issue 2 (Go): Add Substitute, SubstituteVars, SubstituteFuns to Expr
Issue 4 (Go): Add GetDecl, NumArgs, Arg to Expr for AST app introspection
Goal API (Go): Add IsInconsistent and ToDimacsString to Goal
ASTVector (Go): Add public Size, Get, String methods
ASTMap (Go): Add ASTMap type with full CRUD API in spacer.go
Issue 1 (Go): Add Spacer fixedpoint methods QueryFromLvl, GetGroundSatAnswer,
GetRulesAlongTrace, GetRuleNamesAlongTrace, AddInvariant, GetReachable
Issue 1 (Go): Add context-level QE functions ModelExtrapolate, QeLite,
QeModelProject, QeModelProjectSkolem, QeModelProjectWithWitness
Issue 5 (OCaml): Add substitute_funs to z3.ml and z3.mli
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/afa18588-47af-4720-8cea-55fe0544ae55
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* fix: add substitute_funs to Expr module sig in z3.ml
The internal sig...end block in z3.ml (the module type declaration for Expr)
was missing val substitute_funs, causing OCaml compiler error:
The value substitute_funs is required but not provided
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/c6662702-46a3-4aa0-b225-d6b73c2a2505
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
The is_mod handler in theory_lra called ensure_nla(), which
unnecessarily created the NLA solver for pure linear problems, causing
the optimizer to return a finite value instead of -infinity.
Fix: check `m_nla` instead of calling `ensure_nla()`, matching the
pattern used by the is_idiv handler. The mod division is only registered
when NLA is already active due to nonlinear terms.
Update mod_factor tests to use QF_NIA logic and assert the mul term
before the mod term so that internalize_mul triggers ensure_nla() before
mod internalization.
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* mini_quip: port to Python 3 and fix several bugs
examples/python/mini_quip.py was Python 2 only and had several
latent bugs that prevented it from running on Python 3 or producing
correct results on benchmarks beyond horn1..5.
Python 3 / import fixes:
- Convert `print stmt` to `print(...)` calls (lines 457-458, 567,
710, 747, 765, 776).
- The bare `print("Test file: %s") % file` form was applying `%`
to the return value of print() (None); rewrite as
`print("Test file: %s" % file)`.
- Add `import sys` (used by sys.stdout.write/flush) and
`import copy` (used by QReach.state2cube via copy.deepcopy);
neither was previously imported.
- next()/prev() passed `zip(...)` directly to z3.substitute. In
Python 3 zip returns a one-shot generator; wrap with list() the
same way mini_ic3 already does.
Bug fixes:
- is_transition(): when an init rule's body is an And without any
Invariant predicate, is_body() returns (And(...), None). The
function then passed inv0=None to subst_vars and crashed inside
get_vars(). Add an explicit None check so the rule falls through
to is_init() (same fix as mini_ic3).
- generalize(): guard against an empty unsat core. Without the
guard, an empty core can be returned and become
cube2clause([])=Or([])=False, poisoning all frames (same class
of bug as in mini_ic3).
- check_reachable(): self.prev(cube) on an empty cube produced an
empty list which was then added to a solver as a no-op
constraint, so an empty cube would always look reachable. Only
add the constraint when cube is non-empty.
- quip_blocked() at f==0 for must goals contained
`assert is_sat == s.check()` where `is_sat` is undefined in that
scope; the intent is `assert sat == s.check()`.
- Inside the lemma-pushing loop in quip_blocked(), `is_sat == unsat`
was a comparison whose result was discarded; the intended
assignment is `is_sat = unsat`.
Verified on horn1..5 (unchanged behavior, all return same
SAFE/UNSAFE result and validate). Larger benchmarks (h_CRC,
h_FIFO, cache_coherence_three) now at least run without exceptions
(performance is a separate matter).
* mini_quip: guard against None from QReach.intersect in CEX trace loop
In quip_blocked, the must-goal CEX-tracing loop calls
self.reachable.intersect(self.prev(r)) and immediately uses
r.children() on the result. QReach.intersect can return None when
the model literals do not match any state in the partial reachable
set, which crashes with AttributeError: 'NoneType' object has no
attribute 'children'. Reproduces on data/h_FIFO.smt2.
Fix: save the model, and when intersect returns None fall back to
the raw self.project0(model) as the predecessor cube. This still
gives a concrete predecessor and lets the CEX trace make progress
instead of crashing.
* Refactor parallel search tree to use global node selection (SMTS-style) instead of DFS traversal.
Introduce effort-based prioritization, allow activation of any open node, and add controlled/gated
expansion to prevent over-partitioning and improve load balancing.
* clean up code
* ablations
* ablations2: effort
* ablations2: activation
* ablations3: more activations
* ablations4: visit all nodes before splitting
* throttle tree size min is based on workers not activated nodes
* ablate random throttling
* ablate nonlinear effort
* clean up code
* ablate throttle
* ablate where add_effort is
* reset
* clean up a function and add comment
---------
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
Two fixes in examples/python/mini_ic3.py:
1. generalize(): the polarity of the disjointness check was inverted,
and there was no guard against an empty unsat core. With an empty
core, And([])=True so check_disjoint(init, prev(True)) is always
False (init is sat), and the code returned the empty core. That
empty core then became cube2clause([])=Or([])=False, which got
added as a lemma to all frames. The frame became inconsistent and
is_valid() returned And(Or())=False as the "inductive invariant".
Fix: require len(core) > 0 AND check_disjoint(init, prev(core))
(without the spurious 'not'), so the core is only used when it
is genuinely disjoint from init.
2. is_transition(): when an init rule's body happens to be an And
without any Invariant predicate (e.g. (and (not A) (not B) ...)),
is_body() returns (And(...), None). is_transition then passed
inv0=None to subst_vars() which crashed inside get_vars(). Add an
explicit None check so the rule falls through to is_init().
Verified on horn1..5 (unchanged behavior), h_CRC and h_FIFO from the
blocksys benchmarks (now correctly return CEX matching z3 spacer),
and cache_coherence_three (no longer collapses to (and or)).
When a monic x*y has a factor x with mod(x, p) = 0 (fixed), propagate
mod(x*y, p) = 0. This enables Z3 to prove divisibility properties like
x mod p = 0 => (x*y) mod p = 0, which previously timed out even for
p = 2. The lemma fires in the NLA divisions check and allows Gröbner
basis and LIA to subsequently derive distributivity of div over addition.
Extends division tuples from (q, x, y) to (q, x, y, r) to track the
mod lpvar. Also registers bounded divisions from the mod internalization
path in theory_lra, not just the idiv path.
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* fix nlsat clear() and scoped_numeral_vector copy ctor crashes
Reset polynomial cache and assignments in nlsat::solver:👿:clear()
to prevent use-after-free when the solver is destroyed. The missing
resets caused heap corruption when check_assignment's
compute_linear_explanation created cached polynomials and root atoms
that outlived the solver's other data structures during destruction.
Also fix _scoped_numeral_vector copy constructor to read from other
instead of uninitialized self.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* simplify scoped_numeral_vector copy constructor loop
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* revert clear() additions that cause heap corruption
The m_cache.reset(), m_assignment.reset(), m_lo.reset(), m_hi.reset()
calls added to clear() in commit 481eb0327 cause heap corruption when
clear() is called from the destructor. The cache reset frees polynomials
while the polynomial manager still holds references to them, corrupting
the heap. This manifests as 'corrupted double-linked list' crashes
during nlsat solver destruction in the nra check path.
The reset() method already has these calls for solver reuse. The
destructor path via clear() should not duplicate them, as implicit
member destruction handles cleanup in the correct order.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* fix heap corruption from root_function move/sort operations
root_function's move constructor and move assignment were doing deep
copies of algebraic numbers via anum_manager::set() instead of proper
moves. During std::vector reallocation (emplace) and std::sort, this
caused massive allocation churn that corrupted the heap.
Fixes:
1. Move constructor: use std::move(other.val) for proper swap semantics.
2. Move assignment: use val.swap(other.val) instead of deep copy.
3. Add friend swap() for ADL so std::sort uses efficient swaps.
4. Sort root_function partitions via index permutation + swap cycles
instead of std::sort directly on root_function objects.
5. Reserve rfunc vector before emplace in add_linear_approximations().
6. Reserve lhalf/uhalf vectors before collecting root functions.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* Fix apply_permutation to take perm by const reference
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/f81ba8ad-2875-4fcc-ba91-d502905756be
Co-authored-by: levnach <5377127+levnach@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>
root_function's move constructor and move assignment were doing deep
copies of algebraic numbers via anum_manager::set() instead of proper
moves. During std::vector reallocation (emplace) and std::sort, this
caused massive allocation churn that corrupted the heap.
Fixes:
1. Move constructor: use std::move(other.val) for proper swap semantics.
2. Move assignment: use val.swap(other.val) instead of deep copy.
3. Add friend swap() for ADL so std::sort uses efficient swaps.
4. Sort root_function partitions via index permutation + swap cycles
instead of std::sort directly on root_function objects.
5. Reserve rfunc vector before emplace in add_linear_approximations().
6. Reserve lhalf/uhalf vectors before collecting root functions.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The m_cache.reset(), m_assignment.reset(), m_lo.reset(), m_hi.reset()
calls added to clear() in commit 481eb0327 cause heap corruption when
clear() is called from the destructor. The cache reset frees polynomials
while the polynomial manager still holds references to them, corrupting
the heap. This manifests as 'corrupted double-linked list' crashes
during nlsat solver destruction in the nra check path.
The reset() method already has these calls for solver reuse. The
destructor path via clear() should not duplicate them, as implicit
member destruction handles cleanup in the correct order.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Reset polynomial cache and assignments in nlsat::solver:👿:clear()
to prevent use-after-free when the solver is destroyed. The missing
resets caused heap corruption when check_assignment's
compute_linear_explanation created cached polynomials and root atoms
that outlived the solver's other data structures during destruction.
Also fix _scoped_numeral_vector copy constructor to read from other
instead of uninitialized self.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Remove .csproj overwrite in macOS x64 and ARM64 NuGet jobs that
replaced the versioned PackageReference with Version="*", causing
FileNotFoundException for Microsoft.Z3 assembly
- Add validate-build-script-tests job to run scripts/tests/test_*.py,
ensuring JNI arch flag tests from PR #8896 are exercised nightly
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Calling factor_sqf_pp recursively on Hensel-lifted factors corrupts
shared mutable state in the polynomial manager, m_m2pos, m_som_buffer,
m_cheap_som_buffer, m_tmp1, etc., causing assertion violations:
- polynomial.cpp:473 id < m_m2pos.size()
- upolynomial.cpp:2624 sign_a == -sign_b
Use factor_1_sqf_pp/factor_2_sqf_pp for small degrees, push directly
for larger degrees. These don't conflict with the outer call's buffers.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
