From 5672f5cc34c8d2342750a349a7517bc8d3c49eb5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 1 Jan 2022 16:40:48 -0800
Subject: [PATCH] fix #5733

---
 src/model/model_core.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp
index da0cfb883..a23fc9800 100644
--- a/src/model/model_core.cpp
+++ b/src/model/model_core.cpp
@@ -111,6 +111,7 @@ void model_core::unregister_decl(func_decl * d) {
         m_interp[m_const_decls.back()].first = v.first;
         m_const_decls.pop_back();
         m_interp.remove(d);
+        m_decls.erase(d);
         m.dec_ref(k);
         m.dec_ref(v.second);
         return;
@@ -122,6 +123,7 @@ void model_core::unregister_decl(func_decl * d) {
         auto v = ef->get_data().m_value;
         m_finterp.remove(d);
         m_func_decls.erase(d);
+        m_decls.erase(d);
         m.dec_ref(k);
         dealloc(v);
     }