From e1fd167e01d74353431c683b9533c75b2074e087 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 30 Jul 2019 14:35:09 +0800
Subject: [PATCH] remove stale assertions due to lambda #2446

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qsat.cpp              | 1 -
 src/smt/smt_model_finder.cpp | 6 +-----
 2 files changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 33085c811..d1816d807 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -1278,7 +1278,6 @@ namespace qe {
                 in->reset();
                 in->inc_depth();
                 result.push_back(in.get());
-                std::cout << in->models_enabled() << " " << m_model_save.get() << "\n";
                 if (in->models_enabled()) {                    
                     model_converter_ref mc;
                     mc = model2model_converter(m_model_save.get());
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index a34dc787a..013476a34 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -522,7 +522,6 @@ namespace smt {
             }
 
             instantiation_set const * get_uvar_inst_set(quantifier * q, unsigned i) const {
-                //SASSERT(!has_quantifiers(q->get_expr()));
                 ast_idx_pair k(q, i);
                 node * r = nullptr;
                 if (m_uvars.find(k, r))
@@ -1747,7 +1746,6 @@ namespace smt {
                 }
                 CTRACE("model_finder_bug", has_quantifiers(m_flat_q->get_expr()),
                        tout << mk_pp(q, m) << "\n" << mk_pp(m_flat_q, m) << "\n";);
-                // SASSERT(m.is_lambda_def(q) || !has_quantifiers(m_flat_q->get_expr()));
             }
 
             ~quantifier_info() {
@@ -2193,8 +2191,7 @@ namespace smt {
                         m_info->m_is_auf = false; // unexpected occurrence of variable.
                     }
                     else {
-                        SASSERT(is_quantifier(curr)); // no nested quantifiers
-                        //UNREACHABLE();
+                        SASSERT(is_lambda(curr)); 
                     }
                 }
             }
@@ -2380,7 +2377,6 @@ namespace smt {
                 quantifier * q = d->get_flat_q();
                 if (m.is_lambda_def(q)) return;
                 expr * e = q->get_expr();
-                //SASSERT(!has_quantifiers(e));
                 reset_cache();
                 SASSERT(m_ttodo.empty());
                 SASSERT(m_ftodo.empty());