renamed :phase to :layer

1 files changed, 11 insertions, 11 deletions

diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl
index 1d2c9a03..ac2ec1b6 100644
--- a/Test/og/bar.bpl
+++ b/Test/og/bar.bpl
@@ -1,47 +1,47 @@
 // RUN: %boogie -noinfer "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

-var {:phase 1} g:int;

+var {:layer 1} g:int;

 

-procedure {:yields} {:phase 1} PB()

+procedure {:yields} {:layer 1} PB()

 {

   yield;

   call Incr();

   yield;

 }

 

-procedure {:yields} {:phase 0,1} Incr();

+procedure {:yields} {:layer 0,1} Incr();

 ensures {:atomic}

 |{A:

   g := g + 1; return true;

 }|;

 

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

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

 ensures {:atomic}

 |{A:

   g := v; return true;

 }|;

 

-procedure {:yields} {:phase 1} PC()

-ensures {:phase 1} g == old(g);

+procedure {:yields} {:layer 1} PC()

+ensures {:layer 1} g == old(g);

 {

   yield;

-  assert {:phase 1} g == old(g);

+  assert {:layer 1} g == old(g);

 }

 

-procedure {:yields} {:phase 1} PE()

+procedure {:yields} {:layer 1} PE()

 {

   call PC();

 }

 

-procedure {:yields} {:phase 1} PD()

+procedure {:yields} {:layer 1} PD()

 {

   yield;

   call Set(3);

   call PC();

-  assert {:phase 1} g == 3;

+  assert {:layer 1} g == 3;

 }

 

-procedure {:yields} {:phase 1} Main2()

+procedure {:yields} {:layer 1} Main2()

 {

   yield;

   while (*)