From 25e58ebd7627c12dc55be2789813a3d30597ae20 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Fri, 3 Jul 2026 05:21:07 -0700
Subject: [PATCH] Fix lira/array regression: lambda equality wrongly forces
 "unknown"

theory_array_full::has_non_beta_as_array() is an incompleteness guard that
forces FC_GIVEUP (result "unknown") when a lambda term registered with the
legacy array solver has a relevant parent that is neither `default` nor a
beta redex.

After lambdas began being registered with the legacy array solver (so that
`select(lambda, i)` beta axioms and the `default(lambda)` axiom are emitted),
this guard started firing on parents that are actually intrinsic to the array
decision procedure itself:

  * `(= lambda other-array)` array (dis)equality atoms, which are decided by
    extensionality (new_diseq_eh -> instantiate_extensionality), and
  * `(array-ext lambda other-array)` witness-index terms introduced by that
    same extensionality axiom.

Neither is an uninterpreted use of the lambda: extensionality asserts
`select(a, ext(a,b)) != select(b, ext(a,b))`, and the select-lambda beta axiom
reduces those selects, so the lambda is fully axiomatized in these cases.
Treating them as "non beta as array" made the solver give up with "unknown" on
satisfiable (and unsatisfiable) instances that it can in fact decide.

Exclude `is_eq` and `is_array_ext` parents from the lambda giveup check. The
`m_as_array` loop is intentionally left unchanged, since as-array equality is
genuinely incomplete.

Validated by rebuilding z3 and re-running the regressing benchmark
inputs/issues/iss-5454/bug-11.smt2, which returns to `sat` (matching the
recorded oracle), while several nested-store lambda equality/disequality tests
with known answers agree between the `lira` and default tactics.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/smt/theory_array_full.cpp | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index e00f4cff93..3a45929129 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -854,7 +854,16 @@ 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)) {
+                // Equality and array-ext parents are not genuine non-beta-redex uses:
+                // an array (dis)equality between a lambda and another array is decided by
+                // extensionality (new_diseq_eh / instantiate_extensionality), which itself
+                // introduces the array-ext witness index and the select(lambda, ext) beta
+                // redex. Together with the select-lambda beta axiom these fully axiomatize
+                // the lambda, so they must not force the solver into "unknown" the way a
+                // real uninterpreted use (e.g. an uninterpreted function applied to the
+                // lambda) does.
+                if (ctx.is_relevant(p) && !is_default(p) && !m.is_eq(p->get_expr()) &&
+                    !is_array_ext(p->get_expr()) && !ctx.is_beta_redex(p, n)) {
                     TRACE(array, tout << "lambda is not a beta redex " << enode_pp(p, ctx) << "\n");
                     return true;
                 }