Made it produce more trace output for the verification result caching.

1 files changed, 22 insertions, 0 deletions

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index af3821c2..1de1a0ce 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -272,6 +272,8 @@ namespace Microsoft.Boogie
 

     public static void Collect(IEnumerable<Axiom> axioms)

     {

+      var start = DateTime.UtcNow;

+

       var v = new OtherDefinitionAxiomsCollector();

       foreach (var a in axioms)

       {

@@ -279,6 +281,15 @@ namespace Microsoft.Boogie
         v.VisitExpr(a.Expr);

         v.currentAxiom = null;

       }

+

+      var end = DateTime.UtcNow;

+      if (CommandLineOptions.Clo.TraceCaching)

+      {

+        Console.Out.WriteLine("");

+        Console.Out.WriteLine("<trace caching>");

+        Console.Out.WriteLine("Collected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);

+        Console.Out.WriteLine("</trace caching>");

+      }

     }

 

     public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)

@@ -317,8 +328,19 @@ namespace Microsoft.Boogie
 

     public static void Collect(Program program)

     {

+      var start = DateTime.UtcNow;

+

       var dc = new DependencyCollector();

       dc.VisitProgram(program);

+

+      var end = DateTime.UtcNow;

+      if (CommandLineOptions.Clo.TraceCaching)

+      {

+        Console.Out.WriteLine("");

+        Console.Out.WriteLine("<trace caching>");

+        Console.Out.WriteLine("Collected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);

+        Console.Out.WriteLine("</trace caching>");

+      }

     }

 

     public static bool AllFunctionDependenciesAreDefinedAndUnchanged(Procedure oldProc, Program newProg)