renamed :phase to :layer

29 files changed, 472 insertions, 472 deletions

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index ad75f1f9..b74b52c5 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -3,10 +3,10 @@
 type X;

 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;

 const nil: X;

-var {:phase 1} ghostLock: X;

-var {:phase 1} lock: X;

-var {:phase 1} currsize: int;

-var {:phase 1} newsize: int;

+var {:layer 1} ghostLock: X;

+var {:layer 1} lock: X;

+var {:layer 1} currsize: int;

+var {:layer 1} newsize: int;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

@@ -24,27 +24,27 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
     (ghostLock == nil <==> currsize == newsize)

 }

 

-procedure {:yields} {:phase 1} YieldToReadCache({:linear "tid"} tid: X)

-requires {:phase 1} Inv(ghostLock, currsize, newsize) && tid != nil;

-ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;

+procedure {:yields} {:layer 1} YieldToReadCache({:linear "tid"} tid: X)

+requires {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil;

+ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;

 {

    yield;

-   assert {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;

+   assert {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;

 }

 

-procedure {:yields} {:phase 1} YieldToWriteCache({:linear "tid"} tid: X)

-requires {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid != nil;

-ensures {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;

+procedure {:yields} {:layer 1} YieldToWriteCache({:linear "tid"} tid: X)

+requires {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid != nil;

+ensures {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;

 {

     yield;

-    assert {:phase 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;

+    assert {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;

 }

 

 procedure Allocate({:linear_in "tid"} xls': [X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

-ensures {:phase 1} xl != nil;

+ensures {:layer 1} xl != nil;

 

-procedure {:yields} {:phase 1} main({:linear_in "tid"} xls':[X]bool)

-requires {:phase 1} xls' == mapconstbool(true);

+procedure {:yields} {:layer 1} main({:linear_in "tid"} xls':[X]bool)

+requires {:layer 1} xls' == mapconstbool(true);

 {

     var {:linear "tid"} tid: X;

     var {:linear "tid"} xls: [X]bool;

@@ -55,24 +55,24 @@ requires {:phase 1} xls' == mapconstbool(true);
     call Init(xls);

     

     yield;

-    assert {:phase 1} Inv(ghostLock, currsize, newsize);

+    assert {:layer 1} Inv(ghostLock, currsize, newsize);

 

     while (*)

-    invariant {:phase 1} Inv(ghostLock, currsize, newsize);

+    invariant {:layer 1} Inv(ghostLock, currsize, newsize);

     {

         call xls, tid := Allocate(xls);

 	yield;

-    	assert {:phase 1} Inv(ghostLock, currsize, newsize);

+    	assert {:layer 1} Inv(ghostLock, currsize, newsize);

         async call Thread(tid);

 	yield;

-    	assert {:phase 1} Inv(ghostLock, currsize, newsize);

+    	assert {:layer 1} Inv(ghostLock, currsize, newsize);

     }

     yield;

 }

 

-procedure {:yields} {:phase 1} Thread({:linear "tid"} tid: X)

-requires {:phase 1} tid != nil;

-requires {:phase 1} Inv(ghostLock, currsize, newsize);

+procedure {:yields} {:layer 1} Thread({:linear "tid"} tid: X)

+requires {:layer 1} tid != nil;

+requires {:layer 1} Inv(ghostLock, currsize, newsize);

 {

     var start, size, bytesRead: int;

 

@@ -81,11 +81,11 @@ requires {:phase 1} Inv(ghostLock, currsize, newsize);
     call bytesRead := Read(tid, start, size);

 }

 

-procedure {:yields} {:phase 1} Read({:linear "tid"} tid: X, start : int, size : int) returns (bytesRead : int)

-requires {:phase 1} tid != nil;

-requires {:phase 1} 0 <= start && 0 <= size;

-requires {:phase 1} Inv(ghostLock, currsize, newsize);

-ensures {:phase 1} 0 <= bytesRead && bytesRead <= size;

+procedure {:yields} {:layer 1} Read({:linear "tid"} tid: X, start : int, size : int) returns (bytesRead : int)

+requires {:layer 1} tid != nil;

+requires {:layer 1} 0 <= start && 0 <= size;

+requires {:layer 1} Inv(ghostLock, currsize, newsize);

+ensures {:layer 1} 0 <= bytesRead && bytesRead <= size;

 {

     var i, tmp: int;

 

@@ -121,19 +121,19 @@ COPY_TO_BUFFER:
     call ReadCache(tid, start, bytesRead);

 }

 

-procedure {:yields} {:phase 1} WriteCache({:linear "tid"} tid: X, index: int)

-requires {:phase 1} Inv(ghostLock, currsize, newsize);

-requires {:phase 1} ghostLock == tid && tid != nil;

-ensures {:phase 1} ghostLock == tid;

-ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;

+procedure {:yields} {:layer 1} WriteCache({:linear "tid"} tid: X, index: int)

+requires {:layer 1} Inv(ghostLock, currsize, newsize);

+requires {:layer 1} ghostLock == tid && tid != nil;

+ensures {:layer 1} ghostLock == tid;

+ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;

 {

     var j: int;

 

     par YieldToWriteCache(tid);

     call j := ReadCurrsize(tid);

     while (j < index)

-    invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid;

-    invariant {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;

+    invariant {:layer 1} ghostLock == tid && currsize <= j && tid == tid;

+    invariant {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;

     {

         par YieldToWriteCache(tid);

         call WriteCacheEntry(tid, j);

@@ -142,12 +142,12 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsiz
     par YieldToWriteCache(tid);

 }

 

-procedure {:yields} {:phase 1} ReadCache({:linear "tid"} tid: X, start: int, bytesRead: int)

-requires {:phase 1} Inv(ghostLock, currsize, newsize);

-requires {:phase 1} tid != nil;

-requires {:phase 1} 0 <= start && 0 <= bytesRead;

-requires {:phase 1} (bytesRead == 0 || start + bytesRead <= currsize);

-ensures {:phase 1} Inv(ghostLock, currsize, newsize);

+procedure {:yields} {:layer 1} ReadCache({:linear "tid"} tid: X, start: int, bytesRead: int)

+requires {:layer 1} Inv(ghostLock, currsize, newsize);

+requires {:layer 1} tid != nil;

+requires {:layer 1} 0 <= start && 0 <= bytesRead;

+requires {:layer 1} (bytesRead == 0 || start + bytesRead <= currsize);

+ensures {:layer 1} Inv(ghostLock, currsize, newsize);

 {

     var j: int;

 

@@ -155,11 +155,11 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize);
 

     j := 0;

     while(j < bytesRead)

-    invariant {:phase 1} 0 <= j;

-    invariant {:phase 1} bytesRead == 0 || start + bytesRead <= currsize; 

-    invariant {:phase 1} Inv(ghostLock, currsize, newsize);

+    invariant {:layer 1} 0 <= j;

+    invariant {:layer 1} bytesRead == 0 || start + bytesRead <= currsize; 

+    invariant {:layer 1} Inv(ghostLock, currsize, newsize);

     {

-	assert {:phase 1} start + j < currsize;

+	assert {:layer 1} start + j < currsize;

         call ReadCacheEntry(tid, start + j);

         j := j + 1;

 	par YieldToReadCache(tid);

@@ -168,29 +168,29 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize);
     par YieldToReadCache(tid);

 }

 

-procedure {:yields} {:phase 0,1} Init({:linear "tid"} xls:[X]bool);

+procedure {:yields} {:layer 0,1} Init({:linear "tid"} xls:[X]bool);

 ensures {:atomic} |{ A: assert xls == mapconstbool(true); currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|;

 

-procedure {:yields} {:phase 0,1} ReadCurrsize({:linear "tid"} tid: X) returns (val: int);

+procedure {:yields} {:layer 0,1} ReadCurrsize({:linear "tid"} tid: X) returns (val: int);

 ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := currsize; return true; }|;

 

-procedure {:yields} {:phase 0,1} ReadNewsize({:linear "tid"} tid: X) returns (val: int);

+procedure {:yields} {:layer 0,1} ReadNewsize({:linear "tid"} tid: X) returns (val: int);

 ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := newsize; return true; }|;

 

-procedure {:yields} {:phase 0,1} WriteNewsize({:linear "tid"} tid: X, val: int);

+procedure {:yields} {:layer 0,1} WriteNewsize({:linear "tid"} tid: X, val: int);

 ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == nil; newsize := val; ghostLock := tid; return true; }|;

 

-procedure {:yields} {:phase 0,1} WriteCurrsize({:linear "tid"} tid: X, val: int);

+procedure {:yields} {:layer 0,1} WriteCurrsize({:linear "tid"} tid: X, val: int);

 ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == tid; currsize := val; ghostLock := nil; return true; }|;

 

-procedure {:yields} {:phase 0,1} ReadCacheEntry({:linear "tid"} tid: X, index: int);

+procedure {:yields} {:layer 0,1} ReadCacheEntry({:linear "tid"} tid: X, index: int);

 ensures {:atomic} |{ A: assert 0 <= index && index < currsize; return true; }|;

 

-procedure {:yields} {:phase 0,1} WriteCacheEntry({:linear "tid"} tid: X, index: int);

+procedure {:yields} {:layer 0,1} WriteCacheEntry({:linear "tid"} tid: X, index: int);

 ensures {:right} |{ A: assert tid != nil; assert currsize <= index && ghostLock == tid; return true; }|;

 

-procedure {:yields} {:phase 0,1} acquire({:linear "tid"} tid: X);

+procedure {:yields} {:layer 0,1} acquire({:linear "tid"} tid: X);

 ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;

 

-procedure {:yields} {:phase 0,1} release({:linear "tid"} tid: X);

+procedure {:yields} {:layer 0,1} release({:linear "tid"} tid: X);

 ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|;

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 1e98fa6d..9eb11495 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -2,8 +2,8 @@
 // RUN: %diff "%s.expect" "%t"

 type X;

 const nil: X;

-var {:phase 1} l: X;

-var {:phase 1} x: int;

+var {:layer 1} l: X;

+var {:layer 1} x: int;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

@@ -12,9 +12,9 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
 }

 

 procedure Allocate() returns ({:linear "tid"} xls: X);

-ensures {:phase 1} xls != nil;

+ensures {:layer 1} xls != nil;

 

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

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

 {

     var {:linear "tid"} tid: X;

     var val: int;

@@ -29,17 +29,17 @@ procedure {:yields} {:phase 1} main()
     }

     yield;

 }

-procedure {:yields} {:phase 0,1} Lock(tid: X);

+procedure {:yields} {:layer 0,1} Lock(tid: X);

 ensures {:atomic} |{A: assume l == nil; l := tid; return true; }|;

 

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

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

 ensures {:atomic} |{A: l := nil; return true; }|;

 

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

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

 ensures {:atomic} |{A: x := val; return true; }|;

 

-procedure {:yields} {:phase 1} foo({:linear_in "tid"} tid': X, val: int)

-requires {:phase 1} tid' != nil;

+procedure {:yields} {:layer 1} foo({:linear_in "tid"} tid': X, val: int)

+requires {:layer 1} tid' != nil;

 {

     var {:linear "tid"} tid: X;

     tid := tid';

@@ -49,19 +49,19 @@ requires {:phase 1} tid' != nil;
     call tid := Yield(tid);

     call Set(val);

     call tid := Yield(tid);

-    assert {:phase 1} x == val;

+    assert {:layer 1} x == val;

     call tid := Yield(tid);

     call Unlock();

     yield;

 }

 

-procedure {:yields} {:phase 1} Yield({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X)

-requires {:phase 1} tid' != nil;

-ensures {:phase 1} tid == tid';

-ensures {:phase 1} old(l) == tid ==> old(l) == l && old(x) == x;

+procedure {:yields} {:layer 1} Yield({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X)

+requires {:layer 1} tid' != nil;

+ensures {:layer 1} tid == tid';

+ensures {:layer 1} old(l) == tid ==> old(l) == l && old(x) == x;

 {

     tid := tid';

     yield;

-    assert {:phase 1} tid != nil;

-    assert {:phase 1} (old(l) == tid ==> old(l) == l && old(x) == x);

+    assert {:layer 1} tid != nil;

+    assert {:layer 1} (old(l) == tid ==> old(l) == l && old(x) == x);

 }
\ No newline at end of file
diff --git a/Test/og/Program1.bpl b/Test/og/Program1.bpl
index 5a3ba93d..5704b680 100644
--- a/Test/og/Program1.bpl
+++ b/Test/og/Program1.bpl
@@ -1,32 +1,32 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} x:int;

+var {:layer 1} x:int;

 

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

-requires {:phase 1} x >= 5; 

-ensures {:phase 1} x >= 8; 

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

+requires {:layer 1} x >= 5; 

+ensures {:layer 1} x >= 8; 

 { 

     yield;

-    assert {:phase 1} x >= 5; 

+    assert {:layer 1} x >= 5; 

     call Incr(1); 

     yield;

-    assert {:phase 1} x >= 6; 

+    assert {:layer 1} x >= 6; 

     call Incr(1); 

     yield;

-    assert {:phase 1} x >= 7;

+    assert {:layer 1} x >= 7;

     call Incr(1); 

     yield;

-    assert {:phase 1} x >= 8; 

+    assert {:layer 1} x >= 8; 

 }

 

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

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

 { 

     yield;

     call Incr(3); 

     yield;

 }

 

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

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

 ensures {:atomic}

 |{A:

   x := x + val; return true;

diff --git a/Test/og/Program2.bpl b/Test/og/Program2.bpl
index a3fbf231..f9d28a5d 100644
--- a/Test/og/Program2.bpl
+++ b/Test/og/Program2.bpl
@@ -1,18 +1,18 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} x:int;

+var {:layer 1} x:int;

 

-procedure {:yields} {:phase 1} yield_x(n: int)

-requires {:phase 1} x >= n; 

-ensures {:phase 1} x >= n; 

+procedure {:yields} {:layer 1} yield_x(n: int)

+requires {:layer 1} x >= n; 

+ensures {:layer 1} x >= n; 

 {

     yield;

-    assert {:phase 1} x >= n;

+    assert {:layer 1} x >= n;

 }

 

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

-requires {:phase 1} x >= 5; 

-ensures {:phase 1} x >= 8; 

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

+requires {:layer 1} x >= 5; 

+ensures {:layer 1} x >= 8; 

 { 

     call yield_x(5);

     call Incr(1); 

@@ -23,14 +23,14 @@ ensures {:phase 1} x >= 8;
     call yield_x(8);

 }

 

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

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

 { 

     yield;

     call Incr(3); 

     yield;

 }

 

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

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

 ensures {:atomic}

 |{A:

   x := x + val; return true;

diff --git a/Test/og/Program3.bpl b/Test/og/Program3.bpl
index 0933afe8..ae8c6eed 100644
--- a/Test/og/Program3.bpl
+++ b/Test/og/Program3.bpl
@@ -1,17 +1,17 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} x:int;

+var {:layer 1} x:int;

 

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

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

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

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

 {

     yield;

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

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

 }

 

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

-requires {:phase 1} x >= 5; 

-ensures {:phase 1} x >= 8; 

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

+requires {:layer 1} x >= 5; 

+ensures {:layer 1} x >= 8; 

 { 

     call yield_x();

     call Incr(1); 

@@ -22,14 +22,14 @@ ensures {:phase 1} x >= 8;
     call yield_x();

 }

 

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

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

 { 

     yield;

     call Incr(3); 

     yield;

 }

 

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

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

 ensures {:atomic}

 |{A:

   x := x + val; return true;

diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl
index 5005f77c..61d4fcdc 100644
--- a/Test/og/Program4.bpl
+++ b/Test/og/Program4.bpl
@@ -13,11 +13,11 @@ function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
   x

 }

 

-var {:phase 1} a:[Tid]int;

+var {:layer 1} a:[Tid]int;

 

 procedure Allocate() returns ({:linear "tid"} tid:Tid); 

 

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

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

     var {:linear "tid"} tid:Tid;

 

     yield;

@@ -29,28 +29,28 @@ procedure {:yields} {:phase 1} main() {
     yield;

 }

 

-procedure {:yields} {:phase 1} P({:linear "tid"} tid: Tid) 

-ensures {:phase 1} a[tid] == old(a)[tid] + 1; 

+procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid) 

+ensures {:layer 1} a[tid] == old(a)[tid] + 1; 

 { 

     var t:int;

 

     yield;

-    assert {:phase 1} a[tid] == old(a)[tid];

+    assert {:layer 1} a[tid] == old(a)[tid];

     call t := Read(tid); 

     yield;

-    assert {:phase 1} a[tid] == t; 

+    assert {:layer 1} a[tid] == t; 

     call Write(tid, t + 1); 

     yield;

-    assert {:phase 1} a[tid] == t + 1; 

+    assert {:layer 1} a[tid] == t + 1; 

 }

 

-procedure {:yields} {:phase 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);

+procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);

 ensures {:atomic}

 |{A:

   val := a[tid]; return true;

 }|;

 

-procedure {:yields} {:phase 0,1} Write({:linear "tid"} tid: Tid, val: int);

+procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int);

 ensures {:atomic}

 |{A:

   a[tid] := val; return true;

diff --git a/Test/og/Program5.bpl b/Test/og/Program5.bpl
index 51d5fe3c..af87eac5 100644
--- a/Test/og/Program5.bpl
+++ b/Test/og/Program5.bpl
@@ -5,8 +5,8 @@ const unique nil: Tid;
 function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;

 function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;

 

-var {:phase 0,3} Color:int;

-var {:phase 0,3} lock:Tid;

+var {:layer 0,3} Color:int;

+var {:layer 0,3} lock:Tid;

 

 function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool

 {

@@ -26,14 +26,14 @@ function {:inline} White(i:int) returns(bool) { i == 1 }
 function {:inline} Gray(i:int) returns(bool) { i == 2 }

 function {:inline} Black(i:int) returns(bool) { i >= 3 }

 

-procedure {:yields} {:phase 2} YieldColorOnlyGetsDarker()

-ensures {:phase 2} Color >= old(Color);

+procedure {:yields} {:layer 2} YieldColorOnlyGetsDarker()

+ensures {:layer 2} Color >= old(Color);

 {

   yield;

-  assert {:phase 2} Color >= old(Color);

+  assert {:layer 2} Color >= old(Color);

 }

 

-procedure {:yields} {:phase 2,3} TopWriteBarrier({:linear "tid"} tid:Tid)

+procedure {:yields} {:layer 2,3} TopWriteBarrier({:linear "tid"} tid:Tid)

 ensures {:atomic} |{ A: assert tid != nil; goto B, C; 

                      B: assume White(Color); Color := GRAY(); return true; 

                      C: return true;}|;

@@ -46,7 +46,7 @@ ensures {:atomic} |{ A: assert tid != nil; goto B, C;
   yield;

 }

 

-procedure {:yields} {:phase 1,2} MidWriteBarrier({:linear "tid"} tid:Tid)

+procedure {:yields} {:layer 1,2} MidWriteBarrier({:linear "tid"} tid:Tid)

 ensures {:atomic} |{ A: assert tid != nil; goto B, C; 

                      B: assume White(Color); Color := GRAY(); return true; 

                      C: return true; }|;

@@ -60,18 +60,18 @@ ensures {:atomic} |{ A: assert tid != nil; goto B, C;
        yield;

 }

 

-procedure {:yields} {:phase 0,1} AcquireLock({:linear "tid"} tid: Tid);

+procedure {:yields} {:layer 0,1} AcquireLock({:linear "tid"} tid: Tid);

   ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;

 

-procedure {:yields} {:phase 0,1} ReleaseLock({:linear "tid"} tid: Tid);

+procedure {:yields} {:layer 0,1} ReleaseLock({:linear "tid"} tid: Tid);

   ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|;

 

-procedure {:yields} {:phase 0,1} SetColorLocked({:linear "tid"} tid:Tid, newCol:int); 

+procedure {:yields} {:layer 0,1} SetColorLocked({:linear "tid"} tid:Tid, newCol:int); 

   ensures {:atomic} |{A: assert tid != nil; assert lock == tid; Color := newCol; return true;}|;

 

-procedure {:yields} {:phase 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns (col:int);

+procedure {:yields} {:layer 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns (col:int);

   ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|;

 

-procedure {:yields} {:phase 1,2} GetColorNoLock() returns (col:int);

+procedure {:yields} {:layer 1,2} GetColorNoLock() returns (col:int);

   ensures {:atomic} |{A: col := Color; return true;}|;

 

diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl
index f3a4235e..f5d71caa 100644
--- a/Test/og/akash.bpl
+++ b/Test/og/akash.bpl
@@ -19,24 +19,24 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool
 }

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

-ensures {:phase 1} xls != 0;

+ensures {:layer 1} xls != 0;

 

 procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);

-ensures {:phase 1} xls == mapconstbool(true);

+ensures {:layer 1} xls == mapconstbool(true);

 

 procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);

-ensures {:phase 1} xls == mapconstbool(true);

+ensures {:layer 1} xls == mapconstbool(true);

 

-var {:phase 1} g: int;

-var {:phase 1} h: int;

+var {:layer 1} g: int;

+var {:layer 1} h: int;

 

-procedure {:yields} {:phase 0,1} SetG(val:int);

+procedure {:yields} {:layer 0,1} SetG(val:int);

 ensures {:atomic} |{A: g := val; return true; }|;

 

-procedure {:yields} {:phase 0,1} SetH(val:int);

+procedure {:yields} {:layer 0,1} SetH(val:int);

 ensures {:atomic} |{A: h := val; return true; }|;

 

-procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

 {

     var {:linear "1"} x: [int]bool;

     var {:linear "2"} y: [int]bool;

@@ -48,7 +48,7 @@ procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:line
     yield;

     call SetG(0);

     yield;

-    assert {:phase 1} g == 0 && x == mapconstbool(true);    

+    assert {:layer 1} g == 0 && x == mapconstbool(true);    

 

     yield;

     call tid_child := Allocate();

@@ -58,7 +58,7 @@ procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:line
     call SetH(0);

 

     yield;

-    assert {:phase 1} h == 0 && y == mapconstbool(true);    

+    assert {:layer 1} h == 0 && y == mapconstbool(true);    

 

     yield;

     call tid_child := Allocate();

@@ -67,8 +67,8 @@ procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:line
     yield;

 }

 

-procedure {:yields} {:phase 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) 

-requires {:phase 1} x_in != mapconstbool(false);

+procedure {:yields} {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) 

+requires {:layer 1} x_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "1"} x: [int]bool;

@@ -86,8 +86,8 @@ requires {:phase 1} x_in != mapconstbool(false);
     yield;

 }

 

-procedure {:yields} {:phase 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) 

-requires {:phase 1} y_in != mapconstbool(false);

+procedure {:yields} {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) 

+requires {:layer 1} y_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "2"} y: [int]bool;

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 (*)

diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index be519470..e6a673d8 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -15,18 +15,18 @@ function map(lmap): [int]int;
 function cons([int]bool, [int]int) : lmap;

 axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y);

 

-var {:phase 3} {:linear "mem"} g: lmap;

-var {:phase 3} lock: X;

-var {:phase 1} b: bool;

+var {:layer 3} {:linear "mem"} g: lmap;

+var {:layer 3} lock: X;

+var {:layer 1} b: bool;

 

 const p: int;

 

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

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

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

+requires {:layer 1} InvLock(lock, b);

+ensures {:layer 1} InvLock(lock, b);

 {

     yield;

-    assert {:phase 1} InvLock(lock, b);

+    assert {:layer 1} InvLock(lock, b);

 }

 

 function {:inline} InvLock(lock: X, b: bool) : bool

@@ -34,17 +34,17 @@ function {:inline} InvLock(lock: X, b: bool) : bool
     lock != nil <==> b

 }

 

-procedure {:yields} {:phase 2} Yield2()

+procedure {:yields} {:layer 2} Yield2()

 {

     yield;

 }

 

-procedure {:yields} {:phase 3} Yield3()

-requires {:phase 3} Inv(g);

-ensures {:phase 3} Inv(g);

+procedure {:yields} {:layer 3} Yield3()

+requires {:layer 3} Inv(g);

+ensures {:layer 3} Inv(g);

 {

     yield;

-    assert {:phase 3} Inv(g);

+    assert {:layer 3} Inv(g);

 }

 

 function {:inline} Inv(g: lmap) : bool

@@ -52,11 +52,11 @@ function {:inline} Inv(g: lmap) : bool
     dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4]

 }

 

-procedure {:yields} {:phase 3} P({:linear "tid"} tid: X)

-requires {:phase 1} tid != nil && InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

-requires {:phase 3} tid != nil && Inv(g);

-ensures {:phase 3} Inv(g);

+procedure {:yields} {:layer 3} P({:linear "tid"} tid: X)

+requires {:layer 1} tid != nil && InvLock(lock, b);

+ensures {:layer 1} InvLock(lock, b);

+requires {:layer 3} tid != nil && Inv(g);

+ensures {:layer 3} Inv(g);

 {

     var t: int;

     var {:linear "mem"} l: lmap;

@@ -74,49 +74,49 @@ ensures {:phase 3} Inv(g);
 }

 

 

-procedure {:yields} {:phase 2,3} TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap)

+procedure {:yields} {:layer 2,3} TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap)

 ensures {:both} |{ A: assert tid != nil && lock == tid; g := l; return true; }|;

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

+requires {:layer 1} InvLock(lock, b);

+ensures {:layer 1} InvLock(lock, b);

 {

   par Yield1() | Yield2();

   call TransferToGlobal(tid, l);

   par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 2,3} TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap)

