diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp
index fcddce59f..1ed6e3670 100644
--- a/src/model/model_core.cpp
+++ b/src/model/model_core.cpp
@@ -125,3 +125,16 @@ void model_core::unregister_decl(func_decl * d) {
         dealloc(v);
     }
 }
+
+void model_core::add_lambda_defs() {
+    unsigned sz = get_num_decls();
+    for (unsigned i = sz; i-- > 0; ) {
+        func_decl* f = get_decl(i);
+        quantifier* q = m.is_lambda_def(f);
+        if (!q)
+            continue;
+        func_interp* fi = alloc(func_interp, m, f->get_arity());
+        fi->set_else(q);
+        register_decl(f, fi);
+    }
+}
diff --git a/src/model/model_core.h b/src/model/model_core.h
index 8e531a2b6..6a52fa10b 100644
--- a/src/model/model_core.h
+++ b/src/model/model_core.h
@@ -72,6 +72,8 @@ public:
     void unregister_decl(func_decl * d);
     func_interp* update_func_interp(func_decl* f, func_interp* fi);
 
+    void add_lambda_defs();
+
     virtual expr * get_some_value(sort * s) = 0;
     virtual expr * get_fresh_value(sort * s) = 0;
     virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) = 0;
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 9569ec3a8..5f6131f59 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -423,8 +423,14 @@ namespace smt {
         m_value2expr.reset();
 
         TRACE("model_checker", tout << "MODEL_CHECKER INVOKED\n";
-              tout << "model:\n"; model_pp(tout, *m_curr_model););
+        tout << "model:\n"; model_pp(tout, *m_curr_model););
 
+        for (quantifier* q : *m_qm)
+            if (m.is_lambda_def(q)) {
+                md->add_lambda_defs();
+                break;
+            }
+	
         md->compress();
 
         TRACE("model_checker", tout << "MODEL_CHECKER INVOKED\n";