shuffle checks for enable_edge around fix #4159

Author: NikolajBjorner

src/ast/datatype_decl_plugin.h

@@ -346,7 +346,7 @@ namespace datatype {
         bool is_is(app * f) const { return is_app_of(f, fid(), OP_DT_IS);} 
         bool is_is(expr * e) const { return is_app(e) && is_is(to_app(e)); }
         bool is_recognizer(app * f) const { return is_recognizer0(f) || is_is(f); }
-        bool is_accessor(app * f) const { return is_app_of(f, fid(), OP_DT_ACCESSOR); }
+        bool is_accessor(expr * e) const { return is_app(e) && is_app_of(to_app(e), fid(), OP_DT_ACCESSOR); }
         bool is_update_field(app * f) const { return is_app_of(f, fid(), OP_DT_UPDATE_FIELD); }
         app* mk_is(func_decl * c, expr *f);
         ptr_vector<func_decl> const * get_datatype_constructors(sort * ty);

src/ast/rewriter/value_sweep.cpp

@@ -35,7 +35,7 @@ void value_sweep::set_value_core(expr* e, expr* v) {
 }
 
 void value_sweep::set_value(expr* e, expr* v) {
-    if (!is_reducible(e)) {
+    if (!is_reducible(e) || m_dt.is_accessor(e)) {
         set_value_core(e, v);
         m_pinned.push_back(e);
     }

src/smt/CMakeLists.txt

@@ -34,6 +34,7 @@ z3_add_component(smt
     smt_farkas_util.cpp
     smt_for_each_relevant_expr.cpp
     smt_implied_equalities.cpp
+    smt_induction.cpp
     smt_internalizer.cpp
     smt_justification.cpp
     smt_kernel.cpp

src/smt/theory_utvpi_def.h

@@ -510,7 +510,7 @@ namespace smt {
 
     template<typename Ext>
     void theory_utvpi<Ext>::propagate() {
-        bool consistent = true;
+        bool consistent = is_consistent() && !get_context().inconsistent();
         while (consistent && can_propagate()) {
             unsigned idx = m_asserted_atoms[m_asserted_qhead];
             m_asserted_qhead++;
@@ -520,13 +520,9 @@ namespace smt {
 
     template<typename Ext>
     bool theory_utvpi<Ext>::propagate_atom(atom const& a) {
-        context& ctx = get_context();
-        TRACE("utvpi", a.display(*this, tout); tout << "\n";);
-        if (ctx.inconsistent()) {
-            return false;
-        }
+        TRACE("utvpi", a.display(*this, tout); tout << "\n";);       
         int edge_id = a.get_asserted_edge();
-        if (!enable_edge(edge_id) || !is_consistent()) {
+        if (!enable_edge(edge_id)) {
             m_graph.traverse_neg_cycle2(m_params.m_arith_stronger_lemmas, m_nc_functor);
             set_conflict();
             return false;
@@ -698,10 +694,9 @@ namespace smt {
 
     template<typename Ext>
     bool theory_utvpi<Ext>::enable_edge(edge_id id) {
-        return 
-            (id == null_edge_id) || 
-            (m_graph.enable_edge(id) && m_graph.enable_edge(id+1)) ||
-            m_non_utvpi_exprs;
+        return
+            (id == null_edge_id) ||
+            (m_graph.enable_edge(id) && m_graph.enable_edge(id + 1));
     }
 
     template<typename Ext>