+procedure {:yields} {:layer 2,3} TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap)

 ensures {:both} |{ A: assert tid != nil && lock == tid; l := g; return true; }|;

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

+requires {:layer 1} InvLock(lock, b);

+ensures {:layer 1} InvLock(lock, b);

 {

   par Yield1() | Yield2();

   call l := TransferFromGlobal(tid);

   par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 2,3} AcquireProtected({:linear "tid"} tid: X)

+procedure {:yields} {:layer 2,3} AcquireProtected({:linear "tid"} tid: X)

 ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;

-requires {:phase 1} tid != nil && InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

+requires {:layer 1} tid != nil && InvLock(lock, b);

+ensures {:layer 1} InvLock(lock, b);

 {

   par Yield1() | Yield2();

   call Acquire(tid);

   par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 2,3} ReleaseProtected({:linear "tid"} tid: X)

+procedure {:yields} {:layer 2,3} ReleaseProtected({:linear "tid"} tid: X)

 ensures {:left} |{ A: assert tid != nil && lock == tid; lock := nil; return true; }|;

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

+requires {:layer 1} InvLock(lock, b);

+ensures {:layer 1} InvLock(lock, b);

 {

   par Yield1() | Yield2();

   call Release(tid);

   par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 1,2} Acquire({:linear "tid"} tid: X)

