diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp
index 3c10f8704..bef2e6494 100644
--- a/src/model/model_core.cpp
+++ b/src/model/model_core.cpp
@@ -87,3 +87,19 @@ void model_core::register_decl(func_decl * d, func_interp * fi) {
     }
 }
 
+void model_core::unregister_decl(func_decl * d) {
+	decl2expr::obj_map_entry * ec = m_interp.find_core(d);
+	if (ec && ec->get_data().m_value != 0) {
+		m_manager.dec_ref(ec->get_data().m_key);
+		m_manager.dec_ref(ec->get_data().m_value);
+		m_interp.remove(d);
+		return;
+	}
+
+	decl2finterp::obj_map_entry * ef = m_finterp.find_core(d);
+	if (ef && ef->get_data().m_value != 0) {
+		m_manager.dec_ref(ef->get_data().m_key);
+		dealloc(ef->get_data().m_value);
+		m_finterp.remove(d);
+	}
+}
\ No newline at end of file
diff --git a/src/model/model_core.h b/src/model/model_core.h
index 8527a0bca..371106b05 100644
--- a/src/model/model_core.h
+++ b/src/model/model_core.h
@@ -60,6 +60,7 @@ public:
 
     void register_decl(func_decl * d, expr * v);
     void register_decl(func_decl * f, func_interp * fi);
+	void unregister_decl(func_decl * d);
 
     virtual expr * get_some_value(sort * s) = 0;