From 9a033a6dd23183138116c92a4cae06c4448e4247 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 3 Nov 2014 10:16:48 +0100
Subject: Worked on the verification result caching.

---
 Source/VCGeneration/ConditionGeneration.cs | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 8f4ac550..9a2a9117 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1475,12 +1475,13 @@ namespace VC {
 
     public enum CachingAction : byte
     {
-      DoNothing,
+      DoNothingToAssert,
       MarkAsPartiallyVerified,
       MarkAsFullyVerified,
       RecycleError,
       AssumeNegationOfAssumptionVariable,
-      Drop,
+      DropAssume,
+      DropAssert
     }
 
     public long[] CachingActionCounts;
@@ -1547,14 +1548,17 @@ namespace VC {
           var alwaysUseSubsumption = subsumption == CommandLineOptions.SubsumptionOption.Always;
           if (currentImplementation != null
               && currentImplementation.HasCachedSnapshot
+              && checksum != null
+              && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
               && !currentImplementation.AnyErrorsInCachedSnapshot
-              && currentImplementation.InjectedAssumptionVariables.Count == 1)
+              && currentImplementation.InjectedAssumptionVariables.Count == 1
+              && relevantAssumpVars.Count == 1)
           {
-            TraceCachingAction(pc, CachingAction.DoNothing);
+            TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);
           }
           else if (relevantDoomedAssumpVars.Any())
           {
-            TraceCachingAction(pc, CachingAction.DoNothing);
+            TraceCachingAction(pc, CachingAction.DoNothingToAssert);
           }
           else if (currentImplementation != null
                    && currentImplementation.HasCachedSnapshot
@@ -1610,7 +1614,7 @@ namespace VC {
           }
           else
           {
-            TraceCachingAction(pc, CachingAction.DoNothing);
+            TraceCachingAction(pc, CachingAction.DoNothingToAssert);
           }
         }
         else if (pc is AssumeCmd
@@ -1646,7 +1650,7 @@ namespace VC {
         }
         else
         {
-          TraceCachingAction(pc, CachingAction.Drop);
+          TraceCachingAction(pc, pc is AssumeCmd ? CachingAction.DropAssume : CachingAction.DropAssert);
         }
       }
       #endregion
-- 
cgit v1.2.3