-requires {:phase 1} tid != nil && InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

+procedure {:yields} {:layer 1,2} Acquire({:linear "tid"} tid: X)

+requires {:layer 1} tid != nil && InvLock(lock, b);

+ensures {:layer 1} InvLock(lock, b);

 ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|;

 {

     var status: bool;

@@ -124,7 +124,7 @@ ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|;
 

     par Yield1();

     L: 

-	assert {:phase 1} InvLock(lock, b);

+	assert {:layer 1} InvLock(lock, b);

         call status := CAS(tid, false, true);

 	par Yield1();

         goto A, B;

@@ -139,36 +139,36 @@ ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|;
 	goto L;

 }

 

-procedure {:yields} {:phase 1,2} Release({:linear "tid"} tid: X)

+procedure {:yields} {:layer 1,2} Release({:linear "tid"} tid: X)

 ensures {:atomic} |{ A: lock := nil; return true; }|;

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

+requires {:layer 1} InvLock(lock, b);

+ensures {:layer 1} InvLock(lock, b);

 {

     par Yield1();

     call CLEAR(tid, false);

     par Yield1();

 }

 

-procedure {:yields} {:phase 0,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap);

+procedure {:yields} {:layer 0,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap);

 ensures {:atomic} |{ A: g := l; return true; }|;

 

