From c5b91aef6829ea5d8e3d6f1437c98319403d163e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Nov 2012 07:52:07 -0800 Subject: [PATCH] Fixed bug reported by Heizmann at codeplex Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 2 ++ src/smt/proto_model/proto_model.cpp | 9 +++++---- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 74ecc1597..72b4cbbfe 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -3,6 +3,8 @@ RELEASE NOTES Version 4.3.0 ============= +- Fixed bug during model construction reported by Heizmann (http://z3.codeplex.com/workitem/5) + - Remark: We skipped version 4.2 due to a mistake when releasing 4.1.2. Version 4.1.2 was accidentally tagged as 4.2. Thanks to Claude Marche for reporting this issue. From now on, we are also officially moving to a 3 number naming convention for version numbers. diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index f944990ee..4cedea228 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -623,10 +623,11 @@ void proto_model::complete_partial_funcs() { if (m_params.m_model_partial) return; - ptr_vector::iterator it = m_func_decls.begin(); - ptr_vector::iterator end = m_func_decls.end(); - for (; it != end; ++it) - complete_partial_func(*it); + // m_func_decls may be "expanded" when we invoke get_some_value. + // So, we must not use iterators to traverse it. + for (unsigned i = 0; i < m_func_decls.size(); i++) { + complete_partial_func(m_func_decls[i]); + } } model * proto_model::mk_model() {