summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-06-02 11:52:47 -0700
committerGravatar qadeer <unknown>2014-06-02 11:52:47 -0700
commit440a216ca2a62e393611133c2ea3c9e5fe9b4f88 (patch)
treebc439193f2550a6aa6ec0885042787c6bafb7a9a /Test
parent7bef2dd02b949962eaf9849fe41551716efffe71 (diff)
updated golden outputs and removed irrelevant tests
Diffstat (limited to 'Test')
-rw-r--r--Test/og/DeviceCache.bpl.expect4
-rw-r--r--Test/og/DeviceCacheSimplified.bpl158
-rw-r--r--Test/og/DeviceCacheWithBuffer.bpl173
-rw-r--r--Test/og/FlanaganQadeer.bpl.expect4
-rw-r--r--Test/og/akash.bpl.expect4
-rw-r--r--Test/og/async.bpl19
-rw-r--r--Test/og/bar.bpl.expect26
-rw-r--r--Test/og/civl-paper.bpl.expect4
-rw-r--r--Test/og/foo.bpl.expect16
-rw-r--r--Test/og/houd1.bpl24
-rw-r--r--Test/og/linear-set.bpl.expect4
-rw-r--r--Test/og/linear-set2.bpl.expect4
-rw-r--r--Test/og/lock.bpl.expect4
-rw-r--r--Test/og/lock2.bpl.expect4
-rw-r--r--Test/og/multiset.bpl.expect4
-rw-r--r--Test/og/new1.bpl.expect4
-rw-r--r--Test/og/one.bpl.expect4
-rw-r--r--Test/og/parallel1.bpl.expect16
-rw-r--r--Test/og/parallel2.bpl.expect4
-rw-r--r--Test/og/parallel4.bpl.expect12
-rw-r--r--Test/og/parallel5.bpl.expect4
-rw-r--r--Test/og/perm.bpl.expect4
-rw-r--r--Test/og/t1.bpl.expect20
-rw-r--r--Test/og/ticket.bpl.expect4
24 files changed, 75 insertions, 449 deletions
diff --git a/Test/og/DeviceCache.bpl.expect b/Test/og/DeviceCache.bpl.expect
index 11d204a8..9e5be400 100644
--- a/Test/og/DeviceCache.bpl.expect
+++ b/Test/og/DeviceCache.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 35 verified, 0 errors
+
+Boogie program verifier finished with 28 verified, 0 errors
diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl
deleted file mode 100644
index afc3e91b..00000000
--- a/Test/og/DeviceCacheSimplified.bpl
+++ /dev/null
@@ -1,158 +0,0 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// XFAIL: *
-type X;
-
-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
-function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
-{
- MapConstBool(false)[x := true]
-}
-
-function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
-{
- currsize <= newsize && (ghostLock == nil <==> currsize == newsize)
-}
-
-procedure {:yields} YieldToReadCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)
-requires tid' != nil;
-requires Inv(ghostLock, currsize, newsize);
-ensures Inv(ghostLock, currsize, newsize);
-ensures old(currsize) <= currsize;
-ensures tid == tid';
-{
- tid := tid';
- yield;
- assert Inv(ghostLock, currsize, newsize);
- assert old(currsize) <= currsize;
- assert tid != nil;
-}
-
-procedure {:yields} YieldToUpdateCache({:linear "tid"} tid': X, i: int) returns ({:linear "tid"} tid: X)
-requires tid' != nil;
-requires Inv(ghostLock, currsize, newsize);
-requires ghostLock == tid';
-requires currsize <= i;
-ensures Inv(ghostLock, currsize, newsize);
-ensures old(currsize) <= currsize;
-ensures tid == tid';
-ensures ghostLock == tid;
-ensures currsize <= i;
-ensures newsize == old(newsize);
-{
- tid := tid';
- yield;
- assert Inv(ghostLock, currsize, newsize);
- assert old(currsize) <= currsize;
- assert tid != nil;
- assert ghostLock == tid;
- assert currsize <= i;
- assert newsize == old(newsize);
-}
-
-var ghostLock: X;
-var lock: X;
-const nil: X;
-var currsize: int;
-var newsize: int;
-
-procedure acquire(tid: X);
-modifies lock;
-ensures old(lock) == nil && lock == tid;
-
-procedure release(tid: X);
-modifies lock;
-requires lock == tid;
-ensures lock == nil;
-
-procedure {:yields} Read ({:linear "tid"} tid': X, start : int, size : int) returns (bytesread : int)
-requires tid' != nil;
-requires 0 <= start && 0 <= size;
-requires Inv(ghostLock, currsize, newsize);
-ensures 0 <= bytesread && bytesread <= size;
-{
- var copy_currsize: int;
- var i, j, tmp : int;
- var {:linear "tid"} tid: X;
- tid := tid';
-
- bytesread := size;
- call acquire(tid);
- i := currsize;
- if (start + size <= i) {
- call release(tid);
- call tid := YieldToReadCache(tid);
- goto COPY_TO_BUFFER;
- } else if (newsize > i) {
- bytesread := if (start <= i) then (i - start) else 0;
- call release(tid);
- call tid := YieldToReadCache(tid);
- goto COPY_TO_BUFFER;
- } else {
- newsize := start + size;
- ghostLock := tid;
- call release(tid);
- call tid := YieldToUpdateCache(tid, i);
- goto READ_DEVICE;
- }
-
-READ_DEVICE:
- while (i < start + size)
- invariant Inv(ghostLock, currsize, newsize);
- invariant ghostLock == tid;
- invariant tid != nil;
- invariant currsize <= i;
- invariant newsize == start + size;
- {
- call tid := YieldToUpdateCache(tid, i);
- assert currsize <= i;
- i := i + 1;
- }
- call acquire(tid);
- tmp := newsize;
- currsize := tmp;
- ghostLock := nil;
- call release(tid);
- call tid := YieldToReadCache(tid);
-
-COPY_TO_BUFFER:
- j := 0;
- while(j < bytesread)
- invariant 0 <= j;
- invariant Inv(ghostLock, currsize, newsize);
- invariant tid != nil;
- invariant bytesread == 0 || start + bytesread <= currsize;
- {
- call tid := YieldToReadCache(tid);
- assert start + j < currsize;
- j := j + 1;
- }
-}
-
-procedure {:yields} {:stable} thread({:linear "tid"} tid': X)
-requires tid' != nil;
-requires 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 {:entrypoint} {:yields} main()
-requires currsize == 0 && newsize == 0 && ghostLock == nil && lock == nil;
-{
- var {:linear "tid"} tid: X;
-
- while (*)
- {
- call tid := Allocate();
- async call thread(tid);
- }
-}
-
-procedure Allocate() returns ({:linear "tid"} xls: X);
-ensures xls != nil;
diff --git a/Test/og/DeviceCacheWithBuffer.bpl b/Test/og/DeviceCacheWithBuffer.bpl
deleted file mode 100644
index a66dbaca..00000000
--- a/Test/og/DeviceCacheWithBuffer.bpl
+++ /dev/null
@@ -1,173 +0,0 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// XFAIL: *
-type X;
-function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
-const nil: X;
-var {:qed} ghostLock: X;
-var {:qed} lock: X;
-var {:qed} currsize: int;
-var {:qed} newsize: int;
-
-const device: [int]int;
-var {:qed} cache: [int]int;
-
-function {:inline} Inv(ghostLock: X, currsize: int, newsize: int, cache: [int]int) : (bool)
-{
- 0 <= currsize && currsize <= newsize &&
- (ghostLock == nil <==> currsize == newsize) &&
- (forall i: int :: 0 <= i && i < currsize ==> device[i] == cache[i])
-}
-
-procedure {:stable} {:yields} YieldToReadCache()
-requires Inv(ghostLock, currsize, newsize, cache);
-ensures Inv(ghostLock, currsize, newsize, cache) && old(currsize) <= currsize;
-{
-}
-
-procedure {:stable} {:yields} YieldToWriteCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)
-requires Inv(ghostLock, currsize, newsize, cache) && ghostLock == tid' && tid' != nil;
-ensures Inv(ghostLock, currsize, newsize, cache) && ghostLock == tid && tid != nil && tid == tid' && old(currsize) == currsize && old(newsize) == newsize;
-{
- tid := tid';
-}
-
-procedure Allocate({:linear "tid"} xls': [X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
-ensures xl != nil;
-
-procedure {:entrypoint} {:yields} main({:linear "tid"} xls':[X]bool)
-requires xls' == mapconstbool(true);
-{
- var {:linear "tid"} tid: X;
- var {:linear "tid"} xls: [X]bool;
-
- call xls := Init(xls');
-
- while (*)
- invariant Inv(ghostLock, currsize, newsize, cache);
- {
- call xls, tid := Allocate(xls);
- async call Thread(tid);
- }
-}
-
-procedure {:yields} {:stable} Thread({:linear "tid"} tid': X)
-requires tid' != nil;
-requires Inv(ghostLock, currsize, newsize, cache);
-{
- var start, size, bytesRead: int;
- var buffer: [int]int;
- var {:linear "tid"} tid: X;
-
- tid := tid';
- havoc start, size;
- assume (0 <= start && 0 <= size);
- call bytesRead, buffer := Read(tid, start, size);
-}
-
-procedure {:yields} Read({:linear "tid"} tid': X, start : int, size : int) returns (bytesRead : int, buffer : [int]int)
-requires tid' != nil;
-requires 0 <= start && 0 <= size;
-requires Inv(ghostLock, currsize, newsize, cache);
-ensures 0 <= bytesRead && bytesRead <= size;
-ensures (forall i: int :: 0 <= i && i < bytesRead ==> buffer[i] == device[start+i]);
-{
- var i, tmp: int;
- var {:linear "tid"} tid: X;
- tid := tid';
-
- yield;
- assert Inv(ghostLock, currsize, newsize, cache);
- bytesRead := size;
- call tid := acquire(tid);
- call tid, i := ReadCurrsize(tid);
- call tid, tmp := ReadNewsize(tid);
- if (start + size <= i) {
- call tid := release(tid);
- goto COPY_TO_BUFFER;
- } else if (tmp > i) {
- bytesRead := if (start <= i) then (i - start) else 0;
- call tid := release(tid);
- goto COPY_TO_BUFFER;
- } else {
- call tid := WriteNewsize(tid, start + size);
- call tid := release(tid);
- goto READ_DEVICE;
- }
-
-READ_DEVICE:
- par tid := YieldToWriteCache(tid);
- call tid := WriteCache(tid, start + size);
- call tid := acquire(tid);
- call tid, tmp := ReadNewsize(tid);
- call tid := WriteCurrsize(tid, tmp);
- call tid := release(tid);
-
-COPY_TO_BUFFER:
- par YieldToReadCache();
- call buffer := ReadCache(start, bytesRead);
-}
-
-procedure {:yields} WriteCache({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X)
-ensures {:right 1} |{ A: assert ghostLock == tid' && tid' != nil; tid := tid'; cache := (lambda i: int :: if (currsize <= i && i < index) then device[i] else cache[i]); return true; }|;
-{
- var j: int;
- tid := tid';
-
- call tid, j := ReadCurrsize(tid);
- while (j < index)
- invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid';
- invariant {:phase 1} cache == (lambda i: int :: if (currsize <= i && i < j) then device[i] else old(cache)[i]);
- {
- call tid := WriteCacheEntry(tid, j);
- j := j + 1;
- }
-}
-
-procedure {:yields} ReadCache(start: int, bytesRead: int) returns (buffer: [int]int)
-requires 0 <= start && 0 <= bytesRead && (bytesRead == 0 || start + bytesRead <= currsize);
-requires (forall i: int :: 0 <= i && i < currsize ==> cache[i] == device[i]);
-ensures (forall i: int :: 0 <= i && i < bytesRead ==> buffer[i] == device[start+i]);
-{
- var x: int;
- var j: int;
- j := 0;
- while(j < bytesRead)
- invariant bytesRead == 0 || start + j <= currsize;
- invariant (forall i: int :: 0 <= i && i < j ==> buffer[i] == device[start+i]);
- {
- yield;
- assert start + j < currsize;
- assert (forall i: int :: 0 <= i && i < currsize ==> cache[i] == device[i]);
- call x := ReadCacheEntry(start + j);
- buffer[j] := x;
- j := j + 1;
- }
-}
-
-procedure {:yields} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);
-ensures {:both 0} |{ A: assert xls' == mapconstbool(true); xls := xls'; currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|;
-
-procedure {:yields} ReadCurrsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);
-ensures {:right 0} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := currsize; return true; }|;
-
-procedure {:yields} ReadNewsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);
-ensures {:right 0} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := newsize; return true; }|;
-
-procedure {:yields} WriteNewsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);
-ensures {:atomic 0} |{A: assert tid' != nil; assert lock == tid' && ghostLock == nil; tid := tid'; newsize := val; ghostLock := tid; return true; }|;
-
-procedure {:yields} WriteCurrsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);
-ensures {:atomic 0} |{A: assert tid' != nil; assert lock == tid' && ghostLock == tid'; tid := tid'; currsize := val; ghostLock := nil; return true; }|;
-
-procedure {:yields} ReadCacheEntry(index: int) returns (val: int);
-ensures {:atomic 0} |{ A: assert 0 <= index && index < currsize; val := cache[index]; return true; }|;
-
-procedure {:yields} WriteCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);
-ensures {:right 0} |{ A: assert tid' != nil; assert currsize <= index && ghostLock == tid'; tid := tid'; cache[index] := device[index]; return true; }|;
-
-procedure {:yields} acquire({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);
-ensures {:right 0} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lock := tid; return true; }|;
-
-procedure {:yields} release({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);
-ensures {:left 0} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|;
diff --git a/Test/og/FlanaganQadeer.bpl.expect b/Test/og/FlanaganQadeer.bpl.expect
index 9823d44a..5b2909f1 100644
--- a/Test/og/FlanaganQadeer.bpl.expect
+++ b/Test/og/FlanaganQadeer.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 6 verified, 0 errors
+
+Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/og/akash.bpl.expect b/Test/og/akash.bpl.expect
index 9823d44a..5b2909f1 100644
--- a/Test/og/akash.bpl.expect
+++ b/Test/og/akash.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 6 verified, 0 errors
+
+Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/og/async.bpl b/Test/og/async.bpl
deleted file mode 100644
index 2219fe8c..00000000
--- a/Test/og/async.bpl
+++ /dev/null
@@ -1,19 +0,0 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// XFAIL: *
-var {:phase 1} x: int;
-var {:phase 1} y: int;
-
-procedure {:yields} {:phase 1} foo()
-{
- assume x == y;
- x := x + 1;
- async call P();
- y := y + 1;
-}
-
-procedure {:yields} {:phase 1} P()
-requires x != y;
-{
- assert {:phase 1} x != y;
-}
diff --git a/Test/og/bar.bpl.expect b/Test/og/bar.bpl.expect
index d59bd019..4bd6cc8c 100644
--- a/Test/og/bar.bpl.expect
+++ b/Test/og/bar.bpl.expect
@@ -1,13 +1,13 @@
-bar.bpl(28,3): Error: Non-interference check failed
-Execution trace:
- bar.bpl(7,3): anon0
- bar.bpl(7,3): anon0$1
- bar.bpl(14,3): inline$Incr_1$0$this_A
- (0,0): inline$Impl_YieldChecker_PC_1$1$L0
-bar.bpl(28,3): Error: Non-interference check failed
-Execution trace:
- bar.bpl(38,3): anon0
- bar.bpl(38,3): anon0$1
- (0,0): inline$Impl_YieldChecker_PC_1$1$L0
-
-Boogie program verifier finished with 8 verified, 2 errors
+bar.bpl(28,3): Error: Non-interference check failed
+Execution trace:
+ bar.bpl(7,3): anon0
+ bar.bpl(7,3): anon0$1
+ bar.bpl(14,3): inline$Incr_1$0$this_A
+ (0,0): inline$Impl_YieldChecker_PC_1$1$L0
+bar.bpl(28,3): Error: Non-interference check failed
+Execution trace:
+ bar.bpl(38,3): anon0
+ bar.bpl(38,3): anon0$1
+ (0,0): inline$Impl_YieldChecker_PC_1$1$L0
+
+Boogie program verifier finished with 3 verified, 2 errors
diff --git a/Test/og/civl-paper.bpl.expect b/Test/og/civl-paper.bpl.expect
index 812c54cc..ac38b46e 100644
--- a/Test/og/civl-paper.bpl.expect
+++ b/Test/og/civl-paper.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 28 verified, 0 errors
+
+Boogie program verifier finished with 23 verified, 0 errors
diff --git a/Test/og/foo.bpl.expect b/Test/og/foo.bpl.expect
index b386f3f6..287c2b4f 100644
--- a/Test/og/foo.bpl.expect
+++ b/Test/og/foo.bpl.expect
@@ -1,8 +1,8 @@
-foo.bpl(30,3): Error: Non-interference check failed
-Execution trace:
- foo.bpl(7,3): anon0
- foo.bpl(7,3): anon0$1
- foo.bpl(14,3): inline$Incr_1$0$this_A
- (0,0): inline$Impl_YieldChecker_PC_1$1$L0
-
-Boogie program verifier finished with 9 verified, 1 error
+foo.bpl(30,3): Error: Non-interference check failed
+Execution trace:
+ foo.bpl(7,3): anon0
+ foo.bpl(7,3): anon0$1
+ foo.bpl(14,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
diff --git a/Test/og/houd1.bpl b/Test/og/houd1.bpl
deleted file mode 100644
index 8c86f22b..00000000
--- a/Test/og/houd1.bpl
+++ /dev/null
@@ -1,24 +0,0 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// XFAIL: *
-const {:existential true} b0: bool;
-const {:existential true} b1: bool;
-const {:existential true} b2: bool;
-
-var x:int;
-
-procedure A()
-{
- x := x + 1;
- yield;
-}
-
-procedure B()
-{
- x := 5;
- yield;
- assert b0 ==> (x == 5);
- assert b1 ==> (x >= 5);
- assert b2 ==> (x >= 6);
-}
-
diff --git a/Test/og/linear-set.bpl.expect b/Test/og/linear-set.bpl.expect
index 00ddb38b..3de74d3e 100644
--- a/Test/og/linear-set.bpl.expect
+++ b/Test/og/linear-set.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 4 verified, 0 errors
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/og/linear-set2.bpl.expect b/Test/og/linear-set2.bpl.expect
index 00ddb38b..3de74d3e 100644
--- a/Test/og/linear-set2.bpl.expect
+++ b/Test/og/linear-set2.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 4 verified, 0 errors
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/og/lock.bpl.expect b/Test/og/lock.bpl.expect
index 76a9a2bf..05d394c7 100644
--- a/Test/og/lock.bpl.expect
+++ b/Test/og/lock.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 8 verified, 0 errors
+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/og/lock2.bpl.expect b/Test/og/lock2.bpl.expect
index 76a9a2bf..05d394c7 100644
--- a/Test/og/lock2.bpl.expect
+++ b/Test/og/lock2.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 8 verified, 0 errors
+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/og/multiset.bpl.expect b/Test/og/multiset.bpl.expect
index 63682bb4..d72077a6 100644
--- a/Test/og/multiset.bpl.expect
+++ b/Test/og/multiset.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 85 verified, 0 errors
+
+Boogie program verifier finished with 78 verified, 0 errors
diff --git a/Test/og/new1.bpl.expect b/Test/og/new1.bpl.expect
index 00ddb38b..3de74d3e 100644
--- a/Test/og/new1.bpl.expect
+++ b/Test/og/new1.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 4 verified, 0 errors
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/og/one.bpl.expect b/Test/og/one.bpl.expect
index a9949f2e..3de74d3e 100644
--- a/Test/og/one.bpl.expect
+++ b/Test/og/one.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 3 verified, 0 errors
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/og/parallel1.bpl.expect b/Test/og/parallel1.bpl.expect
index 5fc0cbf6..1e0545a9 100644
--- a/Test/og/parallel1.bpl.expect
+++ b/Test/og/parallel1.bpl.expect
@@ -1,8 +1,8 @@
-parallel1.bpl(30,3): Error: Non-interference check failed
-Execution trace:
- parallel1.bpl(7,3): anon0
- parallel1.bpl(7,3): anon0$1
- parallel1.bpl(14,3): inline$Incr_1$0$this_A
- (0,0): inline$Impl_YieldChecker_PC_1$1$L0
-
-Boogie program verifier finished with 7 verified, 1 error
+parallel1.bpl(30,3): Error: Non-interference check failed
+Execution trace:
+ parallel1.bpl(7,3): anon0
+ parallel1.bpl(7,3): anon0$1
+ parallel1.bpl(14,3): inline$Incr_1$0$this_A
+ (0,0): inline$Impl_YieldChecker_PC_1$1$L0
+
+Boogie program verifier finished with 3 verified, 1 error
diff --git a/Test/og/parallel2.bpl.expect b/Test/og/parallel2.bpl.expect
index 76a9a2bf..fef5ddc0 100644
--- a/Test/og/parallel2.bpl.expect
+++ b/Test/og/parallel2.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 8 verified, 0 errors
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/parallel4.bpl.expect b/Test/og/parallel4.bpl.expect
index 7c696364..771d5de9 100644
--- a/Test/og/parallel4.bpl.expect
+++ b/Test/og/parallel4.bpl.expect
@@ -1,6 +1,6 @@
-parallel4.bpl(26,3): Error BP5001: This assertion might not hold.
-Execution trace:
- (0,0): og_init
- parallel4.bpl(24,5): anon0$1
-
-Boogie program verifier finished with 5 verified, 1 error
+parallel4.bpl(26,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ (0,0): og_init
+ parallel4.bpl(24,5): anon0$1
+
+Boogie program verifier finished with 2 verified, 1 error
diff --git a/Test/og/parallel5.bpl.expect b/Test/og/parallel5.bpl.expect
index 76a9a2bf..fef5ddc0 100644
--- a/Test/og/parallel5.bpl.expect
+++ b/Test/og/parallel5.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 8 verified, 0 errors
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/perm.bpl.expect b/Test/og/perm.bpl.expect
index 00ddb38b..3de74d3e 100644
--- a/Test/og/perm.bpl.expect
+++ b/Test/og/perm.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 4 verified, 0 errors
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/og/t1.bpl.expect b/Test/og/t1.bpl.expect
index 9f9e44b1..0fd3fde5 100644
--- a/Test/og/t1.bpl.expect
+++ b/Test/og/t1.bpl.expect
@@ -1,10 +1,10 @@
-t1.bpl(60,5): Error: Non-interference check failed
-Execution trace:
- (0,0): og_init
- t1.bpl(80,13): anon0
- t1.bpl(80,13): anon0$1
- (0,0): inline$SetG_1$0$Entry
- t1.bpl(80,13): anon0$2
- (0,0): inline$Impl_YieldChecker_A_1$1$L2
-
-Boogie program verifier finished with 5 verified, 1 error
+t1.bpl(60,5): Error: Non-interference check failed
+Execution trace:
+ (0,0): og_init
+ t1.bpl(80,13): anon0
+ t1.bpl(80,13): anon0$1
+ (0,0): inline$SetG_1$0$Entry
+ t1.bpl(80,13): anon0$2
+ (0,0): inline$Impl_YieldChecker_A_1$1$L2
+
+Boogie program verifier finished with 2 verified, 1 error
diff --git a/Test/og/ticket.bpl.expect b/Test/og/ticket.bpl.expect
index 812c54cc..bc10e4e3 100644
--- a/Test/og/ticket.bpl.expect
+++ b/Test/og/ticket.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 28 verified, 0 errors
+
+Boogie program verifier finished with 21 verified, 0 errors