-procedure {:yields} {:phase 0,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap);

+procedure {:yields} {:layer 0,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap);

 ensures {:atomic} |{ A: l := g; return true; }|;

 

-procedure {:yields} {:phase 0,3} Load({:linear "mem"} l: lmap, a: int) returns (v: int);

+procedure {:yields} {:layer 0,3} Load({:linear "mem"} l: lmap, a: int) returns (v: int);

 ensures {:both} |{ A: v := map(l)[a]; return true; }|;

 

-procedure {:yields} {:phase 0,3} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);

+procedure {:yields} {:layer 0,3} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);

 ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;

 

-procedure {:yields} {:phase 0,1} CAS(tid: X, prev: bool, next: bool) returns (status: bool);

+procedure {:yields} {:layer 0,1} CAS(tid: X, prev: bool, next: bool) returns (status: bool);

 ensures {:atomic} |{ 

 A: goto B, C; 

 B: assume b == prev; b := next; status := true; lock := tid; return true; 

 C: status := false; return true; 

 }|;

 

-procedure {:yields} {:phase 0,1} CLEAR(tid: X, next: bool);

+procedure {:yields} {:layer 0,1} CLEAR(tid: X, next: bool);

 ensures {:atomic} |{ 

 A: b := next; lock := nil; return true; 

 }|;

diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index eae47e12..bd8c6ef7 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.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 == 3;

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

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

 {

   yield;

   call Set(3);

   yield;

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

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

 }

 

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

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

 {

   call PC();

 }

 

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

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

 {

   call PC();

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

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

 }

 

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

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

 {

   yield;

   while (*)

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index 228062a3..4b6692c5 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -20,26 +20,26 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
   xs

 }

 

-var {:phase 1} x: int;

-var {:phase 1} l: [X]bool;

+var {:layer 1} x: int;

+var {:layer 1} l: [X]bool;

 

 procedure Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);

 ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();

 

 procedure Allocate() returns ({:linear "tid"} xls: [X]bool);

 

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

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

 ensures {:atomic} |{A: x := v; return true; }|;

 

-procedure {:yields} {:phase 0,1} Lock(tidls: [X]bool);

+procedure {:yields} {:layer 0,1} Lock(tidls: [X]bool);

 ensures {:atomic} |{A: assume l == None(); l := tidls; return true; }|;

 

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

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

 ensures {:atomic} |{A: l := None(); return true; }|;

 

 

-procedure {:yields} {:phase 1} main({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) 

-requires {:phase 1} tidls' != None() && xls' == All();

+procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) 

+requires {:layer 1} tidls' != None() && xls' == All();

 {

     var {:linear "tid"} tidls: [X]bool;

     var {:linear "x"} xls: [X]bool;

@@ -52,8 +52,8 @@ requires {:phase 1} tidls' != None() && xls' == All();
     yield;

     call Set(42);

     yield;

-    assert {:phase 1} xls == All();

-    assert {:phase 1} x == 42;

+    assert {:layer 1} xls == All();

+    assert {:layer 1} x == 42;

     call xls1, xls2 := Split(xls);

     call lsChild := Allocate();

     assume (lsChild != None());

@@ -66,8 +66,8 @@ requires {:phase 1} tidls' != None() && xls' == All();
     yield;

 }

 

-procedure {:yields} {:phase 1} thread({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool)

-requires {:phase 1} tidls' != None() && xls' != None();

+procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool)

+requires {:layer 1} tidls' != None() && xls' != None();

 {

     var {:linear "x"} xls: [X]bool;

     var {:linear "tid"} tidls: [X]bool;

@@ -78,12 +78,12 @@ requires {:phase 1} tidls' != None() && xls' != None();
     yield;

     call Lock(tidls);

     yield;

-    assert {:phase 1} tidls != None() && xls != None();

+    assert {:layer 1} tidls != None() && xls != None();

     call Set(0);

     yield;

-    assert {:phase 1} tidls != None() && xls != None();

-    assert {:phase 1} x == 0;

-    assert {:phase 1} tidls != None() && xls != None();

+    assert {:layer 1} tidls != None() && xls != None();

+    assert {:layer 1} x == 0;

+    assert {:layer 1} tidls != None() && xls != None();

     call Unlock();

     yield;

 }

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index 11d24605..93ede868 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -20,8 +20,8 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
   xs

 }

 

-var {:phase 1} x: int;

-var {:phase 1} l: X;

+var {:layer 1} x: int;

+var {:layer 1} l: X;

 const nil: X;

 

 procedure Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);

@@ -30,17 +30,17 @@ ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
 procedure Allocate() returns ({:linear "tid"} xls: X);

 ensures xls != nil;

 

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

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

 ensures {:atomic} |{A: x := v; return true; }|;

 

-procedure {:yields} {:phase 0,1} Lock(tidls: X);

+procedure {:yields} {:layer 0,1} Lock(tidls: X);

 ensures {:atomic} |{A: assume l == nil; l := tidls; return true; }|;

 

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

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

 ensures {:atomic} |{A: l := nil; return true; }|;

 

-procedure {:yields} {:phase 1} main({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool) 

-requires {:phase 1} tidls' != nil && xls' == All();

+procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool) 

+requires {:layer 1} tidls' != nil && xls' == All();

 {

     var {:linear "tid"} tidls: X;

     var {:linear "x"} xls: [X]bool;

@@ -54,8 +54,8 @@ requires {:phase 1} tidls' != nil && xls' == All();
     yield;

     call Set(42);

     yield;

-    assert {:phase 1} xls == All();

-    assert {:phase 1} x == 42;

+    assert {:layer 1} xls == All();

+    assert {:layer 1} x == 42;

     call xls1, xls2 := Split(xls);

     call lsChild := Allocate();

     yield;

@@ -66,8 +66,8 @@ requires {:phase 1} tidls' != nil && xls' == All();
     yield;

 }

 

-procedure {:yields} {:phase 1} thread({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool)

-requires {:phase 1} tidls' != nil && xls' != None();

+procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool)

+requires {:layer 1} tidls' != nil && xls' != None();

 {

     var {:linear "x"} xls: [X]bool;

     var {:linear "tid"} tidls: X;

@@ -78,13 +78,13 @@ requires {:phase 1} tidls' != nil && xls' != None();
     yield;

     call Lock(tidls);

     yield;

-    assert {:phase 1} tidls != nil && xls != None();

+    assert {:layer 1} tidls != nil && xls != None();

     call Set(0);

     yield;

-    assert {:phase 1} tidls != nil && xls != None();

-    assert {:phase 1} x == 0;

+    assert {:layer 1} tidls != nil && xls != None();

+    assert {:layer 1} x == 0;

     yield;

-    assert {:phase 1} tidls != nil && xls != None();

+    assert {:layer 1} tidls != nil && xls != None();

     call Unlock();

     yield;

 }

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

 

diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index 86c382d8..db563cce 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -1,8 +1,8 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 2} b: bool;

+var {:layer 2} b: bool;

 

-procedure {:yields} {:phase 2} main()

+procedure {:yields} {:layer 2} main()

 {

     yield;

     while (*)

@@ -13,7 +13,7 @@ procedure {:yields} {:phase 2} main()
     yield;

 }

 

-procedure {:yields} {:phase 2} Customer()

+procedure {:yields} {:layer 2} Customer()

 {

     yield;

     while (*) 

@@ -26,7 +26,7 @@ procedure {:yields} {:phase 2} Customer()
     yield;

 }

 

-procedure {:yields} {:phase 1,2} Enter() 

+procedure {:yields} {:layer 1,2} Enter() 

 ensures {:atomic} |{ A: assume !b; b := true; return true; }|;

 {

     var status: bool;

@@ -46,12 +46,12 @@ ensures {:atomic} |{ A: assume !b; b := true; return true; }|;
 	goto L;

 }

 

-procedure {:yields} {:phase 0,2} CAS(prev: bool, next: bool) returns (status: bool);

