second checkpoint

10 files changed, 131 insertions, 134 deletions

diff --git a/Test/og/Answer b/Test/og/Answer
index a02a2838..b82acad4 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -1,59 +1,58 @@
 

 -------------------- foo.bpl --------------------

-foo.bpl(14,3): Error: Non-interference check failed

+foo.bpl(28,3): Error: Non-interference check failed

 Execution trace:

-    foo.bpl(6,5): anon0

-    (0,0): inline$Impl_YieldChecker_PC_0$0$L0

+    foo.bpl(5,3): anon0

+    foo.bpl(5,3): anon0$1

+    foo.bpl(12,3): inline$Incr_1$0$this_A

+    (0,0): inline$Impl_YieldChecker_PC_1$1$L0

 

-Boogie program verifier finished with 4 verified, 1 error

+Boogie program verifier finished with 9 verified, 1 error

 

 -------------------- bar.bpl --------------------

-bar.bpl(13,3): Error: Non-interference check failed

+bar.bpl(26,3): Error: Non-interference check failed

 Execution trace:

-    bar.bpl(6,5): anon0

-    (0,0): inline$Impl_YieldChecker_PC_0$0$L0

-bar.bpl(13,3): Error: Non-interference check failed

+    bar.bpl(5,3): anon0

+    bar.bpl(5,3): anon0$1

+    bar.bpl(12,3): inline$Incr_1$0$this_A

+    (0,0): inline$Impl_YieldChecker_PC_1$1$L0

+bar.bpl(26,3): Error: Non-interference check failed

 Execution trace:

-    bar.bpl(23,5): anon0

-    (0,0): inline$Impl_YieldChecker_PC_0$0$L0

+    bar.bpl(36,3): anon0

+    bar.bpl(36,3): anon0$1

+    (0,0): inline$Impl_YieldChecker_PC_1$1$L0

 

-Boogie program verifier finished with 3 verified, 2 errors

+Boogie program verifier finished with 8 verified, 2 errors

 

 -------------------- one.bpl --------------------

 

-Boogie program verifier finished with 2 verified, 0 errors

+Boogie program verifier finished with 3 verified, 0 errors

 

 -------------------- parallel1.bpl --------------------

-parallel1.bpl(10,1): Error: Non-interference check failed

-Execution trace:

-    parallel1.bpl(6,5): anon0

-    (0,0): inline$Proc_YieldChecker_PC_0$0$L0

-parallel1.bpl(14,3): Error: Non-interference check failed

+parallel1.bpl(28,3): Error: Non-interference check failed

 Execution trace:

-    parallel1.bpl(6,5): anon0

-    (0,0): inline$Impl_YieldChecker_PC_0$0$L0

+    parallel1.bpl(5,3): anon0

+    parallel1.bpl(5,3): anon0$1

+    parallel1.bpl(12,3): inline$Incr_1$0$this_A

+    (0,0): inline$Impl_YieldChecker_PC_1$1$L0

 

-Boogie program verifier finished with 3 verified, 2 errors

+Boogie program verifier finished with 7 verified, 1 error

 

 -------------------- linear-set.bpl --------------------

 

-Boogie program verifier finished with 2 verified, 0 errors

+Boogie program verifier finished with 4 verified, 0 errors

 

 -------------------- linear-set2.bpl --------------------

 

-Boogie program verifier finished with 2 verified, 0 errors

+Boogie program verifier finished with 4 verified, 0 errors

 

 -------------------- FlanaganQadeer.bpl --------------------

 

-Boogie program verifier finished with 3 verified, 0 errors

-

--------------------- DeviceCacheSimplified.bpl --------------------

-

-Boogie program verifier finished with 5 verified, 0 errors

+Boogie program verifier finished with 6 verified, 0 errors

 

 -------------------- parallel2.bpl --------------------

 

-Boogie program verifier finished with 4 verified, 0 errors

+Boogie program verifier finished with 8 verified, 0 errors

 

 -------------------- parallel4.bpl --------------------

 parallel4.bpl(24,3): Error BP5001: This assertion might not hold.

@@ -61,40 +60,35 @@ Execution trace:
     (0,0): og_init

     parallel4.bpl(22,5): anon0$1

 

-Boogie program verifier finished with 2 verified, 1 error

+Boogie program verifier finished with 5 verified, 1 error

 

 -------------------- parallel5.bpl --------------------

 

-Boogie program verifier finished with 4 verified, 0 errors

+Boogie program verifier finished with 8 verified, 0 errors

 

 -------------------- akash.bpl --------------------

 

-Boogie program verifier finished with 3 verified, 0 errors

+Boogie program verifier finished with 6 verified, 0 errors

 

 -------------------- t1.bpl --------------------

-t1.bpl(51,5): Error: Non-interference check failed

+t1.bpl(58,5): Error: Non-interference check failed

 Execution trace:

     (0,0): og_init

-    (0,0): inline$Impl_YieldChecker_A_0$0$L1

+    t1.bpl(78,13): anon0

+    t1.bpl(78,13): anon0$1

+    (0,0): inline$SetG_1$0$Entry

+    t1.bpl(78,13): anon0$2

+    (0,0): inline$Impl_YieldChecker_A_1$1$L2

 

-Boogie program verifier finished with 2 verified, 1 error

+Boogie program verifier finished with 5 verified, 1 error

 

 -------------------- new1.bpl --------------------

 

-Boogie program verifier finished with 2 verified, 0 errors

+Boogie program verifier finished with 4 verified, 0 errors

 

 -------------------- perm.bpl --------------------

 

-Boogie program verifier finished with 2 verified, 0 errors

-

--------------------- async.bpl --------------------

-async.bpl(14,1): Error: Non-interference check failed

-Execution trace:

-    async.bpl(7,3): anon0

-    async.bpl(7,3): anon0$1

-    (0,0): inline$Proc_YieldChecker_P_0$1$L0

-

-Boogie program verifier finished with 1 verified, 1 error

+Boogie program verifier finished with 4 verified, 0 errors

 

 -------------------- DeviceCache.bpl --------------------

 

@@ -106,11 +100,11 @@ Boogie program verifier finished with 28 verified, 0 errors
 

 -------------------- lock.bpl --------------------

 

-Boogie program verifier finished with 6 verified, 0 errors

+Boogie program verifier finished with 8 verified, 0 errors

 

 -------------------- lock2.bpl --------------------

 

-Boogie program verifier finished with 6 verified, 0 errors

+Boogie program verifier finished with 8 verified, 0 errors

 

 -------------------- multiset.bpl --------------------

 

@@ -118,4 +112,4 @@ Boogie program verifier finished with 85 verified, 0 errors
 

 -------------------- civl-paper.bpl --------------------

 

-Boogie program verifier finished with 29 verified, 0 errors

+Boogie program verifier finished with 28 verified, 0 errors

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index 0f6383ef..23f36ae5 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -22,18 +22,20 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
     (ghostLock == nil <==> currsize == newsize)

 }

 

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

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

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

+procedure {:yields} {:phase 1} YieldToReadCache({:cnst "tid"} tid: X)

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

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

 {

-   tid := tid';

+   yield;

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

 }

 

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

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

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

