diff --git a/doc/design_recfuns.md b/doc/design_recfuns.md
new file mode 100644
index 000000000..89980931e
--- /dev/null
+++ b/doc/design_recfuns.md
@@ -0,0 +1,93 @@
+# Design for handling recursive functions
+
+Main source of inspiration is [Sutter, Köksal & Kuncak 2011],
+as implemented in Leon, but the main
+differences is that we should unroll function definitions directly from the
+inside of Z3, in a backtracking way. Termination and fairness are ensured by
+iterative-deepening on the maximum number of unrollings in a given branch.
+
+## Unfolding
+
+The idea is that every function definition `f(x1…xn) := rhs[x1…xn]` is
+compiled into:
+
+- a list of cases `A_f_i[x1…xn] => f(x1…xn) = rhs_i[x1…xn]`.
+  When `A_f_i[t1…tn]` becomes true in the model, `f(t1…tn)` is said to be
+  *unfolded* and the clause `A_f_i[t1…tn] => f(t1…tn) = rhs_i[t1…tn]`
+  is added as an auxiliary clause.
+- a list of constraints `Γ_f_i[x1…xn] <=> A_f_i[x1…xn]`
+  that states when `A_f_i[x1…xn]` should be true, depending on inputs `x1…xn`.
+  For every term `f(t1…tn)` present in congruence closure, we
+  immediately add all the `Γ_f_i[t1…tn] <=> A_f_i[t1…tn]` as auxiliary clauses
+  (maybe during internalization of `f(t1…tn)`?).
+
+where each `A_f_i[x1…xn]` is a special new predicate representing the
+given case of `f`, and `rhs_i` does not contain any `ite`.
+We assume pattern matching has been compiled to `ite` beforehand.
+
+For example, `fact(n) := if n<2 then 1 else n * fact(n-1)` is compiled into:
+
+- `A_fact_0[n] => fact(n) = 1`
+- `A_fact_1[n] => fact(n) = n * fact(n-1)`
+- `A_fact_0[n] <=> n < 2`
+- `A_fact_1[n] <=> ¬(n < 2)`
+
+The 2 first clauses are only added when `A_fact_0[t]` is true
+(respectively `A_fact_1[t]` is true).
+The 2 other clauses are added as soon as `fact(t)` is internalized.
+
+## Termination
+
+To ensure termination, we define variables:
+
+- `unfold_depth: int`
+- `current_max_unfold_depth: int`
+- `global_max_unfold_depth: int`
+
+and a special literal `[max_depth=$n]` for each `n:int`.
+Solving is done under the local assumption
+`[max_depth=$current_max_unfold_depth]` (this should be handled in some outer
+loop, e.g. in a custom tactic).
+
+Whenever `A_f_i[t1…tn]` becomes true (for any `f`), we increment
+`unfold_depth`. If `unfold_depth > current_max_unfold_depth`, then
+the conflict clause `[max_depth=$current_max_unfold_depth] => Γ => false`
+where `Γ` is the conjunction of all `A_f_i[t1…tn]` true in the trail.
+
+For non-recursive functions, we don't have to increment `unfold_depth`. Some other functions that are known
+
+If the solver answers "SAT", we have a model.
+Otherwise, if `[max_depth=$current_max_unfold_depth]` is part of the
+unsat-core, then we increase `current_max_unfold_depth`.
+If `current_max_unfold_depth == global_max_unfold_depth` then
+we report "UNKNOWN" (reached global depth limit), otherwise we can
+try to `solve()` again with the new assumption (higher depth limit).
+
+## Tactic
+
+there should be a parametrized tactic `funrec(t, n)` where `t` is the tactic
+used to solve (under assumption that depth is limited to `current_max_unfold_depth`)
+and `n` is an integer that is assigned to `global_max_unfold_depth`.
+
+This way, to try and find models for a problem with recursive functions + LIA,
+one could use something like `(funrec (then simplify dl smt) 100)`.
+
+## Expected benefits
+
+This addition to Z3 would bring many benefits compared to current alternatives (Leon, quantifiers, …)
+
+- should be very fast and lightweight
+  (compared to Leon or quantifiers).
+  In particular, every function call is very lightweight even compared to Leon (no need for full model building, followed by unsat core extraction)
+- possibility of answering "SAT" for any `QF_*` fragment +
+  recursive functions
+- makes `define-funs-rec` a first-class citizen of the language,  usable to model user-defined theories or to analyze functional
+  programs directly
+
+## Optimizations
+
+- maybe `C_f_i` literals should never be decided on
+  (they can always be propagated).
+  Even stronger: they should not be part of conflicts?
+  (i.e. tune conflict resolution to always resolve
+   these literals away, disregarding their level)
diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt
index 54e3c27e4..ce2817b58 100644
--- a/src/ast/CMakeLists.txt
+++ b/src/ast/CMakeLists.txt
@@ -36,6 +36,7 @@ z3_add_component(ast
     occurs.cpp
     pb_decl_plugin.cpp
     pp.cpp
+    recfun_decl_plugin.cpp
     reg_decl_plugins.cpp
     seq_decl_plugin.cpp
     shared_occs.cpp
diff --git a/src/ast/ast_pp.h b/src/ast/ast_pp.h
index 5629f847a..bfb92c920 100644
--- a/src/ast/ast_pp.h
+++ b/src/ast/ast_pp.h
@@ -32,5 +32,27 @@ struct mk_pp : public mk_ismt2_pp {
     }
 };
 
+//<! print vector of ASTs
+class mk_pp_vec {
+    ast_manager &   m;
+    ast_ref_vector  vec;
+public:
+    mk_pp_vec(unsigned len, ast ** vec0, ast_manager & m) : m(m), vec(m) {
+        for (unsigned i=0; i<len; ++i) vec.push_back(vec0[i]);
+    }
+    void display(std::ostream & out) const {
+        bool first = true;
+        for (ast* e : vec) {
+            if (first) { first = false; } else { out << " "; }
+            out << mk_pp(e, m);
+        }
+    }
+};
+
+inline std::ostream& operator<<(std::ostream & out, mk_pp_vec const & pp) {
+    pp.display(out);
+    return out;
+}
+
 #endif
 
diff --git a/src/ast/csp_decl_plugin.cpp b/src/ast/csp_decl_plugin.cpp
index 9cdd20376..21cd798b2 100644
--- a/src/ast/csp_decl_plugin.cpp
+++ b/src/ast/csp_decl_plugin.cpp
@@ -109,12 +109,13 @@ func_decl * csp_decl_plugin::mk_func_decl(
         rng = m_alist_sort;
         break;
     case OP_JS_RESOURCE_AVAILABLE:
-        if (arity != 5) m_manager->raise_exception("add-resource-available expects 5 arguments");        
+        if (arity != 6) m_manager->raise_exception("add-resource-available expects 6 arguments");        
         if (domain[0] != m_resource_sort) m_manager->raise_exception("first argument of add-resource-available expects should be a resource");
-        if (domain[1] != m_int_sort) m_manager->raise_exception("2nd argument of add-resource-available expects should be an integer");
+        if (domain[2] != m_int_sort) m_manager->raise_exception("2nd argument of add-resource-available expects should be an integer");
         if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-resource-available expects should be an integer");
         if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-resource-available expects should be an integer");
-        if (domain[4] != m_alist_sort) m_manager->raise_exception("5th argument of add-resource-available should be an a list of properties");
+        if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-resource-available expects should be an integer");
+        if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-resource-available should be an a list of properties");
         name = symbol("add-resource-available");
         rng = m_alist_sort;
         break;
@@ -290,18 +291,20 @@ bool csp_util::is_job2resource(expr* e, unsigned& j) {
     return is_app_of(e, m_fid, OP_JS_JOB2RESOURCE) && (j = job2id(e), true);
 }
 
-bool csp_util::is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, uint64_t& start, uint64_t& end, svector<symbol>& properties) {
+bool csp_util::is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, unsigned& cap_time, uint64_t& start, uint64_t& end, svector<symbol>& properties) {
     if (!is_app_of(e, m_fid, OP_JS_RESOURCE_AVAILABLE)) return false;
     res = to_app(e)->get_arg(0);
     arith_util a(m);
     rational r;
     if (!a.is_numeral(to_app(e)->get_arg(1), r) || !r.is_unsigned()) return false;
     loadpct = r.get_unsigned();
-    if (!a.is_numeral(to_app(e)->get_arg(2), r) || !r.is_uint64()) return false;
-    start = r.get_uint64();
+    if (!a.is_numeral(to_app(e)->get_arg(2), r) || !r.is_unsigned()) return false;
+    cap_time = r.get_unsigned();
     if (!a.is_numeral(to_app(e)->get_arg(3), r) || !r.is_uint64()) return false;
+    start = r.get_uint64();
+    if (!a.is_numeral(to_app(e)->get_arg(4), r) || !r.is_uint64()) return false;
     end = r.get_uint64();
-    if (!is_js_properties(to_app(e)->get_arg(4), properties)) return false;
+    if (!is_js_properties(to_app(e)->get_arg(5), properties)) return false;
     return true;
 }
 
