mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix #5733
This commit is contained in:
parent
84f514a4f4
commit
5672f5cc34
|
@ -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);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue