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

1 files changed, 3 insertions, 3 deletions

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 240920c5..4eafdbbb 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -18,7 +18,7 @@ namespace Microsoft.Boogie {
     }

 

     public override Implementation VisitImplementation(Implementation node) {

-      Contract.Requires(node != null);

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

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

       //Console.WriteLine("Procedure {0}", node.Name);

       Implementation/*!*/ impl = base.VisitImplementation(node);

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

 

     public override Expr VisitOldExpr(OldExpr node) {

-      Contract.Requires(node != null);

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

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

       insideOldExpr++;

       node.Expr = this.VisitExpr(node.Expr);

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

 

     public override Expr VisitIdentifierExpr(IdentifierExpr node) {

-      Contract.Requires(node != null);

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

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

       if (node.Decl != null) {

         usedVars.Add(node.Decl);