From a05be8a29192d57c0b6596abf0e764fa924f6a6e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 19 Jun 2026 10:41:56 -0700
Subject: [PATCH] block ackermann over nested selects

---
 src/ackermannization/ackr_helper.h | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/ackermannization/ackr_helper.h b/src/ackermannization/ackr_helper.h
index beba57410..9c7c5fc1f 100644
--- a/src/ackermannization/ackr_helper.h
+++ b/src/ackermannization/ackr_helper.h
@@ -52,14 +52,26 @@ public:
         return m_autil.is_select(a) && is_uninterp_const(a->get_arg(0));
     }
 
+    void mark_non_select_rec(expr* t, expr_mark& visited, expr_mark& non_select) {
+        if (visited.is_marked(t))
+            return;
+        visited.mark(t, true);
+        non_select.mark(t, true);
+        if (is_app(t)) {
+            for (expr *arg : *to_app(t))
+                mark_non_select_rec(arg, visited,non_select);
+        }
+    }
+
     void mark_non_select(app* a, expr_mark& non_select) {
         if (m_autil.is_select(a)) {
             bool first = true;
+            expr_mark visited;
             for (expr* arg : *a) {
                 if (first) 
                     first = false; 
                 else 
-                    non_select.mark(arg, true);
+                    mark_non_select_rec(arg, visited, non_select);
             }
         }
         else {