fix #5308

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · May 28, 2021 · f42d4a5 · f42d4a5
1 parent 48beb81
commit f42d4a5
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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: