Commits

Leonardo de Moura committed c5b91ae

Fixed bug reported by Heizmann at codeplex

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

Comments (0)

Files changed (2)

 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. 

src/smt/proto_model/proto_model.cpp

     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() {