#5323

Z3Prover · Jul 18, 2021 · cde3eac · NikolajBjorner · Jul 18, 2021 · cde3eac
1 parent ce1c8ee
commit cde3eac
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
@@ -467,7 +467,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decl
    See normalize_expr
 */
 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";);
+    TRACE("macro_util", tout << mk_pp(head, m_manager) << "\n" << mk_pp(def, m_manager) << "\n";);
     SASSERT(is_macro_head(head, head->get_num_args()) ||
             is_quasi_macro_ok(head, head->get_num_args(), def));
     SASSERT(!occurs(head->get_decl(), def));

diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp
@@ -198,6 +198,7 @@ bool quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant
 
     bit_vector v_seen;
     v_seen.resize(q->get_num_decls(), false);
+    unsigned num_seen = 0;
     for (unsigned i = 0; i < a->get_num_args(); ++i) {
         expr* arg = a->get_arg(i);
         if (!is_var(arg) && !is_ground(arg))
@@ -215,8 +216,11 @@ bool quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant
             var * v = to_var(arg);
             m_new_vars.push_back(v);
             v_seen.set(v->get_idx(), true);
+            ++num_seen;
         }
     }
+    if (num_seen < q->get_num_decls())
+        return false;
 
     // Reverse the new variable names and sorts. [CMW: There is a smarter way to do this.]
     vector<symbol> new_var_names_rev;