diff --git a/src/ast/csp_decl_plugin.h b/src/ast/csp_decl_plugin.h
index 05d6bfa7e..f6f15d70a 100644
--- a/src/ast/csp_decl_plugin.h
+++ b/src/ast/csp_decl_plugin.h
@@ -147,7 +147,7 @@ public:
     bool is_job2resource(expr* e, unsigned& j);
     bool is_resource(expr* e, unsigned& r);
     bool is_makespan(expr* e, unsigned& r);
-    bool is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, uint64_t& start, uint64_t& end, svector<symbol>& properites);
+    bool is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, unsigned& cap_time, uint64_t& start, uint64_t& end, svector<symbol>& properites);
     bool is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end, svector<symbol>& properites); 
     bool is_set_preemptable(expr* e, expr *& job);
     bool is_model(expr* e) const { return is_app_of(e, m_fid, OP_JS_MODEL); }
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
new file mode 100644
index 000000000..f4b237f9a
--- /dev/null
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -0,0 +1,498 @@
+/*++
+Module Name:
+
+    recfun_decl_plugin.cpp
+
+Abstract:
+
+    Declaration and definition of (potentially recursive) functions
+
+Author:
+
+    Simon Cruanes 2017-11
+
+Revision History:
+
+--*/
+
+#include <functional>
+#include <sstream>
+#include "ast/expr_functors.h"
+#include "ast/expr_substitution.h"
+#include "ast/recfun_decl_plugin.h"
+#include "ast/ast_pp.h"
+#include "util/scoped_ptr_vector.h"
+
+#define DEBUG(x) TRACE("recfun", tout << x << '\n';)
+#define VALIDATE_PARAM(m, _pred_) if (!(_pred_)) m.raise_exception("invalid parameter to recfun "  #_pred_);
+
+namespace recfun {
+    case_pred::case_pred(ast_manager & m, family_id fid, std::string const & s, sort_ref_vector const & domain)
+        : m_name(), m_name_buf(s), m_domain(domain), m_decl(m)
+    {
+        m_name = symbol(m_name_buf.c_str());
+        func_decl_info info(fid, OP_FUN_CASE_PRED);
+        m_decl = m.mk_func_decl(m_name, domain.size(), domain.c_ptr(), m.mk_bool_sort(), info);
+    }
+
+    case_def::case_def(ast_manager &m,
+                       family_id fid,
+                       def * d,
+                       std::string & name,
+                       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));
+        }
+    }
+
+    def::def(ast_manager &m, family_id fid, symbol const & s,
+             unsigned arity, sort *const * domain, sort* range)
+        :   m_manager(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)
+            m_domain.push_back(domain[i]);
+
+        SASSERT(arity == get_arity());
+        
+        func_decl_info info(fid, OP_FUN_DEFINED);
+        m_decl = m.mk_func_decl(m_name, arity, domain, range, info);
+    }
+
+    // does `e` contain any `ite` construct?
+    bool def::contains_ite(expr * e) {
+        struct ite_find_p : public i_expr_pred {
+            ast_manager & m;
+            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());
+        return cp(e);
+    }
+
+    /*
+     * compilation of functions to a list of cases.
+     * 
+     * We use a backtracking algorithm in a relatively functional style,
+     * where the multiple states (corresponding to alternatives) are stored in
+     * a region, and deallocated at the end
+     */
+
+    // immutable list of choices of `ite` terms (mapping each one's condition to true/false)
+    struct choice_lst {
+        app *               ite;
+        bool                sign;
+        choice_lst const *  next; // or null for the last one
+        choice_lst(app * ite, bool sign, choice_lst const * next) : ite(ite), sign(sign), next(next) {}
+    };
+
+    struct ite_lst {
+        app *              ite; // invariant: `is_ite(e)`
+        ite_lst const *    next;
+        ite_lst(app * ite, ite_lst const * next) : ite(ite), next(next) {}
+    };
+
+    // immutable stack of expressions to unfold
+    struct unfold_lst {
+        expr *              e;
+        unfold_lst const *  next; // or null for last one
+    };
+
+    // main state for one branch of the search tree.
+    struct branch {
+        choice_lst const *      path; // choices made so far
+        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) {}
+    };
+
+    // state for computing cases from the RHS of a functions' definition
+    class case_state {
+        region              m_reg;
+        ast_manager &       m_manager;
+        vector<branch>      m_branches;
+
+    public:
+        case_state(ast_manager & m) : m_reg(), m_manager(m), m_branches() {}
+        
+        bool empty() const { return m_branches.empty(); }
+        ast_manager & m() const { return m_manager; }
+        region & reg() { return m_reg; }
+
+        branch pop_branch() {
+            branch res = m_branches.back();
+            m_branches.pop_back();
+            return res;
+        }
+
+        void push_branch(branch const & b) { m_branches.push_back(b); }
+
+
+        unfold_lst const * cons_unfold(expr * e, unfold_lst const * next) {
+            return new (reg()) unfold_lst{e, next};
+        }
+        unfold_lst const * cons_unfold(expr * e1, expr * e2, unfold_lst const * next) {
+            return cons_unfold(e1, cons_unfold(e2, next));
+        }
+        unfold_lst const * mk_unfold_lst(expr * e) {
+            return cons_unfold(e, nullptr);
+        }
+
+        ite_lst const * cons_ite(app * ite, ite_lst const * next) {
+            return new (reg()) ite_lst{ite, next};
+        }
+
+        choice_lst const * cons_choice(app * ite, bool sign, choice_lst const * next) {
+            return new (reg()) choice_lst{ite, sign, next};
+        }
+    };
+
+    //<! build a substitution and a list of conditions from a path
+    void convert_path(ast_manager & m,
+                      choice_lst const * choices,
+                      expr_ref_vector & conditions /* out */,
+                      expr_substitution & subst /* out */)
+    {
+        for (; choices != nullptr; choices = choices->next) {
+            app * ite = choices->ite;
+            SASSERT(m.is_ite(ite));
+
+            // condition to add to the guard
+            expr * cond0 = ite->get_arg(0);
+            conditions.push_back(choices->sign ? cond0 : m.mk_not(cond0));
+
+            // binding to add to the substitution
+            subst.insert(ite, choices->sign ? ite->get_arg(1) : ite->get_arg(2));
+        }
+    }
+
+    // substitute `subst` in `e`
+    expr_ref replace_subst(th_rewriter & th_rw, ast_manager & m,
+                           expr_substitution & subst, expr * e) {
+        th_rw.reset();
+        th_rw.set_substitution(&subst);
+        expr_ref res(m);
+        th_rw(e, res);
+        return res;
+    }
+
+    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);
+        c.set_is_immediate(is_imm);
+        DEBUG("add_case " << name << " " << mk_pp(rhs, m())
+              << " :is_imm " << is_imm
+              << " :guards " << mk_pp_vec(n_conditions, (ast**)conditions, m()));
+        m_cases.push_back(c);
+    }
+
+
+    // Compute a set of cases, given the RHS
+    void def::compute_cases(is_immediate_pred & is_i, th_rewriter & th_rw,
+                            unsigned n_vars, var *const * vars, expr* rhs0)
+    {
+        if (m_cases.size() != 0) {
+            DEBUG("bug: cases for " << m_name << " has cases already");
+            UNREACHABLE();
+        }
+        SASSERT(n_vars = m_domain.size());
+
+        DEBUG("compute cases " << mk_pp(rhs0, m()));
+
+        unsigned case_idx = 0;
+        std::string name;
+        
+        name.append("case_");
+        name.append(m_name.bare_str());
+        name.append("_");
+
+        for (unsigned i=0; i<n_vars; ++i)
+            m_vars.push_back(vars[i]);
+
+#if 0
+        // simplify `rhs`
+        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()));
+#else
+        expr*  rhs = rhs0;
+#endif
+        
+        // is the function a macro (unconditional body)?
+        m_macro = n_vars == 0 || !contains_ite(rhs);
+
+        if (m_macro) {
+            // constant function or trivial control flow, only one (dummy) case
+            name.append("dummy");
+            add_case(name, 0, 0, rhs);
+            return;
+        }
+        
+        // analyze control flow of `rhs`, accumulating guards and
+        // 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());
+        {
+            branch b(nullptr, nullptr, st.mk_unfold_lst(rhs));
+            st.push_branch(b);
+        }
+
+        while (! st.empty()) {
+            DEBUG("main loop iter");
+
+            branch b = st.pop_branch();
+
+            // first: unfold expressions, stopping when we meet subterms that are `ite`
+            while (b.to_unfold != nullptr) {
+
+                ptr_vector<expr> stack;
+                stack.push_back(b.to_unfold->e);
+                
+                b.to_unfold = b.to_unfold->next;
+
+                while (! stack.empty()) {
+                    expr * e = stack.back();
+                    stack.pop_back();
+
+                    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)) {
+                        // explore arguments
+                        app * a = to_app(e);
+
+                        for (unsigned i=0; i < a->get_num_args(); ++i)
+                            stack.push_back(a->get_arg(i));
+                    } 
+                }
+            }
+
+            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));
+
+                /* explore both positive choice and negative choice.
+                 * each contains a longer path, with `ite` mapping to `true` (resp. `false),
+                 * and must unfold the `then` (resp. `else`) branch.
+                 * We must also unfold the test itself, for it could contain
+                 * tests.
+                 */
+
+                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));
+                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.push_branch(b_neg);
+                st.push_branch(b_pos);
+            }
+            else {
+                // leaf of the search tree
+
+                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());
+                for (expr * g : conditions_raw) {
+                    expr_ref g_subst(replace_subst(th_rw, m(), subst, g), m());
+                    conditions.push_back(g_subst);
+                }
+
+
+                unsigned old_name_len = name.size();
+                {   // TODO: optimize? this does many copies
+                    std::ostringstream sout;
+                    sout << ((unsigned long) case_idx);
+                    name.append(sout.str());
+                }
+                case_idx ++;
+                
+                // yield new case
+                bool is_imm = is_i(case_rhs);
+                add_case(name, conditions.size(), conditions.c_ptr(), case_rhs, is_imm);
+                name.resize(old_name_len);
+            }
+        }
+
+        DEBUG("done analysing " << get_name());
+    }
+
+    /*
+     * Main manager for defined functions
+     */
+
+    util::util(ast_manager & m, family_id id)
+    : m_manager(m), m_family_id(id), m_th_rw(m), m_plugin(0), m_dlimit_map() {
+        m_plugin = dynamic_cast<decl::plugin*>(m.get_plugin(m_family_id));
+    }
+
+    util::~util() {
+        for (auto & kv : m_dlimit_map) {
+            dealloc(kv.m_value);
+        }
+    }
+
+    def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range) {
+        return alloc(def, m(), m_family_id, name, n, domain, range);
+    }
+
+    void util::set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
+        d.set_definition(n_vars, vars, rhs);
+    }
+
+    // get or create predicate for depth limit
+    depth_limit_pred_ref util::get_depth_limit_pred(unsigned d) {
+        depth_limit_pred * pred = nullptr;
+        if (! m_dlimit_map.find(d, pred)) {
+            pred = alloc(depth_limit_pred, m(), m_family_id, d);
+            m_dlimit_map.insert(d, pred);   
+        }
+        return depth_limit_pred_ref(pred, *this);
+    }
+
+    app_ref util::mk_depth_limit_pred(unsigned d) {
+        depth_limit_pred_ref p = get_depth_limit_pred(d);
+        app_ref res(m().mk_const(p->get_decl()), m());
+        return res;
+    }
+
+    // used to know which `app` are from this theory
+    struct is_imm_pred : is_immediate_pred {
+        util & u;
+        is_imm_pred(util & u) : u(u) {}
+        bool operator()(expr * rhs) {
+            // find an `app` that is an application of a defined function
+            struct find : public i_expr_pred {
+                util & u;
+                find(util & u) : u(u) {}
+                bool operator()(expr * e) override {
+                    //return is_app(e) ? u.owns_app(to_app(e)) : false;
+                    if (! is_app(e)) return false;
+
+                    app * a = to_app(e);
+                    return u.is_defined(a);
+                }
+            };
+            find f(u);
+            check_pred cp(f, u.m());
+            bool contains_defined_fun = cp(rhs);
+            return ! contains_defined_fun;
+        }
+    };
+
+    // set definition 
+    void promise_def::set_definition(unsigned n_vars, var * const * vars, expr * rhs) {
+        SASSERT(n_vars == d->get_arity());
+                    
+        is_imm_pred is_i(*u);
+        d->compute_cases(is_i, u->get_th_rewriter(), n_vars, vars, rhs);
+    }
+
+    depth_limit_pred::depth_limit_pred(ast_manager & m, family_id fid, unsigned d)
+    : m_name_buf(), m_name(""), m_depth(d), m_decl(m) {
+        // build name, then build decl
+        std::ostringstream tmpname;
+        tmpname << "depth_limit_" << d << std::flush;
+        m_name_buf.append(tmpname.str());
+        m_name = symbol(m_name_buf.c_str());
+        parameter params[1] = { parameter(d) };
+        func_decl_info info(fid, OP_DEPTH_LIMIT, 1, params);
+        m_decl = m.mk_const_decl(m_name, m.mk_bool_sort(), info);
+    }
+
+    namespace decl {
+        plugin::plugin() : decl_plugin(), m_defs(), m_case_defs(), m_def_block() {}
+        plugin::~plugin() { finalize(); }
+
+        void plugin::finalize() {
+            for (auto& kv : m_defs) {
+                dealloc(kv.m_value);
+            }
+            m_defs.reset();
+            // m_case_defs does not own its data, no need to deallocate
+            m_case_defs.reset();
+            m_util = 0; // force deletion
+        }
+
+        util & plugin::u() const {
+            SASSERT(m_manager);
+            SASSERT(m_family_id != null_family_id);
+            if (m_util.get() == 0) {
+                m_util = alloc(util, *m_manager, m_family_id);
+            }
+            return *(m_util.get());
+        }
+
+        promise_def plugin::mk_def(symbol const& name, unsigned n, sort *const * params, sort * range) {
+            SASSERT(! m_defs.contains(name));
+            def* d = u().decl_fun(name, n, params, range);
+            m_defs.insert(name, d);
+            return promise_def(&u(), d);
+        }
+        
+        void plugin::set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
+            u().set_definition(d, n_vars, vars, rhs);
+            for (case_def & c : d.get_def()->get_cases()) {
+                m_case_defs.insert(c.get_name(), &c);
+            }
+        }
+
+        def* plugin::mk_def(symbol const& name, unsigned n, sort ** params, sort * range,
+                            unsigned n_vars, var ** vars, expr * rhs) {
+            SASSERT(! m_defs.contains(name));
+            promise_def d = mk_def(name, n, params, range);
+            set_definition(d, n_vars, vars, rhs);
+            return d.get_def();
+        }
+
+        func_decl * plugin::mk_fun_pred_decl(unsigned num_parameters, parameter const * parameters, 
+                                             unsigned arity, sort * const * domain, sort * range)
+        {
+            VALIDATE_PARAM(m(), m().is_bool(range) && num_parameters == 1 && parameters[0].is_ast());
+            func_decl_info info(m_family_id, OP_FUN_CASE_PRED, num_parameters, parameters);
+            info.m_private_parameters = true;
+            return m().mk_func_decl(symbol(parameters[0].get_symbol()), arity, domain, range, info);
+        }
+
+        func_decl * plugin::mk_fun_defined_decl(decl_kind k, unsigned num_parameters,
+                                                parameter const * parameters, 
+                                                unsigned arity, sort * const * domain, sort * range)
+        {
+            VALIDATE_PARAM(m(), num_parameters == 1 && parameters[0].is_ast());
+            func_decl_info info(m_family_id, k, num_parameters, parameters);
+            info.m_private_parameters = true;
+            return m().mk_func_decl(symbol(parameters[0].get_symbol()), arity,
+                                    domain, range, info);
+        }
+
+        // generic declaration of symbols
+        func_decl * plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+                                         unsigned arity, sort * const * domain, sort * range)
+        {
+            switch(k) {
+                case OP_FUN_CASE_PRED:
+                    return mk_fun_pred_decl(num_parameters, parameters, arity, domain, range);
+                case OP_FUN_DEFINED:
+                    return mk_fun_defined_decl(k, num_parameters, parameters, arity, domain, range);
+                default:
+                    UNREACHABLE(); return 0;
+            }
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
new file mode 100644
index 000000000..b51717c1d
--- /dev/null
+++ b/src/ast/recfun_decl_plugin.h
@@ -0,0 +1,286 @@
+/*++
+Module Name:
+
+    recfun_decl_plugin.h
+
+Abstract:
+
+    Declaration and definition of (potentially recursive) functions
+
+Author:
+
+    Simon Cruanes 2017-11
+
+Revision History:
+
+--*/
+
+#pragma once
+
+#include "ast/ast.h"
+#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 promise_def; //!< definition to be complete
+
+    enum op_kind {
+        OP_FUN_DEFINED, // defined function with one or more cases, possibly recursive
+        OP_FUN_CASE_PRED, // predicate guarding a given control flow path
+        OP_DEPTH_LIMIT, // predicate enforcing some depth limit
+    };
+
+    /*! 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).
+    */
+    class case_pred {
+        friend class case_def;
+        symbol                      m_name; //<! symbol for the predicate
+        std::string                 m_name_buf; //<! memory for m_name
+        sort_ref_vector const &     m_domain;
+        func_decl_ref               m_decl; //<! declaration for the predicate
+
+        case_pred(ast_manager & m, family_id fid, std::string const & s, sort_ref_vector const & args);
+    public:
+        symbol const & get_name() const { return m_name; }
+        sort_ref_vector const & get_domain() const { return m_domain; }
+        func_decl * get_decl() const { return m_decl.get(); }
+        unsigned get_arity() const { return m_domain.size(); }
+    };
+
+    typedef var_ref_vector vars;
+
+    class case_def {
+        friend class def;
+        case_pred           m_pred; //<! predicate used for this case
+        expr_ref_vector     m_guards; //<! conjunction that is equivalent to this case
+        expr_ref            m_rhs; //<! if guard is true, `f(t1…tn) = rhs` holds
+        def *               m_def; //<! definition this is a part of
+        bool                m_immediate; //<! does `rhs` contain no defined_fun/case_pred?
+
+        case_def(ast_manager & m,
+                 family_id fid,
+                 def * d,
+                 std::string & name,
+                 sort_ref_vector const & arg_sorts,
+                 unsigned num_guards,
+                 expr** guards,
+                 expr* rhs);
+
+        void add_guard(expr_ref && e) { m_guards.push_back(e); }
+    public:
+        symbol const& get_name() const { return m_pred.get_name(); }
+        case_pred const & get_pred() const { return m_pred; }
+        def * get_def() const { return m_def; }
+        expr_ref_vector const & get_guards() const { return m_guards; }
+        expr * get_guards_c_ptr() const { return *m_guards.c_ptr(); }
+        expr * get_guard(unsigned i) const { return m_guards[i]; }
+        expr * get_rhs() const { return m_rhs; }
+        unsigned num_guards() const { return m_guards.size(); }
+        bool is_immediate() const { return m_immediate; };
+        void set_is_immediate(bool b) { m_immediate = b; }
+    };
+
+    // closure for computing whether a `rhs` expression is immediate
+    struct is_immediate_pred {
+        virtual bool operator()(expr * rhs) = 0;
+    };
+
+    class def {
+        friend class util;
+        friend class promise_def;
+        typedef vector<case_def> cases;
+
+        ast_manager &       m_manager;
+        symbol              m_name; //<! name of function
+        sort_ref_vector     m_domain; //<! type of arguments
+        sort_ref            m_range; //<! return type
+        vars                m_vars; //<! variables of the function
+        cases               m_cases; //!< possible cases
+        func_decl_ref       m_decl; //!< generic declaration
+        family_id           m_fid;
+        bool                m_macro;
+
+        def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort *const * domain, sort* range);
+
+        // compute cases for a function, given its RHS (possibly containing `ite`).
+        void compute_cases(is_immediate_pred &, th_rewriter & th_rw,
+                           unsigned n_vars, var *const * vars, expr* rhs);
+        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; }
+        unsigned get_arity() const { return m_domain.size(); }
+        sort_ref_vector const & get_domain() const { return m_domain; }
+        sort_ref const & get_range() const { return m_range; }
+        func_decl * get_decl() const { return m_decl.get(); }
+
+        bool is_fun_macro() const { return m_macro; }
+        bool is_fun_defined() const { return !is_fun_macro(); }
+
+        expr * get_macro_rhs() const {
+            SASSERT(is_fun_macro());
+            return m_cases[0].get_rhs();
+        }
+    };
+    
+    // definition to be complete (missing RHS)
+    class promise_def {
+        friend class util;
+        util * u;
+        def * d;
+        void set_definition(unsigned n_vars, var * const * vars, expr * rhs); // call only once
+    public:
+        promise_def(util * u, def * d) : u(u), d(d) {}
+        promise_def(promise_def const & from) : u(from.u), d(from.d) {}
+        def * get_def() const { return d; }
+    };
+
+    // predicate for limiting unrolling depth, to be used in assumptions and conflicts
+    class depth_limit_pred {
+        friend class util;
+        std::string     m_name_buf;
+        symbol          m_name;
+        unsigned        m_depth;
+        func_decl_ref   m_decl;
+        unsigned        m_refcount;
+
+        void inc_ref() { m_refcount ++; }
+        void dec_ref() { SASSERT(m_refcount > 0); m_refcount --; }
+    public:
+        depth_limit_pred(ast_manager & m, family_id fid, unsigned d);
+        unsigned get_depth() const { return m_depth; }
+        symbol const & get_name() const { return m_name; }
+        func_decl * get_decl() const { return m_decl.get(); }
+    };
+
+    // A reference to `depth_limit_pred`
+    typedef obj_ref<depth_limit_pred, util> depth_limit_pred_ref;
+
+    namespace decl {
+
+        class plugin : public decl_plugin {
+            typedef map<symbol, def*, symbol_hash_proc, symbol_eq_proc> def_map;
+            typedef map<symbol, case_def*, symbol_hash_proc, symbol_eq_proc> case_def_map;
+
+            mutable scoped_ptr<util> m_util;
+            def_map                 m_defs; // function->def
+            case_def_map            m_case_defs; // case_pred->def
+            svector<symbol>         m_def_block;
+            
+            ast_manager & m() { return *m_manager; }
+        public:
+            plugin();
+            virtual ~plugin() override;
+            virtual void finalize() override;
+
+            util & u() const; // build or return util
+
+            virtual bool is_fully_interp(sort * s) const override { return false; } // might depend on unin sorts
+        
+            virtual decl_plugin * mk_fresh() override { return alloc(plugin); }
+        
+            virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override { UNREACHABLE(); return 0; }
+        
+            virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+                                             unsigned arity, sort * const * domain, sort * range) override;
+
+            promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range);
+
+            void set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
+
+            def* mk_def(symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs);
+
+            bool has_def(const symbol& s) const { return m_defs.contains(s); }
+            def const& get_def(const symbol& s) const { return *(m_defs[s]); }
+            promise_def get_promise_def(const symbol &s) const { return promise_def(&u(), m_defs[s]); }
+            def& get_def(symbol const& s) { return *(m_defs[s]); }
+            bool has_case_def(const symbol& s) const { return m_case_defs.contains(s); }
+            case_def& get_case_def(symbol const& s) { SASSERT(has_case_def(s)); return *(m_case_defs[s]); }
+            bool is_declared(symbol const& s) const { return m_defs.contains(s); }
+        private:
+            func_decl * mk_fun_pred_decl(unsigned num_parameters, parameter const * parameters, 
+                                         unsigned arity, sort * const * domain, sort * range);
+            func_decl * mk_fun_defined_decl(decl_kind k,
+                                            unsigned num_parameters, parameter const * parameters, 
+                                            unsigned arity, sort * const * domain, sort * range);
+        };
+    }
+
+    // Varus utils for recursive functions
+    class util {
+        friend class decl::plugin;
+
+        typedef map<int, depth_limit_pred *, int_hash, default_eq<int>> depth_limit_map;
+        
+        ast_manager &           m_manager;
+        family_id               m_family_id;
+        th_rewriter             m_th_rw;
+        decl::plugin *          m_plugin;
+        depth_limit_map         m_dlimit_map;
+
+        bool compute_is_immediate(expr * rhs);
+        void set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
+    public:
+        util(ast_manager &m, family_id);
+        virtual ~util();
+
+        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 owns_app(app * e) const { return e->get_family_id() == m_family_id; }
+
+        //<! add a function declaration
+        def * decl_fun(symbol const & s, unsigned n_args, sort *const * args, sort * range);
+
+        def& get_def(symbol const & s) {
+            SASSERT(m_plugin->has_def(s));
+            return m_plugin->get_def(s);
+        }
+
+        case_def& get_case_def(symbol const & s) {
+            SASSERT(m_plugin->has_case_def(s));
+            return m_plugin->get_case_def(s);
+        }
+
+        app* mk_fun_defined(def const & d, unsigned n_args, expr * const * args) {
+            return m().mk_app(d.get_decl(), n_args, args);
+        }
+        app* mk_fun_defined(def const & d, ptr_vector<expr> const & args) {
+            return mk_fun_defined(d, args.size(), args.c_ptr());
+        }
+        app* mk_case_pred(case_pred const & p, ptr_vector<expr> const & args) {
+            return m().mk_app(p.get_decl(), args.size(), args.c_ptr());
+        }
+
+        void inc_ref(depth_limit_pred * p) { p->inc_ref(); }
+        void dec_ref(depth_limit_pred * p) {
+            p->dec_ref();
+            if (p->m_refcount == 0) {
+                m_dlimit_map.remove(p->m_depth);
+                dealloc(p);
+            }
+        }
+
+        depth_limit_pred_ref get_depth_limit_pred(unsigned d);
+        app_ref mk_depth_limit_pred(unsigned d);
+    };
+}
+
+typedef recfun::def recfun_def;
+typedef recfun::case_def recfun_case_def;
+typedef recfun::depth_limit_pred recfun_depth_limit_pred;
+typedef recfun::decl::plugin recfun_decl_plugin;
+typedef recfun::util recfun_util;
diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp
index 985ecee9e..f8abe81d8 100644
--- a/src/ast/reg_decl_plugins.cpp
+++ b/src/ast/reg_decl_plugins.cpp
@@ -22,6 +22,7 @@ Revision History:
 #include "ast/array_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
 #include "ast/datatype_decl_plugin.h"
