renamed :phase to :layer

1 files changed, 14 insertions, 14 deletions

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;