mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 12:11:23 +00:00
Code Activity

Fix dealloc order in hypotheses_reducer::reset()

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-17 08:51:33 -07:00
parent 689414d055
commit 9d4784baf6
1 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/muz/spacer/spacer_proof_utils.cpp
View file

@ -174,14 +174,15 @@ proof_ref theory_axiom_reducer::reduce(proof* pr) {
} }
void hypothesis_reducer::reset() { void hypothesis_reducer::reset() {
m_cache.reset();
m_units.reset();
m_active_hyps.reset();
m_parent_hyps.reset(); m_parent_hyps.reset();
for (auto t : m_pinned_active_hyps) dealloc(t); m_active_hyps.reset();
m_pinned_active_hyps.reset(); m_units.reset();
m_cache.reset();
for (auto t : m_pinned_parent_hyps) dealloc(t); for (auto t : m_pinned_parent_hyps) dealloc(t);
m_pinned_parent_hyps.reset(); m_pinned_parent_hyps.reset();
for (auto t : m_pinned_active_hyps) dealloc(t);
m_pinned_active_hyps.reset();
m_pinned.reset();
} }
void hypothesis_reducer::compute_hypsets(proof *pr) { void hypothesis_reducer::compute_hypsets(proof *pr) {