Did more refactoring and addressed several todos.

1 files changed, 3 insertions, 7 deletions

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 93ca9cb7..67d6dde5 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -193,8 +193,7 @@ namespace Microsoft.Boogie
 

     private static void SetAssertionChecksums(Implementation implementation, Program program)

     {

-      // TODO(wuestholz): Maybe we should speed up this lookup.

-      var implPrevSnap = program.Implementations.FirstOrDefault(i => i.Id == implementation.Id);

+      var implPrevSnap = program.FindImplementation(implementation.Id);

       if (implPrevSnap != null)

       {

         implementation.AssertionChecksums = implPrevSnap.AssertionChecksums;

@@ -203,8 +202,7 @@ namespace Microsoft.Boogie
 

     private static void SetAssertionChecksumsInPreviousSnapshot(Implementation implementation, Program program)

     {

-      // TODO(wuestholz): Maybe we should speed up this lookup.

-      var implPrevSnap = program.Implementations.FirstOrDefault(i => i.Id == implementation.Id);

+      var implPrevSnap = program.FindImplementation(implementation.Id);

       if (implPrevSnap != null)

       {

         implementation.AssertionChecksumsInPreviousSnapshot = implPrevSnap.AssertionChecksums;

@@ -215,8 +213,7 @@ namespace Microsoft.Boogie
     {

       var result = base.VisitCallCmd(node);

 

-      // TODO(wuestholz): Maybe we should speed up this lookup.

-      var oldProc = programInCachedSnapshot.Procedures.FirstOrDefault(p => p.Name == node.Proc.Name);

+      var oldProc = programInCachedSnapshot.FindProcedure(node.Proc.Name);

       if (oldProc != null

           && oldProc.DependencyChecksum != node.Proc.DependencyChecksum

           && node.AssignedAssumptionVariable == null)

@@ -326,7 +323,6 @@ namespace Microsoft.Boogie
     {

       Contract.Requires(oldProc != null && newProg != null);

 

-      // TODO(wuestholz): Maybe we should speed up this lookup.

       var funcs = newProg.Functions;

       return oldProc.DependenciesCollected

              && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum)));