diff options
Diffstat (limited to 'Source/Houdini')
-rw-r--r-- | Source/Houdini/Houdini.cs | 4 |
1 files changed, 0 insertions, 4 deletions
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;
|