diff --git a/src/ast/ast.h b/src/ast/ast.h
index c1193dfbd..acef0c659 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -707,6 +707,10 @@ public:
     func_decl * get_decl() const { return m_decl; }
     family_id get_family_id() const { return get_decl()->get_family_id(); }
     decl_kind get_decl_kind() const { return get_decl()->get_decl_kind(); }
+    symbol const& get_name() const { return get_decl()->get_name(); }
+    unsigned get_num_parameters() const { return get_decl()->get_num_parameters(); }
+    parameter const& get_parameter(unsigned idx) const { return get_decl()->get_parameter(idx); }
+    parameter const* get_parameters() const { return get_decl()->get_parameters(); }
     bool is_app_of(family_id fid, decl_kind k) const { return get_family_id() == fid && get_decl_kind() == k; }
     unsigned get_num_args() const { return m_num_args; }
     expr * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; }
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index f4b237f9a..de8bf94b1 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -23,7 +23,7 @@ Revision History:
 #include "ast/ast_pp.h"
 #include "util/scoped_ptr_vector.h"
 
-#define DEBUG(x) TRACE("recfun", tout << x << '\n';)
+#define TRACEFN(x) TRACE("recfun", tout << x << '\n';)
 #define VALIDATE_PARAM(m, _pred_) if (!(_pred_)) m.raise_exception("invalid parameter to recfun "  #_pred_);
 
 namespace recfun {
@@ -42,18 +42,18 @@ namespace recfun {
                        sort_ref_vector const & arg_sorts,
                        unsigned num_guards, expr ** guards, expr* rhs)
     : m_pred(m, fid, name, arg_sorts), m_guards(m), m_rhs(expr_ref(rhs,m)), m_def(d) {
-        for (unsigned i=0; i<num_guards; ++i) {
-            m_guards.push_back(expr_ref(guards[i], m));
+        for (unsigned i = 0; i < num_guards; ++i) {
+            m_guards.push_back(guards[i]);
         }
     }
 
     def::def(ast_manager &m, family_id fid, symbol const & s,
-             unsigned arity, sort *const * domain, sort* range)
-        :   m_manager(m), m_name(s),
+             unsigned arity, sort* const * domain, sort* range)
+        :   m(m), m_name(s),
             m_domain(m), m_range(range, m), m_vars(m), m_cases(),
             m_decl(m), m_fid(fid), m_macro(false)
     {
-        for (unsigned i=0; i < arity; ++i)
+        for (unsigned i = 0; i < arity; ++i)
             m_domain.push_back(domain[i]);
 
         SASSERT(arity == get_arity());
@@ -69,8 +69,8 @@ namespace recfun {
             ite_find_p(ast_manager & m) : m(m) {}
             virtual bool operator()(expr * e) { return m.is_ite(e); }
         };
-        ite_find_p p(m());
-        check_pred cp(p, m());
+        ite_find_p p(m);
+        check_pred cp(p, m);
         return cp(e);
     }
 
@@ -108,8 +108,10 @@ namespace recfun {
         ite_lst const *         to_split; // `ite` terms to make a choice on
         unfold_lst const *      to_unfold; // terms yet to unfold
 
-        branch(choice_lst const * path, ite_lst const * to_split, unfold_lst const * to_unfold) : path(path), to_split(to_split), to_unfold(to_unfold) {}
-        branch(branch const & from) : path(from.path), to_split(from.to_split), to_unfold(from.to_unfold) {}
+        branch(choice_lst const * path, ite_lst const * to_split, unfold_lst const * to_unfold) : 
+            path(path), to_split(to_split), to_unfold(to_unfold) {}
+        branch(branch const & from) : 
+            path(from.path), to_split(from.to_split), to_unfold(from.to_unfold) {}
     };
 
     // state for computing cases from the RHS of a functions' definition
@@ -161,14 +163,14 @@ namespace recfun {
     {
         for (; choices != nullptr; choices = choices->next) {
             app * ite = choices->ite;
-            SASSERT(m.is_ite(ite));
+            expr* c = nullptr, *th = nullptr, *el = nullptr;
+            VERIFY(m.is_ite(ite, c, th, el));
 
             // condition to add to the guard
-            expr * cond0 = ite->get_arg(0);
-            conditions.push_back(choices->sign ? cond0 : m.mk_not(cond0));
+            conditions.push_back(choices->sign ? c : m.mk_not(c));
 
             // binding to add to the substitution
-            subst.insert(ite, choices->sign ? ite->get_arg(1) : ite->get_arg(2));
+            subst.insert(ite, choices->sign ? th : el);
         }
     }
 
@@ -183,11 +185,11 @@ namespace recfun {
     }
 
     void def::add_case(std::string & name, unsigned n_conditions, expr ** conditions, expr * rhs, bool is_imm) {
-        case_def c(m(), m_fid, this, name, get_domain(), n_conditions, conditions, rhs);
+        case_def c(m, m_fid, this, name, get_domain(), n_conditions, conditions, rhs);
         c.set_is_immediate(is_imm);
-        DEBUG("add_case " << name << " " << mk_pp(rhs, m())
+        TRACEFN("add_case " << name << " " << mk_pp(rhs, m)
               << " :is_imm " << is_imm
-              << " :guards " << mk_pp_vec(n_conditions, (ast**)conditions, m()));
+              << " :guards " << mk_pp_vec(n_conditions, (ast**)conditions, m));
         m_cases.push_back(c);
     }
 
@@ -197,12 +199,12 @@ namespace recfun {
                             unsigned n_vars, var *const * vars, expr* rhs0)
     {
         if (m_cases.size() != 0) {
-            DEBUG("bug: cases for " << m_name << " has cases already");
+            TRACEFN("bug: " << m_name << " has cases already");
             UNREACHABLE();
         }
         SASSERT(n_vars = m_domain.size());
 
-        DEBUG("compute cases " << mk_pp(rhs0, m()));
+        TRACEFN("compute cases " << mk_pp(rhs0, m));
 
         unsigned case_idx = 0;
         std::string name;
@@ -211,18 +213,18 @@ namespace recfun {
         name.append(m_name.bare_str());
         name.append("_");
 
-        for (unsigned i=0; i<n_vars; ++i)
+        for (unsigned i = 0; i < n_vars; ++i)
             m_vars.push_back(vars[i]);
 
 #if 0
         // simplify `rhs`
-        expr_ref simplified_rhs(m());
+        expr_ref simplified_rhs(m);
         expr* rhs;
         th_rw.reset();
         th_rw(rhs0, simplified_rhs); 
         rhs = simplified_rhs.get();
 
-        DEBUG("simplified into " << mk_pp(rhs, m()));
+        TRACEFN("simplified into " << mk_pp(rhs, m()));
 #else
         expr*  rhs = rhs0;
 #endif
@@ -241,14 +243,14 @@ namespace recfun {
         // rebuilding a `ite`-free RHS on the fly for each path in `rhs`.
         // Each such `ite`-free term is converted into a case_def and added to definition.
 
-        case_state st(m());
+        case_state st(m);
         {
             branch b(nullptr, nullptr, st.mk_unfold_lst(rhs));
             st.push_branch(b);
         }
 
         while (! st.empty()) {
-            DEBUG("main loop iter");
+            TRACEFN("main loop iter");
 
             branch b = st.pop_branch();
 
@@ -264,15 +266,15 @@ namespace recfun {
                     expr * e = stack.back();
                     stack.pop_back();
 
-                    if (m().is_ite(e)) {
+                    if (m.is_ite(e)) {
                         // need to do a case split on `e`, forking the search space
                         b.to_split = st.cons_ite(to_app(e), b.to_split);
-                    } else if (is_app(e)) {
+                    } 
+                    else if (is_app(e)) {
                         // explore arguments
-                        app * a = to_app(e);
-
-                        for (unsigned i=0; i < a->get_num_args(); ++i)
-                            stack.push_back(a->get_arg(i));
+                        for (expr * arg : *to_app(e)) {
+                            stack.push_back(arg);
+                        }
                     } 
                 }
             }
@@ -280,7 +282,8 @@ namespace recfun {
             if (b.to_split != nullptr) {
                 // split one `ite`, which will lead to distinct (sets of) cases
                 app * ite = b.to_split->ite;
-                SASSERT(m().is_ite(ite));
+                expr* c = nullptr, *th = nullptr, *el = nullptr;
+                VERIFY(m.is_ite(ite, c, th, el));
 
                 /* explore both positive choice and negative choice.
                  * each contains a longer path, with `ite` mapping to `true` (resp. `false),
@@ -291,10 +294,11 @@ namespace recfun {
 
                 branch b_pos(st.cons_choice(ite, true, b.path),
                              b.to_split->next,
-                             st.cons_unfold(ite->get_arg(0), ite->get_arg(1), b.to_unfold));
+                             st.cons_unfold(c, th, b.to_unfold));
+
                 branch b_neg(st.cons_choice(ite, false, b.path),
                              b.to_split->next,
-                             st.cons_unfold(ite->get_arg(0), ite->get_arg(2), b.to_unfold));
+                             st.cons_unfold(c, el, b.to_unfold));
 
                 st.push_branch(b_neg);
                 st.push_branch(b_pos);
@@ -302,20 +306,20 @@ namespace recfun {
             else {
                 // leaf of the search tree
 
-                expr_ref_vector conditions_raw(m());
-                expr_substitution subst(m());
-                convert_path(m(), b.path, conditions_raw, subst);
+                expr_ref_vector conditions_raw(m);
+                expr_substitution subst(m);
+                convert_path(m, b.path, conditions_raw, subst);
                 
                 // substitute, to get rid of `ite` terms
-                expr_ref case_rhs = replace_subst(th_rw, m(), subst, rhs);
-                expr_ref_vector conditions(m());
+                expr_ref case_rhs = replace_subst(th_rw, m, subst, rhs);
+                expr_ref_vector conditions(m);
                 for (expr * g : conditions_raw) {
-                    expr_ref g_subst(replace_subst(th_rw, m(), subst, g), m());
+                    expr_ref g_subst(replace_subst(th_rw, m, subst, g), m);
                     conditions.push_back(g_subst);
                 }
 
 
-                unsigned old_name_len = name.size();
+                size_t old_name_len = name.size();
                 {   // TODO: optimize? this does many copies
                     std::ostringstream sout;
                     sout << ((unsigned long) case_idx);
@@ -330,7 +334,7 @@ namespace recfun {
             }
         }
 
-        DEBUG("done analysing " << get_name());
+        TRACEFN("done analysing " << get_name());
     }
 
     /*
@@ -495,4 +499,4 @@ namespace recfun {
             }
         }
     }
-}
\ No newline at end of file
+}
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index b51717c1d..6c8824a6a 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -21,10 +21,10 @@ Revision History:
 #include "ast/rewriter/th_rewriter.h"
 
 namespace recfun {
-    class case_def; //<! one possible control path of a function
-    class case_pred; //<! a predicate guarding a given control flow path of a function
-    class util; //<! util for other modules
-    class def; //!< definition of a (recursive) function
+    class case_def;    //<! one possible control path of a function
+    class case_pred;   //<! a predicate guarding a given control flow path of a function
+    class util;        //<! util for other modules
+    class def;         //!< definition of a (recursive) function
     class promise_def; //!< definition to be complete
 
     enum op_kind {
@@ -33,12 +33,12 @@ namespace recfun {
         OP_DEPTH_LIMIT, // predicate enforcing some depth limit
     };
 
-    /*! A predicate `p(t1…tn)`, that, if true, means `f(t1…tn)` is following
+    /*! A predicate `p(t1...tn)`, that, if true, means `f(t1...tn)` is following
         a given path of its control flow and can be unrolled.
 
         For example, `fact n := if n<2 then 1 else n * fact(n-1)` would have two cases,
         and therefore two case predicates `C_fact_0` and `C_fact_1`, where
-        `C_fact_0(t)=true` means `t<2` (first path) and `C_fact_1(t)=true` means `¬(t<2)` (second path).
+        `C_fact_0(t)=true` means `t<2` (first path) and `C_fact_1(t)=true` means `not (t<2)` (second path).
     */
     class case_pred {
         friend class case_def;
@@ -98,7 +98,7 @@ namespace recfun {
         friend class promise_def;
         typedef vector<case_def> cases;
 
-        ast_manager &       m_manager;
+        ast_manager &       m;
         symbol              m_name; //<! name of function
         sort_ref_vector     m_domain; //<! type of arguments
         sort_ref            m_range; //<! return type
@@ -116,7 +116,6 @@ namespace recfun {
         void add_case(std::string & name, unsigned n_conds, expr ** conditions, expr* rhs, bool is_imm = false);
         bool contains_ite(expr* e); // expression contains a test?
     public:
-        ast_manager & m() const { return m_manager; }
         symbol const & get_name() const { return m_name; }
         vars const & get_vars() const { return m_vars; }
         cases & get_cases() { return m_cases; }
@@ -237,9 +236,9 @@ namespace recfun {
 
         ast_manager & m() { return m_manager; }
         th_rewriter & get_th_rewriter() { return m_th_rw; }
-        bool is_case_pred(app * e) const { return is_app_of(e, m_family_id, OP_FUN_CASE_PRED); }
-        bool is_defined(app * e) const { return is_app_of(e, m_family_id, OP_FUN_DEFINED); }
-        bool is_depth_limit(app * e) const { return is_app_of(e, m_family_id, OP_DEPTH_LIMIT); }
+        bool is_case_pred(expr * e) const { return is_app_of(e, m_family_id, OP_FUN_CASE_PRED); }
+        bool is_defined(expr * e) const { return is_app_of(e, m_family_id, OP_FUN_DEFINED); }
+        bool is_depth_limit(expr * e) const { return is_app_of(e, m_family_id, OP_DEPTH_LIMIT); }
         bool owns_app(app * e) const { return e->get_family_id() == m_family_id; }
 
         //<! add a function declaration
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index c3e9c3ffc..5902f9b2c 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -859,6 +859,10 @@ namespace smt {
 
         void mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params = 0, parameter * params = nullptr);
 
+        void mk_th_axiom(theory_id tid, literal_vector const& ls, unsigned num_params = 0, parameter * params = nullptr) {
+            mk_th_axiom(tid, ls.size(), ls.c_ptr(), num_params, params);
+        }
+
         /*
          * Provide a hint to the core solver that the specified literals form a "theory case split".
          * The core solver will enforce the condition that exactly one of these literals can be
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index 32c2fe8c5..220cfcbbf 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -29,6 +29,7 @@ namespace smt {
 
     theory_recfun::theory_recfun(ast_manager & m)
         : theory(m.mk_family_id("recfun")), 
+          m(m),
           m_plugin(*reinterpret_cast<recfun_decl_plugin*>(m.get_plugin(get_family_id()))),
           m_util(m_plugin.u()), 
           m_trail(*this),
@@ -42,8 +43,8 @@ namespace smt {
 
     theory_recfun::~theory_recfun() {
         reset_queues();
-        for (auto & kv : m_guards) {
-            m().dec_ref(kv.m_key);
+        for (expr* g : m_guards) {
+            m.dec_ref(g);
         }
         m_guards.reset();
     }
@@ -61,28 +62,26 @@ namespace smt {
     }
 
     bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) {
-        context & ctx = get_context();
         for (expr * arg : *atom) {
-            ctx.internalize(arg, false);
+            ctx().internalize(arg, false);
         }
-        if (!ctx.e_internalized(atom)) {
-            ctx.mk_enode(atom, false, true, false);
+        if (!ctx().e_internalized(atom)) {
+            ctx().mk_enode(atom, false, true, false);
         }
-        if (!ctx.b_internalized(atom)) {
-            bool_var v = ctx.mk_bool_var(atom);
-            ctx.set_var_theory(v, get_id());
+        if (!ctx().b_internalized(atom)) {
+            bool_var v = ctx().mk_bool_var(atom);
+            ctx().set_var_theory(v, get_id());
         }
         return true;
     }
 
     bool theory_recfun::internalize_term(app * term) {
-        context & ctx = get_context();
         for (expr* e : *term) {
-            ctx.internalize(e, false);
+            ctx().internalize(e, false);
         }
         // the internalization of the arguments may have triggered the internalization of term.
-        if (!ctx.e_internalized(term)) {            
-            ctx.mk_enode(term, false, false, true);
+        if (!ctx().e_internalized(term)) {            
+            ctx().mk_enode(term, false, false, true);
         }
         return true; 
     }
@@ -108,7 +107,7 @@ namespace smt {
     void theory_recfun::relevant_eh(app * n) {
         SASSERT(ctx().relevancy());
         if (u().is_defined(n)) {
-            TRACEFN("relevant_eh: (defined) " <<  mk_pp(n, m()));        
+            TRACEFN("relevant_eh: (defined) " <<  mk_pp(n, m));        
             case_expansion e(u(), n);
             push_case_expand(std::move(e));
         }
@@ -143,7 +142,7 @@ namespace smt {
 
         for (literal_vector & c : m_q_clauses) {
             TRACEFN("add axiom " << pp_lits(ctx(), c));
-            ctx().mk_th_axiom(get_id(), c.size(), c.c_ptr());
+            ctx().mk_th_axiom(get_id(), c);
         }
         m_q_clauses.clear();
 
@@ -176,8 +175,8 @@ namespace smt {
             c.push_back(~mk_literal(dlimit));
             SASSERT(ctx().get_assignment(c.back()) == l_true);
         }
-        for (auto& kv : m_guards) {
-            c.push_back(~ mk_literal(kv.m_key));
+        for (expr * g : m_guards) {
+            c.push_back(~ mk_literal(g));
         }
         TRACEFN("max-depth limit: add clause " << pp_lits(ctx(), c));
         SASSERT(std::all_of(c.begin(), c.end(), [&](literal & l) { return ctx().get_assignment(l) == l_false; })); // conflict
@@ -185,18 +184,21 @@ namespace smt {
         m_q_clauses.push_back(std::move(c));
     }
 
-    // if `is_true` and `v = C_f_i(t1...tn)`, then body-expand i-th case of `f(t1...tn)`
+    /**
+     * if `is_true` and `v = C_f_i(t1...tn)`, 
+     *    then body-expand i-th case of `f(t1...tn)`
+     */
     void theory_recfun::assign_eh(bool_var v, bool is_true) {
-        expr* e = get_context().bool_var2expr(v);
+        expr* e = ctx().bool_var2expr(v);
         if (!is_true || !is_app(e)) return;
         app* a = to_app(e);
         if (u().is_case_pred(a)) {
-            TRACEFN("assign_case_pred_true "<< mk_pp(e,m()));
+            TRACEFN("assign_case_pred_true "<< mk_pp(e,m));
             // add to set of local assumptions, for depth-limit purpose
             SASSERT(!m_guards.contains(e));
-            m_guards.insert(e, empty());
-            m().inc_ref(e);
-            insert_ref_map<theory_recfun,guard_set,ast_manager,expr*> trail_elt(m(), m_guards, e);
+            m_guards.insert(e);
+            m.inc_ref(e);
+            insert_ref_map<theory_recfun,guard_set,ast_manager,expr*> trail_elt(m, m_guards, e);
             m_trail.push(trail_elt);
             
             if (m_guards.size() > get_max_depth()) {
@@ -215,18 +217,17 @@ namespace smt {
     expr_ref theory_recfun::apply_args(recfun::vars const & vars,
                                        ptr_vector<expr> const & args,
                                        expr * e) {
-        // check that var order is standard
-        SASSERT(vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0);
-        var_subst subst(m(), true);
-        expr_ref new_body(m());
+        SASSERT(is_standard_order(vars));
+        var_subst subst(m, true);
+        expr_ref new_body(m);
         new_body = subst(e, args.size(), args.c_ptr());
         ctx().get_rewriter()(new_body); // simplify
         return new_body;
     }
     
     app_ref theory_recfun::apply_pred(recfun::case_pred const & p,
-                                       ptr_vector<expr> const & args) {
-        return app_ref(u().mk_case_pred(p, args), m());
+                                      ptr_vector<expr> const & args) {
+        return app_ref(u().mk_case_pred(p, args), m);
     }
     
     literal theory_recfun::mk_literal(expr* e) {
@@ -242,47 +243,54 @@ namespace smt {
         return lit;
     }
 
+    /**
+     * For functions f(args) that are given as macros f(vs) = rhs
+     * 
+     * 1. substitute `e.args` for `vs` into the macro rhs
+     * 2. add unit clause `f(args) = rhs`
+     */
     void theory_recfun::assert_macro_axiom(case_expansion & e) {
-        TRACEFN("assert_macro_axiom " << pp_case_expansion(e, m()));
         SASSERT(e.m_def->is_fun_macro());
         auto & vars = e.m_def->get_vars();
-        expr_ref lhs(e.m_lhs, m());
-        // substitute `e.args` into the macro RHS
-        expr_ref rhs(apply_args(vars, e.m_args, e.m_def->get_macro_rhs()), m());
-        TRACEFN("macro expansion yields" << mk_pp(rhs,m()));
-        // add unit clause `lhs = rhs`
+        expr_ref lhs(e.m_lhs, m);
+        expr_ref rhs(apply_args(vars, e.m_args, e.m_def->get_macro_rhs()), m);
         literal lit = mk_eq_lit(lhs, rhs);
-        TRACEFN("assert_macro_axiom: " << pp_lit(ctx(), lit));
         ctx().mk_th_axiom(get_id(), 1, &lit);
+        TRACEFN("case expansion         " << pp_case_expansion(e, m) << "\n" <<
+                "macro expansion yields " << mk_pp(rhs,m) << "\n" <<
+                "literal                " << pp_lit(ctx(), lit));
     }
 
+    /**
+     * Add case axioms for every case expansion path.
+     *
+     * assert `p(args) <=> And(guards)` (with CNF on the fly)
+     *
+     * also body-expand paths that do not depend on any defined fun
+     */
     void theory_recfun::assert_case_axioms(case_expansion & e) {
-        TRACEFN("assert_case_axioms "<< pp_case_expansion(e,m())
+        TRACEFN("assert_case_axioms "<< pp_case_expansion(e,m)
               << " with " << e.m_def->get_cases().size() << " cases");
         SASSERT(e.m_def->is_fun_defined());
         // add case-axioms for all case-paths
         auto & vars = e.m_def->get_vars();
         for (recfun::case_def const & c : e.m_def->get_cases()) {
             // applied predicate to `args`
-            literal_vector guards;
-            for (auto & g : c.get_guards()) {
-                expr_ref guard = apply_args(vars, e.m_args, g);
-                guards.push_back(~mk_literal(guard));
-            }
             app_ref pred_applied = apply_pred(c.get_pred(), e.m_args);
             SASSERT(u().owns_app(pred_applied));
             literal concl = mk_literal(pred_applied);
 
-            // assert `p(args) <=> And(guards)` (with CNF on the fly)
-
-            for (literal g : guards) {
-                literal c[2] = {~ concl, ~g};
+            literal_vector guards;
+            guards.push_back(concl);
+            for (auto & g : c.get_guards()) {
+                expr_ref ga = apply_args(vars, e.m_args, g);
+                literal guard = mk_literal(ga);
+                guards.push_back(~guard);
+                literal c[2] = {~concl, guard};
                 ctx().mk_th_axiom(get_id(), 2, c);
             }
-            guards.push_back(concl);
-            ctx().mk_th_axiom(get_id(), guards.size(), guards.c_ptr());
+            ctx().mk_th_axiom(get_id(), guards);
 
-            // also body-expand paths that do not depend on any defined fun
             if (c.is_immediate()) {
                 body_expansion be(c, e.m_args);
                 assert_body_axiom(be);
@@ -290,20 +298,21 @@ namespace smt {
         }
     }
 
+    /**
+     * For a guarded definition guards => f(vars) = rhs
+     * and occurrence f(args)
+     *
+     * substitute `args` for `vars` in guards, and rhs
+     * add axiom guards[args/vars] => f(args) = rhs[args/vars]
+     *
+     */
     void theory_recfun::assert_body_axiom(body_expansion & e) {
-        TRACEFN("assert_body_axioms "<< pp_body_expansion(e,m()));
         recfun::def & d = *e.m_cdef->get_def();
         auto & vars = d.get_vars();
         auto & args = e.m_args;
-        // check that var order is standard
-        SASSERT(vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0);
-        expr_ref lhs(u().mk_fun_defined(d, args), m());
-        // substitute `e.args` into the RHS of this particular case
+        SASSERT(is_standard_order(vars));
+        expr_ref lhs(u().mk_fun_defined(d, args), m);
         expr_ref rhs = apply_args(vars, args, e.m_cdef->get_rhs());
-        // substitute `e.args` into the guard of this particular case, to make
-        // the `condition` part of the clause `conds => lhs=rhs`
-
-        // now build the axiom `conds => lhs = rhs`        
 
         literal_vector clause;
         for (auto & g : e.m_cdef->get_guards()) {
@@ -311,8 +320,9 @@ namespace smt {
             clause.push_back(~mk_literal(guard));
         }        
         clause.push_back(mk_eq_lit(lhs, rhs));
-        TRACEFN("assert_body_axiom " << pp_lits(ctx(), clause));
-        ctx().mk_th_axiom(get_id(), clause.size(), clause.c_ptr());   
+        ctx().mk_th_axiom(get_id(), clause);
+        TRACEFN("body   " << pp_body_expansion(e,m));
+        TRACEFN("clause " << pp_lits(ctx(), clause));
     }
     
     final_check_status theory_recfun::final_check_eh() {
@@ -321,15 +331,14 @@ namespace smt {
 
     void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) {
         app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth());
-        TRACEFN("add_theory_assumption " << mk_pp(dlimit.get(), m()));
+        TRACEFN("add_theory_assumption " << mk_pp(dlimit.get(), m));
         assumptions.push_back(dlimit);
     }
 
-
     // if `dlimit` occurs in unsat core, return "unknown"
     lbool theory_recfun::validate_unsat_core(expr_ref_vector & unsat_core) {
         for (auto & e : unsat_core) {
-            if (is_app(e) && m_util.is_depth_limit(to_app(e)))
+            if (u().is_depth_limit(e)) 
                 return l_undef;
         }
         return l_false;
diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h
index 275d2ef59..019ef7918 100644
--- a/src/smt/theory_recfun.h
+++ b/src/smt/theory_recfun.h
@@ -33,7 +33,7 @@ namespace smt {
             stats() { reset(); }
         };
 
-        // one case-expansion of `f(t1…tn)`
+        // one case-expansion of `f(t1...tn)`
         struct case_expansion {
             expr *              m_lhs; // the term to expand
             recfun_def *        m_def;
@@ -64,18 +64,16 @@ namespace smt {
 
         friend std::ostream& operator<<(std::ostream&, pp_case_expansion const &);
 
-        // one body-expansion of `f(t1…tn)` using a `C_f_i(t1…tn)`
+        // one body-expansion of `f(t1...tn)` using a `C_f_i(t1...tn)`
         struct body_expansion {
             recfun_case_def const * m_cdef;
             ptr_vector<expr>        m_args;
 
             body_expansion(recfun_util& u, app * n) : m_cdef(0), m_args() {
                 SASSERT(u.is_case_pred(n));
-                func_decl * d = n->get_decl();
-                const symbol& name = d->get_name();
-                m_cdef = &u.get_case_def(name);
-                for (unsigned i = 0; i < n->get_num_args(); ++i)
-                    m_args.push_back(n->get_arg(i));
+                m_cdef = &u.get_case_def(n->get_name());
+                for (expr * arg : *n) 
+                    m_args.push_back(arg);
             }
             body_expansion(recfun_case_def const & d, ptr_vector<expr> & args) : m_cdef(&d), m_args(args) {}
             body_expansion(body_expansion const & from): m_cdef(from.m_cdef), m_args(from.m_args) {}
@@ -90,11 +88,11 @@ namespace smt {
 
         friend std::ostream& operator<<(std::ostream&, pp_body_expansion const &);
         
-        struct empty{};
 
         typedef trail_stack<theory_recfun>  th_trail_stack;
-        typedef obj_map<expr, empty> guard_set;
+        typedef obj_hashtable<expr> guard_set;
 
+        ast_manager&        m;
         recfun_decl_plugin& m_plugin;
         recfun_util&        m_util;
         stats               m_stats;
@@ -107,7 +105,6 @@ namespace smt {
         vector<literal_vector>      m_q_clauses;
 
         recfun_util & u() const { return m_util; }
-        ast_manager & m() { return get_manager(); }
         bool is_defined(app * f) const { return u().is_defined(f); }
         bool is_case_pred(app * f) const { return u().is_case_pred(f); }
 
@@ -123,6 +120,7 @@ namespace smt {
         void max_depth_conflict(void);
         literal mk_literal(expr* e);
         literal mk_eq_lit(expr* l, expr* r);
+        bool is_standard_order(recfun::vars const& vars) const { return vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0; }
     protected:
         void push_case_expand(case_expansion&& e) { m_q_case_expand.push_back(e); }
         void push_body_expand(body_expansion&& e) { m_q_body_expand.push_back(e); }