diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 316d803a6..005d1b2e6 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -680,19 +680,25 @@ class solve_eqs_tactic : public tactic {
         }
 
         void distribute_and_or(goal & g) {
+            if (m_produce_proofs) 
+                return;
             unsigned size = g.size();
             hoist_rewriter_star rw(m());
             th_rewriter thrw(m());
             expr_ref tmp(m()), tmp2(m());
+            
             // TRACE("solve_eqs", g.display(tout););
             for (unsigned idx = 0; idx < size; idx++) {
                 checkpoint();
                 if (g.is_decided_unsat()) break;
                 expr* f = g.form(idx);
-                thrw(f, tmp);
-                rw(tmp, tmp2);
-                TRACE("solve_eqs", tout << mk_pp(f, m()) << " " << tmp2 << "\n";);
-                g.update(idx, tmp2, g.pr(idx), g.dep(idx));
+                proof_ref pr1(m()), pr2(m());
+                thrw(f, tmp, pr1);
+                rw(tmp, tmp2, pr2);
+                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));
             }
             
         }