From d41a7518de7fd135caf752824670723d06332298 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Fri, 26 Dec 2014 10:41:10 +0100
Subject: Fixed a postcondition.

---
 Source/VCGeneration/VC.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index b989c029..8a549e9d 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1156,7 +1156,7 @@ namespace VC {
 
       public static List<Split/*!*/> FindManualSplits(Implementation/*!*/ impl, Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins, VCGen/*!*/ par) {
         Contract.Requires(impl != null);
-        Contract.Ensures(cce.NonNullElements(Contract.Result<List<Split>>()));
+        Contract.Ensures(Contract.Result<List<Split>>() == null || cce.NonNullElements(Contract.Result<List<Split>>()));
 
         var splitPoints = new Dictionary<Block,int>();
         foreach (var b in impl.Blocks) {
-- 
cgit v1.2.3