From 9d4784baf63b5d9e6b691b65f1c2b78d67f1b659 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 17 May 2018 08:51:33 -0700 Subject: [PATCH] Fix dealloc order in hypotheses_reducer::reset() --- src/muz/spacer/spacer_proof_utils.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp index 42cdcf50b..8ed414c2b 100644 --- a/src/muz/spacer/spacer_proof_utils.cpp +++ b/src/muz/spacer/spacer_proof_utils.cpp @@ -174,14 +174,15 @@ proof_ref theory_axiom_reducer::reduce(proof* pr) { } void hypothesis_reducer::reset() { - m_cache.reset(); - m_units.reset(); - m_active_hyps.reset(); m_parent_hyps.reset(); - for (auto t : m_pinned_active_hyps) dealloc(t); - m_pinned_active_hyps.reset(); + m_active_hyps.reset(); + m_units.reset(); + m_cache.reset(); for (auto t : m_pinned_parent_hyps) dealloc(t); 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) {