From 3aba5ba4ae71402535162ca2d6dece344ecfcfb4 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Thu, 18 Jul 2013 14:33:24 -0700
Subject: Populate a model only once.

---
 Source/VCGeneration/ConditionGeneration.cs | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 8afbf027..f625de75 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -203,15 +203,18 @@ namespace Microsoft.Boogie {
       var filename = CommandLineOptions.Clo.ModelViewFile;
       if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return;
 
-      var m = ModelHasStatesAlready ? Model : this.GetModelWithStates();
+      if (!ModelHasStatesAlready) {
+        PopulateModelWithStates();
+        ModelHasStatesAlready = true;
+      }
 
       if (filename == "-") {
-        m.Write(tw);
+        Model.Write(tw);
         tw.Flush();
       } else {
         using (var wr = new StreamWriter(filename, !firstModelFile)) {
           firstModelFile = false;
-          m.Write(wr);
+          Model.Write(wr);
         }
       }
     }
@@ -227,16 +230,16 @@ namespace Microsoft.Boogie {
       m.Substitute(mapping);
     }
 
-    public Model GetModelWithStates()
+    public void PopulateModelWithStates()
     {
-      if (Model == null) return null;
+      Contract.Requires(Model != null);
 
       Model m = Model;
       ApplyRedirections(m); 
 
       var mvstates = m.TryGetFunc("@MV_state");
       if (MvInfo == null || mvstates == null)
-        return m;
+        return;
 
       Contract.Assert(mvstates.Arity == 2);
 
@@ -282,8 +285,6 @@ namespace Microsoft.Boogie {
           Contract.Assume(false);
         }
       }
-
-      return m;
     }
 
     private Model.Element GetModelValue(Model m, Variable v) {
-- 
cgit v1.2.3