Disabled an expensive contract check. Instead, only check things that are actually used.

1 files changed, 5 insertions, 3 deletions

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index e20ebaed..a2b0c041 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -199,9 +199,11 @@ namespace Microsoft.Boogie.VCExprAST {
         Contract.Requires(boogieVar != null);

         VCExprVar res;

         foreach (Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/ d in Mapping) {

-          Contract.Assert(cce.NonNullElements(d));

-          if (d.TryGetValue(boogieVar, out res))

-            return res;

+          //Contract.Assert(cce.NonNullElements(d));

+            if (d.TryGetValue(boogieVar, out res)) {

+               Contract.Assert(res != null);

+               return res;

+            }

         }

         return null;

       }