diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index d8eea758f..b5a19569a 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1192,7 +1192,6 @@ namespace smt {
 
         bool more_than_k_unassigned_literals(clause * cls, unsigned k);
 
-        void internalize_assertions();
 
         void asserted_inconsistent();
 
@@ -1609,6 +1608,8 @@ namespace smt {
 
         void assert_expr(expr * e, proof * pr);
 
+        void internalize_assertions();
+
         void push();
 
         void pop(unsigned num_scopes);
diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp
index a54a287ec..49f05b019 100644
--- a/src/smt/smt_enode.cpp
+++ b/src/smt/smt_enode.cpp
@@ -50,7 +50,7 @@ namespace smt {
         n->m_lbl_hash         = -1;
         n->m_proof_is_logged = false;
         unsigned num_args     = n->get_num_args();
-        for (unsigned i = 0; i < num_args; i++) {
+        for (unsigned i = 0; i < num_args; i++) {            
             enode * arg  = app2enode[owner->get_arg(i)->get_id()];
             n->m_args[i] = arg;
             SASSERT(n->get_arg(i) == arg);
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 80b3b5062..765513823 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -297,7 +297,7 @@ namespace smt {
         TRACE("datatype", tout << "internalizing term:\n" << mk_pp(term, m) << "\n";);
         unsigned num_args = term->get_num_args();
         for (unsigned i = 0; i < num_args; i++)
-            ctx.internalize(term->get_arg(i), false);
+            ctx.internalize(term->get_arg(i), has_quantifiers(term));
         // the internalization of the arguments may trigger the internalization of term.
         if (ctx.e_internalized(term))
             return true;
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index e21eb2bc5..1a2bf0049 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -246,18 +246,22 @@ namespace smt {
 
     literal theory_recfun::mk_eq_lit(expr* l, expr* r) {
         literal lit;
-        if (m.is_true(r) || m.is_false(r)) {
-            std::swap(l, r);
-        }
-        if (m.is_true(l)) {
-            lit = mk_literal(r);
-        }
-        else if (m.is_false(l)) {
-            lit = ~mk_literal(r);
-        }
-        else {
-            lit = mk_eq(l, r, false);        
+        if (has_quantifiers(l) || has_quantifiers(r)) {
+            expr_ref eq1(m.mk_eq(l, r), m);
+            expr_ref fn(m.mk_fresh_const("rec-eq", m.mk_bool_sort()), m);
+            expr_ref eq(m.mk_eq(fn, eq1), m);
+            ctx.assert_expr(eq);
+            ctx.internalize_assertions();
+            lit = mk_literal(fn);
         }
+        else if (m.is_true(r) || m.is_false(r)) 
+            std::swap(l, r);        
+        else if (m.is_true(l)) 
+            lit = mk_literal(r);        
+        else if (m.is_false(l)) 
+            lit = ~mk_literal(r);        
+        else 
+            lit = mk_eq(l, r, false);                
         ctx.mark_as_relevant(lit);
         return lit;
     }
@@ -282,14 +286,12 @@ namespace smt {
         auto & vars = e.m_def->get_vars();
         expr_ref lhs(e.m_lhs, m);
         unsigned depth = get_depth(e.m_lhs);
-        expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m);	
+        expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m);
         literal lit = mk_eq_lit(lhs, rhs);
         std::function<literal(void)> fn = [&]() { return lit; };
         scoped_trace_stream _tr(*this, fn);
         ctx.mk_th_axiom(get_id(), 1, &lit);
         TRACEFN("macro expansion yields " << pp_lit(ctx, lit));
-	    if (has_quantifiers(rhs))
-	        throw default_exception("quantified formulas in recursive functions are not supported");
     }
 
     /**
@@ -377,6 +379,13 @@ namespace smt {
         unsigned depth = get_depth(e.m_pred);
         expr_ref lhs(u().mk_fun_defined(d, args), m);
         expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs());
+        if (has_quantifiers(rhs)) {
+            expr_ref fn(m.mk_fresh_const("rec-eq", m.mk_bool_sort()), m);
+            expr_ref eq(m.mk_eq(fn, rhs), m);
+            ctx.assert_expr(eq);
+            ctx.internalize_assertions();
+            rhs = fn;
+        }
         literal_vector clause;
         for (auto & g : e.m_cdef->get_guards()) {
             expr_ref guard = apply_args(depth, vars, args, g);
@@ -394,8 +403,6 @@ namespace smt {
         std::function<literal_vector(void)> fn = [&]() { return clause; };
         scoped_trace_stream _tr(*this, fn);
         ctx.mk_th_axiom(get_id(), clause);
-        if (has_quantifiers(rhs))
-            throw default_exception("quantified formulas in recursive functions are not supported");
     }
     
     final_check_status theory_recfun::final_check_eh() {