Worked on the verification result caching.

2 files changed, 13 insertions, 11 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 98f0110a..7fb12589 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1491,6 +1491,7 @@ namespace VC {
         var dropCmd = false;

         var relevantAssumpVars = currentImplementation != null ? currentImplementation.RelevantInjectedAssumptionVariables(incarnationMap) : new List<LocalVariable>();

         var relevantDoomedAssumpVars = currentImplementation != null ? currentImplementation.RelevantDoomedInjectedAssumptionVariables(incarnationMap) : new List<LocalVariable>();

+        var checksum = pc.SugaredCmdChecksum != null ? pc.SugaredCmdChecksum : pc.Checksum;

         if (pc is AssertCmd) {

           var ac = (AssertCmd)pc;

           ac.OrigExpr = ac.Expr;

@@ -1508,9 +1509,9 @@ namespace VC {
           { }

           else if (currentImplementation != null

                    && currentImplementation.HasCachedSnapshot

-                   && ac.Checksum != null

-                   && currentImplementation.IsAssertionChecksumInCachedSnapshot(ac.Checksum)

-                   && !currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum))

+                   && checksum != null

+                   && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)

+                   && !currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))

           {

             bool isTrue;

             var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);

@@ -1539,9 +1540,9 @@ namespace VC {
           else if (currentImplementation != null

                    && currentImplementation.HasCachedSnapshot

                    && relevantAssumpVars.Count == 0

-                   && ac.Checksum != null

-                   && currentImplementation.IsAssertionChecksumInCachedSnapshot(ac.Checksum)

-                   && currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum))

+                   && checksum != null

+                   && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)

+                   && currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))

           {

             if (alwaysUseSubsumption)

             {

@@ -1557,13 +1558,13 @@ namespace VC {
           }

         }

         else if (pc is AssumeCmd

-                 && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot"))

+                 && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot")

+                 && pc.SugaredCmdChecksum != null)

         {

           if (!relevantDoomedAssumpVars.Any()

               && currentImplementation.HasCachedSnapshot

-              && pc.Checksum != null

-              && currentImplementation.IsAssertionChecksumInCachedSnapshot(pc.Checksum)

-              && !currentImplementation.IsErrorChecksumInCachedSnapshot(pc.Checksum))

+              && currentImplementation.IsAssertionChecksumInCachedSnapshot(pc.SugaredCmdChecksum)

+              && !currentImplementation.IsErrorChecksumInCachedSnapshot(pc.SugaredCmdChecksum))

           {

             bool isTrue;

             var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 6a039923..d92f8661 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1626,7 +1626,8 @@ namespace VC {
         outcome = Outcome.Errors;

         foreach (var a in impl.RecycledFailingAssertions)

         {

-          var oldCex = impl.ErrorChecksumToCachedError[a.Checksum] as Counterexample;

+          var checksum = a.SugaredCmdChecksum != null ? a.SugaredCmdChecksum : a.Checksum;

+          var oldCex = impl.ErrorChecksumToCachedError[checksum] as Counterexample;

           if (oldCex != null)

           {

             callback.OnCounterexample(oldCex, null);