updated golden outputs and removed irrelevant tests

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