na

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

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

src/smt/theory_recfun.cpp

@@ -22,7 +22,6 @@ 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';)
@@ -444,7 +443,6 @@ 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;
         }