+procedure {:yields} {:phase 1} YieldToWriteCache({:cnst "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;

 {

-    tid := tid';

+    yield;

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

 }

 

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

@@ -47,7 +49,8 @@ requires {:phase 1} xls' == mapconstbool(true);
 

     yield;

 

-    call xls := Init(xls');

+    xls := xls';

+    call Init(xls);

     

     yield;

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

@@ -64,134 +67,127 @@ requires {:phase 1} xls' == mapconstbool(true);
     }

 }

 

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

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

+procedure {:yields} {:phase 1} Thread({:cnst "tid"} tid: X)

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

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

 {

     var start, size, bytesRead: int;

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

 

-    tid := tid';

     havoc start, size;

     assume (0 <= start && 0 <= size);

     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;

+procedure {:yields} {:phase 1} Read({:cnst "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;

 {

     var i, tmp: int;

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

-    tid := tid';

 

-    par  tid := YieldToReadCache(tid);

+    par YieldToReadCache(tid);

     bytesRead := size;

-    call tid := acquire(tid);

-    call tid, i := ReadCurrsize(tid);

-    call tid, tmp := ReadNewsize(tid);

+    call acquire(tid);

+    call i := ReadCurrsize(tid);

+    call tmp := ReadNewsize(tid);

     if (start + size <= i) {

-        call tid := release(tid); 

+        call release(tid); 

     	goto COPY_TO_BUFFER;

     } else if (tmp > i) {

         bytesRead := if (start <= i) then (i - start) else 0;

-    	call tid := release(tid); 

+    	call release(tid); 

 	goto COPY_TO_BUFFER;

     } else {

-        call tid := WriteNewsize(tid, start + size);

-    	call tid := release(tid); 

+        call WriteNewsize(tid, start + size);

+    	call release(tid); 

 	goto READ_DEVICE;

     }

 

 READ_DEVICE:

-    par  tid := YieldToWriteCache(tid);

-    call tid := WriteCache(tid, start + size);

-    par  tid := YieldToWriteCache(tid);

-    call tid := acquire(tid);

-    call tid, tmp := ReadNewsize(tid);

-    call tid := WriteCurrsize(tid, tmp);

-    call tid := release(tid);

+    par YieldToWriteCache(tid);

+    call WriteCache(tid, start + size);

+    par YieldToWriteCache(tid);

+    call acquire(tid);

+    call tmp := ReadNewsize(tid);

+    call WriteCurrsize(tid, tmp);

+    call release(tid);

 

 COPY_TO_BUFFER:

-    par tid := YieldToReadCache(tid);

-    call tid := ReadCache(tid, start, bytesRead);

+    par YieldToReadCache(tid);

+    call ReadCache(tid, start, bytesRead);

 }

 

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

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

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

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

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

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

 {

     var j: int;

-    tid := tid';

 

-    par tid := YieldToWriteCache(tid);

-    call tid, j := ReadCurrsize(tid);

+    par YieldToWriteCache(tid);

+    call j := ReadCurrsize(tid);

     while (j < index)

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

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

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

     {

-        par tid := YieldToWriteCache(tid);

-        call tid := WriteCacheEntry(tid, j);

+        par YieldToWriteCache(tid);

+        call WriteCacheEntry(tid, j);

 	j := j + 1;

     }

-    par tid := YieldToWriteCache(tid);

+    par YieldToWriteCache(tid);

 }

 

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

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

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

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

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

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

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

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

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

 {

     var j: int;

-    tid := tid';

 

-    par tid := YieldToReadCache(tid);

+    par YieldToReadCache(tid);

 

     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) && tid == tid';

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

     {

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

-        call tid := ReadCacheEntry(tid, start + j);

+        call ReadCacheEntry(tid, start + j);

         j := j + 1;

-	par tid := YieldToReadCache(tid);

+	par YieldToReadCache(tid);

     }

 

-    par tid := YieldToReadCache(tid);

+    par YieldToReadCache(tid);

 }

 

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

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

+procedure {:yields} {:phase 0,1} Init({:cnst "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 ({:linear "tid"} tid: X, val: int);

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

+procedure {:yields} {:phase 0,1} ReadCurrsize({:cnst "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 ({:linear "tid"} tid: X, val: int);

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

+procedure {:yields} {:phase 0,1} ReadNewsize({:cnst "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) returns ({:linear "tid"} tid: X);

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

+procedure {:yields} {:phase 0,1} WriteNewsize({:cnst "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) returns ({:linear "tid"} tid: X);

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

+procedure {:yields} {:phase 0,1} WriteCurrsize({:cnst "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) returns ({:linear "tid"} tid: X);

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

+procedure {:yields} {:phase 0,1} ReadCacheEntry({:cnst "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) returns ({:linear "tid"} tid: X);

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

+procedure {:yields} {:phase 0,1} WriteCacheEntry({:cnst "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) returns ({:linear "tid"} tid: X);

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

+procedure {:yields} {:phase 0,1} acquire({:cnst "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) returns ({:linear "tid"} tid: X);

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

+procedure {:yields} {:phase 0,1} release({:cnst "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 e8df9515..2fddf217 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -17,6 +17,7 @@ procedure {:yields} {:phase 1} main()
     var {:linear "tid"} tid: X;

     var val: int;

 

+    yield;

     while (*) 

     {

         yield;

diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index 4a6e002d..8357d36d 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -2,6 +2,7 @@ var {:phase 2} b: bool;
 

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

 {

+    yield;

     while (*)

     {

         yield;

@@ -14,6 +15,7 @@ procedure {:yields} {:phase 2} main()
 

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

 {

+    yield;

     while (*) 

     {

     	yield;

@@ -26,8 +28,6 @@ procedure {:yields} {:phase 2} Customer()
 

         yield;

     }

-

-    yield;

 }

 

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

diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index b173ecd4..9f5e0be8 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -2,6 +2,7 @@ var {:phase 2} b: int;
 

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

 {

+    yield;

     while (*)

     {

         yield;

@@ -14,6 +15,7 @@ procedure {:yields} {:phase 2} main()
 

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

 {

+    yield;

     while (*) 

     {

     	yield;

@@ -26,14 +28,13 @@ procedure {:yields} {:phase 2} Customer()
 

         yield;

     }

-

-    yield;

 }

 

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

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

 {

     var _old, curr: int;

+    yield;

     while (true) { 

     	yield;

         call _old := CAS(0, 1);

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 3305b63f..459cb470 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -339,6 +339,8 @@ procedure {:yields} {:phase 1} Yield1()
 requires {:phase 1} Inv(valid, elt, owner);

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

 {

+	yield;

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

 }

 

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

diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
index 18050e09..427dc72d 100644
--- a/Test/og/parallel1.bpl
+++ b/Test/og/parallel1.bpl
@@ -37,7 +37,8 @@ procedure {:yields} {:phase 1} PD()
 

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

 {

-  while (true)

+  yield;

+  while (*)

   {

     par PB() | PC() | PD();

   }

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 4a3c1849..1bce7c8a 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -27,7 +27,7 @@ procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid
 

     yield;

     call Write(i, 42);

-    call i := Yield(i);

+    call Yield(i);

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

 }

 

@@ -41,11 +41,9 @@ procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid
     assert {:phase 1} a[i] == 42;

 }

 

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

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

+procedure {:yields} {:phase 1} Yield({:cnst "tid"} i: int)

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

 {

-    i := i';

     yield;

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

 }
\ No newline at end of file
diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index 330b970d..a73af06e 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -17,7 +17,7 @@ procedure {:yields} {:phase 1} main()
     var {:linear "tid"} j: int;

     call i := Allocate();

     call j := Allocate();

-    par i := t(i) | j := Yield(j);

+    par i := t(i) | Yield(j);

     par i := u(i) | j := u(j);

 }

 

@@ -27,7 +27,7 @@ procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid
 

     yield;

     call Write(i, 42);

-    call i := Yield(i);

+    call Yield(i);

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

 }

 

@@ -41,11 +41,9 @@ procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid
     assert {:phase 1} a[i] == 42;

 }

 

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

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

+procedure {:yields} {:phase 1} Yield({:cnst "tid"} i: int)

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

 {

-    i := i';

     yield;

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

 }
\ No newline at end of file
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index ea08dcb5..fb347935 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -65,7 +65,8 @@ requires {:phase 3} true;
 {

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

     tid := tid';

-

+    

+    par Yield1() | Yield2() | Yield();    

     while (*) 

     invariant {:phase 1} Inv1(T, t);

     invariant {:phase 2} tid != nil && Inv2(T, s, cs);

@@ -108,18 +109,23 @@ ensures {:right} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; retu
 

 procedure {:yields} {:phase 3} Yield()

 {

+    yield;

 }

 

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

 requires {:phase 2} Inv2(T, s, cs);

 ensures {:phase 2} Inv2(T, s, cs);

 {

+    yield;

+    assert {:phase 2} Inv2(T, s, cs);

 }

 

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

 requires {:phase 1} Inv1(T, t);

 ensures {:phase 1} Inv1(T,t);

 {

+    yield;

+    assert {:phase 1} Inv1(T,t);

 }

 

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