+procedure {:yields} {:layer 0,2} 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,2} Leave();

+procedure {:yields} {:layer 0,2} Leave();

 ensures {:atomic} |{ A: b := false; return true; }|;

diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index 354821e7..7f0dde84 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -1,8 +1,8 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 2} b: int;

+var {:layer 2} b: int;

 

-procedure {:yields} {:phase 2} main()

+procedure {:yields} {:layer 2} main()

 {

     yield;

     while (*)

@@ -13,7 +13,7 @@ procedure {:yields} {:phase 2} main()
     yield;

 }

 

-procedure {:yields} {:phase 2} Customer()

+procedure {:yields} {:layer 2} Customer()

 {

     yield;

     while (*) 

@@ -26,7 +26,7 @@ procedure {:yields} {:phase 2} Customer()
     yield;

 }

 

-procedure {:yields} {:phase 1,2} Enter() 

+procedure {:yields} {:layer 1,2} Enter() 

 ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|;

 {

     var _old, curr: int;

@@ -49,15 +49,15 @@ ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|;
     yield;

 }

 

-procedure {:yields} {:phase 0,2} Read() returns (val: int);

+procedure {:yields} {:layer 0,2} Read() returns (val: int);

 ensures {:atomic} |{ A: val := b; return true; }|;

 

-procedure {:yields} {:phase 0,2} CAS(prev: int, next: int) returns (_old: int);

+procedure {:yields} {:layer 0,2} CAS(prev: int, next: int) returns (_old: int);

 ensures {:atomic} |{ 

 A: _old := b; goto B, C; 

 B: assume _old == prev; b := next; return true; 

 C: assume _old != prev; return true; 

 }|;

 

-procedure {:yields} {:phase 0,2} Leave();

+procedure {:yields} {:layer 0,2} Leave();

 ensures {:atomic} |{ A: b := 0; return true; }|;

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index a522f304..0f56dd7e 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -20,7 +20,7 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
 

 axiom (max > 0);

 

-procedure {:yields} {:phase 0} acquire(i : int, {:linear "tid"} tid: X);

