Boogie: Fixed some doubly-inherited-contract occurrences.

1 files changed, 3 insertions, 3 deletions

diff --git a/Source/AbsInt/LoopInvariantsOnDemand.cs b/Source/AbsInt/LoopInvariantsOnDemand.cs
index 5bb5916d..b61b1445 100644
--- a/Source/AbsInt/LoopInvariantsOnDemand.cs
+++ b/Source/AbsInt/LoopInvariantsOnDemand.cs
@@ -41,7 +41,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     }

 

     override public object Default(AI.IExpr expr) {

-      Contract.Requires(expr != null);

+      

       if (expr is AI.IVariable) {

         if (!variables.Contains((AI.IVariable)expr)) {

           this.variables.Add((AI.IVariable)expr);

@@ -64,7 +64,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     }

 

     public override object VisitFunApp(AI.IFunApp funapp) {

-      Contract.Requires(funapp != null);

+      

       foreach (AI.IExpr arg in funapp.Arguments) {

         Contract.Assert(arg != null);

         arg.DoVisit(this);

@@ -73,7 +73,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     }

 

     public override object VisitFunction(AI.IFunction fun) {

-      Contract.Requires(fun != null);

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

       fun.Body.DoVisit(this);

       this.variables.Remove(fun.Param);

       return true;