From 335040a4ff8ef472668c9dea3604ca71ab1cd503 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 May 2019 23:06:21 +0300 Subject: [PATCH] track dependencies in context solve Signed-off-by: Nikolaj Bjorner --- src/tactic/core/solve_eqs_tactic.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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.