+procedure {:yields} {:layer 0} acquire(i : int, {:linear "tid"} tid: X);

 ensures {:right} |{ A: 

                       assert 0 <= i && i < max;

                       assert tid != nil && tid != done;

@@ -30,7 +30,7 @@ ensures {:right} |{ A:
                     }|;

 

 

-procedure {:yields} {:phase 0} release(i : int, {:linear "tid"} tid: X);

+procedure {:yields} {:layer 0} release(i : int, {:linear "tid"} tid: X);

 ensures {:left} |{ A: 

                      assert 0 <= i && i < max;

                      assert lock[i] == tid;

@@ -40,7 +40,7 @@ ensures {:left} |{ A:
                     }|;

 

 

-procedure {:yields} {:phase 0,1} getElt(j : int, {:linear "tid"} tid: X) returns (elt_j:int);

+procedure {:yields} {:layer 0,1} getElt(j : int, {:linear "tid"} tid: X) returns (elt_j:int);

 ensures {:both} |{ A: 

                      assert 0 <= j && j < max;

                      assert lock[j] == tid;

@@ -50,7 +50,7 @@ ensures {:both} |{ A:
                     }|;

 

 

-procedure {:yields} {:phase 0,1} setElt(j : int, x : int, {:linear "tid"} tid: X);

+procedure {:yields} {:layer 0,1} setElt(j : int, x : int, {:linear "tid"} tid: X);

 ensures {:both} |{ A: 

                      assert x != null;

                      assert owner[j] == nil;

@@ -63,7 +63,7 @@ ensures {:both} |{ A:
                     }|;

 

 

-procedure {:yields} {:phase 0} setEltToNull(j : int, {:linear "tid"} tid: X);

+procedure {:yields} {:layer 0} setEltToNull(j : int, {:linear "tid"} tid: X);

 ensures {:left} |{ A: 

                      assert owner[j] == tid;

                      assert 0 <= j && j < max;

@@ -75,7 +75,7 @@ ensures {:left} |{ A:
                      return true;

                     }|;

 

-procedure {:yields} {:phase 0} setValid(j : int, {:linear "tid"} tid: X);

+procedure {:yields} {:layer 0} setValid(j : int, {:linear "tid"} tid: X);

 ensures {:both} |{ A: 

                      assert 0 <= j && j < max;

                      assert lock[j] == tid;

@@ -86,7 +86,7 @@ ensures {:both} |{ A:
                      return true;

                     }|;

 

-procedure {:yields} {:phase 0} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool);

+procedure {:yields} {:layer 0} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool);

 ensures {:both} |{ A: 

                        assert 0 <= j && j < max;

                        assert lock[j] == tid;

@@ -95,9 +95,9 @@ ensures {:both} |{ A:
                        return true;

                     }|;

 

-procedure {:yields} {:phase 1} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int)

-requires {:phase 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

-ensures {:phase 1} Inv(valid, elt, owner);

+procedure {:yields} {:layer 1} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int)

+requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

+ensures {:layer 1} Inv(valid, elt, owner);

 ensures {:right}  |{   A: assert tid != nil && tid != done; 

                           assert x != null; 

 			  goto B, C;

@@ -118,8 +118,8 @@ ensures {:right}  |{   A: assert tid != nil && tid != done;
 

 	j := 0;

 	while(j < max)

-        invariant {:phase 1} Inv(valid, elt, owner);

-	invariant {:phase 1} 0 <= j;

+        invariant {:layer 1} Inv(valid, elt, owner);

+	invariant {:layer 1} 0 <= j;

 	{

                 call acquire(j, tid);

                 call elt_j := getElt(j, tid);

@@ -144,11 +144,11 @@ ensures {:right}  |{   A: assert tid != nil && tid != done;
 	return;

 }

 

-procedure {:yields} {:phase 2} Insert(x : int, {:linear "tid"} tid: X) returns (result : bool) 

-requires {:phase 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

-ensures {:phase 1} Inv(valid, elt, owner);

-requires {:phase 2} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

-ensures {:phase 2} Inv(valid, elt, owner);

+procedure {:yields} {:layer 2} Insert(x : int, {:linear "tid"} tid: X) returns (result : bool) 

+requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

+ensures {:layer 1} Inv(valid, elt, owner);

+requires {:layer 2} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

+ensures {:layer 2} Inv(valid, elt, owner);

 ensures {:atomic}  |{ var r:int;

                         A: goto B, C;

                         B: assume (0 <= r && r < max); 

@@ -171,11 +171,11 @@ ensures {:atomic}  |{ var r:int;
 		return;

 	}

         par Yield1();

-        assert {:phase 1} i != -1;

-        assert {:phase 2} i != -1;

+        assert {:layer 1} i != -1;

+        assert {:layer 2} i != -1;

 	call acquire(i, tid);

-        assert {:phase 2} elt[i] == x;

-	assert {:phase 2}  valid[i] == false;

+        assert {:layer 2} elt[i] == x;

+	assert {:layer 2}  valid[i] == false;

         call setValid(i, tid);   

 	call release(i, tid);

 	result := true; 

@@ -183,11 +183,11 @@ ensures {:atomic}  |{ var r:int;
 	return;

 }

 

-procedure {:yields} {:phase 2} InsertPair(x : int, y : int, {:linear "tid"} tid: X) returns (result : bool)

-requires {:phase 1} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 

-ensures {:phase 1} Inv(valid, elt, owner);

-requires {:phase 2} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 

-ensures {:phase 2} Inv(valid, elt, owner);

+procedure {:yields} {:layer 2} InsertPair(x : int, y : int, {:linear "tid"} tid: X) returns (result : bool)

+requires {:layer 1} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 

+ensures {:layer 1} Inv(valid, elt, owner);

+requires {:layer 2} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 

+ensures {:layer 2} Inv(valid, elt, owner);

 ensures {:atomic}  |{ var rx:int;

                         var ry:int;

                         A: goto B, C;

@@ -234,13 +234,13 @@ ensures {:atomic}  |{ var rx:int;
 	}

 

         par Yield1();

-        assert {:phase 2} i != -1 && j != -1;

+        assert {:layer 2} i != -1 && j != -1;

 	call acquire(i, tid);

 	call acquire(j, tid);

-        assert {:phase 2} elt[i] == x;

-        assert {:phase 2} elt[j] == y;

-	assert {:phase 2}  valid[i] == false;

-	assert {:phase 2}  valid[j] == false;

+        assert {:layer 2} elt[i] == x;

+        assert {:layer 2} elt[j] == y;

+	assert {:layer 2}  valid[i] == false;

+	assert {:layer 2}  valid[j] == false;

         call setValid(i, tid);   

         call setValid(j, tid);   

 	call release(j, tid);

@@ -250,11 +250,11 @@ ensures {:atomic}  |{ var rx:int;
 	return;

 }

 

-procedure {:yields} {:phase 2} LookUp(x : int, {:linear "tid"} tid: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool)

-requires {:phase 1} {:phase 2} old_valid == valid && old_elt == elt;

-requires {:phase 1} {:phase 2} Inv(valid, elt, owner);

-requires {:phase 1} {:phase 2} (tid != nil && tid != done);

-ensures {:phase 1} {:phase 2} Inv(valid, elt, owner);

+procedure {:yields} {:layer 2} LookUp(x : int, {:linear "tid"} tid: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool)

+requires {:layer 1} {:layer 2} old_valid == valid && old_elt == elt;

+requires {:layer 1} {:layer 2} Inv(valid, elt, owner);

+requires {:layer 1} {:layer 2} (tid != nil && tid != done);

+ensures {:layer 1} {:layer 2} Inv(valid, elt, owner);

 ensures {:atomic}  |{ A: assert tid != nil && tid != done; 

                           assert x != null;

                           assume found ==> (exists ii:int :: 0 <= ii && ii < max && valid[ii] && elt[ii] == x);

@@ -270,10 +270,10 @@ ensures {:atomic}  |{ A: assert tid != nil && tid != done;
 	j := 0;

 

 	while(j < max)

-        invariant {:phase 1} {:phase 2} Inv(valid, elt, owner);

-        invariant {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < j ==> !(old_valid[ii] && old_elt[ii] == x));

-	invariant {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

-	invariant {:phase 1} {:phase 2} 0 <= j;

+        invariant {:layer 1} {:layer 2} Inv(valid, elt, owner);

+        invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < j ==> !(old_valid[ii] && old_elt[ii] == x));

+	invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

+	invariant {:layer 1} {:layer 2} 0 <= j;

 	{

                 call acquire(j, tid);

                 call isThere := isEltThereAndValid(j, x, tid);

@@ -294,20 +294,20 @@ ensures {:atomic}  |{ A: assert tid != nil && tid != done;
 	return;

 }

 

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

-requires {:phase 1} Inv(valid, elt, owner);

-ensures {:phase 1} Inv(valid, elt, owner);

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

+requires {:layer 1} Inv(valid, elt, owner);

+ensures {:layer 1} Inv(valid, elt, owner);

 {

 	yield;

-	assert {:phase 1} Inv(valid, elt, owner);

+	assert {:layer 1} Inv(valid, elt, owner);

 }

 

-procedure {:yields} {:phase 2} Yield12()

-requires {:phase 1} {:phase 2} Inv(valid, elt, owner);

-ensures {:phase 1} {:phase 2} Inv(valid, elt, owner);

+procedure {:yields} {:layer 2} Yield12()

+requires {:layer 1} {:layer 2} Inv(valid, elt, owner);

+ensures {:layer 1} {:layer 2} Inv(valid, elt, owner);

 {

         yield;

-        assert {:phase 1} {:phase 2} Inv(valid, elt, owner);

+        assert {:layer 1} {:layer 2} Inv(valid, elt, owner);

 }

 

 function {:inline} Inv(valid: [int]bool, elt: [int]int, owner: [int]X): (bool)

@@ -315,10 +315,10 @@ function {:inline} Inv(valid: [int]bool, elt: [int]int, owner: [int]X): (bool)
    (forall i:int :: 0 <= i && i < max ==> (elt[i] == null <==> (!valid[i] && owner[i] == nil)))

 }

 

-procedure {:yields} {:phase 2} YieldLookUp(old_valid: [int]bool, old_elt: [int]int)

-requires {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

-ensures {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

+procedure {:yields} {:layer 2} YieldLookUp(old_valid: [int]bool, old_elt: [int]int)

+requires {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

+ensures {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

 {

     yield;

-    assert {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

+    assert {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

 }

diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index 537a5f4b..3faa9156 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -2,7 +2,7 @@
 // RUN: %diff "%s.expect" "%t"

 function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;

 

-var {:phase 1} g:int;

+var {:layer 1} g:int;

 

 function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool

 {

@@ -13,25 +13,25 @@ procedure Allocate_Perm({:linear_in "Perm"} Permissions: [int]bool) returns ({:l
 requires Permissions == mapconstbool(true);

 ensures xls == mapconstbool(true);

 

-procedure {:yields} {:phase 1} PB({:linear_in "Perm"} permVar_in:[int]bool)

-requires {:phase 1} permVar_in[0] && g == 0;

+procedure {:yields} {:layer 1} PB({:linear_in "Perm"} permVar_in:[int]bool)

+requires {:layer 1} permVar_in[0] && g == 0;

 {

   var {:linear "Perm"} permVar_out: [int]bool;

   permVar_out := permVar_in;

 

   yield;

-  assert {:phase 1} permVar_out[0];

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

+  assert {:layer 1} permVar_out[0];

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

 

   call IncrG();

 

   yield;

-  assert {:phase 1} permVar_out[0];

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

+  assert {:layer 1} permVar_out[0];

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

 }

 

-procedure {:yields} {:phase 1} Main({:linear_in "Perm"} Permissions: [int]bool)

-requires {:phase 0,1} Permissions == mapconstbool(true);

+procedure {:yields} {:layer 1} Main({:linear_in "Perm"} Permissions: [int]bool)

+requires {:layer 0,1} Permissions == mapconstbool(true);

 {

   var {:linear "Perm"} permVar_out: [int]bool;

 

@@ -42,8 +42,8 @@ requires {:phase 0,1} Permissions == mapconstbool(true);
   yield;

 }

 

-procedure {:yields} {:phase 0,1} SetG(val:int);

+procedure {:yields} {:layer 0,1} SetG(val:int);

 ensures {:atomic} |{A: g := val; return true; }|;

 

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

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

 ensures {:atomic} |{A: g := g + 1; return true; }|;

diff --git a/Test/og/one.bpl b/Test/og/one.bpl
index 2da898d6..45cbbda3 100644
--- a/Test/og/one.bpl
+++ b/Test/og/one.bpl
@@ -1,18 +1,18 @@
 // RUN: %boogie -noinfer "%s" > "%t"

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

-var {:phase 1} x:int;

+var {:layer 1} x:int;

 

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

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

 ensures {:atomic}

 |{A:

   x := v; return true;

 }|;

 

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

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

 {

   yield;

   call Set(5);

   yield;

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

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

 }

 

diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
index 6b2ea3a8..96231f5b 100644
--- a/Test/og/parallel1.bpl
+++ b/Test/og/parallel1.bpl
@@ -1,43 +1,43 @@
 // 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 == 3;

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

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

 {

   yield;

   call Set(3);

   yield;

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

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

 }

 

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

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

 {

   call PC();

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

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

   yield;

 }

 

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

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

 {

   yield;

   while (*)

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 1906d00b..20de0875 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} a:[int]int;

+var {:layer 1} a:[int]int;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

 function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

@@ -10,10 +10,10 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

-procedure {:yields} {:phase 0,1} Write(idx: int, val: int);

+procedure {:yields} {:layer 0,1} Write(idx: int, val: int);

 ensures {:atomic} |{A: a[idx] := val; return true; }|;

 

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

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

 {

     var {:linear "tid"} i: int;

     var {:linear "tid"} j: int;

@@ -23,29 +23,29 @@ procedure {:yields} {:phase 1} main()
     par i := u(i) | j := u(j);

 }

 

-procedure {:yields} {:phase 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)

 {

     i := i';

 

     yield;

     call Write(i, 42);

     call Yield(i);

-    assert {:phase 1} a[i] == 42;

+    assert {:layer 1} a[i] == 42;

 }

 

-procedure {:yields} {:phase 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) 

+procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) 

 {

     i := i';

 

     yield;

     call Write(i, 42);

     yield;

-    assert {:phase 1} a[i] == 42;

+    assert {:layer 1} a[i] == 42;

 }

 

-procedure {:yields} {:phase 1} Yield({:linear "tid"} i: int)

-ensures {:phase 1} old(a)[i] == a[i];

+procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int)

+ensures {:layer 1} old(a)[i] == a[i];

 {

     yield;

-    assert {:phase 1} old(a)[i] == a[i];

+    assert {:layer 1} old(a)[i] == a[i];

 }
\ No newline at end of file
diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index f061f8be..bb9c631b 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} a:int;

+var {:layer 1} a:int;

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

@@ -10,7 +10,7 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
   MapConstBool(false)[x := true]

 }

 

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

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

 {

   var {:linear "tid"} i: int;

   var {:linear "tid"} j: int;

@@ -19,19 +19,19 @@ procedure {:yields} {:phase 1} main()
   par i := t(i) | j := t(j);

 }

 

-procedure {:yields} {:phase 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)

 {

   i := i';

   call Yield();

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

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

   call Incr();

   yield;

 }

 

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

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

 ensures {:atomic} |{A: a := a + 1; return true; }|;

 

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

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

 {

   yield;

 }

diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index 751cc666..7ef565e1 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} a:[int]int;

+var {:layer 1} a:[int]int;

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

@@ -10,10 +10,10 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
   MapConstBool(false)[x := true]

 }

 

-procedure {:yields} {:phase 0,1} Write(idx: int, val: int);

+procedure {:yields} {:layer 0,1} Write(idx: int, val: int);

 ensures {:atomic} |{A: a[idx] := val; return true; }|;

 

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

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

 {

     var {:linear "tid"} i: int;

     var {:linear "tid"} j: int;

@@ -23,29 +23,29 @@ procedure {:yields} {:phase 1} main()
     par i := u(i) | j := u(j);

 }

 

-procedure {:yields} {:phase 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)

 {

     i := i';

 

     yield;

     call Write(i, 42);

     call Yield(i);

-    assert {:phase 1} a[i] == 42;

+    assert {:layer 1} a[i] == 42;

 }

 

-procedure {:yields} {:phase 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) 

+procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) 

 {

     i := i';

 

     yield;

     call Write(i, 42);

     yield;

-    assert {:phase 1} a[i] == 42;

+    assert {:layer 1} a[i] == 42;

 }

 

-procedure {:yields} {:phase 1} Yield({:linear "tid"} i: int)

-ensures {:phase 1} old(a)[i] == a[i];

+procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int)

+ensures {:layer 1} old(a)[i] == a[i];

 {

     yield;

-    assert {:phase 1} old(a)[i] == a[i];

+    assert {:layer 1} old(a)[i] == a[i];

 }
\ No newline at end of file
diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index 4df74778..66ae5285 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} x: int;

+var {:layer 1} x: int;

 function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;

 

 function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool;

@@ -14,10 +14,10 @@ procedure Split({:linear_in "Perm"} xls: [int]bool) returns ({:linear "Perm"} xl
   ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);

 

 

-procedure {:yields} {:phase 1} mainE({:linear_in "Perm"} permVar_in: [int]bool)

-   free requires {:phase 1} permVar_in == ch_mapconstbool(true);

-   free requires {:phase 1} permVar_in[0];

-   free requires {:phase 1} x == 0;

+procedure {:yields} {:layer 1} mainE({:linear_in "Perm"} permVar_in: [int]bool)

+   free requires {:layer 1} permVar_in == ch_mapconstbool(true);

+   free requires {:layer 1} permVar_in[0];

+   free requires {:layer 1} x == 0;

 {

     var {:linear "Perm"} permVar_out: [int]bool;

     var {:linear "Perm"} permVarOut2: [int]bool;

@@ -25,33 +25,33 @@ procedure {:yields} {:phase 1} mainE({:linear_in "Perm"} permVar_in: [int]bool)
     permVar_out := permVar_in;

 

     yield;

-    assert {:phase 1} x == 0;

-    assert {:phase 1} permVar_out[0];

-    assert {:phase 1} permVar_out == ch_mapconstbool(true);

+    assert {:layer 1} x == 0;

+    assert {:layer 1} permVar_out[0];

+    assert {:layer 1} permVar_out == ch_mapconstbool(true);

 

     call permVar_out, permVarOut2 := Split(permVar_out);

     async call foo(permVarOut2);

     yield;

 }

 

-procedure {:yields} {:phase 1} foo({:linear_in "Perm"} permVar_in: [int]bool) 

-  free requires {:phase 1} permVar_in != ch_mapconstbool(false);

-  free requires {:phase 1} permVar_in[1];

-  requires {:phase 1} x == 0;

+procedure {:yields} {:layer 1} foo({:linear_in "Perm"} permVar_in: [int]bool) 

+  free requires {:layer 1} permVar_in != ch_mapconstbool(false);

+  free requires {:layer 1} permVar_in[1];

+  requires {:layer 1} x == 0;

 {

   var {:linear "Perm"} permVar_out: [int]bool;

   permVar_out := permVar_in;

   

   yield;

-  assert {:phase 1} permVar_out[1];

-  assert {:phase 1} x == 0;

+  assert {:layer 1} permVar_out[1];

+  assert {:layer 1} x == 0;

 

   call Incr();

 

   yield;

-  assert {:phase 1} permVar_out[1];

-  assert {:phase 1} x == 1;

+  assert {:layer 1} permVar_out[1];

+  assert {:layer 1} x == 1;

 }

 

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

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

 ensures {:atomic} |{A: x := x + 1; return true; }|;
\ No newline at end of file
diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index 3730d490..305f1ed1 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -19,24 +19,24 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool
 }

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

-ensures {:phase 1} xls != 0;

+ensures {:layer 1} xls != 0;

 

 procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);

-ensures {:phase 1} xls == mapconstbool(true);

+ensures {:layer 1} xls == mapconstbool(true);

 

 procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);

-ensures {:phase 1} xls == mapconstbool(true);

+ensures {:layer 1} xls == mapconstbool(true);

 

-var {:phase 1} g: int;

-var {:phase 1} h: int;

+var {:layer 1} g: int;

+var {:layer 1} h: int;

 

-procedure {:yields} {:phase 0,1} SetG(val:int);

+procedure {:yields} {:layer 0,1} SetG(val:int);

 ensures {:atomic} |{A: g := val; return true; }|;

 

-procedure {:yields} {:phase 0,1} SetH(val:int);

+procedure {:yields} {:layer 0,1} SetH(val:int);

 ensures {:atomic} |{A: h := val; return true; }|;

 

-procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

 {

     var {:linear "1"} x: [int]bool;

     var {:linear "2"} y: [int]bool;

@@ -48,22 +48,22 @@ procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:line
     yield;

     call SetG(0);

     yield;

-    assert {:phase 1} x == mapconstbool(true);    

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

+    assert {:layer 1} x == mapconstbool(true);    

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

 

     yield;

     call tid_child := Allocate();

     async call B(tid_child, x);

 

     yield;

-    assert {:phase 1} x == mapconstbool(true);    

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

+    assert {:layer 1} x == mapconstbool(true);    

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

 

     yield;

     call SetH(0);

 

     yield;

-    assert {:phase 1} h == 0 && y == mapconstbool(true);    

+    assert {:layer 1} h == 0 && y == mapconstbool(true);    

 

     yield;

     call tid_child := Allocate();

@@ -72,8 +72,8 @@ procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:line
     yield;

 }

 

-procedure {:yields} {:phase 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) 

-requires {:phase 1} x_in != mapconstbool(false);

+procedure {:yields} {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) 

+requires {:layer 1} x_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "1"} x: [int]bool;

@@ -85,8 +85,8 @@ requires {:phase 1} x_in != mapconstbool(false);
     yield;

 }

 

-procedure {:yields} {:phase 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) 

-requires {:phase 1} y_in != mapconstbool(false);

+procedure {:yields} {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) 

+requires {:layer 1} y_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "2"} y: [int]bool;

diff --git a/Test/og/termination.bpl b/Test/og/termination.bpl
index 35064f77..2d5542dd 100644
--- a/Test/og/termination.bpl
+++ b/Test/og/termination.bpl
@@ -1,12 +1,12 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-procedure {:yields} {:phase 0} X();

+procedure {:yields} {:layer 0} X();

 ensures {:atomic} |{ A: return true; }|;

 

-procedure {:yields} {:phase 0} Y();

+procedure {:yields} {:layer 0} Y();

 ensures {:left} |{ A: return true; }|;

 

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

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

   yield;

   call X();

   while (*)

@@ -14,5 +14,5 @@ procedure {:yields} {:phase 1} main() {
     call Y();

   }

   yield;

-  assert {:phase 1} true;

+  assert {:layer 1} true;

 }

diff --git a/Test/og/termination2.bpl b/Test/og/termination2.bpl
index d0d88a22..840c27c1 100644
--- a/Test/og/termination2.bpl
+++ b/Test/og/termination2.bpl
@@ -1,19 +1,19 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-procedure {:yields} {:phase 0} X();

+procedure {:yields} {:layer 0} X();

 ensures {:atomic} |{ A: return true; }|;

 

-procedure {:yields} {:phase 0} Y();

+procedure {:yields} {:layer 0} Y();

 ensures {:left} |{ A: return true; }|;

 

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

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

   yield;

   call X();

   while (*)

-  invariant {:terminates} {:phase 1} true;

+  invariant {:terminates} {:layer 1} true;

   {

     call Y();

   }

   yield;

-  assert {:phase 1} true;

+  assert {:layer 1} true;

 }

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 9c1b7c9a..70fe1d4c 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -8,10 +8,10 @@ axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
 type X;

 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;

 const nil: X;

-var {:phase 2} t: int;

-var {:phase 2} s: int;

-var {:phase 2} cs: X;

-var {:phase 2} T: [int]bool;

+var {:layer 2} t: int;

+var {:layer 2} s: int;

+var {:layer 2} cs: X;

+var {:layer 2} T: [int]bool;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

@@ -34,10 +34,10 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)
 }

 

 procedure Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

-ensures {:phase 1} {:phase 2} xl != nil;

+ensures {:layer 1} {:layer 2} xl != nil;

 

-procedure {:yields} {:phase 2} main({:linear_in "tid"} xls':[X]bool)

-requires {:phase 2} xls' == mapconstbool(true);

+procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)

+requires {:layer 2} xls' == mapconstbool(true);

 {

     var {:linear "tid"} tid: X;

     var {:linear "tid"} xls: [X]bool;

@@ -50,8 +50,8 @@ requires {:phase 2} xls' == mapconstbool(true);
     par Yield1() | Yield2();

 

     while (*)

-    invariant {:phase 1} Inv1(T, t);

-    invariant {:phase 2} Inv2(T, s, cs);

+    invariant {:layer 1} Inv1(T, t);

+    invariant {:layer 2} Inv2(T, s, cs);

     {

         call xls, tid := Allocate(xls);

         async call Customer(tid);

@@ -60,14 +60,14 @@ requires {:phase 2} xls' == mapconstbool(true);
     par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 2} Customer({:linear_in "tid"} tid: X)

-requires {:phase 1} Inv1(T, t);

-requires {:phase 2} tid != nil && Inv2(T, s, cs);

+procedure {:yields} {:layer 2} Customer({:linear_in "tid"} tid: X)

+requires {:layer 1} Inv1(T, t);

+requires {:layer 2} tid != nil && Inv2(T, s, cs);

 {

     par Yield1() | Yield2();    

     while (*) 

-    invariant {:phase 1} Inv1(T, t);

-    invariant {:phase 2} Inv2(T, s, cs);

+    invariant {:layer 1} Inv1(T, t);

+    invariant {:layer 2} Inv2(T, s, cs);

     {

         call Enter(tid);

         par Yield1() | Yield2() | YieldSpec(tid);

@@ -77,11 +77,11 @@ requires {:phase 2} tid != nil && Inv2(T, s, cs);
     par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 2} Enter({:linear "tid"} tid: X)

-requires {:phase 1} Inv1(T, t);

-ensures {:phase 1} Inv1(T,t);

-requires {:phase 2} tid != nil && Inv2(T, s, cs);

-ensures {:phase 2} Inv2(T, s, cs) && cs == tid;

+procedure {:yields} {:layer 2} Enter({:linear "tid"} tid: X)

+requires {:layer 1} Inv1(T, t);

+ensures {:layer 1} Inv1(T,t);

+requires {:layer 2} tid != nil && Inv2(T, s, cs);

+ensures {:layer 2} Inv2(T, s, cs) && cs == tid;

 {

     var m: int;

 

@@ -92,9 +92,9 @@ ensures {:phase 2} Inv2(T, s, cs) && cs == tid;
     par Yield1() | Yield2() | YieldSpec(tid);

 }

 

-procedure {:yields} {:phase 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int)

-requires {:phase 1} Inv1(T, t);

-ensures {:phase 1} Inv1(T, t);

+procedure {:yields} {:layer 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int)

+requires {:layer 1} Inv1(T, t);

+ensures {:layer 1} Inv1(T, t);

 ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|;

 {

     par Yield1();

@@ -102,39 +102,39 @@ ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|;
     par Yield1();

 }

 

-procedure {:yields} {:phase 2} YieldSpec({:linear "tid"} tid: X)

-requires {:phase 2} tid != nil && cs == tid;

-ensures {:phase 2} cs == tid;

+procedure {:yields} {:layer 2} YieldSpec({:linear "tid"} tid: X)

+requires {:layer 2} tid != nil && cs == tid;

+ensures {:layer 2} cs == tid;

 {

     yield;

-    assert {:phase 2} tid != nil && cs == tid;

+    assert {:layer 2} tid != nil && cs == tid;

 }

 

-procedure {:yields} {:phase 2} Yield2()

-requires {:phase 2} Inv2(T, s, cs);

-ensures {:phase 2} Inv2(T, s, cs);

+procedure {:yields} {:layer 2} Yield2()

+requires {:layer 2} Inv2(T, s, cs);

+ensures {:layer 2} Inv2(T, s, cs);

 {

     yield;

-    assert {:phase 2} Inv2(T, s, cs);

+    assert {:layer 2} Inv2(T, s, cs);

 }

 

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

-requires {:phase 1} Inv1(T, t);

-ensures {:phase 1} Inv1(T,t);

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

+requires {:layer 1} Inv1(T, t);

+ensures {:layer 1} Inv1(T,t);

 {

     yield;

-    assert {:phase 1} Inv1(T,t);

+    assert {:layer 1} Inv1(T,t);

 }

 

-procedure {:yields} {:phase 0,2} Init({:linear "tid"} xls:[X]bool);

+procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool);

 ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

 

-procedure {:yields} {:phase 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);

+procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);

 ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|;

 

-procedure {:yields} {:phase 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int);

+procedure {:yields} {:layer 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int);

 ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|;

 

-procedure {:yields} {:phase 0,2} Leave({:linear "tid"} tid: X);

+procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X);

 ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|;

 

diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl
index 72dc4181..47dcc515 100644
--- a/Test/og/treiber-stack.bpl
+++ b/Test/og/treiber-stack.bpl
@@ -16,24 +16,24 @@ axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true]
 function Remove(x: lmap, i: Node): (lmap);

 axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));

 

