cleaned up the OG code

enabled it to be always on

1 files changed, 13 insertions, 7 deletions

diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index 776a165d..831d2b97 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.bpl
@@ -1,31 +1,37 @@
 var g:int;

 

-procedure PB()

+procedure {:yields} {:stable} PB()

+modifies g;

 {

   g := g + 1;

 }

 

-procedure PC()

-  ensures g == 3;

+procedure {:yields} PC()

+ensures g == 3;

 {

   g := 3;

   yield;

   assert g == 3;

 }

 

-procedure PD()

+procedure {:yields} {:stable} PE()

+{

+  call PC();

+}

+

+procedure {:yields} {:stable} PD()

 {

   call PC();

   assert g == 3;

   yield;

 }

 

-procedure{:entrypoint} Main()

+procedure {:entrypoint} {:yields} Main()

 {

-  while (true)

+  while (*)

   {

     async call PB();

-    async call PC();

+    async call PE();

     async call PD();

   }

 }