1 files changed, 25 insertions, 25 deletions
diff --git a/Test/og/lock-introduced.bpl b/Test/og/lock-introduced.bpl
index 1f576c42..c9650215 100644
--- a/Test/og/lock-introduced.bpl
+++ b/Test/og/lock-introduced.bpl
@@ -8,26 +8,26 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
 
 type X;
 const nil: X;
-var {:phase 0,2} b: bool;
-var {:phase 1,3} lock: X;
+var {:layer 0,2} b: bool;
+var {:layer 1,3} lock: X;
 
-procedure {:yields} {:phase 3} Customer({:linear "tid"} tid: X)
-requires {:phase 2} tid != nil; 
-requires {:phase 2} InvLock(lock, b);
-ensures {:phase 2} InvLock(lock, b);
+procedure {:yields} {:layer 3} Customer({:linear "tid"} tid: X)
+requires {:layer 2} tid != nil; 
+requires {:layer 2} InvLock(lock, b);
+ensures {:layer 2} InvLock(lock, b);
 {
     yield;
-    assert {:phase 2} InvLock(lock, b);
+    assert {:layer 2} InvLock(lock, b);
     while (*) 
-    invariant {:phase 2} InvLock(lock, b);
+    invariant {:layer 2} InvLock(lock, b);
     {
         call Enter(tid);
     	call Leave(tid);
         yield;
-	assert {:phase 2} InvLock(lock, b);
+	assert {:layer 2} InvLock(lock, b);
     }    
     yield;
-    assert {:phase 2} InvLock(lock, b);
+    assert {:layer 2} InvLock(lock, b);
 }
 
 function {:inline} InvLock(lock: X, b: bool) : bool
@@ -35,32 +35,32 @@ function {:inline} InvLock(lock: X, b: bool) : bool
     lock != nil <==> b
 }
 
-procedure {:yields} {:phase 2,3} Enter({:linear "tid"} tid: X)
-requires {:phase 2} tid != nil; 
-requires {:phase 2} InvLock(lock, b);
-ensures {:phase 2} InvLock(lock, b);
+procedure {:yields} {:layer 2,3} Enter({:linear "tid"} tid: X)
+requires {:layer 2} tid != nil; 
+requires {:layer 2} InvLock(lock, b);
+ensures {:layer 2} InvLock(lock, b);
 ensures {:right} |{ A: assume lock == nil && tid != nil; lock := tid; return true; }|;
 {
     yield;
-    assert {:phase 2} InvLock(lock, b);
+    assert {:layer 2} InvLock(lock, b);
     call LowerEnter(tid);
     yield;
-    assert {:phase 2} InvLock(lock, b);
+    assert {:layer 2} InvLock(lock, b);
 }
 
-procedure {:yields} {:phase 2,3} Leave({:linear "tid"} tid:X)
-requires {:phase 2} InvLock(lock, b);
-ensures {:phase 2} InvLock(lock, b);
+procedure {:yields} {:layer 2,3} Leave({:linear "tid"} tid:X)
+requires {:layer 2} InvLock(lock, b);
+ensures {:layer 2} InvLock(lock, b);
 ensures {:atomic} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;
 {
     yield;
-    assert {:phase 2} InvLock(lock, b);
+    assert {:layer 2} InvLock(lock, b);
     call LowerLeave();
     yield;
-    assert {:phase 2} InvLock(lock, b);
+    assert {:layer 2} InvLock(lock, b);
 }
 
-procedure {:yields} {:phase 1,2} LowerEnter({:linear "tid"} tid: X) 
+procedure {:yields} {:layer 1,2} LowerEnter({:linear "tid"} tid: X) 
 ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|;
 {
     var status: bool;
@@ -80,7 +80,7 @@ ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|;
 	goto L;
 }
 
-procedure {:yields} {:phase 1,2} LowerLeave()
+procedure {:yields} {:layer 1,2} LowerLeave()
 ensures {:atomic} |{ A: b := false; lock := nil; return true; }|;
 {
     yield;
@@ -88,13 +88,13 @@ ensures {:atomic} |{ A: b := false; lock := nil; return true; }|;
     yield;
 }
 
-procedure {:yields} {:phase 0,1} CAS(prev: bool, next: bool) returns (status: bool);
+procedure {:yields} {:layer 0,1} CAS(prev: bool, next: bool) returns (status: bool);
 ensures {:atomic} |{ 
 A: goto B, C; 
 B: assume b == prev; b := next; status := true; return true; 
 C: status := false; return true; 
 }|;
 
-procedure {:yields} {:phase 0,1} SET(next: bool);
+procedure {:yields} {:layer 0,1} SET(next: bool);
 ensures {:atomic} |{ A: b := next; return true; }|;