From 6b12da0b45b620f7d169f14f0e2e78b21d04335e Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 4 Mar 2020 18:06:38 +0000
Subject: [PATCH] Fix quasi-macro detection

---
 src/ast/macros/macro_util.cpp | 33 +++++++++++++++++++++++++++++++--
 src/ast/macros/macro_util.h   |  3 ++-
 2 files changed, 33 insertions(+), 3 deletions(-)

diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index 5bfac48ac..07a547e18 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -366,7 +366,36 @@ bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t
 
    Return true if \c n is a quasi-macro. Store the macro head in \c head, and the conditions to apply the macro in \c cond.
 */
-bool macro_util::is_quasi_macro_head(expr * n, unsigned num_decls, expr * def) const {
+bool macro_util::is_quasi_macro_head(expr * n, unsigned num_decls) const {
+    if (is_app(n) &&
+         to_app(n)->get_family_id() == null_family_id &&
+         to_app(n)->get_num_args() >= num_decls) {
+        unsigned num_args = to_app(n)->get_num_args();
+        sbuffer<bool> found_vars;
+        found_vars.resize(num_decls, false);
+        unsigned num_found_vars = 0;
+        for (unsigned i = 0; i < num_args; i++) {
+            expr * arg = to_app(n)->get_arg(i);
+            if (is_var(arg)) {
+                unsigned idx = to_var(arg)->get_idx();
+                if (idx >= num_decls)
+                    return false;
+                if (found_vars[idx] == false) {
+                    found_vars[idx] = true;
+                    num_found_vars++;
+                }
+            }
+            else {
+                if (occurs(to_app(n)->get_decl(), arg))
+                    return false;
+            }
+        }
+        return num_found_vars == num_decls;
+    }
+    return false;
+}
+
+bool macro_util::is_quasi_macro_ok(expr * n, unsigned num_decls, expr * def) const {
     if (is_app(n) &&
         to_app(n)->get_family_id() == null_family_id &&
         to_app(n)->get_num_args() >= num_decls) {
@@ -440,7 +469,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decl
 void macro_util::mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const {
     TRACE("macro_util", tout << mk_pp(head, m_manager) << "\n";);
     SASSERT(is_macro_head(head, head->get_num_args()) ||
-            is_quasi_macro_head(head, head->get_num_args(), def));
+            is_quasi_macro_ok(head, head->get_num_args(), def));
     SASSERT(!occurs(head->get_decl(), def));
     normalize_expr(head, num_decls, def, interp);
 }
diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h
index 57ad2d851..863f2c57e 100644
--- a/src/ast/macros/macro_util.h
+++ b/src/ast/macros/macro_util.h
@@ -112,7 +112,8 @@ public:
     bool is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t);
     bool is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def);
 
-    bool is_quasi_macro_head(expr * n, unsigned num_decls, expr * def = NULL) const;
+    bool is_quasi_macro_head(expr * n, unsigned num_decls) const;
+    bool is_quasi_macro_ok(expr * n, unsigned num_decls, expr * def) const;
     void quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decls, app_ref & head, expr_ref & cond) const;
 
     void mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const;