From 241de8264a32285d371a53d8d91a219625d76922 Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Mon, 7 Mar 2011 05:15:14 +0000
Subject: Fix contracts so runtime checking can be turned on.

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

(limited to 'Source/VCExpr/VCExprASTVisitors.cs')

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 3e65ec23..c43ee478 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -634,9 +634,10 @@ namespace Microsoft.Boogie.VCExprAST {
       return true;
     }
 
-    public static Dictionary<VCExprVar/*!*/, object/*!*/>/*!*/ FreeTermVariables(VCExpr node) {
+    public static Dictionary<VCExprVar/*!*/, object>/*!*/ FreeTermVariables(VCExpr node) {
       Contract.Requires(node != null);
-      Contract.Ensures(cce.NonNullElements(Contract.Result<Dictionary<VCExprVar, object>>()));
+      Contract.Ensures(Contract.Result<Dictionary<VCExprVar, object>>() != null);
+      Contract.Ensures(Contract.ForAll(Contract.Result<Dictionary<VCExprVar, object>>(), ftv => ftv.Key != null));
       FreeVariableCollector collector = new FreeVariableCollector();
       collector.Traverse(node, true);
       return collector.FreeTermVars;
-- 
cgit v1.2.3