diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp
index bef2e6494..6b8ff8d63 100644
--- a/src/model/model_core.cpp
+++ b/src/model/model_core.cpp
@@ -93,6 +93,7 @@ void model_core::unregister_decl(func_decl * d) {
 		m_manager.dec_ref(ec->get_data().m_key);
 		m_manager.dec_ref(ec->get_data().m_value);
 		m_interp.remove(d);
+        m_const_decls.erase(d);
 		return;
 	}
 
@@ -101,5 +102,6 @@ void model_core::unregister_decl(func_decl * d) {
 		m_manager.dec_ref(ef->get_data().m_key);
 		dealloc(ef->get_data().m_value);
 		m_finterp.remove(d);
+        m_func_decls.erase(d);
 	}
 }
\ No newline at end of file