fix #6292

this patches a case where macro-finder is used with arrays. It doesn't work so macro quantifiers have to be re-instated to ensure correctness

src/ast/array_decl_plugin.h

@@ -178,6 +178,7 @@ public:
     bool is_default(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_DEFAULT); }
     bool is_subset(expr const* n) const { return is_app_of(n, m_fid, OP_SET_SUBSET); }
     bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); }
+    bool is_map(func_decl* f, func_decl*& g) const { return is_map(f) && (g = get_map_func_decl(f), true); }
     func_decl * get_as_array_func_decl(expr * n) const;
     func_decl * get_as_array_func_decl(func_decl* f) const;
     func_decl * get_map_func_decl(func_decl* f) const;

src/ast/macros/macro_finder.cpp

@@ -376,7 +376,17 @@ bool macro_finder::expand_macros(unsigned num, justified_expr const * fmls, vect
     return found_new_macro;
 }
 
+void macro_finder::revert_unsafe_macros(vector<justified_expr>& new_fmls) {
+    auto& unsafe_macros = m_macro_manager.unsafe_macros();
+    for (auto* f : unsafe_macros) {
+        quantifier* q = m_macro_manager.get_macro_quantifier(f);
+        new_fmls.push_back(justified_expr(m, q, nullptr));
+    }
+    unsafe_macros.reset();
+}
+
 void macro_finder::operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls) {
+    m_macro_manager.unsafe_macros().reset();
     TRACE("macro_finder", tout << "processing macros...\n";);
     vector<justified_expr> _new_fmls;
     if (expand_macros(n, fmls, _new_fmls)) {
@@ -388,6 +398,7 @@ void macro_finder::operator()(unsigned n, justified_expr const* fmls, vector<jus
                 break;
         }
     }
+    revert_unsafe_macros(_new_fmls);
     new_fmls.append(_new_fmls);
 }
 

src/ast/macros/macro_finder.h

@@ -39,6 +39,8 @@ class macro_finder {
 
     bool is_macro(expr * n, app_ref & head, expr_ref & def);
 
+    void revert_unsafe_macros(vector<justified_expr>& new_fmls);
+
 public:
     macro_finder(ast_manager & m, macro_manager & mm);
     ~macro_finder();

src/ast/macros/macro_manager.cpp

@@ -241,12 +241,14 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter
 struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
     ast_manager& m; 
     macro_manager& mm;
+    array_util a;
     expr_dependency_ref m_used_macro_dependencies; 
     expr_ref_vector m_trail;
 
     macro_expander_cfg(ast_manager& m, macro_manager& mm):
         m(m),
         mm(mm),
+        a(m),
         m_used_macro_dependencies(m),
         m_trail(m)
     {}
@@ -296,7 +298,7 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
             return false;
         app * n = to_app(_n);
         quantifier * q = nullptr;
-        func_decl * d  = n->get_decl();
+        func_decl * d  = n->get_decl(), *d2 = nullptr;
         TRACE("macro_manager", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
         if (mm.m_decl2macro.find(d, q)) {            
             app * head = nullptr;
@@ -343,6 +345,12 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
             m_used_macro_dependencies = m.mk_join(m_used_macro_dependencies, ed); 
             return true;
         }
+        else if (a.is_as_array(d, d2) && mm.m_decl2macro.find(d2, q)) {
+            mm.unsafe_macros().insert(d2);
+        }
+        else if (a.is_map(d, d2) && mm.m_decl2macro.find(d2, q)) {
+            mm.unsafe_macros().insert(d2);
+        }
         return false;
     }
 };

src/ast/macros/macro_manager.h

@@ -47,6 +47,7 @@ class macro_manager {
     expr_dependency_ref_vector       m_macro_deps;
     obj_hashtable<func_decl>         m_forbidden_set;
     func_decl_ref_vector             m_forbidden;
+    obj_hashtable<func_decl>         m_unsafe_macros;
     struct scope {
         unsigned m_decls_lim;
         unsigned m_forbidden_lim;
@@ -86,7 +87,7 @@ public:
     quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = nullptr; m_decl2macro.find(f, q); return q; }
     void get_head_def(quantifier * q, func_decl * d, app * & head, expr_ref & def, bool& revert) const;
     void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep);
-
+    obj_hashtable<func_decl>& unsafe_macros() { return m_unsafe_macros; }
 
 };