+#include "ast/recfun_decl_plugin.h"
 #include "ast/dl_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/pb_decl_plugin.h"
@@ -40,6 +41,9 @@ void reg_decl_plugins(ast_manager & m) {
     if (!m.get_plugin(m.mk_family_id(symbol("datatype")))) {
         m.register_plugin(symbol("datatype"), alloc(datatype_decl_plugin));    
     }
+    if (!m.get_plugin(m.mk_family_id(symbol("recfun")))) {
+        m.register_plugin(symbol("recfun"), alloc(recfun_decl_plugin));    
+    }
     if (!m.get_plugin(m.mk_family_id(symbol("datalog_relation")))) {
         m.register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin));
     }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index a1c47cdce..18b47d012 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -680,6 +680,8 @@ bool cmd_context::logic_has_datatype() const {
     return !has_logic() || smt_logics::logic_has_datatype(m_logic);
 }
 
+bool cmd_context::logic_has_recfun() const { return true; }
+
 void cmd_context::init_manager_core(bool new_manager) {
     SASSERT(m_manager != 0);
     SASSERT(m_pmanager != 0);
@@ -692,6 +694,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         register_plugin(symbol("bv"),       alloc(bv_decl_plugin), logic_has_bv());
         register_plugin(symbol("array"),    alloc(array_decl_plugin), logic_has_array());
         register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype());