-procedure {:yields} {:phase 0} ReadTopOfStack() returns (v:Node);

+procedure {:yields} {:layer 0} ReadTopOfStack() returns (v:Node);

 ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|;

 

-procedure {:yields} {:phase 0} Load(i:Node) returns (v:Node);

+procedure {:yields} {:layer 0} Load(i:Node) returns (v:Node);

 ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C;

 	            B: assume dom(Stack)[i]; v := map(Stack)[i]; return true; 

 		    C: assume !dom(Stack)[i]; return true; }|;

 

-procedure {:yields} {:phase 0} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);

+procedure {:yields} {:layer 0} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);

 ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|;

 

-procedure {:yields} {:phase 0} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);

+procedure {:yields} {:layer 0} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);

 ensures {:atomic} |{ A: assert dom(l_in)[newVal];

 		        goto B,C;

                         B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true;

 			C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|;

 

-procedure {:yields} {:phase 0} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);

+procedure {:yields} {:layer 0} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);

 ensures {:atomic} |{ A: goto B,C;

                         B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true;

 		        C: assume oldVal != TopOfStack; r := false; return true; }|;

@@ -50,10 +50,10 @@ function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool)
 

 var {:linear "Node"} Used: lmap;

 

-procedure {:yields} {:phase 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)

-requires {:phase 1} dom(x_lmap)[x];

