mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

track dependencies in context solve

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-05-16 23:06:21 +03:00
parent 6e3f05b986
commit 335040a4ff
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -604,7 +604,7 @@ class solve_eqs_tactic : public tactic {
expr* f = g.form(idx); expr* f = g.form(idx);
thrw(f, tmp); thrw(f, tmp);
rw(tmp, tmp2); 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; m_num_steps += m_r->get_num_steps() + 1;
if (m_produce_proofs) if (m_produce_proofs)
new_pr = m().mk_transitivity(pr, new_pr); 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); m_norm_subst->insert(v, new_def, new_pr, new_dep);
// we updated the substituting, but we don't need to reset m_r // we updated the substituting, but we don't need to reset m_r
// because all cached values there do not depend on v. // because all cached values there do not depend on v.