Fix contracts so runtime checking can be turned on.

1 files changed, 1 insertions, 6 deletions

diff --git a/Source/ParserHelper/ParserHelper.cs b/Source/ParserHelper/ParserHelper.cs
index 465b9245..a24343c9 100644
--- a/Source/ParserHelper/ParserHelper.cs
+++ b/Source/ParserHelper/ParserHelper.cs
@@ -47,12 +47,7 @@ namespace Microsoft.Boogie {
     public string/*!*/ _val;  // token value

     public Token next;  // ML 2005-03-11 Tokens are kept in linked list

 

-    public static IToken/*!*/ NoToken = new Token();

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(NoToken != null);

-    }

-

+    public static readonly IToken/*!*/ NoToken = new Token();

 

     public Token() {

       this._val = "anything so that it is nonnull";