update

1 files changed, 10 insertions, 10 deletions

diff --git a/Test/linear/async-bug.bpl b/Test/linear/async-bug.bpl
index ff6cdded..ad7020ad 100644
--- a/Test/linear/async-bug.bpl
+++ b/Test/linear/async-bug.bpl
@@ -2,35 +2,35 @@
 // RUN: %diff "%s.expect" "%t"

 const GcTid:int;

 

-procedure {:yields} {:phase 100} Initialize({:linear "tid"} tid:int)

-requires{:phase 100} tid == GcTid;

+procedure {:yields} {:layer 100} Initialize({:linear "tid"} tid:int)

+requires{:layer 100} tid == GcTid;

 {

     yield;

-    assert{:phase 100} tid == GcTid;

+    assert{:layer 100} tid == GcTid;

 

     call GarbageCollect(tid);

 

     yield;

-    assert{:phase 100} tid == GcTid;

+    assert{:layer 100} tid == GcTid;

 

     async call GarbageCollect(tid);

 

     yield;

-    assert{:phase 100} tid == GcTid;

+    assert{:layer 100} tid == GcTid;

 

     async call GarbageCollect(tid);

 

     yield;

-    assert{:phase 100} tid == GcTid;

+    assert{:layer 100} tid == GcTid;

 

     yield;

-    assert{:phase 100} tid == GcTid;

+    assert{:layer 100} tid == GcTid;

 }

 

-procedure {:yields} {:phase 100} GarbageCollect({:linear "tid"} tid:int)

-requires{:phase 100} tid == GcTid;

+procedure {:yields} {:layer 100} GarbageCollect({:linear "tid"} tid:int)

+requires{:layer 100} tid == GcTid;

 {

     yield;

-    assert{:phase 100} tid == GcTid;

+    assert{:layer 100} tid == GcTid;

 }