From 89b5b3e69f5c73a4cc1883eaa9230523bbb10d2e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 10 Mar 2020 13:15:02 -0700
Subject: [PATCH] fix #3223

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/solve_eqs_tactic.cpp | 30 ++++++++++------------------
 1 file changed, 11 insertions(+), 19 deletions(-)

diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 6ee1f95aa..684facd1c 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -452,6 +452,7 @@ class solve_eqs_tactic : public tactic {
             for (unsigned idx = 0; idx < size; idx++) {
                 checkpoint();
                 expr * f = g.form(idx);
+                pr = nullptr;
                 if (solve(f, var, def, pr)) {
                     insert_solution(g, idx, f, var, def, pr);
                 }
@@ -643,8 +644,9 @@ class solve_eqs_tactic : public tactic {
             if (m().is_not(f, f1) && m().is_or(f1)) {
                 flatten_and(f, args);
                 for (unsigned i = 0; i < args.size(); ++i) {
+                    pr = nullptr;
                     expr* arg = args.get(i), *lhs = nullptr, *rhs = nullptr;
-                    if (m().is_eq(arg, lhs, rhs)) { 
+                    if (m().is_eq(arg, lhs, rhs)) {                         
                         if (trivial_solve1(lhs, rhs, var, def, pr) && is_compatible(g, idx, path, var, arg)) {
                             insert_solution(g, idx, arg, var, def, pr);
                         }
@@ -701,8 +703,9 @@ class solve_eqs_tactic : public tactic {
                 proof_ref pr1(m()), pr2(m());
                 thrw(f, tmp, pr1);
                 rw(tmp, tmp2, pr2);
+                TRACE("solve_eqs", tout << mk_pp(f, m()) << " " << tmp << "\n" << tmp2 
+                      << "\n" << pr1 << "\n" << pr2 << "\n" << mk_pp(g.pr(idx), m()) << "\n";);
                 pr1 = m().mk_transitivity(pr1, pr2);
-                TRACE("solve_eqs", tout << mk_pp(f, m()) << " " << tmp2 << "\n" << pr1 << "\n" << mk_pp(g.pr(idx), m()) << "\n";);
                 if (!pr1) pr1 = g.pr(idx); else pr1 = m().mk_modus_ponens(g.pr(idx), pr1);
                 g.update(idx, tmp2, pr1, g.dep(idx));
             }
@@ -860,16 +863,17 @@ class solve_eqs_tactic : public tactic {
             m_norm_subst->reset();
             m_r->set_substitution(m_norm_subst.get());
             
-            expr_ref new_def(m());
-            proof_ref new_pr(m());
+
             expr_dependency_ref new_dep(m());
             for (app * v : m_ordered_vars) {
                 checkpoint();
+				expr_ref new_def(m());
+				proof_ref new_pr(m());
                 expr * def = nullptr;
                 proof * pr = nullptr;
                 expr_dependency * dep = nullptr;
                 m_subst->find(v, def, pr, dep);
-                SASSERT(def != 0);
+                SASSERT(def);
                 m_r->operator()(def, new_def, new_pr, new_dep);
                 m_num_steps += m_r->get_num_steps() + 1;
                 if (m_produce_proofs)
@@ -889,18 +893,6 @@ class solve_eqs_tactic : public tactic {
                       m_norm_subst->find(v, def, pr, dep);
                       tout << mk_ismt2_pp(v, m()) << "\n----->\n" << mk_ismt2_pp(def, m()) << "\n\n";
                   });
-#if 0
-            DEBUG_CODE({
-                    for (expr * v : m_ordered_vars) {
-                        expr * def = 0;
-                        proof * pr = 0;
-                        expr_dependency * dep = 0;
-                        m_norm_subst->find(v, def, pr, dep);
-                        SASSERT(def != 0);
-                        CASSERT("solve_eqs_bug", !occurs(v, def));
-                    }
-                });
-#endif
         }
 
         void substitute(goal & g) {
@@ -1028,12 +1020,12 @@ class solve_eqs_tactic : public tactic {
                 m_subst      = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs);
                 m_norm_subst = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs);
                 while (true) {
-                    if (m_context_solve) {
+                    if (!m_produce_proofs && m_context_solve) {
                         distribute_and_or(*(g.get()));
                     }
                     collect_num_occs(*g);
                     collect(*g);
-                    if (m_context_solve) {
+                    if (!m_produce_proofs && m_context_solve) {
                         collect_hoist(*g);
                     }
                     if (m_subst->empty()) {