fix #6624

Z3Prover · Mar 22, 2023 · 50bd6ef · 50bd6ef
1 parent 03a4480
commit 50bd6ef
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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;