From 50bd6efea4baba343afffa26f742b49a47b30970 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 22 Mar 2023 14:00:09 +0100
Subject: [PATCH] fix #6624

---
 src/smt/theory_array_full.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index a4876ab4d81..079c2f62e0b 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -834,8 +834,8 @@ namespace smt {
         }
         for (enode* n : m_lambdas) 
             for (enode* p : n->get_parents())
-                if (!ctx.is_beta_redex(p, n)) {
-                    TRACE("array", tout << "not a beta redex " << enode_pp(p, ctx) << "\n");
+                if (!is_default(p) && !ctx.is_beta_redex(p, n)) {
+                    TRACE("array", tout << "lambda is not a beta redex " << enode_pp(p, ctx) << "\n");
                     return true;
                 }
         return false;