diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 007751220..923f5ae49 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -154,6 +154,8 @@ namespace sat {
         if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution)
             return;
 
+        // solver::scoped_disable_checkpoint _scoped_disable_checkpoint(s);
+        
         initialize();
 
         CASSERT("sat_solver", s.check_invariant());
@@ -167,7 +169,6 @@ namespace sat {
         CASSERT("sat_solver", s.check_invariant());
         m_need_cleanup = false;
         m_use_list.init(s.num_vars());
-        init_visited();
         m_learned_in_use_lists = false;
         if (learned) {
             register_clauses(s.m_learned);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 9c858a29a..08c70fba5 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -33,6 +33,7 @@ namespace sat {
 
     solver::solver(params_ref const & p, reslimit& l, extension * ext):
         m_rlimit(l),
+        m_checkpoint_enabled(true),
         m_config(p),
         m_ext(ext),
         m_par(0),
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 6c91565aa..42291609d 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -72,6 +72,7 @@ namespace sat {
         struct abort_solver {};
     protected:
         reslimit&               m_rlimit;
+        bool                    m_checkpoint_enabled;
         config                  m_config;
         stats                   m_stats;
         extension *             m_ext;
@@ -214,6 +215,16 @@ namespace sat {
                 }
             }
         };
+        class scoped_disable_checkpoint {
+            solver& s;
+        public:
+            scoped_disable_checkpoint(solver& s): s(s) {
+                s.m_checkpoint_enabled = false;
+            }            
+            ~scoped_disable_checkpoint() {
+                s.m_checkpoint_enabled = true;
+            }
+        };
         unsigned select_watch_lit(clause const & cls, unsigned starting_at) const;
         unsigned select_learned_watch_lit(clause const & cls) const;
         bool simplify_clause(unsigned & num_lits, literal * lits) const;
@@ -257,6 +268,7 @@ namespace sat {
         lbool status(clause const & c) const;        
         clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
         void checkpoint() {
+            if (!m_checkpoint_enabled) return;
             if (!m_rlimit.inc()) {
                 m_mc.reset();
                 m_model_is_current = false;
diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index 7d009a037..f63e07b57 100644
--- a/src/smt/smt_context_inv.cpp
+++ b/src/smt/smt_context_inv.cpp
@@ -433,6 +433,9 @@ namespace smt {
             if (!is_ground(n)) {
                 continue;
             }
+            if (is_quantifier(n) && m.is_rec_fun_def(to_quantifier(n))) {
+                continue;
+            }
             switch (get_assignment(*it)) {
             case l_undef:
                 break;
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index dfdb035c5..279ea20cf 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -316,7 +316,7 @@ namespace smt {
         return false;
     }
 
-    bool model_checker::check_rec_fun(quantifier* q) {
+    bool model_checker::check_rec_fun(quantifier* q, bool strict_rec_fun) {
         TRACE("model_checker", tout << mk_pp(q, m) << "\n";);
         SASSERT(q->get_num_patterns() == 2); // first pattern is the function, second is the body.
         expr* fn = to_app(q->get_pattern(0))->get_arg(0);
@@ -340,7 +340,7 @@ namespace smt {
                 }
                 sub(q->get_expr(), num_decls, args.c_ptr(), tmp);
                 m_curr_model->eval(tmp, result, true);
-                if (m.is_false(result)) {
+                if (strict_rec_fun ? !m.is_true(result) : m.is_false(result)) {
                     add_instance(q, args, 0);
                     return false;
                 }
@@ -365,10 +365,10 @@ namespace smt {
 
     bool model_checker::check(proto_model * md, obj_map<enode, app *> const & root2value) {
         SASSERT(md != 0);
+
         m_root2value = &root2value;
-        ptr_vector<quantifier>::const_iterator it  = m_qm->begin_quantifiers();
-        ptr_vector<quantifier>::const_iterator end = m_qm->end_quantifiers();
-        if (it == end)
+
+        if (m_qm->num_quantifiers() == 0)
             return true;
 
         if (m_iteration_idx >= m_params.m_mbqi_max_iterations) {
@@ -393,6 +393,36 @@ namespace smt {
         bool found_relevant = false;
         unsigned num_failures = 0;
 
+        check_quantifiers(false, found_relevant, num_failures);
+
+        
+        if (found_relevant)
+            m_iteration_idx++;
+
+        TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md););
+        TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);        
+        m_max_cexs += m_params.m_mbqi_max_cexs;
+
+        if (num_failures == 0 && !m_context->validate_model()) {
+            num_failures = 1;
+            // this time force expanding recursive function definitions 
+            // that are not forced true in the current model.
+            check_quantifiers(true, found_relevant, num_failures);
+        }
+        if (num_failures == 0)
+            m_curr_model->cleanup();
+        if (m_params.m_mbqi_trace) {
+            if (num_failures == 0)
+                verbose_stream() << "(smt.mbqi :succeeded true)\n";
+            else
+                verbose_stream() << "(smt.mbqi :num-failures " << num_failures << ")\n";
+        }
+        return num_failures == 0;
+    }
+
+    void model_checker::check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures) {
+        ptr_vector<quantifier>::const_iterator it  = m_qm->begin_quantifiers();
+        ptr_vector<quantifier>::const_iterator end = m_qm->end_quantifiers();
         for (; it != end; ++it) {
             quantifier * q = *it;
 	    if(!m_qm->mbqi_enabled(q)) continue;
@@ -406,7 +436,7 @@ namespace smt {
                 }
                 found_relevant = true;
                 if (m.is_rec_fun_def(q)) {
-                    if (!check_rec_fun(q)) {
+                    if (!check_rec_fun(q, strict_rec_fun)) {
                         TRACE("model_checker", tout << "checking recursive function failed\n";);
                         num_failures++;
                     }
@@ -420,26 +450,6 @@ namespace smt {
                 }
             }
         }
-        
-        if (found_relevant)
-            m_iteration_idx++;
-
-        TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md););
-        TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);        
-        m_max_cexs += m_params.m_mbqi_max_cexs;
-
-        if (num_failures == 0 && !m_context->validate_model()) {
-            num_failures = 1;
-        }
-        if (num_failures == 0)
-            m_curr_model->cleanup();
-        if (m_params.m_mbqi_trace) {
-            if (num_failures == 0)
-                verbose_stream() << "(smt.mbqi :succeeded true)\n";
-            else
-                verbose_stream() << "(smt.mbqi :num-failures " << num_failures << ")\n";
-        }
-        return num_failures == 0;
     }
 
     void model_checker::init_search_eh() {
diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h
index b94ddb6bb..1b7713d59 100644
--- a/src/smt/smt_model_checker.h
+++ b/src/smt/smt_model_checker.h
@@ -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);
+        bool check_rec_fun(quantifier* q, bool strict_rec_fun);
+        void check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures);
 
         struct instance {
             quantifier * m_q;
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index bad788f5d..10e2df988 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -397,6 +397,10 @@ namespace smt {
         return m_imp->m_quantifiers.end();
     }
 
+    unsigned quantifier_manager::num_quantifiers() const {
+        return m_imp->m_quantifiers.size();
+    }
+
     // The default plugin uses E-matching, MBQI and quick-checker
     class default_qm_plugin : public quantifier_manager_plugin {
         quantifier_manager *        m_qm;
diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h
index bc249ed1a..6dcf20583 100644
--- a/src/smt/smt_quantifier.h
+++ b/src/smt/smt_quantifier.h
@@ -91,6 +91,8 @@ namespace smt {
 
         ptr_vector<quantifier>::const_iterator begin_quantifiers() const;
         ptr_vector<quantifier>::const_iterator end_quantifiers() const;
+        unsigned num_quantifiers() const;
+        
     };
 
     class quantifier_manager_plugin {