From 91832a0d858ca6319b737de2e14598509b48f2ae Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 3 Nov 2014 12:45:42 +0100
Subject: Worked on the verification result caching.

---
 Source/VCGeneration/ConditionGeneration.cs | 57 +++++++++++++++---------------
 1 file changed, 28 insertions(+), 29 deletions(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 9a2a9117..a36e2966 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1546,17 +1546,7 @@ namespace VC {
 
           var subsumption = Wlp.Subsumption(ac);
           var alwaysUseSubsumption = subsumption == CommandLineOptions.SubsumptionOption.Always;
-          if (currentImplementation != null
-              && currentImplementation.HasCachedSnapshot
-              && checksum != null
-              && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
-              && !currentImplementation.AnyErrorsInCachedSnapshot
-              && currentImplementation.InjectedAssumptionVariables.Count == 1
-              && relevantAssumpVars.Count == 1)
-          {
-            TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);
-          }
-          else if (relevantDoomedAssumpVars.Any())
+          if (relevantDoomedAssumpVars.Any())
           {
             TraceCachingAction(pc, CachingAction.DoNothingToAssert);
           }
@@ -1566,30 +1556,39 @@ namespace VC {
                    && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
                    && !currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))
           {
-            bool isTrue;
-            var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);
-            if (!isTrue && alwaysUseSubsumption)
+            if (!currentImplementation.AnyErrorsInCachedSnapshot
+                && currentImplementation.InjectedAssumptionVariables.Count == 1
+                && relevantAssumpVars.Count == 1)
             {
-              // Bind the assertion expression to a local variable.
-              var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock);
-              var identExpr = new IdentifierExpr(Token.NoToken, incarnation);
-              incarnationMap[incarnation] = identExpr;
-              ac.IncarnationMap[incarnation] = identExpr;
-              passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));
-              copy = identExpr;
-              passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr)));
               TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);
             }
-            else if (isTrue)
+            else
             {
-              if (alwaysUseSubsumption)
+              bool isTrue;
+              var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);
+              if (!isTrue && alwaysUseSubsumption)
+              {
+                // Bind the assertion expression to a local variable.
+                var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock);
+                var identExpr = new IdentifierExpr(Token.NoToken, incarnation);
+                incarnationMap[incarnation] = identExpr;
+                ac.IncarnationMap[incarnation] = identExpr;
+                passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));
+                copy = identExpr;
+                passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr)));
+                TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);
+              }
+              else if (isTrue)
               {
-                // Turn it into an assume statement.
-                TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);
-                pc = new AssumeCmd(ac.tok, copy);
-                pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);
+                if (alwaysUseSubsumption)
+                {
+                  // Turn it into an assume statement.
+                  TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);
+                  pc = new AssumeCmd(ac.tok, copy);
+                  pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);
+                }
+                dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;
               }
-              dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;
             }
           }
           else if (currentImplementation != null
-- 
cgit v1.2.3