+        register_plugin(symbol("recfun"),   alloc(recfun_decl_plugin), logic_has_recfun());
         register_plugin(symbol("seq"),      alloc(seq_decl_plugin), logic_has_seq());
         register_plugin(symbol("pb"),       alloc(pb_decl_plugin), logic_has_pb());
         register_plugin(symbol("fpa"),      alloc(fpa_decl_plugin), logic_has_fpa());
@@ -708,6 +711,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         load_plugin(symbol("bv"),       logic_has_bv(), fids);
         load_plugin(symbol("array"),    logic_has_array(), fids);
         load_plugin(symbol("datatype"), logic_has_datatype(), fids);
+        load_plugin(symbol("recfun"),   logic_has_recfun(), fids);
         load_plugin(symbol("seq"),      logic_has_seq(), fids);
         load_plugin(symbol("fpa"),      logic_has_fpa(), fids);
         load_plugin(symbol("pb"),       logic_has_pb(), fids);
@@ -891,7 +895,25 @@ void cmd_context::model_del(func_decl* f) {
     m_mc0->hide(f);
 }
 
-void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* e) {
+
+recfun_decl_plugin * cmd_context::get_recfun_plugin() {
+    ast_manager & m = get_ast_manager();
+    family_id id = m.get_family_id("recfun");
+    recfun_decl_plugin* p = reinterpret_cast<recfun_decl_plugin*>(m.get_plugin(id));
+    SASSERT(p);
+    return p;
+}
+
+
+recfun::promise_def cmd_context::decl_rec_fun(const symbol &name, unsigned int arity, sort *const *domain, sort *range) {
+    SASSERT(logic_has_recfun());
+    recfun_decl_plugin* p = get_recfun_plugin();
+    recfun::promise_def def = p->mk_def(name, arity, domain, range);
+    return def;
+}
+
+// insert a recursive function as a regular quantified axiom
+void cmd_context::insert_rec_fun_as_axiom(func_decl *f, expr_ref_vector const& binding, svector<symbol> const &ids, expr* e) {
     expr_ref eq(m());
     app_ref lhs(m());
     lhs = m().mk_app(f, binding.size(), binding.c_ptr());
@@ -922,6 +944,28 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
     assert_expr(eq);
 }
 
+
+void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* rhs) {
+    TRACE("recfun", tout<< "define recfun " << f->get_name()  << " = " << mk_pp(rhs, m()) << "\n";);
+
+    if (gparams::get_value("smt.recfun.native") != "true") {
+        // just use an axiom
+        insert_rec_fun_as_axiom(f, binding, ids, rhs);
+        return;
+    }
+
+    recfun_decl_plugin* p = get_recfun_plugin();
+
+    var_ref_vector vars(m());
+    for (expr* b : binding) {
+        SASSERT(is_var(b));
+        vars.push_back(to_var(b));
+    }
+    
+    recfun::promise_def d = p->get_promise_def(f->get_name());
+    p->set_definition(d, vars.size(), vars.c_ptr(), rhs);
+}
+
 func_decl * cmd_context::find_func_decl(symbol const & s) const {
     builtin_decl d;
     if (m_builtin_decls.find(s, d)) {
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index cb49d1825..acc406dfc 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -32,6 +32,7 @@ Notes:
 #include "ast/ast.h"
 #include "ast/ast_printer.h"
 #include "ast/datatype_decl_plugin.h"
+#include "ast/recfun_decl_plugin.h"
 #include "tactic/generic_model_converter.h"
 #include "solver/solver.h"
 #include "solver/progress_callback.h"
@@ -291,6 +292,7 @@ protected:
     bool logic_has_array() const;
     bool logic_has_datatype() const;
     bool logic_has_fpa() const;
+    bool logic_has_recfun() const;
 
     void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; }
     void print_unsupported_info(symbol const& s, int line, int pos) { if (s != symbol::null) diagnostic_stream() << "; " << s << " line: " << line << " position: " << pos << std::endl;}
@@ -306,6 +308,7 @@ protected:
     void erase_macro(symbol const& s);
     bool macros_find(symbol const& s, unsigned n, expr*const* args, expr*& t) const;
 
+    recfun_decl_plugin * get_recfun_plugin();
 
 public:
     cmd_context(bool main_ctx = true, ast_manager * m = nullptr, symbol const & l = symbol::null);
@@ -384,12 +387,14 @@ public:
     void insert(probe_info * p) { tactic_manager::insert(p); }
     void insert_user_tactic(symbol const & s, sexpr * d);
     void insert_aux_pdecl(pdecl * p);
-    void insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* e);
     void model_add(symbol const & s, unsigned arity, sort *const* domain, expr * t);
     void model_del(func_decl* f);
