Fix contracts so runtime checking can be turned on.

1 files changed, 1 insertions, 2 deletions

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));

     }