From 0539cca7cc85df57f171b33d8a3cd204b9fb9fa8 Mon Sep 17 00:00:00 2001
From: tabarbe <unknown>
Date: Fri, 20 Aug 2010 16:02:01 +0000
Subject: Boogie: Fixed some doubly-inherited-contract occurrences.

---
 Source/VCExpr/TypeErasure.cs | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

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

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index f148dc79..45533115 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -714,7 +714,7 @@ Contract.Ensures(Contract.ValueAtReturn(out var) != null);
     // Type.Int, and Type.Bool
 
     public override Type TypeAfterErasure(Type type) {
-      Contract.Requires(type != null);
+      //Contract.Requires(type != null);
       Contract.Ensures(Contract.Result<Type>() != null);
       if (UnchangedType(type))
         // these types are kept
@@ -726,7 +726,7 @@ Contract.Ensures(Contract.ValueAtReturn(out var) != null);
 
     [Pure]
     public override bool UnchangedType(Type type) {
-      Contract.Requires(type != null);
+      //Contract.Requires(type != null);
       return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays);
     }
 
@@ -1142,9 +1142,9 @@ Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null);
 
     // this method is called by MutatingVCExprVisitor.Visit(VCExprNAry, ...)
     protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List<VCExpr/*!*/>/*!*/ newSubExprs, bool changed, VariableBindings/*!*/ bindings) {
-      Contract.Requires(originalNode != null);
-      Contract.Requires(cce.NonNullElements(newSubExprs));
-      Contract.Requires(bindings != null);
+      //Contract.Requires(originalNode != null);
+      //Contract.Requires(cce.NonNullElements(newSubExprs));
+      //Contract.Requires(bindings != null);
       Contract.Assume(originalNode.Op == VCExpressionGenerator.AndOp ||
              originalNode.Op == VCExpressionGenerator.OrOp);
       return Gen.Function(originalNode.Op,
@@ -1307,8 +1307,8 @@ Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null);
     }
 
     protected override VCExpr StandardResult(VCExprNAry node, VariableBindings bindings) {
-      Contract.Requires(bindings != null);
-      Contract.Requires(node != null);
+      //Contract.Requires(bindings != null);
+      //Contract.Requires(node != null);
       Contract.Ensures(Contract.Result<VCExpr>() != null);
       System.Diagnostics.Debug.Fail("Don't know how to erase types in this expression: " + node);
       Contract.Assert(false);
@@ -1570,7 +1570,7 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
     readonly TypeAxiomBuilderIntBoolU/*!*/ AxBuilder;
 
     protected override bool StandardResult(VCExpr node, bool arg) {
-      Contract.Requires(node != null);
+      //Contract.Requires(node != null);
       return true; // not used
     }
 
-- 
cgit v1.2.3