From 241de8264a32285d371a53d8d91a219625d76922 Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Mon, 7 Mar 2011 05:15:14 +0000
Subject: Fix contracts so runtime checking can be turned on.

---
 Source/Provers/Simplify/ProverInterface.cs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'Source/Provers/Simplify')

diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index 50eefc49..7f7c4686 100644
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ b/Source/Provers/Simplify/ProverInterface.cs
@@ -66,7 +66,7 @@ namespace Microsoft.Boogie.Simplify {
     [StrictReadonly]
     protected readonly ProverOptions options;
     [StrictReadonly]
-    private readonly List<string>/*?*/ commonPrefix;
+    private readonly List<string> commonPrefix;
 
     [ContractInvariantMethod]
     void ObjectInvariant() {
@@ -75,7 +75,6 @@ namespace Microsoft.Boogie.Simplify {
       Contract.Invariant(openActivityString != null);
       Contract.Invariant(closeActivityString != null);
       Contract.Invariant(options != null);
-      Contract.Invariant(cce.NonNullElements(commonPrefix));
     }
 
 
-- 
cgit v1.2.3