From f42d4a58e3680a299f1deb33cdd81956a9861f90 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 28 May 2021 14:10:16 -0700
Subject: [PATCH] fix #5308

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ackermannization/lackr.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp
index 3a310cc34..887f1d519 100644
--- a/src/ackermannization/lackr.cpp
+++ b/src/ackermannization/lackr.cpp
@@ -295,6 +295,8 @@ bool lackr::collect_terms() {
                 }                
                 if (m_autil.is_as_array(curr, f))
                     m_non_funs.mark(f, true);
+                if (m_autil.is_map(curr))
+                    m_non_funs.mark(m_autil.get_map_func_decl(curr), true);
                 break;
             }
             case AST_QUANTIFIER: