4 files changed, 20 insertions, 20 deletions
diff --git a/Source/Provers/Z3/Inspector.cs b/Source/Provers/Z3/Inspector.cs
index 3675f6a7..638acdb0 100644
--- a/Source/Provers/Z3/Inspector.cs
+++ b/Source/Provers/Z3/Inspector.cs
@@ -36,7 +36,7 @@ void ObjectInvariant()
     }
     
     protected override bool StandardResult(VCExpr node, bool arg) {
-      Contract.Requires(node!=null);
+      //Contract.Requires(node!=null);
       VCExprNAry nary = node as VCExprNAry;
       if (nary != null) {
         VCExprLabelOp lab = nary.Op as VCExprLabelOp;
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index c93b364d..a36ca87a 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -234,8 +234,8 @@ namespace Microsoft.Boogie.Z3
     }
 
     protected override void DoBeginCheck(string descriptiveName, string formula) {
-      Contract.Requires(descriptiveName != null);
-      Contract.Requires(formula != null);
+      //Contract.Requires(descriptiveName != null);
+      //Contract.Requires(formula != null);
       ToWriteLine(formula);
       ToWriteLine(String.Format(";   END OF FORMULA {0} - {1}", NumFormulasChecked.ToString(), descriptiveName));
       ToFlush();
@@ -254,7 +254,7 @@ namespace Microsoft.Boogie.Z3
     }
 
     public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler) {
-      Contract.Requires(handler != null);
+      //Contract.Requires(handler != null);
       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
       //ProverOutcome outcome;
       bool isInvalid = false;
@@ -920,7 +920,7 @@ namespace Microsoft.Boogie.Z3
     }
 
     public override void Print(TextWriter writer) {
-      Contract.Requires(writer != null);
+      //Contract.Requires(writer != null);
       if (CommandLineOptions.Clo.PrintErrorModel == 4) {
         PrintReadableModel(writer);
         return;
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 3813c63b..9289b5b7 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -53,7 +53,7 @@ void ObjectInvariant()
     }
     
     protected override Microsoft.Boogie.Simplify.ProverProcess CreateProverProcess(string proverPath) {
-    Contract.Requires(proverPath!= null);
+    //Contract.Requires(proverPath!= null);
     Contract.Ensures(Contract.Result<Microsoft.Boogie.Simplify.ProverProcess>() != null);
 
 
@@ -66,7 +66,7 @@ void ObjectInvariant()
     }
 
     protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions opts) {
-      Contract.Requires(opts != null);
+      //Contract.Requires(opts != null);
       Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
 
       return new Z3VCExprTranslator(gen, (Z3InstanceOptions) opts);
@@ -74,9 +74,9 @@ void ObjectInvariant()
 
     public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
     {
-      Contract.Requires(descriptiveName != null);
-      Contract.Requires(vc != null);
-      Contract.Requires(handler != null);
+      //Contract.Requires(descriptiveName != null);
+      //Contract.Requires(vc != null);
+      //Contract.Requires(handler != null);
       FireUpInspector();
       if (inspector != null) {
         inspector.NewProblem(descriptiveName, vc, handler);
@@ -115,7 +115,7 @@ void ObjectInvariant()
 
     protected override bool Parse(string opt)
     {
-      Contract.Requires(opt!=null);
+      //Contract.Requires(opt!=null);
       return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||
              ParseString(opt, "INSPECTOR", ref Inspector) ||
              ParseBool(opt, "DIST", ref DistZ3) ||
@@ -211,7 +211,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
     } }
 
     public override LineariserOptions AddLetVariable(VCExprVar furtherVar) {
-      Contract.Requires(furtherVar != null);
+      //Contract.Requires(furtherVar != null);
       Contract.Ensures(Contract.Result<LineariserOptions>() != null);
 
       List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();
@@ -221,7 +221,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
     }
     
     public override LineariserOptions AddLetVariables(List<VCExprVar/*!>!*/> furtherVars) {
-      Contract.Requires(furtherVars != null);
+      //Contract.Requires(furtherVars != null);
     Contract.Ensures(Contract.Result<LineariserOptions>() != null);
 
       List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/> ();
@@ -292,14 +292,14 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
 
     public override string Lookup(VCExprVar var)
     {
-      Contract.Requires(var != null);
+      //Contract.Requires(var != null);
       Contract.Ensures(Contract.Result<string>() != null);
 
       return Namer.Lookup(var);
     }
     
     public override string translate(VCExpr expr, int polarity) {
-      Contract.Requires(expr != null);
+      //Contract.Requires(expr != null);
       Contract.Ensures(Contract.Result<string>() != null);
 
       DateTime start = DateTime.Now;
@@ -385,8 +385,8 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
 
     public override object SpawnProver(ProverOptions popts, object ctxt)
     {
-      Contract.Requires(popts != null);
-      Contract.Requires(ctxt != null);
+      //Contract.Requires(popts != null);
+      //Contract.Requires(ctxt != null);
       Contract.Ensures(Contract.Result<object>() != null);
 
       Z3InstanceOptions opts = cce.NonNull((Z3InstanceOptions)popts);
@@ -396,8 +396,8 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
     }
 
     public override object NewProverContext(ProverOptions options) {
-      Contract.Requires(options != null);
-      Contract.Ensures(Contract.Result<object>() != null);
+      //Contract.Requires(options != null);
+      //Contract.Ensures(Contract.Result<object>() != null);
 
       if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
         CommandLineOptions.Clo.BracketIdsInVC = 0;
diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs
index 7cdc6f4f..cd01e325 100644
--- a/Source/Provers/Z3/TypeDeclCollector.cs
+++ b/Source/Provers/Z3/TypeDeclCollector.cs
@@ -73,7 +73,7 @@ void ObjectInvariant()
 
     // not used
     protected override bool StandardResult(VCExpr node, bool arg) {
-      Contract.Requires(node != null);
+      //Contract.Requires(node != null);
       return true;
     }