Fixed an issue in the verification result caching (recycled errors).

1 files changed, 24 insertions, 3 deletions

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 0a2974c8..55c6ba85 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -147,10 +147,13 @@ namespace Microsoft.Boogie
             if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)

             {

               SetErrorChecksumsInCachedSnapshot(impl, vr);

-              var p = ExecutionEngine.CachedProgram(vr.ProgramId);

-              if (p != null)

+              if (vr.ProgramId != null)

               {

-                SetAssertionChecksumsInPreviousSnapshot(impl, p);

+                var p = ExecutionEngine.CachedProgram(vr.ProgramId);

+                if (p != null)

+                {

+                  SetAssertionChecksumsInPreviousSnapshot(impl, p);

+                }

               }

             }

           }

@@ -161,6 +164,14 @@ namespace Microsoft.Boogie
           else if (priority == Priority.SKIP)

           {

             run.SkippedImplementationCount++;

+            if (vr.ProgramId != null)

+            {

+              var p = ExecutionEngine.CachedProgram(vr.ProgramId);

+              if (p != null)

+              {

+                SetAssertionChecksums(impl, p);

+              }

+            }

           }

         }

       }

@@ -180,6 +191,16 @@ 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);

+      if (implPrevSnap != null)

+      {

+        implementation.AssertionChecksums = implPrevSnap.AssertionChecksums;

+      }

+    }

+

     private static void SetAssertionChecksumsInPreviousSnapshot(Implementation implementation, Program program)

     {

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