build

Author: NikolajBjorner

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() {

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,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;