Adding background model to fixedpoint counterexamples and small code contracts fixes

1 files changed, 3 insertions, 1 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 092d12d2..cabc9d9e 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -188,12 +188,14 @@ namespace Microsoft.Boogie {
 

     public static bool firstModelFile = true;

 

+    public bool ModelHasStatesAlready = false;

+

     public void PrintModel()

     {

       var filename = CommandLineOptions.Clo.ModelViewFile;

       if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return;

 

-      var m = this.GetModelWithStates();

+      var m = ModelHasStatesAlready ? Model : this.GetModelWithStates();

 

       if (filename == "-") {

         m.Write(Console.Out);