From 43a7ccbf214840a1440dc8bd92c534a9cbf220b4 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sat, 4 Jul 2026 00:52:30 -0700 Subject: [PATCH] smt: don't give up on lambda equalities in array final check 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> --- src/smt/theory_array_full.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index e00f4cff93..35ed3f655a 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -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; }