+    void insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* e);
+    void insert_rec_fun_as_axiom(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* e);
     func_decl * find_func_decl(symbol const & s) const;
     func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices,
                                unsigned arity, sort * const * domain, sort * range) const;
+    recfun::promise_def decl_rec_fun(const symbol &name, unsigned int arity, sort *const *domain, sort *range);
     psort_decl * find_psort_decl(symbol const & s) const;
     cmd * find_cmd(symbol const & s) const;
     sexpr * find_user_tactic(symbol const & s) const;
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index cd259e8f2..8db6388ab 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -2317,7 +2317,7 @@ namespace smt2 {
             next();
         }
 
-        void parse_rec_fun_decl(func_decl_ref& f, expr_ref_vector& bindings, svector<symbol>& ids) {
+        recfun::promise_def parse_rec_fun_decl(func_decl_ref& f, expr_ref_vector& bindings, svector<symbol>& ids) {
             SASSERT(m_num_bindings == 0);
             check_identifier("invalid function/constant definition, symbol expected");
             symbol id = curr_id();
@@ -2328,7 +2328,8 @@ namespace smt2 {
             unsigned num_vars  = parse_sorted_vars();
             SASSERT(num_vars == m_num_bindings);
             parse_sort("Invalid recursive function definition");
-            f = m().mk_func_decl(id, num_vars, sort_stack().c_ptr() + sort_spos, sort_stack().back());
+            recfun::promise_def pdef = m_ctx.decl_rec_fun(id, num_vars, sort_stack().c_ptr() + sort_spos, sort_stack().back());
+            f = pdef.get_def()->get_decl();
             bindings.append(num_vars, expr_stack().c_ptr() + expr_spos);
             ids.append(num_vars, symbol_stack().c_ptr() + sym_spos);
             symbol_stack().shrink(sym_spos);
@@ -2336,6 +2337,7 @@ namespace smt2 {
             expr_stack().shrink(expr_spos);
             m_env.end_scope();
             m_num_bindings = 0;
+            return pdef;
         }
 
         void parse_rec_fun_bodies(func_decl_ref_vector const& decls, vector<expr_ref_vector> const& bindings, vector<svector<symbol> >const & ids) {
diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index 4b640f8ca..52d3a5943 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -60,6 +60,7 @@ z3_add_component(smt
     theory_lra.cpp
     theory_opt.cpp
     theory_pb.cpp
+    theory_recfun.cpp
     theory_seq.cpp
     theory_str.cpp
     theory_utvpi.cpp
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 650afda25..3f800455b 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -27,6 +27,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_random_seed = p.random_seed();
     m_relevancy_lvl = p.relevancy();
     m_ematching   = p.ematching();
+    m_recfun_max_depth = p.recfun_max_depth();
     m_phase_selection = static_cast<phase_selection>(p.phase_selection());
     m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
     m_restart_factor = p.restart_factor();
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index 8901697b7..a5923089c 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -108,6 +108,9 @@ struct smt_params : public preprocessor_params,
     bool             m_new_core2th_eq;
     bool             m_ematching;
 
+    // TODO: move into its own file?
+    unsigned         m_recfun_max_depth;
+
     // -----------------------------------
     //
     // Case split strategy
@@ -261,6 +264,7 @@ struct smt_params : public preprocessor_params,
         m_display_features(false),
         m_new_core2th_eq(true),
         m_ematching(true),
+        m_recfun_max_depth(50),
         m_case_split_strategy(CS_ACTIVITY_DELAY_NEW),
         m_rel_case_split_order(0),
         m_lookahead_diseq(false),
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 76e9f03b1..828e4f7de 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -95,5 +95,7 @@ def_module_params(module_name='smt',
                           ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),
                           ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'),
                           ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'),
-                          ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy')
+                          ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'),
+                          ('recfun.native', BOOL, False, 'use native rec-fun solver'),
+                          ('recfun.max_depth', UINT, 500, 'maximum depth of unrolling for recursive functions')
                           ))
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 8864d6e78..5049eb3fc 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1614,6 +1614,35 @@ namespace smt {
         void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); }
     };
 
+
+    struct pp_lit {
+        smt::context & ctx;
+        smt::literal lit;
+        pp_lit(smt::context & ctx, smt::literal lit) : ctx(ctx), lit(lit) {}
+    };
+
+    inline std::ostream & operator<<(std::ostream & out, pp_lit const & pp) {
+        pp.ctx.display_detailed_literal(out, pp.lit);
+        return out;
+    }
+
+    struct pp_lits {
+        smt::context & ctx;
+        smt::literal *lits;
+        unsigned len;
+        pp_lits(smt::context & ctx, unsigned len, smt::literal *lits) : ctx(ctx), lits(lits), len(len) {}
+    };
+
+    inline std::ostream & operator<<(std::ostream & out, pp_lits const & pp) {
+        out << "clause{";
+        bool first = true;
+        for (unsigned i = 0; i < pp.len; ++i) {
+            if (first) { first = false; } else { out << " ∨ "; }
+            pp.ctx.display_detailed_literal(out, pp.lits[i]);
+        }
+        return out << "}";
+    }
+
 };
 
 #endif /* SMT_CONTEXT_H_ */
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 585e7e841..cf3f6f1e5 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -28,6 +28,7 @@ Revision History:
 #include "smt/theory_array_full.h"
 #include "smt/theory_bv.h"
 #include "smt/theory_datatype.h"
