Fixed several build errors in the 'Checked' configuration.

1 files changed, 10 insertions, 2 deletions

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 62451caa..2237c2fc 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -57,7 +57,7 @@ namespace Microsoft.Boogie {
 

     public void GetReady()

     {

-      Contract.Requires(status == CheckerStatus.Idle);

+      Contract.Requires(IsIdle);

 

       status = CheckerStatus.Ready;

     }

@@ -268,6 +268,14 @@ namespace Microsoft.Boogie {
       }

     }

 

+    public bool IsReady

+    {

+      get

+      {

+        return status == CheckerStatus.Ready;

+      }

+    }

+

     public bool IsClosed {

       get {

         return status == CheckerStatus.Closed;

@@ -334,7 +342,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(descriptiveName != null);

       Contract.Requires(vc != null);

       Contract.Requires(handler != null);

-      Contract.Requires(status == CheckerStatus.Ready);

+      Contract.Requires(IsReady);

 

       status = CheckerStatus.Busy;

       hasOutput = false;