From 8567d68f7f04f87b2d4270e18713bdcdf4d26031 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 10 Feb 2014 18:14:46 -0800
Subject: Fixed errors in the use of Code Contracts

---
 Source/Houdini/Houdini.cs | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'Source/Houdini')

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index e883d0bd..b05a2e5f 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -248,8 +248,6 @@ namespace Microsoft.Boogie.Houdini {
 
   public class InlineRequiresVisitor : StandardVisitor {
     public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {
-      Contract.Requires(cmdSeq != null);
-      Contract.Ensures(Contract.Result<List<Cmd>>() != null);
       List<Cmd> newCmdSeq = new List<Cmd>();
       for (int i = 0, n = cmdSeq.Count; i < n; i++) {
         Cmd cmd = cmdSeq[i];
@@ -289,8 +287,6 @@ namespace Microsoft.Boogie.Houdini {
     }
 
     public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) {
-      Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<Cmd>() != null);
       node.Requires = base.VisitRequires(node.Requires);
       node.Expr = this.VisitExpr(node.Expr);
       return node;
-- 
cgit v1.2.3