From af1f0e318422f7030f24e20acd057f84b7b53f16 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 8 Jul 2024 14:50:38 -0700
Subject: [PATCH] fix #7268

---
 src/model/model.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/model/model.cpp b/src/model/model.cpp
index c89ff59a2f9..362907e466b 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -248,6 +248,7 @@ void model::compress(bool force_inline) {
     // by substituting in auxiliary definitions that can be eliminated.
 
     func_decl_ref_vector pinned(m);
+    ptr_vector<func_decl> sorted_decls;
     while (true) {
         top_sort ts(m);
         collect_deps(ts);
@@ -259,6 +260,7 @@ void model::compress(bool force_inline) {
         ts.m_occur_count.reset();
         for (func_decl * f : ts.top_sorted()) 
             collect_occs(ts, f);
+        sorted_decls.reset();
         
         // remove auxiliary declarations that are not used.
         for (func_decl * f : ts.top_sorted()) {
@@ -267,11 +269,13 @@ void model::compress(bool force_inline) {
                 unregister_decl(f);
                 removed.insert(f);
             }
+            else
+                sorted_decls.push_back(f);
         }
+        std::swap(m_decls, sorted_decls);
         if (removed.empty())
             break;
         TRACE("model", tout << "remove\n"; for (func_decl* f : removed) tout << f->get_name() << "\n";);
-        remove_decls(m_decls, removed);
         remove_decls(m_func_decls, removed);
         remove_decls(m_const_decls, removed);
     }