From 3845d4e0bcf52113a60d0a360cf25e9e4a33e2d5 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Fri, 17 Oct 2014 11:37:39 +0200
Subject: Worked on the verification result caching.

---
 Source/ExecutionEngine/VerificationResultCache.cs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'Source/ExecutionEngine')

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index f8b29a69..ba995cba 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -223,6 +223,7 @@ namespace Microsoft.Boogie
           && node.AssignedAssumptionVariable == null)
       {
         var before = new List<Cmd>();
+        var beforePrecondtionCheck = new List<Cmd>();
         var after = new List<Cmd>();
         Expr assumedExpr = new LiteralExpr(Token.NoToken, false);
         var canUseSpecs = DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program);
@@ -232,7 +233,7 @@ namespace Microsoft.Boogie
           if (precond != null)
           {
             var assume = new AssumeCmd(Token.NoToken, precond, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
-            before.Add(assume);
+            beforePrecondtionCheck.Add(assume);
           }
 
           assumedExpr = node.Postcondition(oldProc, Program);
@@ -268,7 +269,7 @@ namespace Microsoft.Boogie
           var assumed = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });
           after.Add(assumed);
         }
-        node.ExtendDesugaring(before, after);
+        node.ExtendDesugaring(before, beforePrecondtionCheck, after);
       }
 
       return result;
-- 
cgit v1.2.3