diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index eb18c5262..cdc1df6be 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -326,6 +326,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     m_manager(m),
     m_own_manager(m == 0),
     m_manager_initialized(false),
+    m_rec_fun_declared(false),
     m_pmanager(0),
     m_sexpr_manager(0),
     m_regular("stdout", std::cout),
@@ -830,14 +831,18 @@ void cmd_context::insert(symbol const & s, object_ref * r) {
 }
 
 void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* e) {
-    expr_ref eq(m()), lhs(m());
+    expr_ref eq(m());
+    app_ref lhs(m());
     lhs = m().mk_app(f, binding.size(), binding.c_ptr());
     eq  = m().mk_eq(lhs, e);
     if (!ids.empty()) {
-        eq  = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq);
+        expr* pat = m().mk_pattern(lhs);
+        eq  = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, symbol(":rec-fun"), symbol::null, 1, &pat);
+    }
+    if (!ids.empty() && !m_rec_fun_declared) {
+        warning_msg("recursive functions are currently only partially supported: they are translated into recursive equations without special handling");
+        m_rec_fun_declared = true;
     }
-    warning_msg("recursive functions are currently only partially supported: they are translated into recursive equations without special handling");
-    // TBD: basic implementation asserts axiom. Life-time of recursive equation follows scopes (unlikely to be what SMT-LIB 2.5 wants).
     assert_expr(eq);
 }
 
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 833977a1c..865999042 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -165,6 +165,7 @@ protected:
     ast_manager *                m_manager;
     bool                         m_own_manager;
     bool                         m_manager_initialized;
+    bool                         m_rec_fun_declared;
     pdecl_manager *              m_pmanager;
     sexpr_manager *              m_sexpr_manager;
     check_logic                  m_check_logic;
