Fix some more contracts.

2 files changed, 3 insertions, 2 deletions

diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index 7f7c4686..2645838d 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,6 +75,7 @@ namespace Microsoft.Boogie.Simplify {
       Contract.Invariant(openActivityString != null);

       Contract.Invariant(closeActivityString != null);

       Contract.Invariant(options != null);

+      Contract.Invariant(commonPrefix == null || cce.NonNullElements(commonPrefix));

     }

 

 

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index c43ee478..344d795b 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -623,7 +623,7 @@ namespace Microsoft.Boogie.VCExprAST {
     public readonly List<TypeVariable/*!*/>/*!*/ FreeTypeVars = new List<TypeVariable/*!*/>();

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(cce.NonNullElements(FreeTermVars));

+      Contract.Invariant(FreeTermVars != null && Contract.ForAll(FreeTermVars, entry => entry.Key != null));

       Contract.Invariant(cce.NonNullElements(FreeTypeVars));

     }