1 files changed, 2 insertions, 2 deletions
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;
       }
     }