mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

smt: don't give up on lambda equalities in array final check

Browse source 
theory_array_full::has_non_beta_as_array() forced the array theory to
return FC_GIVEUP (=> 'unknown') whenever a relevant lambda had a parent
that was not a beta redex (select/map/store/default). Since commit
63259d8a4 registers top-level lambda enodes with the legacy array solver
(via apply_sort_cnstr in internalize_lambda), a lambda that only occurs
in an equality atom (lambda = array) is now pushed into m_lambdas and its
'=' parent trips this check, causing a spurious completeness give-up.

Equality between an array/lambda and another array term is fully decided
by the array theory's extensionality / interface-equality reasoning, so
it must not defeat completeness. This mirrors context::is_shared, which
already ignores basic-family (equality) parents. Skip '=' parents in the
lambda loop so these problems are solved again instead of returning
'unknown'.

Fixes a snapshot regression where iss-6748/bug-2.smt2 (and bug-1)
regressed from 'sat' to 'unknown'.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-04 00:52:30 -07:00 • committed by GitHub
parent 3d29d81607
commit 43a7ccbf21
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_array_full.cpp
View file

@ -854,7 +854,12 @@ namespace smt {
}
for (enode* n : m_lambdas)
for (enode* p : n->get_parents())
if (ctx.is_relevant(p) && !is_default(p) && !ctx.is_beta_redex(p, n)) {
if (ctx.is_relevant(p) && !is_default(p) && !m.is_eq(p->get_expr()) && !ctx.is_beta_redex(p, n)) {
// An equality parent (lambda = array) is decided by the array
// theory's extensionality / interface-equality reasoning, so it
// does not defeat completeness and must not force a give-up.
// This mirrors context::is_shared, which likewise ignores
// basic-family (equality) parents when deciding sharing.
TRACE(array, tout << "lambda is not a beta redex " << enode_pp(p, ctx) << "\n");
return true;
}