diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp
index 2c4c960a7fe..2874abd6881 100644
--- a/src/ast/converters/expr_inverter.cpp
+++ b/src/ast/converters/expr_inverter.cpp
@@ -740,7 +740,7 @@ void iexpr_inverter::add_def(expr * v, expr * def) {
         return;
     SASSERT(uncnstr(v));
     SASSERT(to_app(v)->get_num_args() == 0);
-    m_mc->add(to_app(v)->get_decl(), def);
+    m_mc->add(v, def);
 }
 
 void iexpr_inverter::add_defs(unsigned num, expr* const* args, expr* u, expr* identity) {
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 60bdd2710a1..ed54b67680d 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -121,7 +121,7 @@ class elim_uncnstr_tactic : public tactic {
             SASSERT(uncnstr(v));
             SASSERT(to_app(v)->get_num_args() == 0);
             if (m_mc)
-                m_mc->add(to_app(v)->get_decl(), def);
+                m_mc->add(v, def);
         }
         
         void add_defs(unsigned num, expr * const * args, expr * u, expr * identity) {
diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index b2a10fafa08..785409e2701 100644
--- a/src/tactic/core/reduce_args_tactic.cpp
+++ b/src/tactic/core/reduce_args_tactic.cpp
@@ -414,7 +414,7 @@ struct reduce_args_tactic::imp {
             for (auto const& [t, new_def] : *map) {
                 f_mc->hide(new_def);
                 SASSERT(new_def->get_arity() == new_args.size());
-                app * new_t = m.mk_app(new_def, new_args.size(), new_args.data());
+                app * new_t = m.mk_app(new_def, new_args);
                 if (def == nullptr) {
                     def = new_t;
                 }
@@ -429,7 +429,7 @@ struct reduce_args_tactic::imp {
                     if (new_eqs.size() == 1)
                         cond = new_eqs[0];
                     else
-                        cond = m.mk_and(new_eqs.size(), new_eqs.data());
+                        cond = m.mk_and(new_eqs);
                     def = m.mk_ite(cond, new_t, def);
                 }
             }