checkpoint

1 files changed, 11 insertions, 4 deletions

diff --git a/Test/og/one.bpl b/Test/og/one.bpl
index 2a63d60d..1da2f116 100644
--- a/Test/og/one.bpl
+++ b/Test/og/one.bpl
@@ -1,4 +1,10 @@
-var x:int;

+var {:phase 1} x:int;

+

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic}

+|{A:

+  x := v; return true;

+}|;

 

 procedure A()

 modifies x;

@@ -6,10 +12,11 @@ modifies x;
   x := x;

 }

 

-procedure {:yields} B()

+procedure {:yields} {:phase 1} B()

 {

-  x := 5;

   yield;

-  assert x == 5;

+  call Set(5);

+  yield;

+  assert {:phase 1} x == 5;

 }