From c2e0491456e23360f156fe537f90e613e4f19ae0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 26 Apr 2020 17:52:11 -0700
Subject: [PATCH] fix #4113

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qe_mbp.cpp         | 11 ++++++++++-
 src/qe/qsat.cpp           | 19 +++++++++----------
 src/smt/CMakeLists.txt    |  1 +
 src/smt/theory_recfun.cpp |  2 ++
 4 files changed, 22 insertions(+), 11 deletions(-)

diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index d7850d1ef..9692783d8 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -191,6 +191,11 @@ class mbp::impl {
         vars.shrink(j);
     }
 
+    // over-approximation
+    bool contains_uninterpreted(expr* v) {
+        return true;
+    }
+
     bool extract_bools(model_evaluator& eval, expr_ref_vector& fmls, expr* fml) {
         TRACE("qe", tout << "extract bools: " << mk_pp(fml, m) << "\n";);
         ptr_vector<expr> todo;
@@ -209,10 +214,14 @@ class mbp::impl {
             m_visited.mark(e);
             if (m.is_bool(e) && !m.is_true(e) && !m.is_false(e) && m.inc()) {
                 expr_ref val = eval(e);
-                TRACE("qe", tout << "found: " << mk_pp(e, m) << "\n";);
+                TRACE("qe", tout << "found: " << mk_pp(e, m) << " " << val << "\n";);
                 if (!m.inc())
                     continue;
+                if (!m.is_true(val) && !m.is_false(val) && contains_uninterpreted(val)) {
+                    throw default_exception("could not evaluate Boolean in model");
+                }
                 SASSERT(m.is_true(val) || m.is_false(val));
+
                 if (!m_bool_visited.is_marked(e)) {
                     fmls.push_back(m.is_true(val) ? e : mk_not(m, e));
                 }
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index b79fa60f0..2d8e7be01 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -331,7 +331,7 @@ namespace qe {
             } 
             if (sz == args.size()) {
                 if (diff) {
-                    r = m.mk_app(a->get_decl(), sz, args.c_ptr());
+                    r = m.mk_app(a->get_decl(), args);
                     trail.push_back(r);
                 }
                 else {
@@ -424,7 +424,7 @@ namespace qe {
             } 
             if (args.size() == sz) {
                 if (diff) {
-                    r = m.mk_app(a->get_decl(), sz, args.c_ptr());
+                    r = m.mk_app(a->get_decl(), args);
                 }
                 else {
                     r = to_app(a);
@@ -456,9 +456,8 @@ namespace qe {
         
     void pred_abs::display(std::ostream& out) const {
         out << "pred2lit:\n";
-        obj_map<expr, expr*>::iterator it = m_pred2lit.begin(), end = m_pred2lit.end();
-        for (; it != end; ++it) {
-            out << mk_pp(it->m_key, m) << " |-> " << mk_pp(it->m_value, m) << "\n";
+        for (auto const& kv : m_pred2lit) {
+            out << mk_pp(kv.m_key, m) << " |-> " << mk_pp(kv.m_value, m) << "\n";
         }
         for (unsigned i = 0; i < m_preds.size(); ++i) {
             out << "level " << i << "\n";
@@ -477,10 +476,10 @@ namespace qe {
     
     void pred_abs::display(std::ostream& out, expr_ref_vector const& asms) const {
         max_level lvl;       
-        for (unsigned i = 0; i < asms.size(); ++i) {
-            expr* e = asms[i];
-            bool is_not = m.is_not(asms[i], e);
-            out << mk_pp(asms[i], m);
+        for (expr* a : asms) {
+            expr* e = a;
+            bool is_not = m.is_not(a, e);
+            out << mk_pp(a, m);
             if (m_elevel.find(e, lvl)) {
                 lvl.display(out << " - ");
             }
@@ -1010,7 +1009,7 @@ namespace qe {
                         }
                     }
                     if (all_visited) {
-                        r = m.mk_app(a->get_decl(), args.size(), args.c_ptr());
+                        r = m.mk_app(a->get_decl(), args);
                         todo.pop_back();
                         trail.push_back(r);
                         visited.insert(e, r);
diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index f6afd539f..a8f7303e7 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -10,6 +10,7 @@ z3_add_component(smt
     expr_context_simplifier.cpp
     fingerprints.cpp
     mam.cpp
+    model_sweeper.cpp
     old_interval.cpp
     qi_queue.cpp
     seq_axioms.cpp
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index cfe4522de..fa3331816 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -22,6 +22,7 @@ Revision History:
 #include "ast/for_each_expr.h"
 #include "smt/theory_recfun.h"
 #include "smt/params/smt_params_helper.hpp"
+#include "smt/model_sweeper.h"
 
 
 #define TRACEFN(x) TRACE("recfun", tout << x << '\n';)
@@ -443,6 +444,7 @@ namespace smt {
     final_check_status theory_recfun::final_check_eh() {
         TRACEFN("final\n");
         if (can_propagate()) {
+            generate_induction_lemmas(get_context());
             propagate();
             return FC_CONTINUE;
         }