+#include "smt/theory_recfun.h"
 #include "smt/theory_dummy.h"
 #include "smt/theory_dl.h"
 #include "smt/theory_seq_empty.h"
@@ -222,6 +223,7 @@ namespace smt {
     void setup::setup_QF_DT() {
         setup_QF_UF();
         setup_datatypes();
+        setup_recfuns();
     }
 
     void setup::setup_QF_BVRE() {
@@ -878,6 +880,13 @@ namespace smt {
         m_context.register_plugin(alloc(theory_datatype, m_manager, m_params));
     }
 
+    void setup::setup_recfuns() {
+        TRACE("recfun", tout << "registering theory recfun...\n";);
+        theory_recfun * th = alloc(theory_recfun, m_manager);
+        m_context.register_plugin(th);
+        th->setup_params();
+    }
+
     void setup::setup_dl() {
         m_context.register_plugin(mk_theory_dl(m_manager));
     }
@@ -936,6 +945,7 @@ namespace smt {
         setup_arrays();
         setup_bv();
         setup_datatypes();
+        setup_recfuns();
         setup_dl();
         setup_seq_str(st);
         setup_card();
diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h
index 61bfa386e..01a143301 100644
--- a/src/smt/smt_setup.h
+++ b/src/smt/smt_setup.h
@@ -94,6 +94,7 @@ namespace smt {
         void setup_unknown(static_features & st);
         void setup_arrays();
         void setup_datatypes();
+        void setup_recfuns();
         void setup_bv();
         void setup_arith();
         void setup_dl();
diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp
index 0cf2d9be4..880d75d24 100644
--- a/src/smt/theory_jobscheduler.cpp
+++ b/src/smt/theory_jobscheduler.cpp
@@ -94,20 +94,29 @@ namespace smt {
         symbol key, val;
         rational r;
         expr* job, *resource;
-        unsigned j = 0, res = 0, cap = 0, loadpct = 100;
+        unsigned j = 0, res = 0, cap = 0, loadpct = 100, level = 0;
         time_t start = 0, end = std::numeric_limits<time_t>::max(), capacity = 0;
+        js_job_goal goal;
+        js_optimization_objective obj;
         properties ps;
         if (u.is_set_preemptable(cmd, job) && u.is_job(job, j)) {
             set_preemptable(j, true);            
         }
-        else if (u.is_add_resource_available(cmd, resource, loadpct, start, end, ps) && u.is_resource(resource, res)) {
+        else if (u.is_add_resource_available(cmd, resource, loadpct, cap, start, end, ps) && u.is_resource(resource, res)) {
             std::sort(ps.begin(), ps.end(), symbol_cmp());
+            (void) cap; // TBD
             add_resource_available(res, loadpct, start, end, ps);
         }
         else if (u.is_add_job_resource(cmd, job, resource, loadpct, capacity, end, ps) && u.is_job(job, j) && u.is_resource(resource, res)) {
             std::sort(ps.begin(), ps.end(), symbol_cmp());
             add_job_resource(j, res, loadpct, capacity, end, ps);
         }
+        else if (u.is_job_goal(cmd, goal, level, job) && u.is_job(job, j)) {
+            // skip
+        }
+        else if (u.is_objective(cmd, obj)) {
+            // skip
+        }
         else {
             invalid_argument("command not recognized ", cmd);
         }
@@ -487,7 +496,7 @@ namespace smt {
 
     std::ostream& theory_jobscheduler::display(std::ostream & out, job_info const& j) const {
         for (job_resource const& jr : j.m_resources) {
-            display(out << "  ", jr);
+            display(out << "  ", jr) << "\n";
         }
         return out;
     }
@@ -507,10 +516,10 @@ namespace smt {
     void theory_jobscheduler::display(std::ostream & out) const {
         out << "jobscheduler:\n";
         for (unsigned j = 0; j < m_jobs.size(); ++j) {
-            display(out << "job " << j << ":\n", m_jobs[j]);
+            display(out << "job " << j << ":\n", m_jobs[j]) << "\n";
         }
         for (unsigned r = 0; r < m_resources.size(); ++r) {
-            display(out << "resource " << r << ":\n", m_resources[r]);
+            display(out << "resource " << r << ":\n", m_resources[r]) << "\n";
         }
     }
         
@@ -615,8 +624,8 @@ namespace smt {
 
     void theory_jobscheduler::add_job_resource(unsigned j, unsigned r, unsigned loadpct, uint64_t cap, time_t end, properties const& ps) {
         SASSERT(get_context().at_base_level());
-        SASSERT(1 <= loadpct && loadpct <= 100);
-        SASSERT(0 < cap);
+        SASSERT(0 <= loadpct && loadpct <= 100);
+        SASSERT(0 <= cap);
         m_jobs.reserve(j + 1);
         m_resources.reserve(r + 1);
         job_info& ji = m_jobs[j];
@@ -690,7 +699,8 @@ namespace smt {
         }
 
         literal lit;
-
+        unsigned job_id = 0;
+        
         for (job_info const& ji : m_jobs) {
             if (ji.m_resources.empty()) {
                 throw default_exception("every job should be associated with at least one resource");
@@ -719,6 +729,10 @@ namespace smt {
                 // TBD: more accurate estimates for runtime_lb based on gaps
                 // TBD: correct estimate of runtime_ub taking gaps into account.
             }
+            CTRACE("csp", (start_lb > end_ub), tout << "there is no associated resource working time\n";);
+            if (start_lb > end_ub) {
+                warning_msg("Job %d has no associated resource working time", job_id);
+            }
 
             // start(j) >= start_lb
             lit = mk_ge(ji.m_start, start_lb);
@@ -730,6 +744,8 @@ namespace smt {
 
             // start(j) + runtime_lb <= end(j)
             // end(j) <= start(j) + runtime_ub 
+
+            ++job_id;
         }        
         
         TRACE("csp", tout << "add-done end\n";);
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
new file mode 100644
index 000000000..dcb8ad097
--- /dev/null
+++ b/src/smt/theory_recfun.cpp
@@ -0,0 +1,370 @@
+
+#include "util/stats.h"
+#include "ast/ast_util.h"
+#include "smt/theory_recfun.h"
+#include "smt/params/smt_params_helper.hpp"
+
+#define DEBUG(x) TRACE("recfun", tout << x << '\n';)
+
+
+namespace smt {
+
+    theory_recfun::theory_recfun(ast_manager & m)
+        : theory(m.mk_family_id("recfun")), 
+          m_plugin(*reinterpret_cast<recfun_decl_plugin*>(m.get_plugin(get_family_id()))),
+          m_util(m_plugin.u()), 
+          m_trail(*this),
+          m_guards(), m_max_depth(0), m_q_case_expand(), m_q_body_expand(), m_q_clauses()
+        {
+        }
+
+    theory_recfun::~theory_recfun() {
+        reset_queues();
+        for (auto & kv : m_guards) {
+            m().dec_ref(kv.m_key);
+        }
+        m_guards.reset();
+    }
+
+    char const * theory_recfun::get_name() const { return "recfun"; }
+
+    void theory_recfun::setup_params() {
+        // obtain max depth via parameters
+        smt_params_helper p(get_context().get_params());
+        set_max_depth(p.recfun_max_depth());
+    }
+
+    theory* theory_recfun::mk_fresh(context* new_ctx) {
+        return alloc(theory_recfun, new_ctx->get_manager());
+    }
+
+    bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) {
+        context & ctx = get_context();
+        if (! ctx.e_internalized(atom)) {
+            unsigned num_args = atom->get_num_args();
+            for (unsigned i = 0; i < num_args; ++i)
+                ctx.internalize(atom->get_arg(i), false);
+            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());
+        }
+        return true;
+    }
+
+    bool theory_recfun::internalize_term(app * term) {
+        context & ctx = get_context();
+        for (expr* e : *term) ctx.internalize(e, false);
+        // the internalization of the arguments may have triggered the internalization of term.
+        if (ctx.e_internalized(term))
+            return true;
+        ctx.mk_enode(term, false, false, true);
+        return true; // the theory doesn't actually map terms to variables
+    }
+
+    void theory_recfun::reset_queues() {
+        m_q_case_expand.reset();
+        m_q_body_expand.reset();
+        m_q_clauses.reset();
+    }
+
+    void theory_recfun::reset_eh() {
+        m_trail.reset();
+        reset_queues();   
+        m_stats.reset();
+        theory::reset_eh();
+    }
+
+    /*
+     * when `n` becomes relevant, if it's `f(t1…tn)` with `f` defined,
+     * then case-expand `n`. If it's a macro we can also immediately
+     * body-expand it.
+     */
+    void theory_recfun::relevant_eh(app * n) {
+        SASSERT(get_context().relevancy());
+        if (u().is_defined(n)) {
+            DEBUG("relevant_eh: (defined) " <<  mk_pp(n, m()));
+        
+            case_expansion e(u(), n);
+            push_case_expand(std::move(e));
+        }
+    }
+
+    void theory_recfun::push_scope_eh() {
+        DEBUG("push_scope");
+        theory::push_scope_eh();
+        m_trail.push_scope();
+    }
+
+    void theory_recfun::pop_scope_eh(unsigned num_scopes) {
+        DEBUG("pop_scope " << num_scopes);
+        m_trail.pop_scope(num_scopes);
+        theory::pop_scope_eh(num_scopes);
+        reset_queues();
+    }
+    
+    void theory_recfun::restart_eh() {
+        DEBUG("restart");
+        reset_queues();
+        theory::restart_eh();
+    }
+
+    bool theory_recfun::can_propagate() {
+        return ! (m_q_case_expand.empty() &&
+                  m_q_body_expand.empty() &&
+                  m_q_clauses.empty());
+    }
+
+    void theory_recfun::propagate() {
+        context & ctx = get_context();
+
+        for (literal_vector & c : m_q_clauses) {
+            DEBUG("add axiom " << pp_lits(ctx, c.size(), c.c_ptr()));
+            ctx.mk_th_axiom(get_id(), c.size(), c.c_ptr());
+        }
+        m_q_clauses.clear();
+
+        for (case_expansion & e : m_q_case_expand) {
+            if (e.m_def->is_fun_macro()) {
+                // body expand immediately
+                assert_macro_axiom(e);
+            }
+            else {
+                // case expand
+                SASSERT(e.m_def->is_fun_defined());
+                assert_case_axioms(e);                
+            }
+        }
+        m_q_case_expand.clear();
+
+        for (body_expansion & e : m_q_body_expand) {
+            assert_body_axiom(e);
+        }
+        m_q_body_expand.clear();
+    }
+
+    void theory_recfun::max_depth_conflict() {
+        DEBUG("max-depth conflict");
+        context & ctx = get_context();
+        literal_vector c;
+        // make clause `depth_limit => V_{g : guards} ~ g`
+        {
+            // first literal must be the depth limit one
+            app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth());
+            ctx.internalize(dlimit, false);
+            c.push_back(~ ctx.get_literal(dlimit));
+            SASSERT(ctx.get_assignment(ctx.get_literal(dlimit)) == l_true);
+        }
+        for (auto& kv : m_guards) {
+            expr * g = & kv.get_key();
+            c.push_back(~ ctx.get_literal(g));
+        }
+        DEBUG("max-depth limit: add clause " << pp_lits(ctx, c.size(), c.c_ptr()));
+        SASSERT(std::all_of(c.begin(), c.end(), [&](literal & l) { return ctx.get_assignment(l) == l_false; })); // conflict
+
+        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)`
+    void theory_recfun::assign_eh(bool_var v, bool is_true) {
+        expr* e = get_context().bool_var2expr(v);
+        if (!is_true) return;
+        if (!is_app(e)) return;
+        app* a = to_app(e);
+        if (u().is_case_pred(a)) {
+            DEBUG("assign_case_pred_true "<< mk_pp(e,m()));
+            // add to set of local assumptions, for depth-limit purpose
+            {
+                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_trail.push(trail_elt);
+            }
+            if (m_guards.size() > get_max_depth()) {
+                // too many body-expansions: depth-limit conflict
+                max_depth_conflict();
+            }
+            else {
+                // body-expand
+                body_expansion b_e(u(), a);
+                push_body_expand(std::move(b_e));
+            }
+        }
+    }
+
+     // replace `vars` by `args` in `e`
+    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());
+        new_body = subst(e, args.size(), args.c_ptr());
+        get_context().get_rewriter()(new_body); // simplify
+        return new_body;
+    }
+    
+    app_ref theory_recfun::apply_pred(recfun::case_pred const & p,
+                                       ptr_vector<expr> const & args){
+        app_ref res(u().mk_case_pred(p, args), m());
+        return res;
+    }
+    
+    void theory_recfun::assert_macro_axiom(case_expansion & e) {
+        DEBUG("assert_macro_axiom " << pp_case_expansion(e,m()));
+        SASSERT(e.m_def->is_fun_macro());
+        expr_ref lhs(e.m_lhs, m());
+        context & ctx = get_context();
+        auto & vars = e.m_def->get_vars();
+        // substitute `e.args` into the macro RHS
+        expr_ref rhs(apply_args(vars, e.m_args, e.m_def->get_macro_rhs()), m());
+        DEBUG("macro expansion yields" << mk_pp(rhs,m()));
+        // now build the axiom `lhs = rhs`
+        ctx.internalize(rhs, false);
+        // add unit clause `lhs=rhs`
+        literal l(mk_eq(lhs, rhs, true));
+        ctx.mark_as_relevant(l);
+        literal_vector lits;
+        lits.push_back(l);
+        DEBUG("assert_macro_axiom: " << pp_lits(ctx, lits.size(), lits.c_ptr()));
+        ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());   
+    }
+
+    void theory_recfun::assert_case_axioms(case_expansion & e) {
+        DEBUG("assert_case_axioms "<< pp_case_expansion(e,m())
+              << " with " << e.m_def->get_cases().size() << " cases");
+        SASSERT(e.m_def->is_fun_defined());
+        context & ctx = get_context();
+        // 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`
+            app_ref pred_applied = apply_pred(c.get_pred(), e.m_args);
+            SASSERT(u().owns_app(pred_applied));
+            // substitute arguments in `path`
+            expr_ref_vector path(m());
+            for (auto & g : c.get_guards()) {
+                expr_ref g_applied = apply_args(vars, e.m_args, g);
+                path.push_back(g_applied);
+            }
+            // assert `p(args) <=> And(guards)` (with CNF on the fly)
+            ctx.internalize(pred_applied, false);
+            ctx.mark_as_relevant(ctx.get_bool_var(pred_applied));
+            literal concl = ctx.get_literal(pred_applied);
+            {
+                // assert `guards=>p(args)`
+                literal_vector c;
+                c.push_back(concl);
+                for (expr* g : path) {
+                    ctx.internalize(g, false);
+                    c.push_back(~ ctx.get_literal(g));
+                }
+
+                //TRACE("recfun", tout << "assert_case_axioms " << pp_case_expansion(e)
+                //    << " axiom " << mk_pp(*l) <<"\n";);
+                DEBUG("assert_case_axiom " << pp_lits(get_context(), path.size()+1, c.c_ptr()));
+                get_context().mk_th_axiom(get_id(), path.size()+1, c.c_ptr());
+            }
+            {
+                // assert `p(args) => guards[i]` for each `i`
+                for (expr * _g : path) {
+                    SASSERT(ctx.b_internalized(_g));
+                    literal g = ctx.get_literal(_g);
+                    literal c[2] = {~ concl, g};
+
+                    DEBUG("assert_case_axiom " << pp_lits(get_context(), 2, c));
+                    get_context().mk_th_axiom(get_id(), 2, c);
+                }
+            }
+
+            // 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);
+            }
+        }
+    }
+
+    void theory_recfun::assert_body_axiom(body_expansion & e) {
+        DEBUG("assert_body_axioms "<< pp_body_expansion(e,m()));
+        context & ctx = get_context();
+        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
+        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`
+        expr_ref_vector guards(m());
+        for (auto & g : e.m_cdef->get_guards()) {
+            expr_ref new_guard = apply_args(vars, args, g);
+            guards.push_back(new_guard);
+        }        
+        // now build the axiom `conds => lhs = rhs`
+        ctx.internalize(rhs, false);
+        for (auto& g : guards) ctx.internalize(g, false);
+        
+        // add unit clause `conds => lhs=rhs`
+        literal_vector clause;
+        for (auto& g : guards) {
+            ctx.internalize(g, false);
+            literal l = ~ ctx.get_literal(g);
+            ctx.mark_as_relevant(l);
+            clause.push_back(l);
+        }
+        literal l(mk_eq(lhs, rhs, true));
+        ctx.mark_as_relevant(l);
+        clause.push_back(l);
+        DEBUG("assert_body_axiom " << pp_lits(ctx, clause.size(), clause.c_ptr()));
+        ctx.mk_th_axiom(get_id(), clause.size(), clause.c_ptr());   
+    }
+    
+    final_check_status theory_recfun::final_check_eh() {
+        return FC_DONE;
+    }
+
+    void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) {
+        app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth());
+        DEBUG("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)))
+                return l_undef;
+        }
+        return l_false;
+    }
+
+    void theory_recfun::display(std::ostream & out) const {
+        out << "recfun{}";
+    }
+
+    void theory_recfun::collect_statistics(::statistics & st) const {
+        st.update("recfun macro expansion", m_stats.m_macro_expansions);
+        st.update("recfun case expansion", m_stats.m_case_expansions);
+        st.update("recfun body expansion", m_stats.m_body_expansions);
+    }
+
+#ifdef Z3DEBUG
+    std::ostream& operator<<(std::ostream & out, theory_recfun::pp_case_expansion const & e) {
+        return out << "case_exp(" << mk_pp(e.e.m_lhs, e.m) << ")";
+    }
+
+    std::ostream& operator<<(std::ostream & out, theory_recfun::pp_body_expansion const & e) {
+        out << "body_exp(" << e.e.m_cdef->get_name();
+        for (auto* t : e.e.m_args) {
+            out << " " << mk_pp(t,e.m);
+        }
+        return out << ")";
+    }
+#endif
+}
diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h
new file mode 100644
index 000000000..a1d9048c1
--- /dev/null
+++ b/src/smt/theory_recfun.h
@@ -0,0 +1,158 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    theory_recfun.h
+
+Abstract:
+
+    Theory responsible for unrolling recursive functions
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-10-31.
+
+Revision History:
+
+--*/
+#ifndef THEORY_RECFUN_H_
+#define THEORY_RECFUN_H_
+
+#include "smt/smt_theory.h"
+#include "smt/smt_context.h"
+#include "ast/ast_pp.h"
+#include "ast/recfun_decl_plugin.h"
+
+namespace smt {
+
+    class theory_recfun : public theory {
+        struct stats {
+            unsigned m_case_expansions, m_body_expansions, m_macro_expansions;
+            void reset() { memset(this, 0, sizeof(stats)); }
+            stats() { reset(); }
+        };
+
+        // one case-expansion of `f(t1…tn)`
+        struct case_expansion {
+            expr *              m_lhs; // the term to expand
+            recfun_def *        m_def;
+            ptr_vector<expr>    m_args;
+            case_expansion(recfun_util& u, app * n) : m_lhs(n), m_def(0), m_args()
+            {
+                SASSERT(u.is_defined(n));
+                func_decl * d = n->get_decl();
+                const symbol& name = d->get_name();
+                m_def = &u.get_def(name);
+                m_args.append(n->get_num_args(), n->get_args());
+            }
+            case_expansion(case_expansion const & from)
+                : m_lhs(from.m_lhs),
+                  m_def(from.m_def),
+                  m_args(from.m_args) {}
+            case_expansion(case_expansion && from)
+                : m_lhs(from.m_lhs),
+                  m_def(from.m_def),
+                  m_args(std::move(from.m_args)) {}
+        };
+
+        struct pp_case_expansion {
+            case_expansion & e;
+            ast_manager & m;
+            pp_case_expansion(case_expansion & e, ast_manager & m) : e(e), m(m) {}
+        };
+
+        friend std::ostream& operator<<(std::ostream&, pp_case_expansion const &);
+
+        // 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));
+            }
+            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) {}
+            body_expansion(body_expansion && from) : m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {}
+        };
+
+        struct pp_body_expansion {
+            body_expansion & e;
+            ast_manager & m;
+            pp_body_expansion(body_expansion & e, ast_manager & m) : e(e), m(m) {}
+        };
+
+        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;
+
+        recfun_decl_plugin& m_plugin;
+        recfun_util&        m_util;
+        stats               m_stats;
+        th_trail_stack      m_trail;
+        guard_set           m_guards; // true case-preds
+        unsigned            m_max_depth; // for fairness and termination
+
+        vector<case_expansion>      m_q_case_expand;
+        vector<body_expansion>      m_q_body_expand;
+        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); }
+
+        bool is_defined(enode * e) const { return is_defined(e->get_owner()); }
+        bool is_case_pred(enode * e) const { return is_case_pred(e->get_owner()); }
+
+        void reset_queues();
+        expr_ref apply_args(recfun::vars const & vars, ptr_vector<expr> const & args, expr * e); //!< substitute variables by args
+        app_ref apply_pred(recfun::case_pred const & p, ptr_vector<expr> const & args); //<! apply predicate to args
+        void assert_macro_axiom(case_expansion & e);
+        void assert_case_axioms(case_expansion & e);
+        void assert_body_axiom(body_expansion & e);
+        void max_depth_conflict(void);
+    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); }
+
+        bool internalize_atom(app * atom, bool gate_ctx) override;
+        bool internalize_term(app * term) override;
+        void reset_eh() override;
+        void relevant_eh(app * n) override;
+        char const * get_name() const override;
+        final_check_status final_check_eh() override;
+        void assign_eh(bool_var v, bool is_true) override;
+        void push_scope_eh() override;
+        void pop_scope_eh(unsigned num_scopes) override;
+        void restart_eh() override;
+        bool can_propagate() override;
+        void propagate() override;
+        lbool validate_unsat_core(expr_ref_vector &) override;
+
+        void new_eq_eh(theory_var v1, theory_var v2) override {}
+        void new_diseq_eh(theory_var v1, theory_var v2) override {}
+        void add_theory_assumptions(expr_ref_vector & assumptions) override;
+
+    public:
+        theory_recfun(ast_manager & m);
+        virtual ~theory_recfun() override;
+        void setup_params(); // read parameters
+        virtual theory * mk_fresh(context * new_ctx) override;
+        virtual void display(std::ostream & out) const override;
+        virtual void collect_statistics(::statistics & st) const override;
+        unsigned get_max_depth() const { return m_max_depth; }
+        void set_max_depth(unsigned n) { SASSERT(n>0); m_max_depth = n; }
+    };
+}
+
+#endif
diff --git a/src/util/scoped_ptr_vector.h b/src/util/scoped_ptr_vector.h
index 920ecb2c9..52272389a 100644
--- a/src/util/scoped_ptr_vector.h
+++ b/src/util/scoped_ptr_vector.h
@@ -31,6 +31,7 @@ public:
     void reset() { std::for_each(m_vector.begin(), m_vector.end(), delete_proc<T>()); m_vector.reset(); }
     void push_back(T * ptr) { m_vector.push_back(ptr); }
     void pop_back() { SASSERT(!empty()); set(size()-1, nullptr); m_vector.pop_back(); }
+    T * back() const { return m_vector.back(); }
     T * operator[](unsigned idx) const { return m_vector[idx]; }
     void set(unsigned idx, T * ptr) { 
         if (m_vector[idx] == ptr) 
@@ -51,6 +52,13 @@ public:
                 push_back(nullptr);
         }
     }
+    //!< swap last element with given pointer
+    void swap_back(scoped_ptr<T> & ptr) {
+        SASSERT(!empty());
+        T * tmp = ptr.detach();
+        ptr = m_vector.back();
+        m_vector[m_vector.size()-1] = tmp;
+    }
 };
 
 #endif
diff --git a/src/util/trail.h b/src/util/trail.h
index b9f4602c7..fadafe724 100644
--- a/src/util/trail.h
+++ b/src/util/trail.h
@@ -143,6 +143,17 @@ public:
 };
 
 
+template<typename Ctx, typename M, typename Mgr, typename D>
+class insert_ref_map : public trail<Ctx> {
+    Mgr&          m;
+    M&            m_map;
+    D             m_obj;
+public:
+    insert_ref_map(Mgr& m, M& t, D o) : m(m), m_map(t), m_obj(o) {}
+    virtual ~insert_ref_map() {}
+    virtual void undo(Ctx & ctx) { m_map.remove(m_obj); m.dec_ref(m_obj); }
+};
+
 
 template<typename Ctx, typename V>
 class push_back_vector : public trail<Ctx> {