From 55421afd6110138e0719f80e5f35597c8e1d14f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Jun 2022 09:49:25 -0700 Subject: [PATCH] fix regression in top-sort fix #6060 --- src/util/top_sort.h | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/util/top_sort.h b/src/util/top_sort.h index 0f2c32cb7..51a0d9733 100644 --- a/src/util/top_sort.h +++ b/src/util/top_sort.h @@ -87,8 +87,10 @@ class top_sort { public: virtual ~top_sort() { - for (auto * t : m_dep_keys) + for (auto * t : m_dep_keys) { dealloc(get_dep(t)); + m_deps[t->get_small_id()] = nullptr; + } } void topological_sort() { @@ -102,9 +104,12 @@ public: m_dfs_num.reset(); } - void insert(T* t, T_set* s) { + void insert(T* t, T_set* s) { + if (contains_dep(t)) + dealloc(get_dep(t)); + else + m_dep_keys.push_back(t); m_deps.setx(t->get_small_id(), add_tag(s), nullptr); - m_dep_keys.push_back(t); } ptr_vector const& deps() { return m_dep_keys; } @@ -126,7 +131,7 @@ public: bool contains_dep(T* t) const { return m_deps.get(t->get_small_id(), nullptr) != nullptr; } - T_set* get_dep(T* t) const { return del_tag(m_deps.get(t->get_small_id(), nullptr)); } + T_set* get_dep(T* t) const { return del_tag(m_deps.get(t->get_small_id(), nullptr)); } bool is_singleton_partition(T* f) const {