From e3f712b3cfc4588f794ccefa126191977c2f3620 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Apr 2020 13:00:56 -0700
Subject: [PATCH] build

---
 src/ast/rewriter/value_sweep.cpp | 6 ++++--
 src/smt/CMakeLists.txt           | 1 -
 src/smt/theory_recfun.cpp        | 2 ++
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/ast/rewriter/value_sweep.cpp b/src/ast/rewriter/value_sweep.cpp
index fee2c7805..dee6e54cf 100644
--- a/src/ast/rewriter/value_sweep.cpp
+++ b/src/ast/rewriter/value_sweep.cpp
@@ -35,8 +35,10 @@ void value_sweep::set_value_core(expr* e, expr* v) {
 }
 
 void value_sweep::set_value(expr* e, expr* v) {
-    set_value_core(e, v);
-    m_pinned.push_back(e);
+    if (!is_reducible(e)) {
+        set_value_core(e, v);
+        m_pinned.push_back(e);
+    }
 }
 
 void value_sweep::reset_values() {
diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index a8f7303e7..f6afd539f 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -10,7 +10,6 @@ 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..c0eeea9d5 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';)
@@ -442,6 +443,7 @@ namespace smt {
     
     final_check_status theory_recfun::final_check_eh() {
         TRACEFN("final\n");
+        generate_induction_lemmas(get_context());
         if (can_propagate()) {
             propagate();
             return FC_CONTINUE;