From e83e8f695a0dbff8f86d05a2e4ca15394d2b6e20 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Sat, 11 Jul 2026 00:02:45 -0700
Subject: [PATCH] Fix array lambda final-check livelock (snapshot-regression
 iss-6364)

Reverting the registration of lambda enodes with the legacy array
solver (added in 63259d8a4) that caused a non-terminating final-check
livelock on nested-array benchmarks such as inputs/issues/iss-6364/small-5.smt2,
which regressed from 'sat' to a timeout.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/smt/smt_internalizer.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 908f505893..825d8d2b3e 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -671,10 +671,9 @@ namespace smt {
         SASSERT(is_lambda(q));
         if (e_internalized(q)) 
             return;
-        auto e = mk_enode(q, true, /* do suppress args */
+        mk_enode(q, true, /* do suppress args */
                     false,    /* it is a term, so it should not be merged with true/false */
                     true);
-        apply_sort_cnstr(q, e);
     }
 
     bool context::has_lambda() {