From 284d59978839205663687fe3b013295c1971e3bf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Jul 2021 05:14:14 -0700 Subject: [PATCH] #5323 https://github.com/Z3Prover/z3/issues/5323#issuecomment-866503616 --- src/smt/proto_model/proto_model.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index c3e34f0de..d1614f521 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -213,11 +213,12 @@ void proto_model::cleanup() { TRACE("model_bug", model_v2_pp(tout, *this);); func_decl_set found_aux_fs; expr_ref_vector trail(m); - for (auto const& kv : m_finterp) { - TRACE("model_bug", tout << kv.m_key->get_name() << "\n";); - func_interp * fi = kv.m_value; + ptr_buffer finterps; + for (auto const& kv : m_finterp) + finterps.push_back(kv.m_value); + for (auto* fi : finterps) cleanup_func_interp(trail, fi, found_aux_fs); - } + for (unsigned i = 0; i < m_const_decls.size(); ++i) { func_decl* d = m_const_decls[i]; expr* e = m_interp[d].second;