fix #3649

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/ast.cpp

@@ -1834,7 +1834,7 @@ ast * ast_manager::register_node_core(ast * n) {
 
     n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
 
-    // track_id(n, 70);
+    //track_id(n, 1354);
 
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
@@ -1920,19 +1920,6 @@ ast * ast_manager::register_node_core(ast * n) {
         break;
     }
 
-#if 0
-    // std::cout << n->m_id << " " << n->hash() << "\n";
-    if (n->m_id == 1523) {
-        std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
-    }
-    if (n->m_id == 1524) {
-        std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
-        VERIFY(false);
-    }
-    if (n->m_id == 1525) {
-        std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
-    }
-#endif
     return n;
 }
 

src/ast/expr_substitution.cpp

@@ -66,6 +66,8 @@ std::ostream& expr_substitution::display(std::ostream& out) {
 
 void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_dependency * def_dep) {
     obj_map<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, nullptr); 
+    SASSERT(!def_pr || to_app(m_manager.get_fact(def_pr))->get_arg(0) == c);
+    SASSERT(!def_pr || to_app(m_manager.get_fact(def_pr))->get_arg(1) == def);
     if (entry->get_data().m_value == nullptr) {
         // new entry
         m_manager.inc_ref(c);

src/ast/rewriter/rewriter.cpp

@@ -42,6 +42,16 @@ void rewriter_core::del_cache_stack() {
     }
 }
 
+bool rewriter_core::rewrites_from(expr* t, proof* p) {
+    return !p || (to_app(m().get_fact(p))->get_arg(0) == t);
+}
+
+bool rewriter_core::rewrites_to(expr* t, proof* p) {
+    return !p || (to_app(m().get_fact(p))->get_arg(1) == t); 
+}
+
+
+
 void rewriter_core::cache_shifted_result(expr * k, unsigned offset, expr * v) {
 #if 0
     // trace for tracking cache usage

src/ast/rewriter/rewriter.h

@@ -87,6 +87,8 @@ protected:
         push_frame_core(t, must_cache(t), st);
     } 
 
+    bool rewrites_to(expr* t, proof* p);
+    bool rewrites_from(expr* t, proof* p);
     void init_cache_stack();
     void del_cache_stack();
     void reset_cache();

src/ast/rewriter/rewriter_def.h

@@ -100,6 +100,8 @@ bool rewriter_tpl<Config>::process_const(app * t0) {
     case BR_DONE:
         result_stack().push_back(m_r.get());
         if (ProofGen) {
+            SASSERT(rewrites_from(t0, m_pr));
+            SASSERT(rewrites_to(t0, m_pr));
             if (m_pr)
                 result_pr_stack().push_back(m_pr);
             else
@@ -139,6 +141,8 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
         SASSERT(m().get_sort(t) == m().get_sort(new_t));
         result_stack().push_back(new_t);
         set_new_child_flag(t, new_t);
+        SASSERT(rewrites_from(t, new_t_pr));
+        SASSERT(rewrites_to(new_t, new_t_pr));
         if (ProofGen)
             result_pr_stack().push_back(new_t_pr);
         return true;
@@ -167,6 +171,8 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
             if (ProofGen) {
                 proof * pr = get_cached_pr(t);
                 result_pr_stack().push_back(pr);
+                SASSERT(rewrites_from(t, pr));
+                SASSERT(rewrites_to(r, pr));
             }
             return true;
         }
@@ -286,14 +292,22 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
             else {
                 new_t = m().mk_app(f, new_num_args, new_args);
                 m_pr  = m().mk_congruence(t, new_t, num_prs, result_pr_stack().c_ptr() + fr.m_spos);
+                SASSERT(rewrites_from(t, m_pr));
+                SASSERT(rewrites_to(new_t, m_pr));
             }
         }
+        m_pr2 = nullptr;
         br_status st = m_cfg.reduce_app(f, new_num_args, new_args, m_r, m_pr2);       
+        
+        if (st != BR_FAILED && !rewrites_to(m_r, m_pr2)) enable_trace("reduce_app");
         CTRACE("reduce_app", st != BR_FAILED,
               tout << mk_bounded_pp(t, m()) << "\n";
               tout << "st: " << st;
               if (m_r) tout << " --->\n" << mk_bounded_pp(m_r, m());
-              tout << "\n";);
+              tout << "\n";
+              tout << m_pr2 << "\n";
+              );
+        SASSERT(st == BR_FAILED || rewrites_to(m_r, m_pr2));
         SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
         if (st != BR_FAILED) {
             result_stack().shrink(fr.m_spos);
@@ -491,6 +505,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
     }
 }
 
+
 template<typename Config>
 template<bool ProofGen>
 void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {

src/ast/rewriter/th_rewriter.cpp

@@ -571,7 +571,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         }
     }
 
-    void log_rewrite_axiom_instantiation(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+    void log_rewrite_axiom_instantiation(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
         family_id fid = f->get_family_id();
         if (fid == m_b_rw.get_fid()) {
             decl_kind k = f->get_decl_kind();
@@ -587,8 +587,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         app_ref tmp(m());
         tmp = m().mk_app(f, num, args);
         m().trace_stream() << "[inst-discovered] theory-solving " << static_cast<void *>(nullptr) << " " << m().get_family_name(fid) << "# ; #" << tmp->get_id() << "\n";
-        if (m().proofs_enabled())
-            result_pr = m().mk_rewrite(tmp, result);
         tmp = m().mk_eq(tmp, result);
         m().trace_stream() << "[instance] " << static_cast<void *>(nullptr) << " #" << tmp->get_id() << "\n";
 
@@ -618,7 +616,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         br_status st = reduce_app_core(f, num, args, result);
 
         if (st != BR_FAILED && m().has_trace_stream()) {
-            log_rewrite_axiom_instantiation(f, num, args, result, result_pr);
+            log_rewrite_axiom_instantiation(f, num, args, result);
         }
 
         if (st != BR_DONE && st != BR_FAILED) {

src/math/lp/lar_solver.h

@@ -578,7 +578,7 @@ public:
     }
 
     void subs_term_columns(lar_term& t) {
-        vector<std::pair<unsigned,unsigned>> columns_to_subs;
+        svector<std::pair<unsigned,unsigned>> columns_to_subs;
         for (const auto & m : t) {
             unsigned tj = adjust_column_index_to_term_index(m.var().index());
             if (tj == m.var().index()) continue;

src/tactic/core/propagate_values_tactic.cpp

@@ -60,13 +60,13 @@ class propagate_values_tactic : public tactic {
         if (m.is_value(arg1) && is_shared(arg2)) {
             lhs   = arg2;
             value = arg1;
-            inverted = false;
+            inverted = true;
             return true;
         }
         if (m.is_value(arg2) && is_shared(arg1)) {
             lhs   = arg1;
             value = arg2;
-            inverted = true;
+            inverted = false;
             return true;
         }
         return false;