diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index f15039b9e..a3aebe80a 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1461,8 +1461,8 @@ ast_manager::~ast_manager() {
                 else {
                     std::cout << mk_ll_pp(a, *this, false) << "id: " << a->get_id() << "\n";
                 });
-
-            dec_ref(a);
+            a->m_ref_count = 0;
+            delete_node(a);
         }
     }
     if (m_format_manager != 0)
diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp
index e43adee02..ee211c44f 100644
--- a/src/ast/macros/macro_finder.cpp
+++ b/src/ast/macros/macro_finder.cpp
@@ -28,7 +28,7 @@ bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
     TRACE("macro_finder", tout << "processing: " << mk_pp(n, m_manager) << "\n";);
     expr * body        = to_quantifier(n)->get_expr();
     unsigned num_decls = to_quantifier(n)->get_num_decls();
-    return m_util.is_ite_macro(body, num_decls, head, def);
+    return m_util.is_simple_macro(body, num_decls, head, def);
 }
 
 /**
diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index 4fb8b3db6..ce8834cc7 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -189,21 +189,6 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he
     return false;
 }
 
-bool macro_util::is_ite_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref& def) const {
-    if (is_simple_macro(n, num_decls, head, def)) {
-        return true;
-    }
-    expr* c, *t, *e;
-    expr_ref def1(m_manager), def2(m_manager);
-    app_ref head2(m_manager);
-    if (m_manager.is_ite(n, c, t, e) &&
-        is_ite_macro(t, num_decls, head,  def1) &&
-        is_ite_macro(e, num_decls, head2, def2) && head == head2) {
-        def = m_manager.mk_ite(c, def1, def2);
-        return true;
-    }
-    return false;
-}
 
 /**
    \brief Return true if n is of the form
diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h
index bb1b4777b..18b00c1f7 100644
--- a/src/ast/macros/macro_util.h
+++ b/src/ast/macros/macro_util.h
@@ -107,7 +107,6 @@ public:
     bool is_simple_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref & def) const {
         return is_left_simple_macro(n, num_decls, head, def) || is_right_simple_macro(n, num_decls, head, def); 
     }
-    bool is_ite_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref& def) const;
 
     bool is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const;
     bool is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const {