Made it collect more statistics about the more advanced verification result caching.

1 files changed, 29 insertions, 22 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 2af65733..74d299d1 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -435,28 +435,7 @@ namespace Microsoft.Boogie
 

       if (0 < CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)

       {

-        var snapshotsByVersion = new List<List<string>>();

-        for (int version = 0; true; version++)

-        {

-          var nextSnapshot = new List<string>();

-          foreach (var name in fileNames)

-          {

-            var versionedName = name.Replace(Path.GetExtension(name), ".v" + version + Path.GetExtension(name));

-            if (File.Exists(versionedName))

-            {

-              nextSnapshot.Add(versionedName);

-            }

-          }

-          if (nextSnapshot.Any())

-          {

-            snapshotsByVersion.Add(nextSnapshot);

-          }

-          else

-          {

-            break;

-          }

-        }

-

+        var snapshotsByVersion = LookForSnapshots(fileNames);

         foreach (var s in snapshotsByVersion)

         {

           ProcessFiles(new List<string>(s), false);

@@ -527,6 +506,34 @@ namespace Microsoft.Boogie
       }

     }

 

+    public static List<List<string>> LookForSnapshots(List<string> fileNames)

+    {

+      Contract.Requires(fileNames != null);

+

+      var result = new List<List<string>>();

+      for (int version = 0; true; version++)

+      {

+        var nextSnapshot = new List<string>();

+        foreach (var name in fileNames)

+        {

+          var versionedName = name.Replace(Path.GetExtension(name), ".v" + version + Path.GetExtension(name));

+          if (File.Exists(versionedName))

+          {

+            nextSnapshot.Add(versionedName);

+          }

+        }

+        if (nextSnapshot.Any())

+        {

+          result.Add(nextSnapshot);

+        }

+        else

+        {

+          break;

+        }

+      }

+      return result;

+    }

+

 

     public static void CoalesceBlocks(Program program)

     {