From 4a722d4576f4afdb578552a48da948d1010733e6 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Wed, 15 Oct 2014 23:49:55 +0200
Subject: Worked on the verification result caching.

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

(limited to 'Source/ExecutionEngine')

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index bc529849..eed92d31 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -223,9 +223,10 @@ namespace Microsoft.Boogie
         if (DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program))
         {
           var before = new List<Cmd>();
-          if (oldProc.Requires.Any())
+          var pre = node.CheckedPrecondition(oldProc, Program);
+          if (pre != null)
           {
-            var pre = node.CheckedPrecondition(oldProc, Program);
+            
             var assume = new AssumeCmd(Token.NoToken, pre, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
             before.Add(assume);
           }
@@ -241,7 +242,14 @@ namespace Microsoft.Boogie
                          new List<AssignLhs> { new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, mPre)) },
                          new List<Expr> { new IdentifierExpr(Token.NoToken, m.Decl) }));
             var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, mPre), new IdentifierExpr(Token.NoToken, m.Decl));
-            post = LiteralExpr.And(post, eq);
+            if (post == null)
+            {
+              post = eq;
+            }
+            else
+            {
+              post = LiteralExpr.And(post, eq);
+            }
           }
 
           if (post != null)
-- 
cgit v1.2.3