Boogie: Commented out all occurences of repeated inherited contracts - makes fewer error messages when compiling with runtime checking on.

1 files changed, 4 insertions, 4 deletions

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index c30211ca..e677f85c 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -257,7 +257,7 @@ namespace Microsoft.Boogie {
 

       [Pure]

       public object DoVisit(AI.ExprVisitor visitor) {

-        Contract.Requires(visitor != null);

+        //Contract.Requires(visitor != null);

         return visitor.VisitFunApp(this);

       }

 

@@ -284,7 +284,7 @@ namespace Microsoft.Boogie {
       }

 

       public AI.IFunApp CloneWithArguments(IList/*<IExpr!>*/ args) {

-        Contract.Requires(args != null);

+        //Contract.Requires(args != null);

         Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

         Contract.Assume(args.Count == 1);

 

@@ -336,7 +336,7 @@ namespace Microsoft.Boogie {
 

       [Pure]

       public object DoVisit(AI.ExprVisitor visitor) {

-        Contract.Requires(visitor != null);

+        //Contract.Requires(visitor != null);

         return visitor.VisitFunction(this);

       }

 

@@ -377,7 +377,7 @@ namespace Microsoft.Boogie {
         }

       }

       public AI.IFunction CloneWithBody(AI.IExpr body) {

-        Contract.Requires(body != null);

+        //Contract.Requires(body != null);

         Contract.Ensures(Contract.Result<AI.IFunction>() != null);

         BinderExpr realquant;