Boogie: Fixed some doubly-inherited-contract occurrences.

1 files changed, 2 insertions, 2 deletions

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index a17cea23..d5505dd4 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -563,10 +563,10 @@ public abstract VCExpressionGenerator VCExprGen { get; }
         throw new NotImplementedException();

       }

     }

-    public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler){Contract.Requires(descriptiveName != null); Contract.Requires(vc != null);Contract.Requires(handler != null);throw new NotImplementedException();}

+    public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler){/*Contract.Requires(descriptiveName != null);*/ Contract.Requires(vc != null);Contract.Requires(handler != null);throw new NotImplementedException();}

     [NoDefaultContract]

     public override Outcome CheckOutcome(ErrorHandler handler){

-    Contract.Requires(handler != null);

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

       Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);

     throw new NotImplementedException();}

   }