diff --git a/src/math/automata/symbolic_automata.h b/src/math/automata/symbolic_automata.h
index cd553eeef..cc3a0f5a8 100644
--- a/src/math/automata/symbolic_automata.h
+++ b/src/math/automata/symbolic_automata.h
@@ -34,6 +34,9 @@ class symbolic_automata {
     typedef vector<move_t>     moves_t;
     typedef obj_ref<T, M>      ref_t;
     typedef ref_vector<T, M>   refs_t;
+    typedef std::pair<unsigned, unsigned> unsigned_pair;
+    template<class V> class u2_map : public map<unsigned_pair, V, pair_hash<unsigned_hash, unsigned_hash>, default_eq<unsigned_pair> > {};
+
 
     M&    m;
     ba_t& m_ba;
diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h
index 50c115d39..2df5275c2 100644
--- a/src/math/automata/symbolic_automata_def.h
+++ b/src/math/automata/symbolic_automata_def.h
@@ -25,7 +25,6 @@ Revision History:
 #include "symbolic_automata.h"
 #include "hashtable.h"
 
-typedef std::pair<unsigned, unsigned> unsigned_pair;
 
 
 
@@ -234,7 +233,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
     unsigned new_init = pblocks[blocks[a.init()]].get_representative();
 
     // set moves
-    map<unsigned_pair, T*, pair_hash<unsigned_hash, unsigned_hash>, default_eq<unsigned_pair> > conds;
+    u2_map<T*> conds;
     svector<unsigned_pair> keys;
     moves_t new_moves;
 
@@ -276,25 +275,22 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
 
 template<class T, class M>
 typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_product(automaton_t& a, automaton_t& b) {
-    map<unsigned_pair, unsigned, pair_hash<unsigned_hash, unsigned_hash>, default_eq<unsigned_pair> > state_ids;
+    u2_map<unsigned> pair2id;
     unsigned_pair init_pair(a.init(), b.init());
     svector<unsigned_pair> todo;
     todo.push_back(init_pair);
-    state_ids.insert(init_pair, 0);
+    pair2id.insert(init_pair, 0);
     moves_t mvs;
     unsigned_vector final;
     if (a.is_final_state(a.init()) && b.is_final_state(b.init())) {
         final.push_back(0);
     }
-    if (false) {
-        mk_minimize(a);
-    }
     unsigned n = 1;
     moves_t mvsA, mvsB;
     while (!todo.empty()) {
         unsigned_pair curr_pair = todo.back();
         todo.pop_back();
-        unsigned src = state_ids[curr_pair];
+        unsigned src = pair2id[curr_pair];
         mvsA.reset(); mvsB.reset();
         a.get_moves_from(curr_pair.first,  mvsA, true);
         b.get_moves_from(curr_pair.second, mvsB, true);
@@ -310,9 +306,9 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_produ
                 }
                 unsigned_pair tgt_pair(mvsA[i].dst(), mvsB[j].dst());
                 unsigned tgt;
-                if (!state_ids.find(tgt_pair, tgt)) {
+                if (!pair2id.find(tgt_pair, tgt)) {
                     tgt = n++;
-                    state_ids.insert(tgt_pair, tgt);
+                    pair2id.insert(tgt_pair, tgt);
                     todo.push_back(tgt_pair);
                     if (a.is_final_state(tgt_pair.first) && b.is_final_state(tgt_pair.second)) {
                         final.push_back(tgt);
@@ -366,6 +362,130 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_produ
     }
 } 
 
+#if 0
+template<class T, class M>
+unsigned symbolic_automata<T, M>::get_product_state_id(u2_map<unsigned>& pair2id, unsigned_pair const& p, unsigned& id) {
+    unsigned result = 0;
+    if (!pair2id.find(p, result)) {
+        result = id++;
+        pair2id.insert(p, result);
+    }
+    return result;
+}
+#endif
 
+template<class T, class M>
+typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_difference(automaton_t& a, automaton_t& b) {
+#if 0
+    map<uint_set, unsigned, uint_set_hash, uint_set_eq> bs2id;   // set of b-states to unique id
+    vector<uintset> id2bs;                                       // unique id to set of b-states
+    u2_map<unsigned> pair2id;                                    // pair of states to new state id
+    unsigned sink_state = UINT_MAX;
+    uint_set bset;
+    moves_t new_moves;                                           // moves in the resulting automaton
+    unsigned_vector new_final_states;                            // new final states
+    unsigned p_state_id = 0;                                     // next state identifier
+    bs2id.insert(uint_set(), sink_state);                        // the sink state has no b-states
+    bset.insert(b.init());                                       // the initial state has a single initial b state
+    bs2id.insert(bset, 0);                                       // the index to the initial b state is 0
+    id2bs.push_back(bset);
+    if (!b.is_final_state(b.init()) && a.is_final_state(a.init())) {
+        new_final_states.push_back(p_state_id);
+    }
+
+    svector<unsigned_pair> todo;
+    unsigned_pair state(a.init(), 0);
+    todo.push_back(state);
+    pair2id.insert(state, p_state_id++);
+
+    // or just make todo a vector whose indices coincide with state_id.
+    while (!todo.empty()) {
+        state = todo.back();
+        unsigned state_id = pair2id[state];
+        todo.pop_back();
+        mvsA.reset();
+        a.get_moves_from(state.first, mvsA, true);
+        if (state.second == sink_state) {
+            for (unsigned i = 0; i < mvsA.size(); ++i) {
+                unsigned_pair dst(mvsA[i].dst(), sink_state);
+                bool is_new = !pair2id.contains(dst);
+                unsigned dst_id = get_product_state_id(pair2id, dst, p_state_id);
+                new_moves.push_back(move_t(m, state_id, dst_id, mvsA[i].t()));
+                if (is_new && a.is_final_state(mvsA[i].dst())) {
+                    new_final_states.push_back(dst_id);
+                    todo.push_back(dst);
+                }
+            }
+        }
+        else {
+            get_moves_from(b, id2bs[state.second], mvsB);
+            generate_min_terms(mvsB, min_terms);
+            for (unsigned j = 0; j < min_terms.size(); ++j) {
+                for (unsigned i = 0; i < mvsA.size(); ++i) {
+                    ref_t cond(m_ba.mk_and(mvsA[i].t(), min_terms[j].second), m);
+                    switch (m_ba.is_sat(cond)) {
+                    case l_false:
+                        break;
+                    case l_true:
+                        ab_combinations.push_back(ab_comb(i, min_terms[j].first, cond));
+                        break;
+                    case l_undef:
+                        return 0;
+                    }
+                }
+            }
+
+            for (unsigned i = 0; i < ab_combinations.size(); ++i) {
+                move_t const& mvA = mvsA[ab_combinations[i].A];
+                bset.reset();
+                bool is_final = a.is_final_state(mvA.dst());
+                for (unsigned j = 0; j < mvsB.size(); ++j) {
+                    if (ab_combinations[i].B[j]) {
+                        bset.insert(mvsB[j].dst());
+                        is_final &= !b.is_final_state(mvsB[j].dst());
+                    }
+                }
+                unsigned new_b;
+                if (bset.empty()) {
+                    new_b = sink_state;
+                }
+                else if (!bs2id.find(bset, new_b)) {
+                    new_b = id2bs.size();
+                    id2bs.push_back(bset);
+                    bs2id.insert(bset, new_b);
+                }
+                unsigned_pair dst(mvA.dst(), new_b);
+                bool is_new = !pair2id.contains(dst);
+                dst_id = get_product_state_id(pair2id, dst, p_state_id);
+                move_t new_move(m, state_id, dst_id, ab_combinations[i].cond);
+                new_moves.push_back(new_move);
+                if (is_new) {
+                    if (is_final) {
+                        new_final_states.push_back(dst_id);
+                    }
+                    todo.push_back(dst);
+                }   
+            }
+        }
+    }
+    
+    
+    if (new_final_states.empty()) {
+        return alloc(automaton_t, m);
+    }
+
+    automaton_t* result = alloc(automaton_t, m, 0, new_final_states, new_moves); 
+
+#if 0
+    result->isEpsilonFree = true;
+    if (A.IsDeterministic)
+        result->isDeterministic = true;    
+    result->EliminateDeadStates();
+#endif
+    return result;
+
+#endif
+    return 0;
+}
 
 #endif 
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index b294bf4c9..d67b6a3eb 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -31,7 +31,7 @@ Revision History:
 namespace smt {
 
     model_checker::model_checker(ast_manager & m, qi_params const & p, model_finder & mf):
-        m_manager(m),
+        m(m),
         m_params(p),
         m_qm(0),
         m_context(0),
@@ -93,9 +93,9 @@ namespace smt {
         obj_hashtable<expr>::iterator end = universe.end();
         for (; it != end; ++it) {
             expr * e = *it;
-            eqs.push_back(m_manager.mk_eq(sk, e));
+            eqs.push_back(m.mk_eq(sk, e));
         }
-        m_aux_context->assert_expr(m_manager.mk_or(eqs.size(), eqs.c_ptr()));
+        m_aux_context->assert_expr(m.mk_or(eqs.size(), eqs.c_ptr()));
     }
 
 #define PP_DEPTH 8
@@ -106,16 +106,16 @@ namespace smt {
        The variables are replaced by skolem constants. These constants are stored in sks.
     */
     void model_checker::assert_neg_q_m(quantifier * q, expr_ref_vector & sks) {
-        expr_ref tmp(m_manager);
+        expr_ref tmp(m);
         m_curr_model->eval(q->get_expr(), tmp, true);
-        TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m_manager) << "\n";);        
+        TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);        
         ptr_buffer<expr> subst_args;
         unsigned num_decls = q->get_num_decls();
         subst_args.resize(num_decls, 0);
         sks.resize(num_decls, 0);
         for (unsigned i = 0; i < num_decls; i++) {
             sort * s  = q->get_decl_sort(num_decls - i - 1);
-            expr * sk = m_manager.mk_fresh_const(0, s);
+            expr * sk = m.mk_fresh_const(0, s);
             sks[num_decls - i - 1]        = sk;
             subst_args[num_decls - i - 1] = sk;
             if (m_curr_model->is_finite(s)) {
@@ -123,12 +123,12 @@ namespace smt {
             }
         }
 
-        expr_ref sk_body(m_manager);
-        var_subst s(m_manager);
+        expr_ref sk_body(m);
+        var_subst s(m);
         s(tmp, subst_args.size(), subst_args.c_ptr(), sk_body);
-        expr_ref r(m_manager);
-        r = m_manager.mk_not(sk_body);
-        TRACE("model_checker", tout << "mk_neg_q_m:\n" << mk_ismt2_pp(r, m_manager) << "\n";);
+        expr_ref r(m);
+        r = m.mk_not(sk_body);
+        TRACE("model_checker", tout << "mk_neg_q_m:\n" << mk_ismt2_pp(r, m) << "\n";);
         m_aux_context->assert_expr(r);
     }
 
@@ -138,13 +138,13 @@ namespace smt {
         unsigned num_decls = q->get_num_decls();
         // Remark: sks were created for the flat version of q.
         SASSERT(sks.size() >= num_decls);
-        expr_ref_buffer bindings(m_manager);
+        expr_ref_vector bindings(m);
         bindings.resize(num_decls);
         unsigned max_generation = 0;
         for (unsigned i = 0; i < num_decls; i++) {
             expr * sk = sks.get(num_decls - i - 1);
             func_decl * sk_d = to_app(sk)->get_decl();
-            expr_ref sk_value(m_manager);
+            expr_ref sk_value(m);
             sk_value  = cex->get_const_interp(sk_d);
             if (sk_value == 0) {
                 sk_value = cex->get_some_value(sk_d->get_range());
@@ -155,7 +155,7 @@ namespace smt {
                 unsigned sk_term_gen;
                 expr * sk_term = m_model_finder.get_inv(q, i, sk_value, sk_term_gen);
                 if (sk_term != 0) {
-                    SASSERT(!m_manager.is_model_value(sk_term));
+                    SASSERT(!m.is_model_value(sk_term));
                     if (sk_term_gen > max_generation)
                         max_generation = sk_term_gen;
                     sk_value = sk_term;
@@ -177,27 +177,30 @@ namespace smt {
         
         TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: ";
               for (unsigned i = 0; i < num_decls; i++) {
-                  tout << mk_ismt2_pp(bindings[i], m_manager) << " ";
+                  tout << mk_ismt2_pp(bindings[i].get(), m) << " ";
               }
               tout << "\n";);
         
-        for (unsigned i = 0; i < num_decls; i++) 
+        add_instance(q, bindings, max_generation);
+        return true;
+    }
+
+    void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) {
+        for (unsigned i = 0; i < bindings.size(); i++) 
             m_new_instances_bindings.push_back(bindings[i]);
         void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls()));
         instance * new_inst = new (mem) instance(q, bindings.c_ptr(), max_generation);
         m_new_instances.push_back(new_inst);
-
-        return true;
     }
 
     void model_checker::operator()(expr *n) {
-        if (m_manager.is_model_value(n)) {
+        if (m.is_model_value(n)) {
             throw is_model_value();
         }
     }
 
     bool model_checker::contains_model_value(expr* n) {
-        if (m_manager.is_model_value(n)) {
+        if (m.is_model_value(n)) {
             return true;
         }
         if (is_app(n) && to_app(n)->get_num_args() == 0) {
@@ -217,22 +220,22 @@ namespace smt {
     bool model_checker::add_blocking_clause(model * cex, expr_ref_vector & sks) {
         SASSERT(cex != 0);
         unsigned num_sks  = sks.size();
-        expr_ref_buffer diseqs(m_manager);
+        expr_ref_buffer diseqs(m);
         for (unsigned i = 0; i < num_sks; i++) {
             expr * sk        = sks.get(i);
             func_decl * sk_d = to_app(sk)->get_decl();
-            expr_ref sk_value(m_manager);
+            expr_ref sk_value(m);
             sk_value  = cex->get_const_interp(sk_d);
             if (sk_value == 0) {
                 sk_value = cex->get_some_value(sk_d->get_range());
                 if (sk_value == 0)
                     return false; // get_some_value failed... aborting add_blocking_clause
             }
-            diseqs.push_back(m_manager.mk_not(m_manager.mk_eq(sk, sk_value)));
+            diseqs.push_back(m.mk_not(m.mk_eq(sk, sk_value)));
         }
-        expr_ref blocking_clause(m_manager);
-        blocking_clause = m_manager.mk_or(diseqs.size(), diseqs.c_ptr());
-        TRACE("model_checker", tout << "blocking clause:\n" << mk_ismt2_pp(blocking_clause, m_manager) << "\n";);
+        expr_ref blocking_clause(m);
+        blocking_clause = m.mk_or(diseqs.size(), diseqs.c_ptr());
+        TRACE("model_checker", tout << "blocking clause:\n" << mk_ismt2_pp(blocking_clause, m) << "\n";);
         m_aux_context->assert_expr(blocking_clause);
         return true;
     }
@@ -245,15 +248,15 @@ namespace smt {
         m_aux_context->push();
         
         quantifier * flat_q = get_flat_quantifier(q);
-        TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m_manager) << "\n" << 
-              mk_ismt2_pp(flat_q->get_expr(), m_manager) << "\n";);
-        expr_ref_vector sks(m_manager);
+        TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << 
+              mk_ismt2_pp(flat_q->get_expr(), m) << "\n";);
+        expr_ref_vector sks(m);
 
         assert_neg_q_m(flat_q, sks);
         TRACE("model_checker", tout << "skolems:\n"; 
               for (unsigned i = 0; i < sks.size(); i++) {
                   expr * sk = sks.get(i);
-                  tout << mk_ismt2_pp(sk, m_manager) << " " << mk_pp(m_manager.get_sort(sk), m_manager) << "\n";
+                  tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n";
               });
         
         lbool r = m_aux_context->check();
@@ -301,6 +304,43 @@ namespace smt {
         return false;
     }
 
+    bool model_checker::check_rec_fun(quantifier* q) {
+        TRACE("model_checker", tout << mk_pp(q, m) << "\n";);
+        SASSERT(q->get_num_patterns() == 1);
+        expr* fn = to_app(q->get_pattern(0))->get_arg(0);
+        SASSERT(is_app(fn));
+        func_decl* f = to_app(fn)->get_decl();
+        enode_vector::const_iterator it  = m_context->begin_enodes_of(f);
+        enode_vector::const_iterator end = m_context->end_enodes_of(f);
+
+        bool is_undef = false;
+        expr_ref_vector args(m);
+        unsigned num_decls = q->get_num_decls();
+        args.resize(num_decls, 0);
+        var_subst sub(m);
+        expr_ref tmp(m), result(m);
+        for (; it != end; ++it) {
+            if (m_context->is_relevant(*it)) {
+                app* e = (*it)->get_owner();
+                for (unsigned i = 0; i < e->get_num_args(); ++i) {
+                    args[num_decls - i - 1] = e->get_arg(i);
+                }
+                sub(q->get_expr(), num_decls, args.c_ptr(), tmp);
+                m_curr_model->eval(tmp, result, true);
+                if (m.is_true(result)) {
+                    continue;
+                }
+                if (m.is_false(result)) {
+                    add_instance(q, args, 0);
+                    return false;
+                }
+                TRACE("model_checker", tout << tmp << "evaluates to undetermined " << result << "\n";);
+                is_undef = true;
+            }
+        }
+        return !is_undef;
+    }
+
     void model_checker::init_aux_context() {
         if (!m_fparams) {
             m_fparams = alloc(smt_params, m_context->get_fparams());
@@ -347,7 +387,7 @@ namespace smt {
             quantifier * q = *it;
 	    if(!m_qm->mbqi_enabled(q)) continue;
             TRACE("model_checker", 
-                  tout << "Check: " << mk_pp(q, m_manager) << "\n";
+                  tout << "Check: " << mk_pp(q, m) << "\n";
                   tout << m_context->get_assignment(q) << "\n";);
 
             if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) {
@@ -355,7 +395,12 @@ namespace smt {
                     verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";
                 }
                 found_relevant = true;
-                if (!check(q)) {
+                if (q->get_qid() == symbol(":rec-fun")) {
+                    if (!check_rec_fun(q)) {
+                        num_failures++;
+                    }
+                }
+                else if (!check(q)) {
                     if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
                         verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n";
                     }
@@ -425,22 +470,22 @@ namespace smt {
                 for (unsigned i = 0; i < num_decls; i++) {
                     expr * b = inst->m_bindings[i];
                     if (!m_context->e_internalized(b)) {
-                        TRACE("model_checker_bug_detail", tout << "internalizing b:\n" << mk_pp(b, m_manager) << "\n";);
+                        TRACE("model_checker_bug_detail", tout << "internalizing b:\n" << mk_pp(b, m) << "\n";);
                         m_context->internalize(b, false, gen);
                     }
                     bindings.push_back(m_context->get_enode(b));
                 }
-                TRACE("model_checker_bug_detail", tout << "instantiating... q:\n" << mk_pp(q, m_manager) << "\n";
+                TRACE("model_checker_bug_detail", tout << "instantiating... q:\n" << mk_pp(q, m) << "\n";
                       tout << "inconsistent: " << m_context->inconsistent() << "\n";
                       tout << "bindings:\n";
                       for (unsigned i = 0; i < num_decls; i++) {
                           expr * b = inst->m_bindings[i];
-                          tout << mk_pp(b, m_manager) << "\n";
+                          tout << mk_pp(b, m) << "\n";
                       });
                 TRACE("model_checker_instance", 
-                      expr_ref inst_expr(m_manager);
-                      instantiate(m_manager, q, inst->m_bindings, inst_expr);
-                      tout << "(assert " << mk_ismt2_pp(inst_expr, m_manager) << ")\n";);
+                      expr_ref inst_expr(m);
+                      instantiate(m, q, inst->m_bindings, inst_expr);
+                      tout << "(assert " << mk_ismt2_pp(inst_expr, m) << ")\n";);
                 m_context->add_instance(q, 0, num_decls, bindings.c_ptr(), gen, gen, gen, dummy);
                 TRACE("model_checker_bug_detail", tout << "after instantiating, inconsistent: " << m_context->inconsistent() << "\n";);
             }
diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h
index 2b8f1aa4d..b94ddb6bb 100644
--- a/src/smt/smt_model_checker.h
+++ b/src/smt/smt_model_checker.h
@@ -37,7 +37,7 @@ namespace smt {
     class quantifier_manager;
 
     class model_checker {
-        ast_manager &                               m_manager;
+        ast_manager &                               m; // _manager;
         qi_params const &                           m_params;
         // copy of smt_params for auxiliary context. 
         // the idea is to use a different configuration for the aux context (e.g., disable relevancy)
@@ -59,7 +59,8 @@ namespace smt {
         void assert_neg_q_m(quantifier * q, expr_ref_vector & sks);
         bool add_blocking_clause(model * cex, expr_ref_vector & sks);
         bool check(quantifier * q);
-        
+        bool check_rec_fun(quantifier* q);
+
         struct instance {
             quantifier * m_q;
             unsigned     m_generation;
@@ -82,6 +83,7 @@ namespace smt {
         struct is_model_value {};
         expr_mark m_visited;
         bool contains_model_value(expr* e);
+        void add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation);
 
     public:
         model_checker(ast_manager & m, qi_params const & p, model_finder & mf);
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index e06480bc5..0501714ee 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -40,6 +40,7 @@ namespace smt {
         ptr_vector<quantifier>                 m_quantifiers;
         scoped_ptr<quantifier_manager_plugin>  m_plugin;
         unsigned                               m_num_instances;
+        symbol                                 m_rec_fun;
         
         imp(quantifier_manager & wrapper, context & ctx, smt_params & p, quantifier_manager_plugin * plugin):
             m_wrapper(wrapper),
@@ -47,7 +48,8 @@ namespace smt {
             m_params(p),
             m_qi_queue(m_wrapper, ctx, p),
             m_qstat_gen(ctx.get_manager(), ctx.get_region()),
-            m_plugin(plugin) {
+            m_plugin(plugin),
+            m_rec_fun(":rec-fun") {
             m_num_instances = 0;
             m_qi_queue.setup();
         }
@@ -184,6 +186,10 @@ namespace smt {
             m_qi_queue.instantiate();
         }
         
+        bool check_quantifier(quantifier* q) {
+            return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // TBD: && q->get_qid() != m_rec_fun;
+        }
+
         bool quick_check_quantifiers() {
             if (m_params.m_qi_quick_checker == MC_NO)
                 return true;
@@ -195,7 +201,7 @@ namespace smt {
             ptr_vector<quantifier>::const_iterator it  = m_quantifiers.begin();
             ptr_vector<quantifier>::const_iterator end = m_quantifiers.end();
             for (; it != end; ++it)
-                if (m_context.is_relevant(*it) && m_context.get_assignment(*it) == l_true && mc.instantiate_unsat(*it))
+                if (check_quantifier(*it) && mc.instantiate_unsat(*it))
                     result = false;
             if (m_params.m_qi_quick_checker == MC_UNSAT || !result) {
                 m_qi_queue.instantiate();
@@ -206,7 +212,7 @@ namespace smt {
             IF_VERBOSE(10, verbose_stream() << "quick checking quantifiers (not sat)...\n";);
             it  = m_quantifiers.begin();
             for (; it != end; ++it)
-                if (m_context.is_relevant(*it) && m_context.get_assignment(*it) == l_true && mc.instantiate_not_sat(*it))
+                if (check_quantifier(*it) && mc.instantiate_not_sat(*it))
                     result = false;
             m_qi_queue.instantiate();
             return result;
diff --git a/src/test/expr_rand.cpp b/src/test/expr_rand.cpp
index 972c6e242..96d21a44c 100644
--- a/src/test/expr_rand.cpp
+++ b/src/test/expr_rand.cpp
@@ -38,7 +38,7 @@ void tst_expr_arith(unsigned num_files) {
         er.get_next(m.mk_bool_sort(), e);
         ast_smt_pp pp(m);
 
-        pp.set_logic("QF_AUFLIA");
+        pp.set_logic(symbol("QF_AUFLIA"));
         std::ostringstream buffer;
         buffer << "random_arith_" << i << ".smt";
         std::cout << buffer.str() << "\n";
@@ -81,7 +81,7 @@ void tst_expr_rand(unsigned num_files) {
         er.get_next(m.mk_bool_sort(), e);
         ast_smt_pp pp(m);
 
-        pp.set_logic("QF_AUFBV");
+        pp.set_logic(symbol("QF_AUFBV"));
         std::ostringstream buffer;
         buffer << "random_bv_" << i << ".smt";
         std::cout << buffer.str() << "\n";