Merge

2 files changed, 4 insertions, 0 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 0c9538d4..32b27ae6 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2112,6 +2112,7 @@ namespace Microsoft.Boogie {
         stream.WriteLine(this, level, "// " + Comment);

       }

       stream.Write(this, level, "{0}ensures ", Free ? "free " : "");

+      Cmd.EmitAttributes(stream, Attributes);

       this.Condition.Emit(stream);

       stream.WriteLine(";");

     }

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 2f7f120d..0bcbad35 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -25,6 +25,7 @@ namespace VC
         private Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;

         public bool PersistCallTree;

         public static Dictionary<string, int> callTree = null;

+        public int numInlined = 0;

         public readonly static string recordProcName = "boogie_si_record";

 

         [ContractInvariantMethod]

@@ -1576,6 +1577,8 @@ namespace VC
             #endregion

             coverageManager.stop();

 

+            numInlined = (calls.candidateParent.Keys.Count + 1) - (calls.currCandidates.Count);

+

             // Store current call tree

             if (PersistCallTree && (ret == Outcome.Correct || ret == Outcome.Errors || ret == Outcome.ReachedBound))

             {