1 files changed, 7 insertions, 2 deletions
diff --git a/Test/linear/async-bug.bpl b/Test/linear/async-bug.bpl
index faa1a65d..ff6cdded 100644
--- a/Test/linear/async-bug.bpl
+++ b/Test/linear/async-bug.bpl
@@ -2,12 +2,17 @@
 // RUN: %diff "%s.expect" "%t"
 const GcTid:int;
 
-procedure {:yields} {:phase 100} Initialize({:cnst "tid"} tid:int)
+procedure {:yields} {:phase 100} Initialize({:linear "tid"} tid:int)
 requires{:phase 100} tid == GcTid;
 {
     yield;
     assert{:phase 100} tid == GcTid;
 
+    call GarbageCollect(tid);
+
+    yield;
+    assert{:phase 100} tid == GcTid;
+
     async call GarbageCollect(tid);
 
     yield;
@@ -22,7 +27,7 @@ requires{:phase 100} tid == GcTid;
     assert{:phase 100} tid == GcTid;
 }
 
-procedure {:yields} {:phase 100} GarbageCollect({:cnst "tid"} tid:int)
+procedure {:yields} {:phase 100} GarbageCollect({:linear "tid"} tid:int)
 requires{:phase 100} tid == GcTid;
 {
     yield;