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();
   }
 }