diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 1fc0c1f41..6d361bc22 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -604,7 +604,7 @@ class solve_eqs_tactic : public tactic {
                 expr* f = g.form(idx);
                 thrw(f, tmp);
                 rw(tmp, tmp2);
-                g.update(idx, tmp2);
+                g.update(idx, tmp2, g.pr(idx), g.dep(idx));
             }
             
         }
@@ -774,8 +774,7 @@ class solve_eqs_tactic : public tactic {
                 m_num_steps += m_r->get_num_steps() + 1;
                 if (m_produce_proofs)
                     new_pr = m().mk_transitivity(pr, new_pr);
-                if (m_produce_unsat_cores)
-                    new_dep = m().mk_join(dep, new_dep);
+                new_dep = m().mk_join(dep, new_dep);
                 m_norm_subst->insert(v, new_def, new_pr, new_dep);
                 // we updated the substituting, but we don't need to reset m_r
                 // because all cached values there do not depend on v.