From 001ddef0580187e1cc954517efa1cf115f986283 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 29 Nov 2019 09:46:41 -0800
Subject: [PATCH] fix #2749

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/macros/macro_util.cpp | 42 +++++++++++++++++------------------
 src/smt/mam.cpp               |  1 +
 src/smt/smt_model_finder.cpp  |  4 ++--
 3 files changed, 23 insertions(+), 24 deletions(-)

diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index 2858614d9..3fae80e3e 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -175,15 +175,14 @@ bool macro_util::is_macro_head(expr * n, unsigned num_decls) const {
 
 */
 bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const {
-    if (m_manager.is_eq(n)) {
-        expr * lhs = to_app(n)->get_arg(0);
-        expr * rhs = to_app(n)->get_arg(1);
-        if (is_macro_head(lhs, num_decls) && !is_forbidden(to_app(lhs)->get_decl()) &&
-            !occurs(to_app(lhs)->get_decl(), rhs)) {
-            head = to_app(lhs);
-            def  = rhs;
-            return true;
-        }
+    expr * lhs = nullptr, * rhs = nullptr;
+    if (m_manager.is_eq(n, lhs, rhs) && 
+        is_macro_head(lhs, num_decls) && 
+        !is_forbidden(to_app(lhs)->get_decl()) &&
+        !occurs(to_app(lhs)->get_decl(), rhs)) {
+        head = to_app(lhs);
+        def  = rhs;
+        return true;
     }
     return false;
 }
@@ -207,15 +206,14 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he
 
 */
 bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const {
-    if (m_manager.is_eq(n)) {
-        expr * lhs = to_app(n)->get_arg(0);
-        expr * rhs = to_app(n)->get_arg(1);
-        if (is_macro_head(rhs, num_decls) && !is_forbidden(to_app(rhs)->get_decl()) &&
-            !occurs(to_app(rhs)->get_decl(), lhs)) {
-            head = to_app(rhs);
-            def  = lhs;
-            return true;
-        }
+    expr * lhs = nullptr, * rhs = nullptr;
+    if (m_manager.is_eq(n, lhs, rhs) &&
+        is_macro_head(rhs, num_decls) && 
+        !is_forbidden(to_app(rhs)->get_decl()) &&
+        !occurs(to_app(rhs)->get_decl(), lhs)) {
+        head = to_app(rhs);
+        def  = lhs;
+        return true;
     }
     return false;
 }
@@ -304,10 +302,9 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
    \brief Auxiliary function for is_pseudo_predicate_macro. It detects the pattern (= (f X) t)
 */
 bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t) {
-    if (!m_manager.is_eq(n))
+    expr* lhs = nullptr, *rhs = nullptr;
+    if (!m_manager.is_eq(n, lhs, rhs))
         return false;
-    expr * lhs = to_app(n)->get_arg(0);
-    expr * rhs = to_app(n)->get_arg(1);
     if (!is_ground(lhs) && !is_ground(rhs))
         return false;
     sort * s = m_manager.get_sort(lhs);
@@ -675,6 +672,7 @@ void macro_util::insert_macro(app * head, unsigned num_decls, expr * def, expr *
 
 void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom,
                                     bool hint, macro_candidates & r) {
+    TRACE("macro_util", tout << expr_ref(head, m_manager) << "\n";);
     if (!is_macro_head(head, head->get_num_args())) {
         app_ref  new_head(m_manager);
         expr_ref extra_cond(m_manager);
@@ -874,7 +872,7 @@ void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls,
 
     TRACE("macro_util", tout << "Candidate check for: " << mk_ismt2_pp(atom, m_manager) << std::endl;);
 
-    if (m_manager.is_eq(atom, lhs, rhs) || m_manager.is_iff(atom, lhs, rhs)) {
+    if (m_manager.is_eq(atom, lhs, rhs)) {
         if (is_quasi_macro_head(lhs, num_decls) &&
             !is_forbidden(to_app(lhs)->get_decl()) &&
             !occurs(to_app(lhs)->get_decl(), rhs) &&
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index abd47f156..20e2de2a8 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -2116,6 +2116,7 @@ namespace smt {
                     enode * p2 = *it2;
                     if (p2->get_decl() == f &&
                         num_args == n->get_num_args() && 
+                        num_args == p2->get_num_args() &&
                         m_context.is_relevant(p2) &&
                         p2->is_cgr() &&
                         p2->get_arg(i)->get_root() == p) {
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 20ab4f936..47cb85180 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -739,7 +739,7 @@ namespace smt {
                     }
                     // TBD: add support for the else of bitvectors.
                     // Idea: get the term t with the minimal interpretation and use t - 1.
-                }
+                } 
                 n->set_else((*(elems.begin())).m_key);
             }
 
@@ -881,7 +881,6 @@ namespace smt {
             }
 
             void mk_simple_proj(node * n) {
-                TRACE("model_finder", n->display(tout, m););
                 set_projection_else(n);
                 ptr_buffer<expr> values;
                 get_instantiation_set_values(n, values);
@@ -897,6 +896,7 @@ namespace smt {
                     pi->insert_new_entry(&v, v);
                 }
                 n->set_proj(p);
+                TRACE("model_finder", n->display(tout << p->get_name() << "\n", m););
             }
 
             void mk_projections() {