From 09696e989e56f83f9ea218434509809fb9158a12 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 27 Aug 2021 11:57:26 -0700
Subject: [PATCH] add missing lambda defs per #5509

the result is now unknown because the nested expression contains exists, which doesn't get replaced by universal quantifier which is assumed by the legacy core.
The legacy core should not depend on universal quantifiers only, but fixing this is a risk. Workaround is to rewrite goals using forall only (replace exists by de-Morgan dual).
---
 src/model/model_core.cpp      | 13 +++++++++++++
 src/model/model_core.h        |  2 ++
 src/smt/smt_model_checker.cpp |  8 +++++++-
 3 files changed, 22 insertions(+), 1 deletion(-)

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";