From 495d07eb040d3e04e5266ea6dec3999c4f3e0df1 Mon Sep 17 00:00:00 2001
From: tabarbe <unknown>
Date: Thu, 19 Aug 2010 22:27:55 +0000
Subject: Boogie: Fixed a few contracts errors

---
 Source/VCExpr/VCExprAST.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 40fadfac..7d4746e2 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -800,7 +800,7 @@ TypeSeq/*!*/ res = new TypeSeq();
     }
     public override Type Type {
       get {
-        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<VCExpr>>()));
+        Contract.Ensures(Contract.Result<Type>()!=null);
         throw new NotImplementedException();
       }
     }
@@ -929,7 +929,7 @@ TypeSeq/*!*/ res = new TypeSeq();
 
     public override Type Type {
       get {
-        Contract.Ensures(Contract.Result<VCExpr>() != null);
+        Contract.Ensures(Contract.Result<Type>() != null);
         return ExprType;
       }
     }
-- 
cgit v1.2.3