From e818b7bd2732c87dbbee30b17e6563b9c652427c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 10 Sep 2018 15:15:00 -0700
Subject: [PATCH] fix #1812

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.cpp               |  6 +++++
 src/ast/ast.h                 |  1 +
 src/smt/smt_model_checker.cpp | 45 +++++++++++++++++++++++++++++++----
 src/smt/smt_model_checker.h   |  3 +++
 4 files changed, 51 insertions(+), 4 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 11a15492c..65d3c7821 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1656,6 +1656,12 @@ bool ast_manager::are_distinct(expr* a, expr* b) const {
     return false;
 }
 
+func_decl* ast_manager::get_rec_fun_decl(quantifier* q) const {
+    SASSERT(is_rec_fun_def(q)); 
+    return to_app(to_app(q->get_pattern(0))->get_arg(0))->get_decl(); 
+}
+
+
 void ast_manager::register_plugin(family_id id, decl_plugin * plugin) {
     SASSERT(m_plugins.get(id, 0) == 0);
     m_plugins.setx(id, plugin, 0);
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 89df04961..c1193dfbd 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1632,6 +1632,7 @@ public:
 
     bool is_rec_fun_def(quantifier* q) const { return q->get_qid() == m_rec_fun; }
     bool is_lambda_def(quantifier* q) const { return q->get_qid() == m_lambda_def; }
+    func_decl* get_rec_fun_decl(quantifier* q) const;
     
     symbol const& rec_fun_qid() const { return m_rec_fun; }
 
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 0fea4d13d..c3af41dcf 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -47,6 +47,7 @@ namespace smt {
         m_model_finder(mf),
         m_max_cexs(1),
         m_iteration_idx(0),
+        m_has_rec_fun(false),
         m_curr_model(nullptr),
         m_pinned_exprs(m) {
     }
@@ -351,9 +352,7 @@ namespace smt {
     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);
-        SASSERT(is_app(fn));
-        func_decl* f = to_app(fn)->get_decl();
+        func_decl* f = m.get_rec_fun_decl(q);
 
         expr_ref_vector args(m);
         unsigned num_decls = q->get_num_decls();
@@ -433,7 +432,7 @@ namespace smt {
         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()) {
+        if (num_failures == 0 && (!m_context->validate_model() || has_rec_under_quantifiers())) {
             num_failures = 1;
             // this time force expanding recursive function definitions
             // that are not forced true in the current model.
@@ -450,6 +449,43 @@ namespace smt {
         return num_failures == 0;
     }
 
+    struct has_rec_fun_proc {
+        obj_hashtable<func_decl>& m_rec_funs;
+        bool m_has_rec_fun;
+
+        bool has_rec_fun() const { return m_has_rec_fun; }
+
+        has_rec_fun_proc(obj_hashtable<func_decl>& rec_funs):
+            m_rec_funs(rec_funs),
+            m_has_rec_fun(false) {}
+
+        void operator()(app* fn) {
+            m_has_rec_fun |= m_rec_funs.contains(fn->get_decl());
+        }
+        void operator()(expr*) {}
+    };
+
+    bool model_checker::has_rec_under_quantifiers() {
+        if (!m_has_rec_fun) {
+            return false;
+        }
+        obj_hashtable<func_decl> rec_funs;
+        for (quantifier * q : *m_qm) {
+            if (m.is_rec_fun_def(q)) {
+                rec_funs.insert(m.get_rec_fun_decl(q));
+            }            
+        }
+        expr_fast_mark1 visited;
+        has_rec_fun_proc proc(rec_funs);
+        for (quantifier * q : *m_qm) {
+            if (!m.is_rec_fun_def(q)) {
+                quick_for_each_expr(proc, visited, q);
+                if (proc.has_rec_fun()) return true;
+            }            
+        }
+        return false;
+    }
+
     // 
     // (repeated from defined_names.cpp)
     // NB. The pattern for lambdas is incomplete.
@@ -479,6 +515,7 @@ namespace smt {
             }
             found_relevant = true;
             if (m.is_rec_fun_def(q)) {
+                m_has_rec_fun = true;
                 if (!check_rec_fun(q, strict_rec_fun)) {
                     TRACE("model_checker", tout << "checking recursive function failed\n";);
                     num_failures++;
diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h
index 40a58efea..57edf3034 100644
--- a/src/smt/smt_model_checker.h
+++ b/src/smt/smt_model_checker.h
@@ -51,8 +51,10 @@ namespace smt {
         scoped_ptr<context>                         m_aux_context; // Auxiliary context used for model checking quantifiers.
         unsigned                                    m_max_cexs;
         unsigned                                    m_iteration_idx;
+        bool                                        m_has_rec_fun;
         proto_model *                               m_curr_model;
         obj_map<expr, expr *>                       m_value2expr;
+
         friend class instantiation_set;
 
         void init_aux_context();
@@ -64,6 +66,7 @@ namespace smt {
         bool add_blocking_clause(model * cex, expr_ref_vector & sks);
         bool check(quantifier * q);
         bool check_rec_fun(quantifier* q, bool strict_rec_fun);
+        bool has_rec_under_quantifiers();
         void check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures);
 
         struct instance {