-requires {:phase 1} Inv(TopOfStack, Stack);

-ensures {:phase 1} Inv(TopOfStack, Stack);

+procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)

+requires {:layer 1} dom(x_lmap)[x];

+requires {:layer 1} Inv(TopOfStack, Stack);

+ensures {:layer 1} Inv(TopOfStack, Stack);

 ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; return true; }|;

 {

   var t: Node;

@@ -61,30 +61,30 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret
   var {:linear "Node"} t_lmap: lmap;

 

   yield;

-  assert {:phase 1} Inv(TopOfStack, Stack);

+  assert {:layer 1} Inv(TopOfStack, Stack);

   t_lmap := x_lmap;

   while (true)

-  invariant {:phase 1} dom(t_lmap) == dom(x_lmap);

-  invariant {:phase 1} Inv(TopOfStack, Stack);

+  invariant {:layer 1} dom(t_lmap) == dom(x_lmap);

+  invariant {:layer 1} Inv(TopOfStack, Stack);

   {

     call t := ReadTopOfStack();

     call t_lmap := Store(t_lmap, x, t);

     call g, t_lmap := TransferToStack(t, x, t_lmap); 

     if (g) {

-      assert {:phase 1} map(Stack)[x] == t;

+      assert {:layer 1} map(Stack)[x] == t;

       break;

     }

     yield; 

-    assert {:phase 1} dom(t_lmap) == dom(x_lmap);

-    assert {:phase 1} Inv(TopOfStack, Stack);

+    assert {:layer 1} dom(t_lmap) == dom(x_lmap);

+    assert {:layer 1} Inv(TopOfStack, Stack);

   }

   yield; 

-  assert {:expand} {:phase 1} Inv(TopOfStack, Stack);

+  assert {:expand} {:layer 1} Inv(TopOfStack, Stack);

 }

 

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

-requires {:phase 1} Inv(TopOfStack, Stack);

-ensures {:phase 1} Inv(TopOfStack, Stack);

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

+requires {:layer 1} Inv(TopOfStack, Stack);

+ensures {:layer 1} Inv(TopOfStack, Stack);

 ensures {:atomic} |{ var t: Node; 

                      A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;

 {

@@ -93,9 +93,9 @@ ensures {:atomic} |{ var t: Node;
   var t: Node;

 

   yield;

-  assert {:phase 1} Inv(TopOfStack, Stack);

+  assert {:layer 1} Inv(TopOfStack, Stack);

   while (true)

-  invariant {:phase 1} Inv(TopOfStack, Stack);

+  invariant {:layer 1} Inv(TopOfStack, Stack);

   {

     call t := ReadTopOfStack();

     if (t != null) {

@@ -106,10 +106,10 @@ ensures {:atomic} |{ var t: Node;
       }

     }

     yield;

-    assert {:phase 1} Inv(TopOfStack, Stack);

+    assert {:layer 1} Inv(TopOfStack, Stack);

   }

   yield;

-  assert {:phase 1} Inv(TopOfStack, Stack);

+  assert {:layer 1} Inv(TopOfStack, Stack);

 }

 

 function Equal([int]bool, [int]bool) returns (bool);