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<func_decl>::iterator it  = m_func_decls.begin();
-    ptr_vector<func_decl>::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() {