1 files changed, 7 insertions, 3 deletions
diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index 8ee5e436..c583cb3c 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -1,16 +1,20 @@
 var a:[int]int;
 
+procedure Allocate() returns ({:linear "tid"} xls: int);
+
 procedure {:entrypoint} main() 
 {
     var {:linear "tid"} i: int;
     var {:linear "tid"} j: int;
+    call i := Allocate();
+    call j := Allocate();
     call i := t(i) | j := Yield(j);
     call i := u(i) | j := u(j);
 }
 
 procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
 {
-    assume i == i';
+    i := i';
 
     a[i] := 42;
     call i := Yield(i);
@@ -19,7 +23,7 @@ procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
 
 procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 
 {
-    assume i == i';
+    i := i';
 
     a[i] := 42;
     yield;
@@ -30,7 +34,7 @@ procedure Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
 ensures i == i';
 ensures old(a)[i] == a[i];
 {
-    assume i == i';
+    i := i';
     yield;
     assert old(a)[i] == a[i];
 }
 \ No newline at end of file