Boogie: Added boolean code expressions (sans well-formedness checks on the input).

1 files changed, 7 insertions, 7 deletions

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 64cc5c09..d29223a9 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -15,11 +15,11 @@ namespace VC {
   public class VCContext 

   {

     [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(Label2absy!=null);

+    void ObjectInvariant() 

+    {

+      Contract.Invariant(Label2absy!=null);

       Contract.Invariant(Ctxt != null);

-}

+    }

 

     [Rep] public readonly Hashtable/*<int, Absy!>*/ Label2absy;

     [Rep] public readonly ProverContext Ctxt;

@@ -52,9 +52,9 @@ void ObjectInvariant()
     public static VCExpr Block(Block b, VCExpr N, VCContext ctxt)

       //modifies ctxt.*;

     {

-    Contract.Requires(b != null);

-    Contract.Requires(N != null);

-    Contract.Requires(ctxt != null);

+      Contract.Requires(b != null);

+      Contract.Requires(N != null);

+      Contract.Requires(ctxt != null);

       Contract.Ensures(Contract.Result<VCExpr>() != null);

 

       VCExpressionGenerator gen = ctxt.Ctxt.ExprGen;