Normalise line endings using a .gitattributes file. Unfortunately

this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.

59 files changed, 3109 insertions, 3109 deletions

diff --git a/Test/civl/DeviceCache.bpl b/Test/civl/DeviceCache.bpl
index f439b607..01b1be01 100644
--- a/Test/civl/DeviceCache.bpl
+++ b/Test/civl/DeviceCache.bpl
@@ -1,210 +1,210 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-type X;

-function {:builtin "MapConst"} mapconstbool(bool): [X]bool;

-const nil: X;

-var {:layer 0,1} ghostLock: X;

-var {:layer 0,1} lock: X;

-var {:layer 0,1} currsize: int;

-var {:layer 0,1} newsize: int;

-

-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

-function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

-{

-  MapConstBool(false)[x := true]

-}

-function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool

-{

-  x

-}

-

-function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)

-{

-    0 <= currsize && currsize <= newsize && 

-    (ghostLock == nil <==> currsize == newsize)

-}

-

-procedure {:yields} {:layer 1} Yield()

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

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

-{

-   yield;

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

-}

-

-procedure {:yields} {:layer 1} YieldToReadCache({:linear "tid"} tid: X)

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

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

-{

-   yield;

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

-}

-

-procedure {:yields} {:layer 1} YieldToWriteCache({:linear "tid"} tid: X)

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

-ensures {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;

-{

-    yield;

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

-}

-

-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X)

-ensures {:layer 1} xl != nil;

-{

-    yield;

-    call xl := AllocateLow();

-    yield;

-}

-

-procedure {:yields} {:layer 1} main({:linear_in "tid"} xls: [X]bool)

-requires {:layer 1} xls == mapconstbool(true);

-{

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

-

-    yield;

-

-    call Init(xls);

-    

-    yield;

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

-

-    while (*)

-    invariant {:layer 1} Inv(ghostLock, currsize, newsize);

-    {

-        par tid := Allocate() | Yield();

-	yield;

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

-        async call Thread(tid);

-	yield;

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

-    }

-    yield;

-}

-

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

-requires {:layer 1} tid != nil;

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

-{

-    var start, size, bytesRead: int;

-

-    havoc start, size;

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

-    call bytesRead := Read(tid, start, size);

-}

-

-procedure {:yields} {:layer 1} Read({:linear "tid"} tid: X, start : int, size : int) returns (bytesRead : int)

-requires {:layer 1} tid != nil;

-requires {:layer 1} 0 <= start && 0 <= size;

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

-ensures {:layer 1} 0 <= bytesRead && bytesRead <= size;

-{

-    var i, tmp: int;

-

-    par YieldToReadCache(tid);

-    bytesRead := size;

-    call acquire(tid);

-    call i := ReadCurrsize(tid);

-    call tmp := ReadNewsize(tid);

-    if (start + size <= i) {

-        call release(tid); 

-    	goto COPY_TO_BUFFER;

-    } else if (tmp > i) {

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

-    	call release(tid); 

-	goto COPY_TO_BUFFER;

-    } else {

-        call WriteNewsize(tid, start + size);

-    	call release(tid); 

-	goto READ_DEVICE;

-    }

-

-READ_DEVICE:

-    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 YieldToReadCache(tid);

-    call ReadCache(tid, start, bytesRead);

-}

-

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

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

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

-ensures {:layer 1} ghostLock == tid;

-ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;

-{

-    var j: int;

-

-    par YieldToWriteCache(tid);

-    call j := ReadCurrsize(tid);

-    while (j < index)

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

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

-    {

-        par YieldToWriteCache(tid);

-        call WriteCacheEntry(tid, j);

-	j := j + 1;

-    }

-    par YieldToWriteCache(tid);

-}

-

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

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

-requires {:layer 1} tid != nil;

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

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

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

-{

-    var j: int;

-

-    par YieldToReadCache(tid);

-

-    j := 0;

-    while(j < bytesRead)

-    invariant {:layer 1} 0 <= j;

-    invariant {:layer 1} bytesRead == 0 || start + bytesRead <= currsize; 

-    invariant {:layer 1} Inv(ghostLock, currsize, newsize);

-    {

-	assert {:layer 1} start + j < currsize;

-        call ReadCacheEntry(tid, start + j);

-        j := j + 1;

-	par YieldToReadCache(tid);

-    }

-

-    par YieldToReadCache(tid);

-}

-

-procedure {:yields} {:layer 0,1} Init({:linear_in "tid"} xls:[X]bool);

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

-

-procedure {:yields} {:layer 0,1} ReadCurrsize({:linear "tid"} tid: X) returns (val: int);

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

-

-procedure {:yields} {:layer 0,1} ReadNewsize({:linear "tid"} tid: X) returns (val: int);

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

-

-procedure {:yields} {:layer 0,1} WriteNewsize({:linear "tid"} tid: X, val: int);

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

-

-procedure {:yields} {:layer 0,1} WriteCurrsize({:linear "tid"} tid: X, val: int);

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

-

-procedure {:yields} {:layer 0,1} ReadCacheEntry({:linear "tid"} tid: X, index: int);

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

-

-procedure {:yields} {:layer 0,1} WriteCacheEntry({:linear "tid"} tid: X, index: int);

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

-

-procedure {:yields} {:layer 0,1} acquire({:linear "tid"} tid: X);

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

-

-procedure {:yields} {:layer 0,1} release({:linear "tid"} tid: X);

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

-

-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: X);

-ensures {:atomic} |{ A: assume tid != nil; return true; }|;

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
+const nil: X;
+var {:layer 0,1} ghostLock: X;
+var {:layer 0,1} lock: X;
+var {:layer 0,1} currsize: int;
+var {:layer 0,1} newsize: int;
+
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+  MapConstBool(false)[x := true]
+}
+function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool
+{
+  x
+}
+
+function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
+{
+    0 <= currsize && currsize <= newsize && 
+    (ghostLock == nil <==> currsize == newsize)
+}
+
+procedure {:yields} {:layer 1} Yield()
+requires {:layer 1} Inv(ghostLock, currsize, newsize);
+ensures {:layer 1} Inv(ghostLock, currsize, newsize);
+{
+   yield;
+   assert {:layer 1} Inv(ghostLock, currsize, newsize);
+}
+
+procedure {:yields} {:layer 1} YieldToReadCache({:linear "tid"} tid: X)
+requires {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil;
+ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;
+{
+   yield;
+   assert {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;
+}
+
+procedure {:yields} {:layer 1} YieldToWriteCache({:linear "tid"} tid: X)
+requires {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid != nil;
+ensures {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;
+{
+    yield;
+    assert {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;
+}
+
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X)
+ensures {:layer 1} xl != nil;
+{
+    yield;
+    call xl := AllocateLow();
+    yield;
+}
+
+procedure {:yields} {:layer 1} main({:linear_in "tid"} xls: [X]bool)
+requires {:layer 1} xls == mapconstbool(true);
+{
+    var {:linear "tid"} tid: X;
+
+    yield;
+
+    call Init(xls);
+    
+    yield;
+    assert {:layer 1} Inv(ghostLock, currsize, newsize);
+
+    while (*)
+    invariant {:layer 1} Inv(ghostLock, currsize, newsize);
+    {
+        par tid := Allocate() | Yield();
+	yield;
+    	assert {:layer 1} Inv(ghostLock, currsize, newsize);
+        async call Thread(tid);
+	yield;
+    	assert {:layer 1} Inv(ghostLock, currsize, newsize);
+    }
+    yield;
+}
+
+procedure {:yields} {:layer 1} Thread({:linear "tid"} tid: X)
+requires {:layer 1} tid != nil;
+requires {:layer 1} Inv(ghostLock, currsize, newsize);
+{
+    var start, size, bytesRead: int;
+
+    havoc start, size;
+    assume (0 <= start && 0 <= size);
+    call bytesRead := Read(tid, start, size);
+}
+
+procedure {:yields} {:layer 1} Read({:linear "tid"} tid: X, start : int, size : int) returns (bytesRead : int)
+requires {:layer 1} tid != nil;
+requires {:layer 1} 0 <= start && 0 <= size;
+requires {:layer 1} Inv(ghostLock, currsize, newsize);
+ensures {:layer 1} 0 <= bytesRead && bytesRead <= size;
+{
+    var i, tmp: int;
+
+    par YieldToReadCache(tid);
+    bytesRead := size;
+    call acquire(tid);
+    call i := ReadCurrsize(tid);
+    call tmp := ReadNewsize(tid);
+    if (start + size <= i) {
+        call release(tid); 
+    	goto COPY_TO_BUFFER;
+    } else if (tmp > i) {
+        bytesRead := if (start <= i) then (i - start) else 0;
+    	call release(tid); 
+	goto COPY_TO_BUFFER;
+    } else {
+        call WriteNewsize(tid, start + size);
+    	call release(tid); 
+	goto READ_DEVICE;
+    }
+
+READ_DEVICE:
+    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 YieldToReadCache(tid);
+    call ReadCache(tid, start, bytesRead);
+}
+
+procedure {:yields} {:layer 1} WriteCache({:linear "tid"} tid: X, index: int)
+requires {:layer 1} Inv(ghostLock, currsize, newsize);
+requires {:layer 1} ghostLock == tid && tid != nil;
+ensures {:layer 1} ghostLock == tid;
+ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;
+{
+    var j: int;
+
+    par YieldToWriteCache(tid);
+    call j := ReadCurrsize(tid);
+    while (j < index)
+    invariant {:layer 1} ghostLock == tid && currsize <= j && tid == tid;
+    invariant {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;
+    {
+        par YieldToWriteCache(tid);
+        call WriteCacheEntry(tid, j);
+	j := j + 1;
+    }
+    par YieldToWriteCache(tid);
+}
+
+procedure {:yields} {:layer 1} ReadCache({:linear "tid"} tid: X, start: int, bytesRead: int)
+requires {:layer 1} Inv(ghostLock, currsize, newsize);
+requires {:layer 1} tid != nil;
+requires {:layer 1} 0 <= start && 0 <= bytesRead;
+requires {:layer 1} (bytesRead == 0 || start + bytesRead <= currsize);
+ensures {:layer 1} Inv(ghostLock, currsize, newsize);
+{
+    var j: int;
+
+    par YieldToReadCache(tid);
+
+    j := 0;
+    while(j < bytesRead)
+    invariant {:layer 1} 0 <= j;
+    invariant {:layer 1} bytesRead == 0 || start + bytesRead <= currsize; 
+    invariant {:layer 1} Inv(ghostLock, currsize, newsize);
+    {
+	assert {:layer 1} start + j < currsize;
+        call ReadCacheEntry(tid, start + j);
+        j := j + 1;
+	par YieldToReadCache(tid);
+    }
+
+    par YieldToReadCache(tid);
+}
+
+procedure {:yields} {:layer 0,1} Init({:linear_in "tid"} xls:[X]bool);
+ensures {:atomic} |{ A: assert xls == mapconstbool(true); currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|;
+
+procedure {:yields} {:layer 0,1} ReadCurrsize({:linear "tid"} tid: X) returns (val: int);
+ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := currsize; return true; }|;
+
+procedure {:yields} {:layer 0,1} ReadNewsize({:linear "tid"} tid: X) returns (val: int);
+ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := newsize; return true; }|;
+
+procedure {:yields} {:layer 0,1} WriteNewsize({:linear "tid"} tid: X, val: int);
+ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == nil; newsize := val; ghostLock := tid; return true; }|;
+
+procedure {:yields} {:layer 0,1} WriteCurrsize({:linear "tid"} tid: X, val: int);
+ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == tid; currsize := val; ghostLock := nil; return true; }|;
+
+procedure {:yields} {:layer 0,1} ReadCacheEntry({:linear "tid"} tid: X, index: int);
+ensures {:atomic} |{ A: assert 0 <= index && index < currsize; return true; }|;
+
+procedure {:yields} {:layer 0,1} WriteCacheEntry({:linear "tid"} tid: X, index: int);
+ensures {:right} |{ A: assert tid != nil; assert currsize <= index && ghostLock == tid; return true; }|;
+
+procedure {:yields} {:layer 0,1} acquire({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;
+
+procedure {:yields} {:layer 0,1} release({:linear "tid"} tid: X);
+ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|;
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assume tid != nil; return true; }|;
diff --git a/Test/civl/DeviceCache.bpl.expect b/Test/civl/DeviceCache.bpl.expect
index 9ec7a92d..c4cf5ccf 100644
--- a/Test/civl/DeviceCache.bpl.expect
+++ b/Test/civl/DeviceCache.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 30 verified, 0 errors

+
+Boogie program verifier finished with 30 verified, 0 errors
diff --git a/Test/civl/FlanaganQadeer.bpl b/Test/civl/FlanaganQadeer.bpl
index 7345b5b2..97df7ce2 100644
--- a/Test/civl/FlanaganQadeer.bpl
+++ b/Test/civl/FlanaganQadeer.bpl
@@ -1,75 +1,75 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-type X;

-const nil: X;

-var {:layer 0,1} l: X;

-var {:layer 0,1} x: int;

-

-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

-function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

-{

-  MapConstBool(false)[x := true]

-}

-

-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X)

-ensures {:layer 1} xl != nil;

-{

-    yield;

-    call xl := AllocateLow();

-    yield;

-}

-

-procedure {:yields} {:layer 1} main()

-{

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

-    var val: int;

-

-    yield;

-    while (*) 

-    {

-        call tid := Allocate();

-        havoc val;

-        async call foo(tid, val);

-	yield;

-    }

-    yield;

-}

-procedure {:yields} {:layer 0,1} Lock(tid: X);

-ensures {:atomic} |{A: assume l == nil; l := tid; return true; }|;

-

-procedure {:yields} {:layer 0,1} Unlock();

-ensures {:atomic} |{A: l := nil; return true; }|;

-

-procedure {:yields} {:layer 0,1} Set(val: int);

-ensures {:atomic} |{A: x := val; return true; }|;

-

-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xl: X);

-ensures {:atomic} |{ A: assume xl != nil; return true; }|;

-

-procedure {:yields} {:layer 1} foo({:linear_in "tid"} tid': X, val: int)

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

-{

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

-    tid := tid';

-

-    yield;

-    call Lock(tid);    

-    call tid := Yield(tid);

-    call Set(val);

-    call tid := Yield(tid);

-    assert {:layer 1} x == val;

-    call tid := Yield(tid);

-    call Unlock();

-    yield;

-}

-

-procedure {:yields} {:layer 1} Yield({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X)

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

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

-ensures {:layer 1} old(l) == tid ==> old(l) == l && old(x) == x;

-{

-    tid := tid';

-    yield;

-    assert {:layer 1} tid != nil;

-    assert {:layer 1} (old(l) == tid ==> old(l) == l && old(x) == x);

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+const nil: X;
+var {:layer 0,1} l: X;
+var {:layer 0,1} x: int;
+
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+  MapConstBool(false)[x := true]
+}
+
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X)
+ensures {:layer 1} xl != nil;
+{
+    yield;
+    call xl := AllocateLow();
+    yield;
+}
+
+procedure {:yields} {:layer 1} main()
+{
+    var {:linear "tid"} tid: X;
+    var val: int;
+
+    yield;
+    while (*) 
+    {
+        call tid := Allocate();
+        havoc val;
+        async call foo(tid, val);
+	yield;
+    }
+    yield;
+}
+procedure {:yields} {:layer 0,1} Lock(tid: X);
+ensures {:atomic} |{A: assume l == nil; l := tid; return true; }|;
+
+procedure {:yields} {:layer 0,1} Unlock();
+ensures {:atomic} |{A: l := nil; return true; }|;
+
+procedure {:yields} {:layer 0,1} Set(val: int);
+ensures {:atomic} |{A: x := val; return true; }|;
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xl: X);
+ensures {:atomic} |{ A: assume xl != nil; return true; }|;
+
+procedure {:yields} {:layer 1} foo({:linear_in "tid"} tid': X, val: int)
+requires {:layer 1} tid' != nil;
+{
+    var {:linear "tid"} tid: X;
+    tid := tid';
+
+    yield;
+    call Lock(tid);    
+    call tid := Yield(tid);
+    call Set(val);
+    call tid := Yield(tid);
+    assert {:layer 1} x == val;
+    call tid := Yield(tid);
+    call Unlock();
+    yield;
+}
+
+procedure {:yields} {:layer 1} Yield({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X)
+requires {:layer 1} tid' != nil;
+ensures {:layer 1} tid == tid';
+ensures {:layer 1} old(l) == tid ==> old(l) == l && old(x) == x;
+{
+    tid := tid';
+    yield;
+    assert {:layer 1} tid != nil;
+    assert {:layer 1} (old(l) == tid ==> old(l) == l && old(x) == x);
 }
\ No newline at end of file
diff --git a/Test/civl/FlanaganQadeer.bpl.expect b/Test/civl/FlanaganQadeer.bpl.expect
index fef5ddc0..00ddb38b 100644
--- a/Test/civl/FlanaganQadeer.bpl.expect
+++ b/Test/civl/FlanaganQadeer.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 4 verified, 0 errors

+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/Program1.bpl b/Test/civl/Program1.bpl
index f405b92a..5fe49480 100644
--- a/Test/civl/Program1.bpl
+++ b/Test/civl/Program1.bpl
@@ -1,33 +1,33 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var {:layer 0,1} x:int;

-

-procedure {:yields} {:layer 1} p() 

-requires {:layer 1} x >= 5; 

-ensures {:layer 1} x >= 8; 

-{ 

-    yield;

-    assert {:layer 1} x >= 5; 

-    call Incr(1); 

-    yield;

-    assert {:layer 1} x >= 6; 

-    call Incr(1); 

-    yield;

-    assert {:layer 1} x >= 7;

-    call Incr(1); 

-    yield;

-    assert {:layer 1} x >= 8; 

-}

-

-procedure {:yields} {:layer 1} q() 

-{ 

-    yield;

-    call Incr(3); 

-    yield;

-}

-

-procedure {:yields} {:layer 0,1} Incr(val: int);

-ensures {:atomic}

-|{A:

-  x := x + val; return true;

-}|;

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,1} x:int;
+
+procedure {:yields} {:layer 1} p() 
+requires {:layer 1} x >= 5; 
+ensures {:layer 1} x >= 8; 
+{ 
+    yield;
+    assert {:layer 1} x >= 5; 
+    call Incr(1); 
+    yield;
+    assert {:layer 1} x >= 6; 
+    call Incr(1); 
+    yield;
+    assert {:layer 1} x >= 7;
+    call Incr(1); 
+    yield;
+    assert {:layer 1} x >= 8; 
+}
+
+procedure {:yields} {:layer 1} q() 
+{ 
+    yield;
+    call Incr(3); 
+    yield;
+}
+
+procedure {:yields} {:layer 0,1} Incr(val: int);
+ensures {:atomic}
+|{A:
+  x := x + val; return true;
+}|;
diff --git a/Test/civl/Program1.bpl.expect b/Test/civl/Program1.bpl.expect
index 3de74d3e..41374b00 100644
--- a/Test/civl/Program1.bpl.expect
+++ b/Test/civl/Program1.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 2 verified, 0 errors

+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/civl/Program2.bpl b/Test/civl/Program2.bpl
index 75c83c67..16b20cf2 100644
--- a/Test/civl/Program2.bpl
+++ b/Test/civl/Program2.bpl
@@ -1,37 +1,37 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var {:layer 0,1} x:int;

-

-procedure {:yields} {:layer 1} yield_x(n: int)

-requires {:layer 1} x >= n; 

-ensures {:layer 1} x >= n; 

-{

-    yield;

-    assert {:layer 1} x >= n;

-}

-

-procedure {:yields} {:layer 1} p() 

-requires {:layer 1} x >= 5; 

-ensures {:layer 1} x >= 8; 

-{ 

-    call yield_x(5);

-    call Incr(1); 

-    call yield_x(6);

-    call Incr(1); 

-    call yield_x(7);

-    call Incr(1); 

-    call yield_x(8);

-}

-

-procedure {:yields} {:layer 1} q() 

-{ 

-    yield;

-    call Incr(3); 

-    yield;

-}

-

-procedure {:yields} {:layer 0,1} Incr(val: int);

-ensures {:atomic}

-|{A:

-  x := x + val; return true;

-}|;

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,1} x:int;
+
+procedure {:yields} {:layer 1} yield_x(n: int)
+requires {:layer 1} x >= n; 
+ensures {:layer 1} x >= n; 
+{
+    yield;
+    assert {:layer 1} x >= n;
+}
+
+procedure {:yields} {:layer 1} p() 
+requires {:layer 1} x >= 5; 
+ensures {:layer 1} x >= 8; 
+{ 
+    call yield_x(5);
+    call Incr(1); 
+    call yield_x(6);
+    call Incr(1); 
+    call yield_x(7);
+    call Incr(1); 
+    call yield_x(8);
+}
+
+procedure {:yields} {:layer 1} q() 
+{ 
+    yield;
+    call Incr(3); 
+    yield;
+}
+
+procedure {:yields} {:layer 0,1} Incr(val: int);
+ensures {:atomic}
+|{A:
+  x := x + val; return true;
+}|;
diff --git a/Test/civl/Program2.bpl.expect b/Test/civl/Program2.bpl.expect
index 5b2909f1..a9949f2e 100644
--- a/Test/civl/Program2.bpl.expect
+++ b/Test/civl/Program2.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 3 verified, 0 errors

+
+Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/civl/Program3.bpl b/Test/civl/Program3.bpl
index f8c4e132..565279e7 100644
--- a/Test/civl/Program3.bpl
+++ b/Test/civl/Program3.bpl
@@ -1,36 +1,36 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var {:layer 0,1} x:int;

-

-procedure {:yields} {:layer 1} yield_x()

-ensures {:layer 1} x >= old(x); 

-{

-    yield;

-    assert {:layer 1} x >= old(x);

-}

-

-procedure {:yields} {:layer 1} p() 

-requires {:layer 1} x >= 5; 

-ensures {:layer 1} x >= 8; 

-{ 

-    call yield_x();

-    call Incr(1); 

-    call yield_x();

-    call Incr(1); 

-    call yield_x();

-    call Incr(1); 

-    call yield_x();

-}

-

-procedure {:yields} {:layer 1} q() 

-{ 

-    yield;

-    call Incr(3); 

-    yield;

-}

-

-procedure {:yields} {:layer 0,1} Incr(val: int);

-ensures {:atomic}

-|{A:

-  x := x + val; return true;

-}|;

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,1} x:int;
+
+procedure {:yields} {:layer 1} yield_x()
+ensures {:layer 1} x >= old(x); 
+{
+    yield;
+    assert {:layer 1} x >= old(x);
+}
+
+procedure {:yields} {:layer 1} p() 
+requires {:layer 1} x >= 5; 
+ensures {:layer 1} x >= 8; 
+{ 
+    call yield_x();
+    call Incr(1); 
+    call yield_x();
+    call Incr(1); 
+    call yield_x();
+    call Incr(1); 
+    call yield_x();
+}
+
+procedure {:yields} {:layer 1} q() 
+{ 
+    yield;
+    call Incr(3); 
+    yield;
+}
+
+procedure {:yields} {:layer 0,1} Incr(val: int);
+ensures {:atomic}
+|{A:
+  x := x + val; return true;
+}|;
diff --git a/Test/civl/Program3.bpl.expect b/Test/civl/Program3.bpl.expect
index 5b2909f1..a9949f2e 100644
--- a/Test/civl/Program3.bpl.expect
+++ b/Test/civl/Program3.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 3 verified, 0 errors

+
+Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl
index 7f2f9c44..68c2a5f3 100644
--- a/Test/civl/Program4.bpl
+++ b/Test/civl/Program4.bpl
@@ -1,68 +1,68 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-type Tid; 

-var {:layer 0,1} a:[Tid]int;

-

-procedure {:yields} {:layer 1} main() { 

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

-

-    yield;

-    while (true) { 

-        call tid := Allocate(); 

-	async call P(tid); 

-	yield;

-    }

-    yield;

-}

-

-procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid) 

-ensures {:layer 1} a[tid] == old(a)[tid] + 1; 

-{ 

-    var t:int;

-

-    yield;

-    assert {:layer 1} a[tid] == old(a)[tid];

-    call t := Read(tid); 

-    yield;

-    assert {:layer 1} a[tid] == t; 

-    call Write(tid, t + 1); 

-    yield;

-    assert {:layer 1} a[tid] == t + 1; 

-}

-

-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid)

-{

-    yield;

-    call tid := AllocateLow();

-    yield;

-}

-

-procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);

-ensures {:atomic}

-|{A:

-  val := a[tid]; return true;

-}|;

-

-procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int);

-ensures {:atomic}

-|{A:

-  a[tid] := val; return true;

-}|;

-

-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid);

-ensures {:atomic} |{ A: return true; }|;

-

-

-

-function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;

-function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;

-

-function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool

-{

-  MapConstBool(false)[x := true]

-}

-function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool

-{

-  x

-}

-

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type Tid; 
+var {:layer 0,1} a:[Tid]int;
+
+procedure {:yields} {:layer 1} main() { 
+    var {:linear "tid"} tid:Tid;
+
+    yield;
+    while (true) { 
+        call tid := Allocate(); 
+	async call P(tid); 
+	yield;
+    }
+    yield;
+}
+
+procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid) 
+ensures {:layer 1} a[tid] == old(a)[tid] + 1; 
+{ 
+    var t:int;
+
+    yield;
+    assert {:layer 1} a[tid] == old(a)[tid];
+    call t := Read(tid); 
+    yield;
+    assert {:layer 1} a[tid] == t; 
+    call Write(tid, t + 1); 
+    yield;
+    assert {:layer 1} a[tid] == t + 1; 
+}
+
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid)
+{
+    yield;
+    call tid := AllocateLow();
+    yield;
+}
+
+procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);
+ensures {:atomic}
+|{A:
+  val := a[tid]; return true;
+}|;
+
+procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int);
+ensures {:atomic}
+|{A:
+  a[tid] := val; return true;
+}|;
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid);
+ensures {:atomic} |{ A: return true; }|;
+
+
+
+function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;
+function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;
+
+function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
+{
+  MapConstBool(false)[x := true]
+}
+function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
+{
+  x
+}
+
diff --git a/Test/civl/Program4.bpl.expect b/Test/civl/Program4.bpl.expect
index 5b2909f1..a9949f2e 100644
--- a/Test/civl/Program4.bpl.expect
+++ b/Test/civl/Program4.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 3 verified, 0 errors

+
+Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/civl/Program5.bpl.expect b/Test/civl/Program5.bpl.expect
index d7c0ff95..fde7e712 100644
--- a/Test/civl/Program5.bpl.expect
+++ b/Test/civl/Program5.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 18 verified, 0 errors

+
+Boogie program verifier finished with 18 verified, 0 errors
diff --git a/Test/civl/akash.bpl b/Test/civl/akash.bpl
index c826b810..fabfcea5 100644
--- a/Test/civl/akash.bpl
+++ b/Test/civl/akash.bpl
@@ -1,106 +1,106 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

-

-function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

-function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

-{

-  MapConstBool(false)[x := true]

-}

-

-function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool

-{

-  x

-}

-

-function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool

-{

-  x

-}

-

-var {:layer 0,1} g: int;

-var {:layer 0,1} h: int;

-

-procedure {:yields} {:layer 0,1} SetG(val:int);

-ensures {:atomic} |{A: g := val; return true; }|;

-

-procedure {:yields} {:layer 0,1} SetH(val:int);

-ensures {:atomic} |{A: h := val; return true; }|;

-

-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int)

-ensures {:layer 1} xl != 0;

-{

-    yield;

-    call xl := AllocateLow();

-    yield;

-}

-

-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int);

-ensures {:atomic} |{ A: assume xls != 0; return true; }|;

-

-procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int)

-requires {:layer 1} x == mapconstbool(true);

-requires {:layer 1} y == mapconstbool(true);

-{

-    var {:linear "tid"} tid_child: int;

-    tid_out := tid_in;    

-

-    yield;

-    call SetG(0);

-    yield;

-    assert {:layer 1} g == 0 && x == mapconstbool(true);    

-

-    yield;

-    call tid_child := Allocate();

-    async call B(tid_child, x);

-

-    yield;

-    call SetH(0);

-

-    yield;

-    assert {:layer 1} h == 0 && y == mapconstbool(true);    

-

-    yield;

-    call tid_child := Allocate();

-    async call C(tid_child, y);

-

-    yield;

-}

-

-procedure {:yields} {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) 

-requires {:layer 1} x_in != mapconstbool(false);

-{

-    var {:linear "tid"} tid_out: int;

-    var {:linear "1"} x: [int]bool;

-    tid_out := tid_in;

-    x := x_in;    

-

-    yield;

-

-    call SetG(1);

-

-    yield;

-

-    call SetG(2);

-

-    yield;

-}

-

-procedure {:yields} {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) 

-requires {:layer 1} y_in != mapconstbool(false);

-{

-    var {:linear "tid"} tid_out: int;

-    var {:linear "2"} y: [int]bool;

-    tid_out := tid_in;

-    y := y_in;    

-

-    yield;

-

-    call SetH(1);

-

-    yield;

-

-    call SetH(2);

-

-    yield;

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
+
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
+{
+  MapConstBool(false)[x := true]
+}
+
+function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool
+{
+  x
+}
+
+function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool
+{
+  x
+}
+
+var {:layer 0,1} g: int;
+var {:layer 0,1} h: int;
+
+procedure {:yields} {:layer 0,1} SetG(val:int);
+ensures {:atomic} |{A: g := val; return true; }|;
+
+procedure {:yields} {:layer 0,1} SetH(val:int);
+ensures {:atomic} |{A: h := val; return true; }|;
+
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int)
+ensures {:layer 1} xl != 0;
+{
+    yield;
+    call xl := AllocateLow();
+    yield;
+}
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int);
+ensures {:atomic} |{ A: assume xls != 0; return true; }|;
+
+procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int)
+requires {:layer 1} x == mapconstbool(true);
+requires {:layer 1} y == mapconstbool(true);
+{
+    var {:linear "tid"} tid_child: int;
+    tid_out := tid_in;    
+
+    yield;
+    call SetG(0);
+    yield;
+    assert {:layer 1} g == 0 && x == mapconstbool(true);    
+
+    yield;
+    call tid_child := Allocate();
+    async call B(tid_child, x);
+
+    yield;
+    call SetH(0);
+
+    yield;
+    assert {:layer 1} h == 0 && y == mapconstbool(true);    
+
+    yield;
+    call tid_child := Allocate();
+    async call C(tid_child, y);
+
+    yield;
+}
+
+procedure {:yields} {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) 
+requires {:layer 1} x_in != mapconstbool(false);
+{
+    var {:linear "tid"} tid_out: int;
+    var {:linear "1"} x: [int]bool;
+    tid_out := tid_in;
+    x := x_in;    
+
+    yield;
+
+    call SetG(1);
+
+    yield;
+
+    call SetG(2);
+
+    yield;
+}
+
+procedure {:yields} {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) 
+requires {:layer 1} y_in != mapconstbool(false);
+{
+    var {:linear "tid"} tid_out: int;
+    var {:linear "2"} y: [int]bool;
+    tid_out := tid_in;
+    y := y_in;    
+
+    yield;
+
+    call SetH(1);
+
+    yield;
+
+    call SetH(2);
+
+    yield;
 }
\ No newline at end of file
diff --git a/Test/civl/akash.bpl.expect b/Test/civl/akash.bpl.expect
index fef5ddc0..00ddb38b 100644
--- a/Test/civl/akash.bpl.expect
+++ b/Test/civl/akash.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 4 verified, 0 errors

+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/bar.bpl b/Test/civl/bar.bpl
index 4eef8378..b5068edd 100644
--- a/Test/civl/bar.bpl
+++ b/Test/civl/bar.bpl
@@ -1,57 +1,57 @@
-// RUN: %boogie -noinfer "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var {:layer 0,1} g:int;

-

-procedure {:yields} {:layer 1} PB()

-{

-  yield;

-  call Incr();

-  yield;

-}

-

-procedure {:yields} {:layer 0,1} Incr();

-ensures {:atomic}

-|{A:

-  g := g + 1; return true;

-}|;

-

-procedure {:yields} {:layer 0,1} Set(v: int);

-ensures {:atomic}

-|{A:

-  g := v; return true;

-}|;

-

-procedure {:yields} {:layer 1} PC()

-ensures {:layer 1} g == old(g);

-{

-  yield;

-  assert {:layer 1} g == old(g);

-}

-

-procedure {:yields} {:layer 1} PE()

-{

-  call PC();

-}

-

-procedure {:yields} {:layer 1} PD()

-{

-  yield;

-  call Set(3);

-  call PC();

-  assert {:layer 1} g == 3;

-}

-

-procedure {:yields} {:layer 1} Main2()

-{

-  yield;

-  while (*)

-  {

-    async call PB();

-    yield;

-    async call PE();

-    yield;

-    async call PD();

-    yield;

-  }

-  yield;

-}

+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,1} g:int;
+
+procedure {:yields} {:layer 1} PB()
+{
+  yield;
+  call Incr();
+  yield;
+}
+
+procedure {:yields} {:layer 0,1} Incr();
+ensures {:atomic}
+|{A:
+  g := g + 1; return true;
+}|;
+
+procedure {:yields} {:layer 0,1} Set(v: int);
+ensures {:atomic}
+|{A:
+  g := v; return true;
+}|;
+
+procedure {:yields} {:layer 1} PC()
+ensures {:layer 1} g == old(g);
+{
+  yield;
+  assert {:layer 1} g == old(g);
+}
+
+procedure {:yields} {:layer 1} PE()
+{
+  call PC();
+}
+
+procedure {:yields} {:layer 1} PD()
+{
+  yield;
+  call Set(3);
+  call PC();
+  assert {:layer 1} g == 3;
+}
+
+procedure {:yields} {:layer 1} Main2()
+{
+  yield;
+  while (*)
+  {
+    async call PB();
+    yield;
+    async call PE();
+    yield;
+    async call PD();
+    yield;
+  }
+  yield;
+}
diff --git a/Test/civl/chris.bpl b/Test/civl/chris.bpl
index b54292ef..d755c76d 100644
--- a/Test/civl/chris.bpl
+++ b/Test/civl/chris.bpl
@@ -1,28 +1,28 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var{:layer 1} x:int;

-

-procedure{:yields}{:layer 2} Havoc()

-  ensures{:atomic} |{ A: return true; }|;

-{

-  yield;

-}

-

-procedure{:yields}{:layer 1} Recover()

-  ensures{:atomic} |{ A: assert x == 5; return true; }|;

-{

-  yield;

-}

-

-procedure{:yields}{:layer 3} P()

-  ensures{:atomic} |{ A: return true; }|;

-  requires{:layer 2,3} x == 5;

-  ensures {:layer 2,3} x == 5;

-{

-

-  yield; assert{:layer 2,3} x == 5;

-  call Havoc();

-  yield; assert{:layer 3} x == 5;

-  call Recover();

-  yield; assert{:layer 2,3} x == 5;

-}

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var{:layer 1} x:int;
+
+procedure{:yields}{:layer 2} Havoc()
+  ensures{:atomic} |{ A: return true; }|;
+{
+  yield;
+}
+
+procedure{:yields}{:layer 1} Recover()
+  ensures{:atomic} |{ A: assert x == 5; return true; }|;
+{
+  yield;
+}
+
+procedure{:yields}{:layer 3} P()
+  ensures{:atomic} |{ A: return true; }|;
+  requires{:layer 2,3} x == 5;
+  ensures {:layer 2,3} x == 5;
+{
+
+  yield; assert{:layer 2,3} x == 5;
+  call Havoc();
+  yield; assert{:layer 3} x == 5;
+  call Recover();
+  yield; assert{:layer 2,3} x == 5;
+}
diff --git a/Test/civl/chris.bpl.expect b/Test/civl/chris.bpl.expect
index be6b95ba..9823d44a 100644
--- a/Test/civl/chris.bpl.expect
+++ b/Test/civl/chris.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 6 verified, 0 errors

+
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/civl/chris2.bpl b/Test/civl/chris2.bpl
index 73f112ed..268c6aa3 100644
--- a/Test/civl/chris2.bpl
+++ b/Test/civl/chris2.bpl
@@ -1,34 +1,34 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var{:layer 20} x:int;

-

-procedure{:yields}{:layer 20,25} p_gt1_lower();

-  ensures{:both}

-  |{

-    A:

-    x := x + 1;

-    return true;

-  }|;

-

-procedure{:yields}{:layer 25,40} p_gt1()

-  ensures{:both}

-  |{

-    A:

-    x := x + 1;

-    return true;

-  }|;

-{

-  yield;

-  call p_gt1_lower();

-  yield;

-}

-

-procedure{:yields}{:layer 20,40} p_gt2();

-  ensures{:both}

-  |{

-    A:

-    assert x == 0;

-    return true;

-  }|;

-

-

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var{:layer 20} x:int;
+
+procedure{:yields}{:layer 20,25} p_gt1_lower();
+  ensures{:both}
+  |{
+    A:
+    x := x + 1;
+    return true;
+  }|;
+
+procedure{:yields}{:layer 25,40} p_gt1()
+  ensures{:both}
+  |{
+    A:
+    x := x + 1;
+    return true;
+  }|;
+{
+  yield;
+  call p_gt1_lower();
+  yield;
+}
+
+procedure{:yields}{:layer 20,40} p_gt2();
+  ensures{:both}
+  |{
+    A:
+    assert x == 0;
+    return true;
+  }|;
+
+
diff --git a/Test/civl/chris2.bpl.expect b/Test/civl/chris2.bpl.expect
index 2bf339f7..ddb8537e 100644
--- a/Test/civl/chris2.bpl.expect
+++ b/Test/civl/chris2.bpl.expect
@@ -1,18 +1,18 @@
-(0,0): Error BP5003: A postcondition might not hold on this return path.

-chris2.bpl(30,5): Related location: Gate not preserved by p_gt1_lower

-Execution trace:

-    (0,0): this_A

-(0,0): Error BP5003: A postcondition might not hold on this return path.

-(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1_lower

-Execution trace:

-    (0,0): this_A

-(0,0): Error BP5003: A postcondition might not hold on this return path.

-chris2.bpl(30,5): Related location: Gate not preserved by p_gt1

-Execution trace:

-    (0,0): this_A

-(0,0): Error BP5003: A postcondition might not hold on this return path.

-(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1

-Execution trace:

-    (0,0): this_A

-

-Boogie program verifier finished with 1 verified, 4 errors

+(0,0): Error BP5003: A postcondition might not hold on this return path.
+chris2.bpl(30,5): Related location: Gate not preserved by p_gt1_lower
+Execution trace:
+    (0,0): this_A
+(0,0): Error BP5003: A postcondition might not hold on this return path.
+(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1_lower
+Execution trace:
+    (0,0): this_A
+(0,0): Error BP5003: A postcondition might not hold on this return path.
+chris2.bpl(30,5): Related location: Gate not preserved by p_gt1
+Execution trace:
+    (0,0): this_A
+(0,0): Error BP5003: A postcondition might not hold on this return path.
+(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1
+Execution trace:
+    (0,0): this_A
+
+Boogie program verifier finished with 1 verified, 4 errors
diff --git a/Test/civl/civl-paper.bpl b/Test/civl/civl-paper.bpl
index a7042c6a..6cac5cea 100644
--- a/Test/civl/civl-paper.bpl
+++ b/Test/civl/civl-paper.bpl
@@ -1,175 +1,175 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-type X;

-const nil: X;

-

-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

-function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

-{

-  MapConstBool(false)[x := true]

-}

-

-type lmap;

-function {:linear "mem"} dom(lmap): [int]bool;

-function map(lmap): [int]int;

-function cons([int]bool, [int]int) : lmap;

-axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y);

-

-var {:layer 0,3} {:linear "mem"} g: lmap;

-var {:layer 0,3} lock: X;

-var {:layer 0,1} b: bool;

-

-const p: int;

-

-procedure {:yields} {:layer 1} Yield1()

-requires {:layer 1} InvLock(lock, b);

-ensures {:layer 1} InvLock(lock, b);

-{

-    yield;

-    assert {:layer 1} InvLock(lock, b);

-}

-

-function {:inline} InvLock(lock: X, b: bool) : bool

-{

-    lock != nil <==> b

-}

-

-procedure {:yields} {:layer 2} Yield2()

-{

-    yield;

-}

-

-procedure {:yields} {:layer 3} Yield3()

-requires {:layer 3} Inv(g);

-ensures {:layer 3} Inv(g);

-{

-    yield;

-    assert {:layer 3} Inv(g);

-}

-

-function {:inline} Inv(g: lmap) : bool

-{

-    dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4]

-}

-

-procedure {:yields} {:layer 3} P({:linear "tid"} tid: X)

-requires {:layer 1} tid != nil && InvLock(lock, b);

-ensures {:layer 1} InvLock(lock, b);

-requires {:layer 3} tid != nil && Inv(g);

-ensures {:layer 3} Inv(g);

-{

-    var t: int;

-    var {:linear "mem"} l: lmap;

-

-    par Yield3() | Yield1();

-    call AcquireProtected(tid);

-    call l := TransferFromGlobalProtected(tid);

-    call t := Load(l, p);

-    call l := Store(l, p, t+1);

-    call t := Load(l, p+4);

-    call l := Store(l, p+4, t+1);

-    call TransferToGlobalProtected(tid, l);

-    call ReleaseProtected(tid);

-    par Yield3() | Yield1();

-}

-

-

-procedure {:yields} {:layer 2,3} TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap)

-ensures {:both} |{ A: assert tid != nil && lock == tid; g := l; return true; }|;

-requires {:layer 1} InvLock(lock, b);

-ensures {:layer 1} InvLock(lock, b);

-{

-  par Yield1() | Yield2();

-  call TransferToGlobal(tid, l);

-  par Yield1() | Yield2();

-}

-

-procedure {:yields} {:layer 2,3} TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap)

-ensures {:both} |{ A: assert tid != nil && lock == tid; l := g; return true; }|;

-requires {:layer 1} InvLock(lock, b);

-ensures {:layer 1} InvLock(lock, b);

-{

-  par Yield1() | Yield2();

-  call l := TransferFromGlobal(tid);

-  par Yield1() | Yield2();

-}

-

-procedure {:yields} {:layer 2,3} AcquireProtected({:linear "tid"} tid: X)

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

-requires {:layer 1} tid != nil && InvLock(lock, b);

-ensures {:layer 1} InvLock(lock, b);

-{

-  par Yield1() | Yield2();

-  call Acquire(tid);

-  par Yield1() | Yield2();

-}

-

-procedure {:yields} {:layer 2,3} ReleaseProtected({:linear "tid"} tid: X)

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

-requires {:layer 1} InvLock(lock, b);

-ensures {:layer 1} InvLock(lock, b);

-{

-  par Yield1() | Yield2();

-  call Release(tid);

-  par Yield1() | Yield2();

-}

-

-procedure {:yields} {:layer 1,2} Acquire({:linear "tid"} tid: X)

-requires {:layer 1} tid != nil && InvLock(lock, b);

-ensures {:layer 1} InvLock(lock, b);

-ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|;

-{

-    var status: bool;

-    var tmp: X;

-

-    par Yield1();

-    L: 

-	assert {:layer 1} InvLock(lock, b);

-        call status := CAS(tid, false, true);

-	par Yield1();

-        goto A, B;

-

-    A: 

-        assume status;

-	par Yield1();	

-	return;

-

-    B:

-        assume !status;

-	goto L;

-}

-

-procedure {:yields} {:layer 1,2} Release({:linear "tid"} tid: X)

-ensures {:atomic} |{ A: lock := nil; return true; }|;

-requires {:layer 1} InvLock(lock, b);

-ensures {:layer 1} InvLock(lock, b);

-{

-    par Yield1();

-    call CLEAR(tid, false);

-    par Yield1();

-}

-

-procedure {:yields} {:layer 0,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap);

-ensures {:atomic} |{ A: g := l; return true; }|;

-

-procedure {:yields} {:layer 0,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap);

-ensures {:atomic} |{ A: l := g; return true; }|;

-

-procedure {:yields} {:layer 0,3} Load({:linear "mem"} l: lmap, a: int) returns (v: int);

-ensures {:both} |{ A: v := map(l)[a]; return true; }|;

-

-procedure {:yields} {:layer 0,3} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);

-ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;

-

-procedure {:yields} {:layer 0,1} CAS(tid: X, prev: bool, next: bool) returns (status: bool);

-ensures {:atomic} |{ 

-A: goto B, C; 

-B: assume b == prev; b := next; status := true; lock := tid; return true; 

-C: status := false; return true; 

-}|;

-

-procedure {:yields} {:layer 0,1} CLEAR(tid: X, next: bool);

-ensures {:atomic} |{ 

-A: b := next; lock := nil; return true; 

-}|;

-

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+const nil: X;
+
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+  MapConstBool(false)[x := true]
+}
+
+type lmap;
+function {:linear "mem"} dom(lmap): [int]bool;
+function map(lmap): [int]int;
+function cons([int]bool, [int]int) : lmap;
+axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y);
+
+var {:layer 0,3} {:linear "mem"} g: lmap;
+var {:layer 0,3} lock: X;
+var {:layer 0,1} b: bool;
+
+const p: int;
+
+procedure {:yields} {:layer 1} Yield1()
+requires {:layer 1} InvLock(lock, b);
+ensures {:layer 1} InvLock(lock, b);
+{
+    yield;
+    assert {:layer 1} InvLock(lock, b);
+}
+
+function {:inline} InvLock(lock: X, b: bool) : bool
+{
+    lock != nil <==> b
+}
+
+procedure {:yields} {:layer 2} Yield2()
+{
+    yield;
+}
+
+procedure {:yields} {:layer 3} Yield3()
+requires {:layer 3} Inv(g);
+ensures {:layer 3} Inv(g);
+{
+    yield;
+    assert {:layer 3} Inv(g);
+}
+
+function {:inline} Inv(g: lmap) : bool
+{
+    dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4]
+}
+
+procedure {:yields} {:layer 3} P({:linear "tid"} tid: X)
+requires {:layer 1} tid != nil && InvLock(lock, b);
+ensures {:layer 1} InvLock(lock, b);
+requires {:layer 3} tid != nil && Inv(g);
+ensures {:layer 3} Inv(g);
+{
+    var t: int;
+    var {:linear "mem"} l: lmap;
+
+    par Yield3() | Yield1();
+    call AcquireProtected(tid);
+    call l := TransferFromGlobalProtected(tid);
+    call t := Load(l, p);
+    call l := Store(l, p, t+1);
+    call t := Load(l, p+4);
+    call l := Store(l, p+4, t+1);
+    call TransferToGlobalProtected(tid, l);
+    call ReleaseProtected(tid);
+    par Yield3() | Yield1();
+}
+
+
+procedure {:yields} {:layer 2,3} TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap)
+ensures {:both} |{ A: assert tid != nil && lock == tid; g := l; return true; }|;
+requires {:layer 1} InvLock(lock, b);
+ensures {:layer 1} InvLock(lock, b);
+{
+  par Yield1() | Yield2();
+  call TransferToGlobal(tid, l);
+  par Yield1() | Yield2();
+}
+
+procedure {:yields} {:layer 2,3} TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap)
+ensures {:both} |{ A: assert tid != nil && lock == tid; l := g; return true; }|;
+requires {:layer 1} InvLock(lock, b);
+ensures {:layer 1} InvLock(lock, b);
+{
+  par Yield1() | Yield2();
+  call l := TransferFromGlobal(tid);
+  par Yield1() | Yield2();
+}
+
+procedure {:yields} {:layer 2,3} AcquireProtected({:linear "tid"} tid: X)
+ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;
+requires {:layer 1} tid != nil && InvLock(lock, b);
+ensures {:layer 1} InvLock(lock, b);
+{
+  par Yield1() | Yield2();
+  call Acquire(tid);
+  par Yield1() | Yield2();
+}
+
+procedure {:yields} {:layer 2,3} ReleaseProtected({:linear "tid"} tid: X)
+ensures {:left} |{ A: assert tid != nil && lock == tid; lock := nil; return true; }|;
+requires {:layer 1} InvLock(lock, b);
+ensures {:layer 1} InvLock(lock, b);
+{
+  par Yield1() | Yield2();
+  call Release(tid);
+  par Yield1() | Yield2();
+}
+
+procedure {:yields} {:layer 1,2} Acquire({:linear "tid"} tid: X)
+requires {:layer 1} tid != nil && InvLock(lock, b);
+ensures {:layer 1} InvLock(lock, b);
+ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|;
+{
+    var status: bool;
+    var tmp: X;
+
+    par Yield1();
+    L: 
+	assert {:layer 1} InvLock(lock, b);
+        call status := CAS(tid, false, true);
+	par Yield1();
+        goto A, B;
+
+    A: 
+        assume status;
+	par Yield1();	
+	return;
+
+    B:
+        assume !status;
+	goto L;
+}
+
+procedure {:yields} {:layer 1,2} Release({:linear "tid"} tid: X)
+ensures {:atomic} |{ A: lock := nil; return true; }|;
+requires {:layer 1} InvLock(lock, b);
+ensures {:layer 1} InvLock(lock, b);
+{
+    par Yield1();
+    call CLEAR(tid, false);
+    par Yield1();
+}
+
+procedure {:yields} {:layer 0,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap);
+ensures {:atomic} |{ A: g := l; return true; }|;
+
+procedure {:yields} {:layer 0,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap);
+ensures {:atomic} |{ A: l := g; return true; }|;
+
+procedure {:yields} {:layer 0,3} Load({:linear "mem"} l: lmap, a: int) returns (v: int);
+ensures {:both} |{ A: v := map(l)[a]; return true; }|;
+
+procedure {:yields} {:layer 0,3} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);
+ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;
+
+procedure {:yields} {:layer 0,1} CAS(tid: X, prev: bool, next: bool) returns (status: bool);
+ensures {:atomic} |{ 
+A: goto B, C; 
+B: assume b == prev; b := next; status := true; lock := tid; return true; 
+C: status := false; return true; 
+}|;
+
+procedure {:yields} {:layer 0,1} CLEAR(tid: X, next: bool);
+ensures {:atomic} |{ 
+A: b := next; lock := nil; return true; 
+}|;
+
diff --git a/Test/civl/civl-paper.bpl.expect b/Test/civl/civl-paper.bpl.expect
index 4bcd03fb..11d204a8 100644
--- a/Test/civl/civl-paper.bpl.expect
+++ b/Test/civl/civl-paper.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 35 verified, 0 errors

+
+Boogie program verifier finished with 35 verified, 0 errors
diff --git a/Test/civl/foo.bpl b/Test/civl/foo.bpl
index 7eeab890..8b7b4aa6 100644
--- a/Test/civl/foo.bpl
+++ b/Test/civl/foo.bpl
@@ -1,57 +1,57 @@
-// RUN: %boogie -noinfer "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var {:layer 0,1} g:int;

-

-procedure {:yields} {:layer 1} PB()

-{

-  yield;

-  call Incr();

-  yield;

-}

-

-procedure {:yields} {:layer 0,1} Incr();

-ensures {:atomic}

-|{A:

-  g := g + 1; return true;

-}|;

-

-procedure {:yields} {:layer 0,1} Set(v: int);

-ensures {:atomic}

-|{A:

-  g := v; return true;

-}|;

-

-procedure {:yields} {:layer 1} PC()

-ensures {:layer 1} g == 3;

-{

-  yield;

-  call Set(3);

-  yield;

-  assert {:layer 1} g == 3;

-}

-

-procedure {:yields} {:layer 1} PE()

-{

-  call PC();

-}

-

-procedure {:yields} {:layer 1} PD()

-{

-  call PC();

-  assert {:layer 1} g == 3;

-}

-

-procedure {:yields} {:layer 1} Main()

-{

-  yield;

-  while (*)

-  {

-    async call PB();

-    yield;

-    async call PE();

-    yield;

-    async call PD();

-    yield;

-  }

-  yield;

-}

+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,1} g:int;
+
+procedure {:yields} {:layer 1} PB()
+{
+  yield;
+  call Incr();
+  yield;
+}
+
+procedure {:yields} {:layer 0,1} Incr();
+ensures {:atomic}
+|{A:
+  g := g + 1; return true;
+}|;
+
+procedure {:yields} {:layer 0,1} Set(v: int);
+ensures {:atomic}
+|{A:
+  g := v; return true;
+}|;
+
+procedure {:yields} {:layer 1} PC()
+ensures {:layer 1} g == 3;
+{
+  yield;
+  call Set(3);
+  yield;
+  assert {:layer 1} g == 3;
+}
+
+procedure {:yields} {:layer 1} PE()
+{
+  call PC();
+}
+
+procedure {:yields} {:layer 1} PD()
+{
+  call PC();
+  assert {:layer 1} g == 3;
+}
+
+procedure {:yields} {:layer 1} Main()
+{
+  yield;
+  while (*)
+  {
+    async call PB();
+    yield;
+    async call PE();
+    yield;
+    async call PD();
+    yield;
+  }
+  yield;
+}
diff --git a/Test/civl/linear-set.bpl b/Test/civl/linear-set.bpl
index e481291a..de7f72f4 100644
--- a/Test/civl/linear-set.bpl
+++ b/Test/civl/linear-set.bpl
@@ -1,105 +1,105 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-type X;

-function {:builtin "MapConst"} MapConstInt(int) : [X]int;

-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

-function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;

-

-function {:inline} None() : [X]bool

-{

-    MapConstBool(false)

-}

-

-function {:inline} All() : [X]bool

-{

-    MapConstBool(true)

-}

-

-function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool

-{

-  xs

-}

-

-var {:layer 0,1} x: int;

-var {:layer 0,1} l: [X]bool;

-

-

-procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool)

-ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();

-{

-  yield;

-  call xls1, xls2 := SplitLow(xls);

-  yield;

-}

-

-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: [X]bool)

-{

-  yield;

-  call xls := AllocateLow();

-  yield;

-}

-

-procedure {:yields} {:layer 0,1} Set(v: int);

-ensures {:atomic} |{A: x := v; return true; }|;

-

-procedure {:yields} {:layer 0,1} Lock(tidls: [X]bool);

-ensures {:atomic} |{A: assume l == None(); l := tidls; return true; }|;

-

-procedure {:yields} {:layer 0,1} Unlock();

-ensures {:atomic} |{A: l := None(); return true; }|;

-

-procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);

-ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|;

-

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

-ensures {:atomic} |{ A: return true; }|;

-

-procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) 

-requires {:layer 1} tidls' != None() && xls' == All();

-{

-    var {:linear "tid"} tidls: [X]bool;

-    var {:linear "x"} xls: [X]bool;

-    var {:linear "tid"} lsChild: [X]bool;

-    var {:linear "x"} xls1: [X]bool;

-    var {:linear "x"} xls2: [X]bool;

-

-    tidls := tidls';

-    xls := xls';

-    yield;

-    call Set(42);

-    yield;

-    assert {:layer 1} xls == All();

-    assert {:layer 1} x == 42;

-    call xls1, xls2 := Split(xls);

-    call lsChild := Allocate();

-    assume (lsChild != None());

-    yield;

-    async call thread(lsChild, xls1);

-    call lsChild := Allocate();

-    assume (lsChild != None());

-    yield;

-    async call thread(lsChild, xls2);

-    yield;

-}

-

-procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool)

-requires {:layer 1} tidls' != None() && xls' != None();

-{

-    var {:linear "x"} xls: [X]bool;

-    var {:linear "tid"} tidls: [X]bool;

-

-    tidls := tidls';

-    xls := xls';

-

-    yield;

-    call Lock(tidls);

-    yield;

-    assert {:layer 1} tidls != None() && xls != None();

-    call Set(0);

-    yield;

-    assert {:layer 1} tidls != None() && xls != None();

-    assert {:layer 1} x == 0;

-    assert {:layer 1} tidls != None() && xls != None();

-    call Unlock();

-    yield;

-}

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+function {:builtin "MapConst"} MapConstInt(int) : [X]int;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
+
+function {:inline} None() : [X]bool
+{
+    MapConstBool(false)
+}
+
+function {:inline} All() : [X]bool
+{
+    MapConstBool(true)
+}
+
+function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
+{
+  xs
+}
+
+var {:layer 0,1} x: int;
+var {:layer 0,1} l: [X]bool;
+
+
+procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool)
+ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
+{
+  yield;
+  call xls1, xls2 := SplitLow(xls);
+  yield;
+}
+
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: [X]bool)
+{
+  yield;
+  call xls := AllocateLow();
+  yield;
+}
+
+procedure {:yields} {:layer 0,1} Set(v: int);
+ensures {:atomic} |{A: x := v; return true; }|;
+
+procedure {:yields} {:layer 0,1} Lock(tidls: [X]bool);
+ensures {:atomic} |{A: assume l == None(); l := tidls; return true; }|;
+
+procedure {:yields} {:layer 0,1} Unlock();
+ensures {:atomic} |{A: l := None(); return true; }|;
+
+procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
+ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|;
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: [X]bool);
+ensures {:atomic} |{ A: return true; }|;
+
+procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) 
+requires {:layer 1} tidls' != None() && xls' == All();
+{
+    var {:linear "tid"} tidls: [X]bool;
+    var {:linear "x"} xls: [X]bool;
+    var {:linear "tid"} lsChild: [X]bool;
+    var {:linear "x"} xls1: [X]bool;
+    var {:linear "x"} xls2: [X]bool;
+
+    tidls := tidls';
+    xls := xls';
+    yield;
+    call Set(42);
+    yield;
+    assert {:layer 1} xls == All();
+    assert {:layer 1} x == 42;
+    call xls1, xls2 := Split(xls);
+    call lsChild := Allocate();
+    assume (lsChild != None());
+    yield;
+    async call thread(lsChild, xls1);
+    call lsChild := Allocate();
+    assume (lsChild != None());
+    yield;
+    async call thread(lsChild, xls2);
+    yield;
+}
+
+procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool)
+requires {:layer 1} tidls' != None() && xls' != None();
+{
+    var {:linear "x"} xls: [X]bool;
+    var {:linear "tid"} tidls: [X]bool;
+
+    tidls := tidls';
+    xls := xls';
+
+    yield;
+    call Lock(tidls);
+    yield;
+    assert {:layer 1} tidls != None() && xls != None();
+    call Set(0);
+    yield;
+    assert {:layer 1} tidls != None() && xls != None();
+    assert {:layer 1} x == 0;
+    assert {:layer 1} tidls != None() && xls != None();
+    call Unlock();
+    yield;
+}
diff --git a/Test/civl/linear-set.bpl.expect b/Test/civl/linear-set.bpl.expect
index fef5ddc0..00ddb38b 100644
--- a/Test/civl/linear-set.bpl.expect
+++ b/Test/civl/linear-set.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 4 verified, 0 errors

+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/linear-set2.bpl b/Test/civl/linear-set2.bpl
index 24d8a13a..4a0c6a1f 100644
--- a/Test/civl/linear-set2.bpl
+++ b/Test/civl/linear-set2.bpl
@@ -1,106 +1,106 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-type X;

-function {:builtin "MapConst"} MapConstInt(int) : [X]int;

-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

-function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;

-

-function {:inline} None() : [X]bool

-{

-    MapConstBool(false)

-}

-

-function {:inline} All() : [X]bool

-{

-    MapConstBool(true)

-}

-

-function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool

-{

-  xs

-}

-

-var {:layer 0,1} x: int;

-var {:layer 0,1} l: X;

-const nil: X;

-

-procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool)

-ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();

-{

-  yield;

-  call xls1, xls2 := SplitLow(xls);

-  yield;

-}

-

-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X)

-ensures {:layer 1} xls != nil;

-{

-  yield;

-  call xls := AllocateLow();

-  yield;

-}

-

-procedure {:yields} {:layer 0,1} Set(v: int);

-ensures {:atomic} |{A: x := v; return true; }|;

-

-procedure {:yields} {:layer 0,1} Lock(tidls: X);

-ensures {:atomic} |{A: assume l == nil; l := tidls; return true; }|;

-

-procedure {:yields} {:layer 0,1} Unlock();

-ensures {:atomic} |{A: l := nil; return true; }|;

-

-procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);

-ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|;

-

-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: X);

-ensures {:atomic} |{ A: assume xls != nil; return true; }|;

-

-procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool) 

-requires {:layer 1} tidls' != nil && xls' == All();

-{

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

-    var {:linear "x"} xls: [X]bool;

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

-    var {:linear "x"} xls1: [X]bool;

-    var {:linear "x"} xls2: [X]bool;

-

-    tidls := tidls';

-    xls := xls';

-

-    yield;

-    call Set(42);

-    yield;

-    assert {:layer 1} xls == All();

-    assert {:layer 1} x == 42;

-    call xls1, xls2 := Split(xls);

-    call lsChild := Allocate();

-    yield;

-    async call thread(lsChild, xls1);

-    call lsChild := Allocate();

-    yield;

-    async call thread(lsChild, xls2);

-    yield;

-}

-

-procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool)

-requires {:layer 1} tidls' != nil && xls' != None();

-{

-    var {:linear "x"} xls: [X]bool;

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

-

-    tidls := tidls';

-    xls := xls';

-

-    yield;

-    call Lock(tidls);

-    yield;

-    assert {:layer 1} tidls != nil && xls != None();

-    call Set(0);

-    yield;

-    assert {:layer 1} tidls != nil && xls != None();

-    assert {:layer 1} x == 0;

-    yield;

-    assert {:layer 1} tidls != nil && xls != None();

-    call Unlock();

-    yield;

-}

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+function {:builtin "MapConst"} MapConstInt(int) : [X]int;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
+
+function {:inline} None() : [X]bool
+{
+    MapConstBool(false)
+}
+
+function {:inline} All() : [X]bool
+{
+    MapConstBool(true)
+}
+
+function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
+{
+  xs
+}
+
+var {:layer 0,1} x: int;
+var {:layer 0,1} l: X;
+const nil: X;
+
+procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool)
+ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
+{
+  yield;
+  call xls1, xls2 := SplitLow(xls);
+  yield;
+}
+
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X)
+ensures {:layer 1} xls != nil;
+{
+  yield;
+  call xls := AllocateLow();
+  yield;
+}
+
+procedure {:yields} {:layer 0,1} Set(v: int);
+ensures {:atomic} |{A: x := v; return true; }|;
+
+procedure {:yields} {:layer 0,1} Lock(tidls: X);
+ensures {:atomic} |{A: assume l == nil; l := tidls; return true; }|;
+
+procedure {:yields} {:layer 0,1} Unlock();
+ensures {:atomic} |{A: l := nil; return true; }|;
+
+procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
+ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|;
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: X);
+ensures {:atomic} |{ A: assume xls != nil; return true; }|;
+
+procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool) 
+requires {:layer 1} tidls' != nil && xls' == All();
+{
+    var {:linear "tid"} tidls: X;
+    var {:linear "x"} xls: [X]bool;
+    var {:linear "tid"} lsChild: X;
+    var {:linear "x"} xls1: [X]bool;
+    var {:linear "x"} xls2: [X]bool;
+
+    tidls := tidls';
+    xls := xls';
+
+    yield;
+    call Set(42);
+    yield;
+    assert {:layer 1} xls == All();
+    assert {:layer 1} x == 42;
+    call xls1, xls2 := Split(xls);
+    call lsChild := Allocate();
+    yield;
+    async call thread(lsChild, xls1);
+    call lsChild := Allocate();
+    yield;
+    async call thread(lsChild, xls2);
+    yield;
+}
+
+procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool)
+requires {:layer 1} tidls' != nil && xls' != None();
+{
+    var {:linear "x"} xls: [X]bool;
+    var {:linear "tid"} tidls: X;
+
+    tidls := tidls';
+    xls := xls';
+
+    yield;
+    call Lock(tidls);
+    yield;
+    assert {:layer 1} tidls != nil && xls != None();
+    call Set(0);
+    yield;
+    assert {:layer 1} tidls != nil && xls != None();
+    assert {:layer 1} x == 0;
+    yield;
+    assert {:layer 1} tidls != nil && xls != None();
+    call Unlock();
+    yield;
+}
diff --git a/Test/civl/linear-set2.bpl.expect b/Test/civl/linear-set2.bpl.expect
index fef5ddc0..00ddb38b 100644
--- a/Test/civl/linear-set2.bpl.expect
+++ b/Test/civl/linear-set2.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 4 verified, 0 errors

+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/lock-introduced.bpl b/Test/civl/lock-introduced.bpl
index c9650215..fa0a3977 100644
--- a/Test/civl/lock-introduced.bpl
+++ b/Test/civl/lock-introduced.bpl
@@ -1,100 +1,100 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

-function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

-{

-  MapConstBool(false)[x := true]

-}

-

-type X;

-const nil: X;

-var {:layer 0,2} b: bool;

-var {:layer 1,3} lock: X;

-

-procedure {:yields} {:layer 3} Customer({:linear "tid"} tid: X)

-requires {:layer 2} tid != nil; 

-requires {:layer 2} InvLock(lock, b);

-ensures {:layer 2} InvLock(lock, b);

-{

-    yield;

-    assert {:layer 2} InvLock(lock, b);

-    while (*) 

-    invariant {:layer 2} InvLock(lock, b);

-    {

-        call Enter(tid);

-    	call Leave(tid);

-        yield;

-	assert {:layer 2} InvLock(lock, b);

-    }    

-    yield;

-    assert {:layer 2} InvLock(lock, b);

-}

-

-function {:inline} InvLock(lock: X, b: bool) : bool

-{

-    lock != nil <==> b

-}

-

-procedure {:yields} {:layer 2,3} Enter({:linear "tid"} tid: X)

-requires {:layer 2} tid != nil; 

-requires {:layer 2} InvLock(lock, b);

-ensures {:layer 2} InvLock(lock, b);

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

-{

-    yield;

-    assert {:layer 2} InvLock(lock, b);

-    call LowerEnter(tid);

-    yield;

-    assert {:layer 2} InvLock(lock, b);

-}

-

-procedure {:yields} {:layer 2,3} Leave({:linear "tid"} tid:X)

-requires {:layer 2} InvLock(lock, b);

-ensures {:layer 2} InvLock(lock, b);

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

-{

-    yield;

-    assert {:layer 2} InvLock(lock, b);

-    call LowerLeave();

-    yield;

-    assert {:layer 2} InvLock(lock, b);

-}

-

-procedure {:yields} {:layer 1,2} LowerEnter({:linear "tid"} tid: X) 

-ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|;

-{

-    var status: bool;

-    yield;

-    L: 

-        call status := CAS(false, true);

-	yield;

-        goto A, B;

-

-    A: 

-        assume status;

-	yield;

-	return;

-

-    B:

-        assume !status;

-	goto L;

-}

-

-procedure {:yields} {:layer 1,2} LowerLeave()

-ensures {:atomic} |{ A: b := false; lock := nil; return true; }|;

-{

-    yield;

-    call SET(false);

-    yield;

-}

-

-procedure {:yields} {:layer 0,1} CAS(prev: bool, next: bool) returns (status: bool);

-ensures {:atomic} |{ 

-A: goto B, C; 

-B: assume b == prev; b := next; status := true; return true; 

-C: status := false; return true; 

-}|;

-

-procedure {:yields} {:layer 0,1} SET(next: bool);

-ensures {:atomic} |{ A: b := next; return true; }|;

-

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+  MapConstBool(false)[x := true]
+}
+
+type X;
+const nil: X;
+var {:layer 0,2} b: bool;
+var {:layer 1,3} lock: X;
+
+procedure {:yields} {:layer 3} Customer({:linear "tid"} tid: X)
+requires {:layer 2} tid != nil; 
+requires {:layer 2} InvLock(lock, b);
+ensures {:layer 2} InvLock(lock, b);
+{
+    yield;
+    assert {:layer 2} InvLock(lock, b);
+    while (*) 
+    invariant {:layer 2} InvLock(lock, b);
+    {
+        call Enter(tid);
+    	call Leave(tid);
+        yield;
+	assert {:layer 2} InvLock(lock, b);
+    }    
+    yield;
+    assert {:layer 2} InvLock(lock, b);
+}
+
+function {:inline} InvLock(lock: X, b: bool) : bool
+{
+    lock != nil <==> b
+}
+
+procedure {:yields} {:layer 2,3} Enter({:linear "tid"} tid: X)
+requires {:layer 2} tid != nil; 
+requires {:layer 2} InvLock(lock, b);
+ensures {:layer 2} InvLock(lock, b);
+ensures {:right} |{ A: assume lock == nil && tid != nil; lock := tid; return true; }|;
+{
+    yield;
+    assert {:layer 2} InvLock(lock, b);
+    call LowerEnter(tid);
+    yield;
+    assert {:layer 2} InvLock(lock, b);
+}
+
+procedure {:yields} {:layer 2,3} Leave({:linear "tid"} tid:X)
+requires {:layer 2} InvLock(lock, b);
+ensures {:layer 2} InvLock(lock, b);
+ensures {:atomic} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;
+{
+    yield;
+    assert {:layer 2} InvLock(lock, b);
+    call LowerLeave();
+    yield;
+    assert {:layer 2} InvLock(lock, b);
+}
+
+procedure {:yields} {:layer 1,2} LowerEnter({:linear "tid"} tid: X) 
+ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|;
+{
+    var status: bool;
+    yield;
+    L: 
+        call status := CAS(false, true);
+	yield;
+        goto A, B;
+
+    A: 
+        assume status;
+	yield;
+	return;
+
+    B:
+        assume !status;
+	goto L;
+}
+
+procedure {:yields} {:layer 1,2} LowerLeave()
+ensures {:atomic} |{ A: b := false; lock := nil; return true; }|;
+{
+    yield;
+    call SET(false);
+    yield;
+}
+
+procedure {:yields} {:layer 0,1} CAS(prev: bool, next: bool) returns (status: bool);
+ensures {:atomic} |{ 
+A: goto B, C; 
+B: assume b == prev; b := next; status := true; return true; 
+C: status := false; return true; 
+}|;
+
+procedure {:yields} {:layer 0,1} SET(next: bool);
+ensures {:atomic} |{ A: b := next; return true; }|;
+
diff --git a/Test/civl/lock-introduced.bpl.expect b/Test/civl/lock-introduced.bpl.expect
index f62a8f46..f08c6e00 100644
--- a/Test/civl/lock-introduced.bpl.expect
+++ b/Test/civl/lock-introduced.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 12 verified, 0 errors

+
+Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Test/civl/lock.bpl b/Test/civl/lock.bpl
index 9341591f..ee736029 100644
--- a/Test/civl/lock.bpl
+++ b/Test/civl/lock.bpl
@@ -1,57 +1,57 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var {:layer 0,2} b: bool;

-

-procedure {:yields} {:layer 2} main()

-{

-    yield;

-    while (*)

-    {

-        async call Customer();

-        yield;

-    }

-    yield;

-}

-

-procedure {:yields} {:layer 2} Customer()

-{

-    yield;

-    while (*) 

-    {

-        call Enter();

-    	yield;

-    	call Leave();

-        yield;

-    }

-    yield;

-}

-

-procedure {:yields} {:layer 1,2} Enter() 

-ensures {:atomic} |{ A: assume !b; b := true; return true; }|;

-{

-    var status: bool;

-    yield;

-    L: 

-        call status := CAS(false, true);

-	yield;

-        goto A, B;

-

-    A: 

-        assume status;

-	yield;

-	return;

-

-    B:

-        assume !status;

-	goto L;

-}

-

-procedure {:yields} {:layer 0,2} CAS(prev: bool, next: bool) returns (status: bool);

-ensures {:atomic} |{ 

-A: goto B, C; 

-B: assume b == prev; b := next; status := true; return true; 

-C: status := false; return true; 

-}|;

-

-procedure {:yields} {:layer 0,2} Leave();

-ensures {:atomic} |{ A: b := false; return true; }|;

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,2} b: bool;
+
+procedure {:yields} {:layer 2} main()
+{
+    yield;
+    while (*)
+    {
+        async call Customer();
+        yield;
+    }
+    yield;
+}
+
+procedure {:yields} {:layer 2} Customer()
+{
+    yield;
+    while (*) 
+    {
+        call Enter();
+    	yield;
+    	call Leave();
+        yield;
+    }
+    yield;
+}
+
+procedure {:yields} {:layer 1,2} Enter() 
+ensures {:atomic} |{ A: assume !b; b := true; return true; }|;
+{
+    var status: bool;
+    yield;
+    L: 
+        call status := CAS(false, true);
+	yield;
+        goto A, B;
+
+    A: 
+        assume status;
+	yield;
+	return;
+
+    B:
+        assume !status;
+	goto L;
+}
+
+procedure {:yields} {:layer 0,2} CAS(prev: bool, next: bool) returns (status: bool);
+ensures {:atomic} |{ 
+A: goto B, C; 
+B: assume b == prev; b := next; status := true; return true; 
+C: status := false; return true; 
+}|;
+
+procedure {:yields} {:layer 0,2} Leave();
+ensures {:atomic} |{ A: b := false; return true; }|;
diff --git a/Test/civl/lock.bpl.expect b/Test/civl/lock.bpl.expect
index 05d394c7..3e6d423a 100644
--- a/Test/civl/lock.bpl.expect
+++ b/Test/civl/lock.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 5 verified, 0 errors

+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/civl/lock2.bpl b/Test/civl/lock2.bpl
index 4809a8f5..e84d0a6f 100644
--- a/Test/civl/lock2.bpl
+++ b/Test/civl/lock2.bpl
@@ -1,63 +1,63 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var {:layer 0,2} b: int;

-

-procedure {:yields} {:layer 2} main()

-{

-    yield;

-    while (*)

-    {

-        async call Customer();

-        yield;

-    }

-    yield;

-}

-

-procedure {:yields} {:layer 2} Customer()

-{

-    yield;

-    while (*) 

-    {

-        call Enter();

-    	yield;

-    	call Leave();

-        yield;

-    }

-    yield;

-}

-

-procedure {:yields} {:layer 1,2} Enter() 

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

-{

-    var _old, curr: int;

-    yield;

-    while (true) { 

-        call _old := CAS(0, 1);

-	yield;

-        if (_old == 0) {

-	    break;

-	}

-	while (true) {

-	    call curr := Read();

-	    yield;

-	    if (curr == 0) {

-	        break;

-	    }

-	}

-	yield;

-    }

-    yield;

-}

-

-procedure {:yields} {:layer 0,2} Read() returns (val: int);

-ensures {:atomic} |{ A: val := b; return true; }|;

-

-procedure {:yields} {:layer 0,2} CAS(prev: int, next: int) returns (_old: int);

-ensures {:atomic} |{ 

-A: _old := b; goto B, C; 

-B: assume _old == prev; b := next; return true; 

-C: assume _old != prev; return true; 

-}|;

-

-procedure {:yields} {:layer 0,2} Leave();

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,2} b: int;
+
+procedure {:yields} {:layer 2} main()
+{
+    yield;
+    while (*)
+    {
+        async call Customer();
+        yield;
+    }
+    yield;
+}
+
+procedure {:yields} {:layer 2} Customer()
+{
+    yield;
+    while (*) 
+    {
+        call Enter();
+    	yield;
+    	call Leave();
+        yield;
+    }
+    yield;
+}
+
+procedure {:yields} {:layer 1,2} Enter() 
+ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|;
+{
+    var _old, curr: int;
+    yield;
+    while (true) { 
+        call _old := CAS(0, 1);
+	yield;
+        if (_old == 0) {
+	    break;
+	}
+	while (true) {
+	    call curr := Read();
+	    yield;
+	    if (curr == 0) {
+	        break;
+	    }
+	}
+	yield;
+    }
+    yield;
+}
+
+procedure {:yields} {:layer 0,2} Read() returns (val: int);
+ensures {:atomic} |{ A: val := b; return true; }|;
+
+procedure {:yields} {:layer 0,2} CAS(prev: int, next: int) returns (_old: int);
+ensures {:atomic} |{ 
+A: _old := b; goto B, C; 
+B: assume _old == prev; b := next; return true; 
+C: assume _old != prev; return true; 
+}|;
+
+procedure {:yields} {:layer 0,2} Leave();
+ensures {:atomic} |{ A: b := 0; return true; }|;
diff --git a/Test/civl/lock2.bpl.expect b/Test/civl/lock2.bpl.expect
index 05d394c7..3e6d423a 100644
--- a/Test/civl/lock2.bpl.expect
+++ b/Test/civl/lock2.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 5 verified, 0 errors

+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/civl/multiset.bpl b/Test/civl/multiset.bpl
index 7fb0a081..ec391380 100644
--- a/Test/civl/multiset.bpl
+++ b/Test/civl/multiset.bpl
@@ -1,324 +1,324 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-type X;

-

-const unique null : int;

-const unique nil: X;

-const unique done: X;

-

-var {:layer 0} elt : [int]int;

-var {:layer 0} valid : [int]bool;

-var {:layer 0} lock : [int]X;

-var {:layer 0} owner : [int]X;

-const max : int;

-

-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

-function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

-{

-  MapConstBool(false)[x := true]

-}

-

-axiom (max > 0);

-

-procedure {:yields} {:layer 0} acquire(i : int, {:linear "tid"} tid: X);

-ensures {:right} |{ A: 

-                      assert 0 <= i && i < max;

-                      assert tid != nil && tid != done;

-                      assume lock[i] == nil;

-	              lock[i] := tid;

-                      return true;

-                    }|;

-

-

-procedure {:yields} {:layer 0} release(i : int, {:linear "tid"} tid: X);

-ensures {:left} |{ A: 

-                     assert 0 <= i && i < max;

-                     assert lock[i] == tid;

-                     assert tid != nil && tid != done; 

-	             lock[i] := nil;

-                     return true;

-                    }|;

-

-

-procedure {:yields} {:layer 0,1} getElt(j : int, {:linear "tid"} tid: X) returns (elt_j:int);

-ensures {:both} |{ A: 

-                     assert 0 <= j && j < max;

-                     assert lock[j] == tid;

-                     assert tid != nil && tid != done;

-	             elt_j := elt[j];

-                     return true;

-                    }|;

-

-

-procedure {:yields} {:layer 0,1} setElt(j : int, x : int, {:linear "tid"} tid: X);

-ensures {:both} |{ A: 

-                     assert x != null;

-                     assert owner[j] == nil;

-                     assert 0 <= j && j < max;

-                     assert lock[j] == tid;

-                     assert tid != nil && tid != done;

-	             elt[j] := x;

-                     owner[j] := tid;

-                     return true;

-                    }|;

-

-

-procedure {:yields} {:layer 0,2} setEltToNull(j : int, {:linear "tid"} tid: X);

-ensures {:left} |{ A: 

-                     assert owner[j] == tid;

-                     assert 0 <= j && j < max;

-                     assert lock[j] == tid;

-                     assert !valid[j];

-                     assert tid != nil  && tid != done;

-	             elt[j] := null;

-                     owner[j] := nil;

-                     return true;

-                    }|;

-

-procedure {:yields} {:layer 0,2} setValid(j : int, {:linear "tid"} tid: X);

-ensures {:both} |{ A: 

-                     assert 0 <= j && j < max;

-                     assert lock[j] == tid;

-                     assert tid != nil && tid != done;

-                     assert owner[j] == tid;

-	             valid[j] := true;

-                     owner[j] := done;

-                     return true;

-                    }|;

-

-procedure {:yields} {:layer 0,2} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool);

-ensures {:both} |{ A: 

-                       assert 0 <= j && j < max;

-                       assert lock[j] == tid;

-                       assert tid != nil && tid != done;

-                       fnd := (elt[j] == x) && valid[j];

-                       return true;

-                    }|;

-

-procedure {:yields} {:layer 1,2} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int)

-requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

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

-ensures {:right}  |{   A: assert tid != nil && tid != done; 

-                          assert x != null; 

-			  goto B, C;

-                       B: assume (0 <= r && r < max); 

-                                            assume elt[r] == null; 

-                                            assume owner[r] == nil;

-					    assume !valid[r];

-                                            elt[r] := x; 

-                                            owner[r] := tid;

-                                            return true;

-                       C: assume (r == -1); return true; 

-                   }|;

-{

-	var j : int;

-	var elt_j : int;

-        

-        par Yield1();

-

-	j := 0;

-	while(j < max)

-        invariant {:layer 1} Inv(valid, elt, owner);

-	invariant {:layer 1} 0 <= j;

-	{

-                call acquire(j, tid);

-                call elt_j := getElt(j, tid);

-		if(elt_j == null)

-		{

-                        call setElt(j, x, tid);

-			call release(j, tid);

-			r := j;

-

-                        par Yield1();

-			return;		

-		}

-		call release(j,tid);

-

-                par Yield1();

-

-		j := j + 1;	

-	}

-	r := -1;

-

-        par Yield1();

-	return;

-}

-

-procedure {:yields} {:layer 2} Insert(x : int, {:linear "tid"} tid: X) returns (result : bool) 

-requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

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

-requires {:layer 2} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

-ensures {:layer 2} Inv(valid, elt, owner);

-ensures {:atomic}  |{ var r:int;

-                        A: goto B, C;

-                        B: assume (0 <= r && r < max); 

-                           assume valid[r] == false; 

-                           assume elt[r] == null; 

-                           assume owner[r] == nil; 

-                           elt[r] := x; valid[r] := true; owner[r] := done;

-                           result := true; return true;

-                        C: result := false; return true; 

-                      }|;

- {

-        var i: int;

-        par Yield12();

-        call i := FindSlot(x, tid);

-        

-	if(i == -1)

-	{

-		result := false;

-                par Yield12();

-		return;

-	}

-        par Yield1();

-        assert {:layer 1} i != -1;

-        assert {:layer 2} i != -1;

-	call acquire(i, tid);

-        assert {:layer 2} elt[i] == x;

-	assert {:layer 2}  valid[i] == false;

-        call setValid(i, tid);   

-	call release(i, tid);

-	result := true; 

-        par Yield12();

-	return;

-}

-

-procedure {:yields} {:layer 2} InsertPair(x : int, y : int, {:linear "tid"} tid: X) returns (result : bool)

-requires {:layer 1} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 

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

-requires {:layer 2} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 

-ensures {:layer 2} Inv(valid, elt, owner);

-ensures {:atomic}  |{ var rx:int;

-                        var ry:int;

-                        A: goto B, C;

-                        B: assume (0 <= rx && rx < max && 0 <= ry && ry < max && rx != ry); 

-                           assume valid[rx] == false; 

-                           assume valid[ry] == false; 

-                           assume elt[rx] == null; 

-                           assume elt[rx] == null; 

-                           elt[rx] := x; 

-                           elt[ry] := y; 

-                           valid[rx] := true; 

-                           valid[ry] := true;

-                           owner[rx] := done;

-                           owner[ry] := done; 

-                           result := true; return true;

-                        C: result := false; return true; 

-                      }|;

- {

-        var i : int; 

-        var j : int;

-        par Yield12();

-

-        call i := FindSlot(x, tid);

-        

-	if (i == -1)

-	{

-	 	result := false;

-                par Yield12();

-		return;

-	}

-

-        par Yield1();

-        call j := FindSlot(y, tid);

-        

-	if(j == -1)

-	{

-                par Yield1();

-                call acquire(i,tid);  

-                call setEltToNull(i, tid);

-                call release(i,tid);  

-		result := false;

-                par Yield12();

-		return;

-	}

-

-        par Yield1();

-        assert {:layer 2} i != -1 && j != -1;

-	call acquire(i, tid);

-	call acquire(j, tid);

-        assert {:layer 2} elt[i] == x;

-        assert {:layer 2} elt[j] == y;

-	assert {:layer 2}  valid[i] == false;

-	assert {:layer 2}  valid[j] == false;

-        call setValid(i, tid);   

-        call setValid(j, tid);   

-	call release(j, tid);

-	call release(i, tid);

-	result := true; 

-        par Yield12();

-	return;

-}

-

-procedure {:yields} {:layer 2} LookUp(x : int, {:linear "tid"} tid: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool)

-requires {:layer 1} {:layer 2} old_valid == valid && old_elt == elt;

-requires {:layer 1} {:layer 2} Inv(valid, elt, owner);

-requires {:layer 1} {:layer 2} (tid != nil && tid != done);

-ensures {:layer 1} {:layer 2} Inv(valid, elt, owner);

-ensures {:atomic}  |{ A: assert tid != nil && tid != done; 

-                          assert x != null;

-                          assume found ==> (exists ii:int :: 0 <= ii && ii < max && valid[ii] && elt[ii] == x);

-			  assume !found ==> (forall ii:int :: 0 <= ii && ii < max ==> !(old_valid[ii] && old_elt[ii] == x));

-                          return true;

-                    }|;

-{

-	var j : int;

-	var isThere : bool;

-        

-        par Yield12() | YieldLookUp(old_valid, old_elt);

-

-	j := 0;

-

-	while(j < max)

-        invariant {:layer 1} {:layer 2} Inv(valid, elt, owner);

-        invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < j ==> !(old_valid[ii] && old_elt[ii] == x));

-	invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

-	invariant {:layer 1} {:layer 2} 0 <= j;

-	{

-                call acquire(j, tid);

-                call isThere := isEltThereAndValid(j, x, tid);

-		if(isThere)

-		{

-			 call release(j, tid);

-                         found := true; 

-                         par Yield12() | YieldLookUp(old_valid, old_elt);

-		 	 return;		

-		}

-		call release(j,tid);

-                par Yield12() | YieldLookUp(old_valid, old_elt);

-		j := j + 1;	

-	}

-	found := false;

-

-        par Yield12() | YieldLookUp(old_valid, old_elt);

-	return;

-}

-

-procedure {:yields} {:layer 1} Yield1()

-requires {:layer 1} Inv(valid, elt, owner);

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

-{

-	yield;

-	assert {:layer 1} Inv(valid, elt, owner);

-}

-

-procedure {:yields} {:layer 2} Yield12()

-requires {:layer 1} {:layer 2} Inv(valid, elt, owner);

-ensures {:layer 1} {:layer 2} Inv(valid, elt, owner);

-{

-        yield;

-        assert {:layer 1} {:layer 2} Inv(valid, elt, owner);

-}

-

-function {:inline} Inv(valid: [int]bool, elt: [int]int, owner: [int]X): (bool)

-{

-   (forall i:int :: 0 <= i && i < max ==> (elt[i] == null <==> (!valid[i] && owner[i] == nil)))

-}

-

-procedure {:yields} {:layer 2} YieldLookUp(old_valid: [int]bool, old_elt: [int]int)

-requires {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

-ensures {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

-{

-    yield;

-    assert {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

-}

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+
+const unique null : int;
+const unique nil: X;
+const unique done: X;
+
+var {:layer 0} elt : [int]int;
+var {:layer 0} valid : [int]bool;
+var {:layer 0} lock : [int]X;
+var {:layer 0} owner : [int]X;
+const max : int;
+
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+  MapConstBool(false)[x := true]
+}
+
+axiom (max > 0);
+
+procedure {:yields} {:layer 0} acquire(i : int, {:linear "tid"} tid: X);
+ensures {:right} |{ A: 
+                      assert 0 <= i && i < max;
+                      assert tid != nil && tid != done;
+                      assume lock[i] == nil;
+	              lock[i] := tid;
+                      return true;
+                    }|;
+
+
+procedure {:yields} {:layer 0} release(i : int, {:linear "tid"} tid: X);
+ensures {:left} |{ A: 
+                     assert 0 <= i && i < max;
+                     assert lock[i] == tid;
+                     assert tid != nil && tid != done; 
+	             lock[i] := nil;
+                     return true;
+                    }|;
+
+
+procedure {:yields} {:layer 0,1} getElt(j : int, {:linear "tid"} tid: X) returns (elt_j:int);
+ensures {:both} |{ A: 
+                     assert 0 <= j && j < max;
+                     assert lock[j] == tid;
+                     assert tid != nil && tid != done;
+	             elt_j := elt[j];
+                     return true;
+                    }|;
+
+
+procedure {:yields} {:layer 0,1} setElt(j : int, x : int, {:linear "tid"} tid: X);
+ensures {:both} |{ A: 
+                     assert x != null;
+                     assert owner[j] == nil;
+                     assert 0 <= j && j < max;
+                     assert lock[j] == tid;
+                     assert tid != nil && tid != done;
+	             elt[j] := x;
+                     owner[j] := tid;
+                     return true;
+                    }|;
+
+
+procedure {:yields} {:layer 0,2} setEltToNull(j : int, {:linear "tid"} tid: X);
+ensures {:left} |{ A: 
+                     assert owner[j] == tid;
+                     assert 0 <= j && j < max;
+                     assert lock[j] == tid;
+                     assert !valid[j];
+                     assert tid != nil  && tid != done;
+	             elt[j] := null;
+                     owner[j] := nil;
+                     return true;
+                    }|;
+
+procedure {:yields} {:layer 0,2} setValid(j : int, {:linear "tid"} tid: X);
+ensures {:both} |{ A: 
+                     assert 0 <= j && j < max;
+                     assert lock[j] == tid;
+                     assert tid != nil && tid != done;
+                     assert owner[j] == tid;
+	             valid[j] := true;
+                     owner[j] := done;
+                     return true;
+                    }|;
+
+procedure {:yields} {:layer 0,2} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool);
+ensures {:both} |{ A: 
+                       assert 0 <= j && j < max;
+                       assert lock[j] == tid;
+                       assert tid != nil && tid != done;
+                       fnd := (elt[j] == x) && valid[j];
+                       return true;
+                    }|;
+
+procedure {:yields} {:layer 1,2} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int)
+requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 
+ensures {:layer 1} Inv(valid, elt, owner);
+ensures {:right}  |{   A: assert tid != nil && tid != done; 
+                          assert x != null; 
+			  goto B, C;
+                       B: assume (0 <= r && r < max); 
+                                            assume elt[r] == null; 
+                                            assume owner[r] == nil;
+					    assume !valid[r];
+                                            elt[r] := x; 
+                                            owner[r] := tid;
+                                            return true;
+                       C: assume (r == -1); return true; 
+                   }|;
+{
+	var j : int;
+	var elt_j : int;
+        
+        par Yield1();
+
+	j := 0;
+	while(j < max)
+        invariant {:layer 1} Inv(valid, elt, owner);
+	invariant {:layer 1} 0 <= j;
+	{
+                call acquire(j, tid);
+                call elt_j := getElt(j, tid);
+		if(elt_j == null)
+		{
+                        call setElt(j, x, tid);
+			call release(j, tid);
+			r := j;
+
+                        par Yield1();
+			return;		
+		}
+		call release(j,tid);
+
+                par Yield1();
+
+		j := j + 1;	
+	}
+	r := -1;
+
+        par Yield1();
+	return;
+}
+
+procedure {:yields} {:layer 2} Insert(x : int, {:linear "tid"} tid: X) returns (result : bool) 
+requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 
+ensures {:layer 1} Inv(valid, elt, owner);
+requires {:layer 2} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 
+ensures {:layer 2} Inv(valid, elt, owner);
+ensures {:atomic}  |{ var r:int;
+                        A: goto B, C;
+                        B: assume (0 <= r && r < max); 
+                           assume valid[r] == false; 
+                           assume elt[r] == null; 
+                           assume owner[r] == nil; 
+                           elt[r] := x; valid[r] := true; owner[r] := done;
+                           result := true; return true;
+                        C: result := false; return true; 
+                      }|;
+ {
+        var i: int;
+        par Yield12();
+        call i := FindSlot(x, tid);
+        
+	if(i == -1)
+	{
+		result := false;
+                par Yield12();
+		return;
+	}
+        par Yield1();
+        assert {:layer 1} i != -1;
+        assert {:layer 2} i != -1;
+	call acquire(i, tid);
+        assert {:layer 2} elt[i] == x;
+	assert {:layer 2}  valid[i] == false;
+        call setValid(i, tid);   
+	call release(i, tid);
+	result := true; 
+        par Yield12();
+	return;
+}
+
+procedure {:yields} {:layer 2} InsertPair(x : int, y : int, {:linear "tid"} tid: X) returns (result : bool)
+requires {:layer 1} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 
+ensures {:layer 1} Inv(valid, elt, owner);
+requires {:layer 2} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 
+ensures {:layer 2} Inv(valid, elt, owner);
+ensures {:atomic}  |{ var rx:int;
+                        var ry:int;
+                        A: goto B, C;
+                        B: assume (0 <= rx && rx < max && 0 <= ry && ry < max && rx != ry); 
+                           assume valid[rx] == false; 
+                           assume valid[ry] == false; 
+                           assume elt[rx] == null; 
+                           assume elt[rx] == null; 
+                           elt[rx] := x; 
+                           elt[ry] := y; 
+                           valid[rx] := true; 
+                           valid[ry] := true;
+                           owner[rx] := done;
+                           owner[ry] := done; 
+                           result := true; return true;
+                        C: result := false; return true; 
+                      }|;
+ {
+        var i : int; 
+        var j : int;
+        par Yield12();
+
+        call i := FindSlot(x, tid);
+        
+	if (i == -1)
+	{
+	 	result := false;
+                par Yield12();
+		return;
+	}
+
+        par Yield1();
+        call j := FindSlot(y, tid);
+        
+	if(j == -1)
+	{
+                par Yield1();
+                call acquire(i,tid);  
+                call setEltToNull(i, tid);
+                call release(i,tid);  
+		result := false;
+                par Yield12();
+		return;
+	}
+
+        par Yield1();
+        assert {:layer 2} i != -1 && j != -1;
+	call acquire(i, tid);
+	call acquire(j, tid);
+        assert {:layer 2} elt[i] == x;
+        assert {:layer 2} elt[j] == y;
+	assert {:layer 2}  valid[i] == false;
+	assert {:layer 2}  valid[j] == false;
+        call setValid(i, tid);   
+        call setValid(j, tid);   
+	call release(j, tid);
+	call release(i, tid);
+	result := true; 
+        par Yield12();
+	return;
+}
+
+procedure {:yields} {:layer 2} LookUp(x : int, {:linear "tid"} tid: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool)
+requires {:layer 1} {:layer 2} old_valid == valid && old_elt == elt;
+requires {:layer 1} {:layer 2} Inv(valid, elt, owner);
+requires {:layer 1} {:layer 2} (tid != nil && tid != done);
+ensures {:layer 1} {:layer 2} Inv(valid, elt, owner);
+ensures {:atomic}  |{ A: assert tid != nil && tid != done; 
+                          assert x != null;
+                          assume found ==> (exists ii:int :: 0 <= ii && ii < max && valid[ii] && elt[ii] == x);
+			  assume !found ==> (forall ii:int :: 0 <= ii && ii < max ==> !(old_valid[ii] && old_elt[ii] == x));
+                          return true;
+                    }|;
+{
+	var j : int;
+	var isThere : bool;
+        
+        par Yield12() | YieldLookUp(old_valid, old_elt);
+
+	j := 0;
+
+	while(j < max)
+        invariant {:layer 1} {:layer 2} Inv(valid, elt, owner);
+        invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < j ==> !(old_valid[ii] && old_elt[ii] == x));
+	invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);
+	invariant {:layer 1} {:layer 2} 0 <= j;
+	{
+                call acquire(j, tid);
+                call isThere := isEltThereAndValid(j, x, tid);
+		if(isThere)
+		{
+			 call release(j, tid);
+                         found := true; 
+                         par Yield12() | YieldLookUp(old_valid, old_elt);
+		 	 return;		
+		}
+		call release(j,tid);
+                par Yield12() | YieldLookUp(old_valid, old_elt);
+		j := j + 1;	
+	}
+	found := false;
+
+        par Yield12() | YieldLookUp(old_valid, old_elt);
+	return;
+}
+
+procedure {:yields} {:layer 1} Yield1()
+requires {:layer 1} Inv(valid, elt, owner);
+ensures {:layer 1} Inv(valid, elt, owner);
+{
+	yield;
+	assert {:layer 1} Inv(valid, elt, owner);
+}
+
+procedure {:yields} {:layer 2} Yield12()
+requires {:layer 1} {:layer 2} Inv(valid, elt, owner);
+ensures {:layer 1} {:layer 2} Inv(valid, elt, owner);
+{
+        yield;
+        assert {:layer 1} {:layer 2} Inv(valid, elt, owner);
+}
+
+function {:inline} Inv(valid: [int]bool, elt: [int]int, owner: [int]X): (bool)
+{
+   (forall i:int :: 0 <= i && i < max ==> (elt[i] == null <==> (!valid[i] && owner[i] == nil)))
+}
+
+procedure {:yields} {:layer 2} YieldLookUp(old_valid: [int]bool, old_elt: [int]int)
+requires {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);
+ensures {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);
+{
+    yield;
+    assert {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);
+}
diff --git a/Test/civl/multiset.bpl.expect b/Test/civl/multiset.bpl.expect
index d72077a6..0a77c517 100644
--- a/Test/civl/multiset.bpl.expect
+++ b/Test/civl/multiset.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 78 verified, 0 errors

+
+Boogie program verifier finished with 78 verified, 0 errors
diff --git a/Test/civl/new1.bpl b/Test/civl/new1.bpl
index b80b6315..c2feb179 100644
--- a/Test/civl/new1.bpl
+++ b/Test/civl/new1.bpl
@@ -1,42 +1,42 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;

-

-var {:layer 0,1} g:int;

-

-function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool

-{

-  x

-}

-

-procedure {:yields} {:layer 1} PB({:linear_in "Perm"} permVar_in:[int]bool)

-requires {:layer 1} permVar_in[0] && g == 0;

-{

-  var {:linear "Perm"} permVar_out: [int]bool;

-  permVar_out := permVar_in;

-

-  yield;

-  assert {:layer 1} permVar_out[0];

-  assert {:layer 1} g == 0;

-

-  call IncrG();

-

-  yield;

-  assert {:layer 1} permVar_out[0];

-  assert {:layer 1} g == 1;

-}

-

-procedure {:yields} {:layer 1} Main({:linear_in "Perm"} Permissions: [int]bool)

-requires {:layer 1} Permissions == mapconstbool(true);

-{

-  yield;

-  call SetG(0);

-  async call PB(Permissions);

-  yield;

-}

-

-procedure {:yields} {:layer 0,1} SetG(val:int);

-ensures {:atomic} |{A: g := val; return true; }|;

-

-procedure {:yields} {:layer 0,1} IncrG();

-ensures {:atomic} |{A: g := g + 1; return true; }|;

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;
+
+var {:layer 0,1} g:int;
+
+function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
+{
+  x
+}
+
+procedure {:yields} {:layer 1} PB({:linear_in "Perm"} permVar_in:[int]bool)
+requires {:layer 1} permVar_in[0] && g == 0;
+{
+  var {:linear "Perm"} permVar_out: [int]bool;
+  permVar_out := permVar_in;
+
+  yield;
+  assert {:layer 1} permVar_out[0];
+  assert {:layer 1} g == 0;
+
+  call IncrG();
+
+  yield;
+  assert {:layer 1} permVar_out[0];
+  assert {:layer 1} g == 1;
+}
+
+procedure {:yields} {:layer 1} Main({:linear_in "Perm"} Permissions: [int]bool)
+requires {:layer 1} Permissions == mapconstbool(true);
+{
+  yield;
+  call SetG(0);
+  async call PB(Permissions);
+  yield;
+}
+
+procedure {:yields} {:layer 0,1} SetG(val:int);
+ensures {:atomic} |{A: g := val; return true; }|;
+
+procedure {:yields} {:layer 0,1} IncrG();
+ensures {:atomic} |{A: g := g + 1; return true; }|;
diff --git a/Test/civl/new1.bpl.expect b/Test/civl/new1.bpl.expect
index 3de74d3e..41374b00 100644
--- a/Test/civl/new1.bpl.expect
+++ b/Test/civl/new1.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 2 verified, 0 errors

+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/civl/one.bpl b/Test/civl/one.bpl
index 663b2da0..3b370fa7 100644
--- a/Test/civl/one.bpl
+++ b/Test/civl/one.bpl
@@ -1,18 +1,18 @@
-// RUN: %boogie -noinfer "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var {:layer 0,1} x:int;

-

-procedure {:yields} {:layer 0,1} Set(v: int);

-ensures {:atomic}

-|{A:

-  x := v; return true;

-}|;

-

-procedure {:yields} {:layer 1} B()

-{

-  yield;

-  call Set(5);

-  yield;

-  assert {:layer 1} x == 5;

-}

-

+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,1} x:int;
+
+procedure {:yields} {:layer 0,1} Set(v: int);
+ensures {:atomic}
+|{A:
+  x := v; return true;
+}|;
+
+procedure {:yields} {:layer 1} B()
+{
+  yield;
+  call Set(5);
+  yield;
+  assert {:layer 1} x == 5;
+}
+
diff --git a/Test/civl/one.bpl.expect b/Test/civl/one.bpl.expect
index 6abb715b..37fad75c 100644
--- a/Test/civl/one.bpl.expect
+++ b/Test/civl/one.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 1 verified, 0 errors

+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/civl/parallel1.bpl b/Test/civl/parallel1.bpl
index 20dd3c79..ec24342e 100644
--- a/Test/civl/parallel1.bpl
+++ b/Test/civl/parallel1.bpl
@@ -1,48 +1,48 @@
-// RUN: %boogie -noinfer "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var {:layer 0,1} g:int;

-

-procedure {:yields} {:layer 1} PB()

-{

-  yield;

-  call Incr();

-  yield;

-}

-

-procedure {:yields} {:layer 0,1} Incr();

-ensures {:atomic}

-|{A:

-  g := g + 1; return true;

-}|;

-

-procedure {:yields} {:layer 0,1} Set(v: int);

-ensures {:atomic}

-|{A:

-  g := v; return true;

-}|;

-

-procedure {:yields} {:layer 1} PC()

-ensures {:layer 1} g == 3;

-{

-  yield;

-  call Set(3);

-  yield;

-  assert {:layer 1} g == 3;

-}

-

-procedure {:yields} {:layer 1} PD()

-{

-  call PC();

-  assert {:layer 1} g == 3;

-  yield;

-}

-

-procedure {:yields} {:layer 1} Main()

-{

-  yield;

-  while (*)

-  {

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

-  }

-  yield;

-}

+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,1} g:int;
+
+procedure {:yields} {:layer 1} PB()
+{
+  yield;
+  call Incr();
+  yield;
+}
+
+procedure {:yields} {:layer 0,1} Incr();
+ensures {:atomic}
+|{A:
+  g := g + 1; return true;
+}|;
+
+procedure {:yields} {:layer 0,1} Set(v: int);
+ensures {:atomic}
+|{A:
+  g := v; return true;
+}|;
+
+procedure {:yields} {:layer 1} PC()
+ensures {:layer 1} g == 3;
+{
+  yield;
+  call Set(3);
+  yield;
+  assert {:layer 1} g == 3;
+}
+
+procedure {:yields} {:layer 1} PD()
+{
+  call PC();
+  assert {:layer 1} g == 3;
+  yield;
+}
+
+procedure {:yields} {:layer 1} Main()
+{
+  yield;
+  while (*)
+  {
+    par PB() | PC() | PD();
+  }
+  yield;
+}
diff --git a/Test/civl/parallel2.bpl b/Test/civl/parallel2.bpl
index c28edf2b..540e9810 100644
--- a/Test/civl/parallel2.bpl
+++ b/Test/civl/parallel2.bpl
@@ -1,59 +1,59 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var {:layer 0,1} a:[int]int;

-

-function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

-function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

-{

-  MapConstBool(false)[x := true]

-}

-

-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int)

-{

-    yield;

-    call tid := AllocateLow();

-    yield;

-}

-

-procedure {:yields} {:layer 0,1} Write(idx: int, val: int);

-ensures {:atomic} |{A: a[idx] := val; return true; }|;

-

-procedure {:yields} {:layer 1} main() 

-{

-    var {:linear "tid"} i: int;

-    var {:linear "tid"} j: int;

-    call i := Allocate();

-    call j := Allocate();

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

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

-}

-

-procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)

-{

-    i := i';

-

-    yield;

-    call Write(i, 42);

-    call Yield(i);

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

-}

-

-procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) 

-{

-    i := i';

-

-    yield;

-    call Write(i, 42);

-    yield;

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

-}

-

-procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int)

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

-{

-    yield;

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

-}

-

-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int);

-ensures {:atomic} |{ A: return true; }|;

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,1} a:[int]int;
+
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
+{
+  MapConstBool(false)[x := true]
+}
+
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int)
+{
+    yield;
+    call tid := AllocateLow();
+    yield;
+}
+
+procedure {:yields} {:layer 0,1} Write(idx: int, val: int);
+ensures {:atomic} |{A: a[idx] := val; return true; }|;
+
+procedure {:yields} {:layer 1} main() 
+{
+    var {:linear "tid"} i: int;
+    var {:linear "tid"} j: int;
+    call i := Allocate();
+    call j := Allocate();
+    par i := t(i) | j := t(j);
+    par i := u(i) | j := u(j);
+}
+
+procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)
+{
+    i := i';
+
+    yield;
+    call Write(i, 42);
+    call Yield(i);
+    assert {:layer 1} a[i] == 42;
+}
+
+procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) 
+{
+    i := i';
+
+    yield;
+    call Write(i, 42);
+    yield;
+    assert {:layer 1} a[i] == 42;
+}
+
+procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int)
+ensures {:layer 1} old(a)[i] == a[i];
+{
+    yield;
+    assert {:layer 1} old(a)[i] == a[i];
+}
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int);
+ensures {:atomic} |{ A: return true; }|;
diff --git a/Test/civl/parallel2.bpl.expect b/Test/civl/parallel2.bpl.expect
index 05d394c7..3e6d423a 100644
--- a/Test/civl/parallel2.bpl.expect
+++ b/Test/civl/parallel2.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 5 verified, 0 errors

+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/civl/parallel4.bpl b/Test/civl/parallel4.bpl
index f06ff4b8..33a21446 100644
--- a/Test/civl/parallel4.bpl
+++ b/Test/civl/parallel4.bpl
@@ -1,45 +1,45 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var {:layer 0,1} a:int;

-

-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int)

-{

-    yield;

-    call tid := AllocateLow();

-    yield;

-}

-

-function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

-function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

-{

-  MapConstBool(false)[x := true]

-}

-

-procedure {:yields} {:layer 1} main() 

-{

-  var {:linear "tid"} i: int;

-  var {:linear "tid"} j: int;

-  call i := Allocate();

-  call j := Allocate();

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

-}

-

-procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)

-{

-  i := i';

-  call Yield();

-  assert {:layer 1} a == old(a);

-  call Incr();

-  yield;

-}

-

-procedure {:yields} {:layer 0,1} Incr();

-ensures {:atomic} |{A: a := a + 1; return true; }|;

-

-procedure {:yields} {:layer 1} Yield()

-{

-  yield;

-}

-

-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int);

-ensures {:atomic} |{ A: return true; }|;

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,1} a:int;
+
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int)
+{
+    yield;
+    call tid := AllocateLow();
+    yield;
+}
+
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
+{
+  MapConstBool(false)[x := true]
+}
+
+procedure {:yields} {:layer 1} main() 
+{
+  var {:linear "tid"} i: int;
+  var {:linear "tid"} j: int;
+  call i := Allocate();
+  call j := Allocate();
+  par i := t(i) | j := t(j);
+}
+
+procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)
+{
+  i := i';
+  call Yield();
+  assert {:layer 1} a == old(a);
+  call Incr();
+  yield;
+}
+
+procedure {:yields} {:layer 0,1} Incr();
+ensures {:atomic} |{A: a := a + 1; return true; }|;
+
+procedure {:yields} {:layer 1} Yield()
+{
+  yield;
+}
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int);
+ensures {:atomic} |{ A: return true; }|;
diff --git a/Test/civl/parallel4.bpl.expect b/Test/civl/parallel4.bpl.expect
index 25ad398c..2d4c8148 100644
--- a/Test/civl/parallel4.bpl.expect
+++ b/Test/civl/parallel4.bpl.expect
@@ -1,6 +1,6 @@
-parallel4.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    parallel4.bpl(29,5): anon0

-    (0,0): anon01

-

-Boogie program verifier finished with 3 verified, 1 error

+parallel4.bpl(31,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    parallel4.bpl(29,5): anon0
+    (0,0): anon01
+
+Boogie program verifier finished with 3 verified, 1 error
diff --git a/Test/civl/parallel5.bpl b/Test/civl/parallel5.bpl
index 87afc888..6d3deb8e 100644
--- a/Test/civl/parallel5.bpl
+++ b/Test/civl/parallel5.bpl
@@ -1,59 +1,59 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var {:layer 0,1} a:[int]int;

-

-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int)

-{

-    yield;

-    call tid := AllocateLow();

-    yield;

-}

-

-function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

-function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

-{

-  MapConstBool(false)[x := true]

-}

-

-procedure {:yields} {:layer 0,1} Write(idx: int, val: int);

-ensures {:atomic} |{A: a[idx] := val; return true; }|;

-

-procedure {:yields} {:layer 1} main() 

-{

-    var {:linear "tid"} i: int;

-    var {:linear "tid"} j: int;

-    call i := Allocate();

-    call j := Allocate();

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

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

-}

-

-procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)

-{

-    i := i';

-

-    yield;

-    call Write(i, 42);

-    call Yield(i);

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

-}

-

-procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) 

-{

-    i := i';

-

-    yield;

-    call Write(i, 42);

-    yield;

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

-}

-

-procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int)

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

-{

-    yield;

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

-}

-

-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int);

-ensures {:atomic} |{ A: return true; }|;

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,1} a:[int]int;
+
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int)
+{
+    yield;
+    call tid := AllocateLow();
+    yield;
+}
+
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
+{
+  MapConstBool(false)[x := true]
+}
+
+procedure {:yields} {:layer 0,1} Write(idx: int, val: int);
+ensures {:atomic} |{A: a[idx] := val; return true; }|;
+
+procedure {:yields} {:layer 1} main() 
+{
+    var {:linear "tid"} i: int;
+    var {:linear "tid"} j: int;
+    call i := Allocate();
+    call j := Allocate();
+    par i := t(i) | Yield(j);
+    par i := u(i) | j := u(j);
+}
+
+procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)
+{
+    i := i';
+
+    yield;
+    call Write(i, 42);
+    call Yield(i);
+    assert {:layer 1} a[i] == 42;
+}
+
+procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) 
+{
+    i := i';
+
+    yield;
+    call Write(i, 42);
+    yield;
+    assert {:layer 1} a[i] == 42;
+}
+
+procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int)
+ensures {:layer 1} old(a)[i] == a[i];
+{
+    yield;
+    assert {:layer 1} old(a)[i] == a[i];
+}
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int);
+ensures {:atomic} |{ A: return true; }|;
diff --git a/Test/civl/parallel5.bpl.expect b/Test/civl/parallel5.bpl.expect
index 05d394c7..3e6d423a 100644
--- a/Test/civl/parallel5.bpl.expect
+++ b/Test/civl/parallel5.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 5 verified, 0 errors

+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/civl/perm.bpl b/Test/civl/perm.bpl
index 5bc75324..5d6e0d21 100644
--- a/Test/civl/perm.bpl
+++ b/Test/civl/perm.bpl
@@ -1,49 +1,49 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var {:layer 0,1} x: int;

-function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;

-

-function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool;

-

-function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool

-{

-  x

-}

-

-procedure {:yields} {:layer 1} mainE({:linear_in "Perm"} permVar_in: [int]bool)

-   requires {:layer 1} permVar_in == ch_mapconstbool(true);

-   requires {:layer 1} x == 0;

-{

-    var {:linear "Perm"} permVar_out: [int]bool;

-

-    permVar_out := permVar_in;

-

-    yield;

-    assert {:layer 1} x == 0;

-    assert {:layer 1} permVar_out == ch_mapconstbool(true);

-

-    async call foo(permVar_out);

-    yield;

-}

-

-procedure {:yields} {:layer 1} foo({:linear_in "Perm"} permVar_in: [int]bool) 

-  requires {:layer 1} permVar_in != ch_mapconstbool(false);

-  requires {:layer 1} permVar_in[1];

-  requires {:layer 1} x == 0;

-{

-  var {:linear "Perm"} permVar_out: [int]bool;

-  permVar_out := permVar_in;

-  

-  yield;

-  assert {:layer 1} permVar_out[1];

-  assert {:layer 1} x == 0;

-

-  call Incr();

-

-  yield;

-  assert {:layer 1} permVar_out[1];

-  assert {:layer 1} x == 1;

-}

-

-procedure {:yields} {:layer 0,1} Incr();

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,1} x: int;
+function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;
+
+function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool;
+
+function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
+{
+  x
+}
+
+procedure {:yields} {:layer 1} mainE({:linear_in "Perm"} permVar_in: [int]bool)
+   requires {:layer 1} permVar_in == ch_mapconstbool(true);
+   requires {:layer 1} x == 0;
+{
+    var {:linear "Perm"} permVar_out: [int]bool;
+
+    permVar_out := permVar_in;
+
+    yield;
+    assert {:layer 1} x == 0;
+    assert {:layer 1} permVar_out == ch_mapconstbool(true);
+
+    async call foo(permVar_out);
+    yield;
+}
+
+procedure {:yields} {:layer 1} foo({:linear_in "Perm"} permVar_in: [int]bool) 
+  requires {:layer 1} permVar_in != ch_mapconstbool(false);
+  requires {:layer 1} permVar_in[1];
+  requires {:layer 1} x == 0;
+{
+  var {:linear "Perm"} permVar_out: [int]bool;
+  permVar_out := permVar_in;
+  
+  yield;
+  assert {:layer 1} permVar_out[1];
+  assert {:layer 1} x == 0;
+
+  call Incr();
+
+  yield;
+  assert {:layer 1} permVar_out[1];
+  assert {:layer 1} x == 1;
+}
+
+procedure {:yields} {:layer 0,1} Incr();
 ensures {:atomic} |{A: x := x + 1; return true; }|;
\ No newline at end of file
diff --git a/Test/civl/perm.bpl.expect b/Test/civl/perm.bpl.expect
index 3de74d3e..41374b00 100644
--- a/Test/civl/perm.bpl.expect
+++ b/Test/civl/perm.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 2 verified, 0 errors

+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/civl/t1.bpl b/Test/civl/t1.bpl
index 675b3842..ef468347 100644
--- a/Test/civl/t1.bpl
+++ b/Test/civl/t1.bpl
@@ -1,103 +1,103 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

-

-function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

-function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

-{

-  MapConstBool(false)[x := true]

-}

-

-function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool

-{

-  x

-}

-

-function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool

-{

-  x

-}

-

-var {:layer 0,1} g: int;

-var {:layer 0,1} h: int;

-

-procedure {:yields} {:layer 0,1} SetG(val:int);

-ensures {:atomic} |{A: g := val; return true; }|;

-

-procedure {:yields} {:layer 0,1} SetH(val:int);

-ensures {:atomic} |{A: h := val; return true; }|;

-

-procedure {:yields} {:layer 1} Yield({:linear "1"} x: [int]bool)

-requires {:layer 1} x == mapconstbool(true) && g == 0;    

-ensures {:layer 1} x == mapconstbool(true) && g == 0;    

-{

-    yield;

-    assert {:layer 1} x == mapconstbool(true) && g == 0;    

-}

-

-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int)

-ensures {:layer 1} xl != 0;

-{

-    yield;

-    call xl := AllocateLow();

-    yield;

-}

-

-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int);

-ensures {:atomic} |{ A: assume xls != 0; return true; }|;

-

-procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int) 

-requires {:layer 1} x == mapconstbool(true);

-requires {:layer 1} y == mapconstbool(true);

-{

-    var {:linear "tid"} tid_child: int;

-    tid_out := tid_in;

-

-    yield;

-    call SetG(0);

-    

-    par tid_child := Allocate() | Yield(x);

-

-    async call B(tid_child, x);

-

-    yield;

-    assert {:layer 1} x == mapconstbool(true);    

-    assert {:layer 1} g == 0;

-

-    call SetH(0);

-

-    yield;

-    assert {:layer 1} h == 0 && y == mapconstbool(true);    

-

-    yield;

-    call tid_child := Allocate();

-    async call C(tid_child, y);

-

-    yield;

-}

-

-procedure {:yields} {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) 

-requires {:layer 1} x_in != mapconstbool(false);

-{

-    var {:linear "tid"} tid_out: int;

-    var {:linear "1"} x: [int]bool;

-    tid_out := tid_in;

-    x := x_in;    

-

-    yield;

-    call SetG(1);

-    yield;

-}

-

-procedure {:yields} {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) 

-requires {:layer 1} y_in != mapconstbool(false);

-{

-    var {:linear "tid"} tid_out: int;

-    var {:linear "2"} y: [int]bool;

-    tid_out := tid_in;

-    y := y_in;   

-

-    yield;

-    call SetH(1);

-    yield;

-}

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
+
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
+{
+  MapConstBool(false)[x := true]
+}
+
+function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool
+{
+  x
+}
+
+function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool
+{
+  x
+}
+
+var {:layer 0,1} g: int;
+var {:layer 0,1} h: int;
+
+procedure {:yields} {:layer 0,1} SetG(val:int);
+ensures {:atomic} |{A: g := val; return true; }|;
+
+procedure {:yields} {:layer 0,1} SetH(val:int);
+ensures {:atomic} |{A: h := val; return true; }|;
+
+procedure {:yields} {:layer 1} Yield({:linear "1"} x: [int]bool)
+requires {:layer 1} x == mapconstbool(true) && g == 0;    
+ensures {:layer 1} x == mapconstbool(true) && g == 0;    
+{
+    yield;
+    assert {:layer 1} x == mapconstbool(true) && g == 0;    
+}
+
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int)
+ensures {:layer 1} xl != 0;
+{
+    yield;
+    call xl := AllocateLow();
+    yield;
+}
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int);
+ensures {:atomic} |{ A: assume xls != 0; return true; }|;
+
+procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int) 
+requires {:layer 1} x == mapconstbool(true);
+requires {:layer 1} y == mapconstbool(true);
+{
+    var {:linear "tid"} tid_child: int;
+    tid_out := tid_in;
+
+    yield;
+    call SetG(0);
+    
+    par tid_child := Allocate() | Yield(x);
+
+    async call B(tid_child, x);
+
+    yield;
+    assert {:layer 1} x == mapconstbool(true);    
+    assert {:layer 1} g == 0;
+
+    call SetH(0);
+
+    yield;
+    assert {:layer 1} h == 0 && y == mapconstbool(true);    
+
+    yield;
+    call tid_child := Allocate();
+    async call C(tid_child, y);
+
+    yield;
+}
+
+procedure {:yields} {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) 
+requires {:layer 1} x_in != mapconstbool(false);
+{
+    var {:linear "tid"} tid_out: int;
+    var {:linear "1"} x: [int]bool;
+    tid_out := tid_in;
+    x := x_in;    
+
+    yield;
+    call SetG(1);
+    yield;
+}
+
+procedure {:yields} {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) 
+requires {:layer 1} y_in != mapconstbool(false);
+{
+    var {:linear "tid"} tid_out: int;
+    var {:linear "2"} y: [int]bool;
+    tid_out := tid_in;
+    y := y_in;   
+
+    yield;
+    call SetH(1);
+    yield;
+}
diff --git a/Test/civl/termination.bpl b/Test/civl/termination.bpl
index 2d5542dd..7741fd19 100644
--- a/Test/civl/termination.bpl
+++ b/Test/civl/termination.bpl
@@ -1,18 +1,18 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-procedure {:yields} {:layer 0} X();

-ensures {:atomic} |{ A: return true; }|;

-

-procedure {:yields} {:layer 0} Y();

-ensures {:left} |{ A: return true; }|;

-

-procedure {:yields} {:layer 1} main() {

-  yield;

-  call X();

-  while (*)

-  {

-    call Y();

-  }

-  yield;

-  assert {:layer 1} true;

-}

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure {:yields} {:layer 0} X();
+ensures {:atomic} |{ A: return true; }|;
+
+procedure {:yields} {:layer 0} Y();
+ensures {:left} |{ A: return true; }|;
+
+procedure {:yields} {:layer 1} main() {
+  yield;
+  call X();
+  while (*)
+  {
+    call Y();
+  }
+  yield;
+  assert {:layer 1} true;
+}
diff --git a/Test/civl/termination.bpl.expect b/Test/civl/termination.bpl.expect
index d216a01d..adfbec48 100644
--- a/Test/civl/termination.bpl.expect
+++ b/Test/civl/termination.bpl.expect
@@ -1,3 +1,3 @@
 termination.bpl(9,31): Error: Implementation main fails simulation check C at layer 1. Transactions must be separated by a yield.
-

-1 type checking errors detected in termination.bpl

+
+1 type checking errors detected in termination.bpl
diff --git a/Test/civl/termination2.bpl b/Test/civl/termination2.bpl
index 840c27c1..1743c6a1 100644
--- a/Test/civl/termination2.bpl
+++ b/Test/civl/termination2.bpl
@@ -1,19 +1,19 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-procedure {:yields} {:layer 0} X();

-ensures {:atomic} |{ A: return true; }|;

-

-procedure {:yields} {:layer 0} Y();

-ensures {:left} |{ A: return true; }|;

-

-procedure {:yields} {:layer 1} main() {

-  yield;

-  call X();

-  while (*)

-  invariant {:terminates} {:layer 1} true;

-  {

-    call Y();

-  }

-  yield;

-  assert {:layer 1} true;

-}

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure {:yields} {:layer 0} X();
+ensures {:atomic} |{ A: return true; }|;
+
+procedure {:yields} {:layer 0} Y();
+ensures {:left} |{ A: return true; }|;
+
+procedure {:yields} {:layer 1} main() {
+  yield;
+  call X();
+  while (*)
+  invariant {:terminates} {:layer 1} true;
+  {
+    call Y();
+  }
+  yield;
+  assert {:layer 1} true;
+}
diff --git a/Test/civl/termination2.bpl.expect b/Test/civl/termination2.bpl.expect
index 6abb715b..37fad75c 100644
--- a/Test/civl/termination2.bpl.expect
+++ b/Test/civl/termination2.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 1 verified, 0 errors

+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl
index 91863e1a..9fc55646 100644
--- a/Test/civl/ticket.bpl
+++ b/Test/civl/ticket.bpl
@@ -1,147 +1,147 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-function RightOpen(n: int) : [int]bool;

-function RightClosed(n: int) : [int]bool;

-axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);

-axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);

-

-type X;

-function {:builtin "MapConst"} mapconstbool(bool): [X]bool;

-const nil: X;

-var {:layer 0,2} t: int;

-var {:layer 0,2} s: int;

-var {:layer 0,2} cs: X;

-var {:layer 0,2} T: [int]bool;

-

-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

-function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

-{

-  MapConstBool(false)[x := true]

-}

-function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool

-{

-  x

-}

-

-function {:inline} Inv1(tickets: [int]bool, ticket: int): (bool)

-{

-    tickets == RightOpen(ticket)

-}

-

-function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)

-{

-    if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket)

-}

-

-procedure {:yields} {:layer 2} Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X)

-ensures {:layer 1} {:layer 2} xl != nil;

-{

-    yield;

-    call xls, xl := AllocateLow(xls');

-    yield;

-}

-

-procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)

-requires {:layer 2} xls' == mapconstbool(true);

-{

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

-    var {:linear "tid"} xls: [X]bool;

-

-    yield;

-

-    call Init(xls');

-    xls := xls';

-

-    par Yield1() | Yield2();

-

-    while (*)

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

-    invariant {:layer 2} Inv2(T, s, cs);

-    {

-        par xls, tid := Allocate(xls) | Yield1() | Yield2();

-        async call Customer(tid);

-    	par Yield1() | Yield2();

-    }

-    par Yield1() | Yield2();

-}

-

-procedure {:yields} {:layer 2} Customer({:linear_in "tid"} tid: X)

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

-requires {:layer 2} tid != nil && Inv2(T, s, cs);

-{

-    par Yield1() | Yield2();    

-    while (*) 

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

-    invariant {:layer 2} Inv2(T, s, cs);

-    {

-        call Enter(tid);

-        par Yield1() | Yield2() | YieldSpec(tid);

-    	call Leave(tid);

-        par Yield1() | Yield2();

-    }

-    par Yield1() | Yield2();

-}

-

-procedure {:yields} {:layer 2} Enter({:linear "tid"} tid: X)

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

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

-requires {:layer 2} tid != nil && Inv2(T, s, cs);

-ensures {:layer 2} Inv2(T, s, cs) && cs == tid;

-{

-    var m: int;

-

-    par Yield1() | Yield2();

-    call m := GetTicketAbstract(tid);

-    par Yield1();

-    call WaitAndEnter(tid, m);

-    par Yield1() | Yield2() | YieldSpec(tid);

-}

-

-procedure {:yields} {:layer 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int)

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

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

-ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|;

-{

-    par Yield1();

-    call m := GetTicket(tid);

-    par Yield1();

-}

-

-procedure {:yields} {:layer 2} YieldSpec({:linear "tid"} tid: X)

-requires {:layer 2} tid != nil && cs == tid;

-ensures {:layer 2} cs == tid;

-{

-    yield;

-    assert {:layer 2} tid != nil && cs == tid;

-}

-

-procedure {:yields} {:layer 2} Yield2()

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

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

-{

-    yield;

-    assert {:layer 2} Inv2(T, s, cs);

-}

-

-procedure {:yields} {:layer 1} Yield1()

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

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

-{

-    yield;

-    assert {:layer 1} Inv1(T,t);

-}

-

-procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool);

-ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

-

-procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);

-ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|;

-

-procedure {:yields} {:layer 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int);

-ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|;

-

-procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X);

-ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|;

-

-procedure {:yields} {:layer 0,2} AllocateLow({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

-ensures {:atomic} |{ A: assume xl != nil; return true; }|;

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function RightOpen(n: int) : [int]bool;
+function RightClosed(n: int) : [int]bool;
+axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);
+axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
+
+type X;
+function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
+const nil: X;
+var {:layer 0,2} t: int;
+var {:layer 0,2} s: int;
+var {:layer 0,2} cs: X;
+var {:layer 0,2} T: [int]bool;
+
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+  MapConstBool(false)[x := true]
+}
+function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool
+{
+  x
+}
+
+function {:inline} Inv1(tickets: [int]bool, ticket: int): (bool)
+{
+    tickets == RightOpen(ticket)
+}
+
+function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)
+{
+    if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket)
+}
+
+procedure {:yields} {:layer 2} Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X)
+ensures {:layer 1} {:layer 2} xl != nil;
+{
+    yield;
+    call xls, xl := AllocateLow(xls');
+    yield;
+}
+
+procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)
+requires {:layer 2} xls' == mapconstbool(true);
+{
+    var {:linear "tid"} tid: X;
+    var {:linear "tid"} xls: [X]bool;
+
+    yield;
+
+    call Init(xls');
+    xls := xls';
+
+    par Yield1() | Yield2();
+
+    while (*)
+    invariant {:layer 1} Inv1(T, t);
+    invariant {:layer 2} Inv2(T, s, cs);
+    {
+        par xls, tid := Allocate(xls) | Yield1() | Yield2();
+        async call Customer(tid);
+    	par Yield1() | Yield2();
+    }
+    par Yield1() | Yield2();
+}
+
+procedure {:yields} {:layer 2} Customer({:linear_in "tid"} tid: X)
+requires {:layer 1} Inv1(T, t);
+requires {:layer 2} tid != nil && Inv2(T, s, cs);
+{
+    par Yield1() | Yield2();    
+    while (*) 
+    invariant {:layer 1} Inv1(T, t);
+    invariant {:layer 2} Inv2(T, s, cs);
+    {
+        call Enter(tid);
+        par Yield1() | Yield2() | YieldSpec(tid);
+    	call Leave(tid);
+        par Yield1() | Yield2();
+    }
+    par Yield1() | Yield2();
+}
+
+procedure {:yields} {:layer 2} Enter({:linear "tid"} tid: X)
+requires {:layer 1} Inv1(T, t);
+ensures {:layer 1} Inv1(T,t);
+requires {:layer 2} tid != nil && Inv2(T, s, cs);
+ensures {:layer 2} Inv2(T, s, cs) && cs == tid;
+{
+    var m: int;
+
+    par Yield1() | Yield2();
+    call m := GetTicketAbstract(tid);
+    par Yield1();
+    call WaitAndEnter(tid, m);
+    par Yield1() | Yield2() | YieldSpec(tid);
+}
+
+procedure {:yields} {:layer 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int)
+requires {:layer 1} Inv1(T, t);
+ensures {:layer 1} Inv1(T, t);
+ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|;
+{
+    par Yield1();
+    call m := GetTicket(tid);
+    par Yield1();
+}
+
+procedure {:yields} {:layer 2} YieldSpec({:linear "tid"} tid: X)
+requires {:layer 2} tid != nil && cs == tid;
+ensures {:layer 2} cs == tid;
+{
+    yield;
+    assert {:layer 2} tid != nil && cs == tid;
+}
+
+procedure {:yields} {:layer 2} Yield2()
+requires {:layer 2} Inv2(T, s, cs);
+ensures {:layer 2} Inv2(T, s, cs);
+{
+    yield;
+    assert {:layer 2} Inv2(T, s, cs);
+}
+
+procedure {:yields} {:layer 1} Yield1()
+requires {:layer 1} Inv1(T, t);
+ensures {:layer 1} Inv1(T,t);
+{
+    yield;
+    assert {:layer 1} Inv1(T,t);
+}
+
+procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool);
+ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
+
+procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);
+ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|;
+
+procedure {:yields} {:layer 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int);
+ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|;
+
+procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|;
+
+procedure {:yields} {:layer 0,2} AllocateLow({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
+ensures {:atomic} |{ A: assume xl != nil; return true; }|;
diff --git a/Test/civl/ticket.bpl.expect b/Test/civl/ticket.bpl.expect
index 28c26eab..b072912b 100644
--- a/Test/civl/ticket.bpl.expect
+++ b/Test/civl/ticket.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 16 verified, 0 errors

+
+Boogie program verifier finished with 16 verified, 0 errors
diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl
index 286c7dd1..751ce861 100644
--- a/Test/civl/treiber-stack.bpl
+++ b/Test/civl/treiber-stack.bpl
@@ -1,200 +1,200 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-type Node = int;

-const unique null: Node;

-type lmap;

-function {:linear "Node"} dom(lmap): [Node]bool;

-function map(lmap): [Node]Node;

-function {:builtin "MapConst"} MapConstBool(bool) : [Node]bool;

-

-function EmptyLmap(): (lmap);

-axiom (dom(EmptyLmap()) == MapConstBool(false));

-

-function Add(x: lmap, i: Node, v: Node): (lmap);

-axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);

-

-function Remove(x: lmap, i: Node): (lmap);

-axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));

-

-procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:Node);

-ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|;

-

-procedure {:yields} {:layer 0,1} Load(i:Node) returns (v:Node);

-ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C;

-	            B: assume dom(Stack)[i]; v := map(Stack)[i]; return true; 

-		    C: assume !dom(Stack)[i]; return true; }|;

-

-procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);

-ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|;

-

-procedure {:yields} {:layer 0,1} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);

-ensures {:atomic} |{ A: assert dom(l_in)[newVal];

-		        goto B,C;

-                        B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true;

-			C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|;

-

-procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);

-ensures {:atomic} |{ A: goto B,C;

-                        B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true;

-		        C: assume oldVal != TopOfStack; r := false; return true; }|;

-

-var {:layer 0} TopOfStack: Node;

-var {:linear "Node"} {:layer 0} Stack: lmap;

-

-

-function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool)

-{

-  BetweenSet(map(Stack), TopOfStack, null)[TopOfStack] &&

-  Subset(BetweenSet(map(Stack), TopOfStack, null), Union(Singleton(null), dom(Stack)))

-}

-

-var {:linear "Node"} {:layer 0} Used: lmap;

-

-procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)

-requires {:layer 1} dom(x_lmap)[x];

-requires {:layer 1} Inv(TopOfStack, Stack);

-ensures {:layer 1} Inv(TopOfStack, Stack);

-ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; return true; }|;

-{

-  var t: Node;

-  var g: bool;

-  var {:linear "Node"} t_lmap: lmap;

-

-  yield;

-  assert {:layer 1} Inv(TopOfStack, Stack);

-  t_lmap := x_lmap;

-  while (true)

-  invariant {:layer 1} dom(t_lmap) == dom(x_lmap);

-  invariant {:layer 1} Inv(TopOfStack, Stack);

-  {

-    call t := ReadTopOfStack();

-    call t_lmap := Store(t_lmap, x, t);

-    call g, t_lmap := TransferToStack(t, x, t_lmap); 

-    if (g) {

-      assert {:layer 1} map(Stack)[x] == t;

-      break;

-    }

-    yield; 

-    assert {:layer 1} dom(t_lmap) == dom(x_lmap);

-    assert {:layer 1} Inv(TopOfStack, Stack);

-  }

-  yield; 

-  assert {:expand} {:layer 1} Inv(TopOfStack, Stack);

-}

-

-procedure {:yields} {:layer 1} pop() returns (t: Node)

-requires {:layer 1} Inv(TopOfStack, Stack);

-ensures {:layer 1} Inv(TopOfStack, Stack);

-ensures {:atomic} |{ A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;

-{

-  var g: bool;

-  var x: Node;

-

-  yield;

-  assert {:layer 1} Inv(TopOfStack, Stack);

-  while (true)

-  invariant {:layer 1} Inv(TopOfStack, Stack);

-  {

-    call t := ReadTopOfStack();

-    if (t != null) {

-      call x := Load(t);

-      call g := TransferFromStack(t, x); 

-      if (g) { 

-        break;

-      }

-    }

-    yield;

-    assert {:layer 1} Inv(TopOfStack, Stack);

-  }

-  yield;

-  assert {:layer 1} Inv(TopOfStack, Stack);

-}

-

-function Equal([int]bool, [int]bool) returns (bool);

-function Subset([int]bool, [int]bool) returns (bool);

-

-function Empty() returns ([int]bool);

-function Singleton(int) returns ([int]bool);

-function Reachable([int,int]bool, int) returns ([int]bool);

-function Union([int]bool, [int]bool) returns ([int]bool);

-

-axiom(forall x:int :: !Empty()[x]);

-

-axiom(forall x:int, y:int :: {Singleton(y)[x]} Singleton(y)[x] <==> x == y);

-axiom(forall y:int :: {Singleton(y)} Singleton(y)[y]);

-

-axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T)[x]}{Union(S,T),S[x]}{Union(S,T),T[x]} Union(S,T)[x] <==> S[x] || T[x]);

-

-axiom(forall S:[int]bool, T:[int]bool :: {Equal(S,T)} Equal(S,T) <==> Subset(S,T) && Subset(T,S));

-axiom(forall x:int, S:[int]bool, T:[int]bool :: {S[x],Subset(S,T)}{T[x],Subset(S,T)} S[x] && Subset(S,T) ==> T[x]);

-axiom(forall S:[int]bool, T:[int]bool :: {Subset(S,T)} Subset(S,T) || (exists x:int :: S[x] && !T[x]));

-

-////////////////////

-// Between predicate

-//////////////////// 

-function Between(f: [int]int, x: int, y: int, z: int) returns (bool);

-function Avoiding(f: [int]int, x: int, y: int, z: int) returns (bool);

-

-

-//////////////////////////

-// Between set constructor

-//////////////////////////

-function BetweenSet(f: [int]int, x: int, z: int) returns ([int]bool);

-

-////////////////////////////////////////////////////

-// axioms relating Between and BetweenSet

-////////////////////////////////////////////////////

-axiom(forall f: [int]int, x: int, y: int, z: int :: {BetweenSet(f, x, z)[y]} BetweenSet(f, x, z)[y] <==> Between(f, x, y, z));

-axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z), BetweenSet(f, x, z)} Between(f, x, y, z) ==> BetweenSet(f, x, z)[y]);

-axiom(forall f: [int]int, x: int, z: int :: {BetweenSet(f, x, z)} Between(f, x, x, x));

-axiom(forall f: [int]int, x: int, z: int :: {BetweenSet(f, x, z)} Between(f, z, z, z));

-

-

-//////////////////////////

-// Axioms for Between

-//////////////////////////

-

-// reflexive

-axiom(forall f: [int]int, x: int :: Between(f, x, x, x));

-

-// step

-axiom(forall f: [int]int, x: int, y: int, z: int, w:int :: {Between(f, y, z, w), f[x]} Between(f, x, f[x], f[x])); 

-

-// reach

-axiom(forall f: [int]int, x: int, y: int :: {f[x], Between(f, x, y, y)} Between(f, x, y, y) ==> x == y || Between(f, x, f[x], y));

-

-// cycle

-axiom(forall f: [int]int, x: int, y:int :: {f[x], Between(f, x, y, y)} f[x] == x && Between(f, x, y, y) ==> x == y);

-

-// sandwich

-axiom(forall f: [int]int, x: int, y: int :: {Between(f, x, y, x)} Between(f, x, y, x) ==> x == y);

-

-// order1

-axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, y), Between(f, x, z, z)} Between(f, x, y, y) && Between(f, x, z, z) ==> Between(f, x, y, z) || Between(f, x, z, y));

-

-// order2

-axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z)} Between(f, x, y, z) ==> Between(f, x, y, y) && Between(f, y, z, z));

-

-// transitive1

-axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, y), Between(f, y, z, z)} Between(f, x, y, y) && Between(f, y, z, z) ==> Between(f, x, z, z));

-

-// transitive2

-axiom(forall f: [int]int, x: int, y: int, z: int, w: int :: {Between(f, x, y, z), Between(f, y, w, z)} Between(f, x, y, z) && Between(f, y, w, z) ==> Between(f, x, y, w) && Between(f, x, w, z));

-

-// transitive3

-axiom(forall f: [int]int, x: int, y: int, z: int, w: int :: {Between(f, x, y, z), Between(f, x, w, y)} Between(f, x, y, z) && Between(f, x, w, y) ==> Between(f, x, w, z) && Between(f, w, y, z));

-

-// This axiom is required to deal with the incompleteness of the trigger for the reflexive axiom.  

-// It cannot be proved using the rest of the axioms.

-axiom(forall f: [int]int, u:int, x: int :: {Between(f, u, x, x)} Between(f, u, x, x) ==> Between(f, u, u, x));

-

-// relation between Avoiding and Between

-axiom(forall f: [int]int, x: int, y: int, z: int :: {Avoiding(f, x, y, z)} Avoiding(f, x, y, z) <==> (Between(f, x, y, z) || (Between(f, x, y, y) && !Between(f, x, z, z))));

-axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z)} Between(f, x, y, z) <==> (Avoiding(f, x, y, z) && Avoiding(f, x, z, z)));

-

-// update

-axiom(forall f: [int]int, u: int, v: int, x: int, p: int, q: int :: {Avoiding(f[p := q], u, v, x)} Avoiding(f[p := q], u, v, x) <==> ((Avoiding(f, u, v, p) && Avoiding(f, u, v, x)) || (Avoiding(f, u, p, x) && p != x && Avoiding(f, q, v, p) && Avoiding(f, q, v, x))));

-

-axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} Avoiding(f, u, w, p) ==> Equal(BetweenSet(f[p := q], u, w), BetweenSet(f, u, w)));

-axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} p != w && Avoiding(f, u, p, w) && Avoiding(f, q, w, p) ==> Equal(BetweenSet(f[p := q], u, w), Union(BetweenSet(f, u, p), BetweenSet(f, q, w))));

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type Node = int;
+const unique null: Node;
+type lmap;
+function {:linear "Node"} dom(lmap): [Node]bool;
+function map(lmap): [Node]Node;
+function {:builtin "MapConst"} MapConstBool(bool) : [Node]bool;
+
+function EmptyLmap(): (lmap);
+axiom (dom(EmptyLmap()) == MapConstBool(false));
+
+function Add(x: lmap, i: Node, v: Node): (lmap);
+axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);
+
+function Remove(x: lmap, i: Node): (lmap);
+axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));
+
+procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:Node);
+ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|;
+
+procedure {:yields} {:layer 0,1} Load(i:Node) returns (v:Node);
+ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C;
+	            B: assume dom(Stack)[i]; v := map(Stack)[i]; return true; 
+		    C: assume !dom(Stack)[i]; return true; }|;
+
+procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);
+ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|;
+
+procedure {:yields} {:layer 0,1} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);
+ensures {:atomic} |{ A: assert dom(l_in)[newVal];
+		        goto B,C;
+                        B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true;
+			C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|;
+
+procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);
+ensures {:atomic} |{ A: goto B,C;
+                        B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true;
+		        C: assume oldVal != TopOfStack; r := false; return true; }|;
+
+var {:layer 0} TopOfStack: Node;
+var {:linear "Node"} {:layer 0} Stack: lmap;
+
+
+function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool)
+{
+  BetweenSet(map(Stack), TopOfStack, null)[TopOfStack] &&
+  Subset(BetweenSet(map(Stack), TopOfStack, null), Union(Singleton(null), dom(Stack)))
+}
+
+var {:linear "Node"} {:layer 0} Used: lmap;
+
+procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)
+requires {:layer 1} dom(x_lmap)[x];
+requires {:layer 1} Inv(TopOfStack, Stack);
+ensures {:layer 1} Inv(TopOfStack, Stack);
+ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; return true; }|;
+{
+  var t: Node;
+  var g: bool;
+  var {:linear "Node"} t_lmap: lmap;
+
+  yield;
+  assert {:layer 1} Inv(TopOfStack, Stack);
+  t_lmap := x_lmap;
+  while (true)
+  invariant {:layer 1} dom(t_lmap) == dom(x_lmap);
+  invariant {:layer 1} Inv(TopOfStack, Stack);
+  {
+    call t := ReadTopOfStack();
+    call t_lmap := Store(t_lmap, x, t);
+    call g, t_lmap := TransferToStack(t, x, t_lmap); 
+    if (g) {
+      assert {:layer 1} map(Stack)[x] == t;
+      break;
+    }
+    yield; 
+    assert {:layer 1} dom(t_lmap) == dom(x_lmap);
+    assert {:layer 1} Inv(TopOfStack, Stack);
+  }
+  yield; 
+  assert {:expand} {:layer 1} Inv(TopOfStack, Stack);
+}
+
+procedure {:yields} {:layer 1} pop() returns (t: Node)
+requires {:layer 1} Inv(TopOfStack, Stack);
+ensures {:layer 1} Inv(TopOfStack, Stack);
+ensures {:atomic} |{ A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;
+{
+  var g: bool;
+  var x: Node;
+
+  yield;
+  assert {:layer 1} Inv(TopOfStack, Stack);
+  while (true)
+  invariant {:layer 1} Inv(TopOfStack, Stack);
+  {
+    call t := ReadTopOfStack();
+    if (t != null) {
+      call x := Load(t);
+      call g := TransferFromStack(t, x); 
+      if (g) { 
+        break;
+      }
+    }
+    yield;
+    assert {:layer 1} Inv(TopOfStack, Stack);
+  }
+  yield;
+  assert {:layer 1} Inv(TopOfStack, Stack);
+}
+
+function Equal([int]bool, [int]bool) returns (bool);
+function Subset([int]bool, [int]bool) returns (bool);
+
+function Empty() returns ([int]bool);
+function Singleton(int) returns ([int]bool);
+function Reachable([int,int]bool, int) returns ([int]bool);
+function Union([int]bool, [int]bool) returns ([int]bool);
+
+axiom(forall x:int :: !Empty()[x]);
+
+axiom(forall x:int, y:int :: {Singleton(y)[x]} Singleton(y)[x] <==> x == y);
+axiom(forall y:int :: {Singleton(y)} Singleton(y)[y]);
+
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T)[x]}{Union(S,T),S[x]}{Union(S,T),T[x]} Union(S,T)[x] <==> S[x] || T[x]);
+
+axiom(forall S:[int]bool, T:[int]bool :: {Equal(S,T)} Equal(S,T) <==> Subset(S,T) && Subset(T,S));
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {S[x],Subset(S,T)}{T[x],Subset(S,T)} S[x] && Subset(S,T) ==> T[x]);
+axiom(forall S:[int]bool, T:[int]bool :: {Subset(S,T)} Subset(S,T) || (exists x:int :: S[x] && !T[x]));
+
+////////////////////
+// Between predicate
+//////////////////// 
+function Between(f: [int]int, x: int, y: int, z: int) returns (bool);
+function Avoiding(f: [int]int, x: int, y: int, z: int) returns (bool);
+
+
+//////////////////////////
+// Between set constructor
+//////////////////////////
+function BetweenSet(f: [int]int, x: int, z: int) returns ([int]bool);
+
+////////////////////////////////////////////////////
+// axioms relating Between and BetweenSet
+////////////////////////////////////////////////////
+axiom(forall f: [int]int, x: int, y: int, z: int :: {BetweenSet(f, x, z)[y]} BetweenSet(f, x, z)[y] <==> Between(f, x, y, z));
+axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z), BetweenSet(f, x, z)} Between(f, x, y, z) ==> BetweenSet(f, x, z)[y]);
+axiom(forall f: [int]int, x: int, z: int :: {BetweenSet(f, x, z)} Between(f, x, x, x));
+axiom(forall f: [int]int, x: int, z: int :: {BetweenSet(f, x, z)} Between(f, z, z, z));
+
+
+//////////////////////////
+// Axioms for Between
+//////////////////////////
+
+// reflexive
+axiom(forall f: [int]int, x: int :: Between(f, x, x, x));
+
+// step
+axiom(forall f: [int]int, x: int, y: int, z: int, w:int :: {Between(f, y, z, w), f[x]} Between(f, x, f[x], f[x])); 
+
+// reach
+axiom(forall f: [int]int, x: int, y: int :: {f[x], Between(f, x, y, y)} Between(f, x, y, y) ==> x == y || Between(f, x, f[x], y));
+
+// cycle
+axiom(forall f: [int]int, x: int, y:int :: {f[x], Between(f, x, y, y)} f[x] == x && Between(f, x, y, y) ==> x == y);
+
+// sandwich
+axiom(forall f: [int]int, x: int, y: int :: {Between(f, x, y, x)} Between(f, x, y, x) ==> x == y);
+
+// order1
+axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, y), Between(f, x, z, z)} Between(f, x, y, y) && Between(f, x, z, z) ==> Between(f, x, y, z) || Between(f, x, z, y));
+
+// order2
+axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z)} Between(f, x, y, z) ==> Between(f, x, y, y) && Between(f, y, z, z));
+
+// transitive1
+axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, y), Between(f, y, z, z)} Between(f, x, y, y) && Between(f, y, z, z) ==> Between(f, x, z, z));
+
+// transitive2
+axiom(forall f: [int]int, x: int, y: int, z: int, w: int :: {Between(f, x, y, z), Between(f, y, w, z)} Between(f, x, y, z) && Between(f, y, w, z) ==> Between(f, x, y, w) && Between(f, x, w, z));
+
+// transitive3
+axiom(forall f: [int]int, x: int, y: int, z: int, w: int :: {Between(f, x, y, z), Between(f, x, w, y)} Between(f, x, y, z) && Between(f, x, w, y) ==> Between(f, x, w, z) && Between(f, w, y, z));
+
+// This axiom is required to deal with the incompleteness of the trigger for the reflexive axiom.  
+// It cannot be proved using the rest of the axioms.
+axiom(forall f: [int]int, u:int, x: int :: {Between(f, u, x, x)} Between(f, u, x, x) ==> Between(f, u, u, x));
+
+// relation between Avoiding and Between
+axiom(forall f: [int]int, x: int, y: int, z: int :: {Avoiding(f, x, y, z)} Avoiding(f, x, y, z) <==> (Between(f, x, y, z) || (Between(f, x, y, y) && !Between(f, x, z, z))));
+axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z)} Between(f, x, y, z) <==> (Avoiding(f, x, y, z) && Avoiding(f, x, z, z)));
+
+// update
+axiom(forall f: [int]int, u: int, v: int, x: int, p: int, q: int :: {Avoiding(f[p := q], u, v, x)} Avoiding(f[p := q], u, v, x) <==> ((Avoiding(f, u, v, p) && Avoiding(f, u, v, x)) || (Avoiding(f, u, p, x) && p != x && Avoiding(f, q, v, p) && Avoiding(f, q, v, x))));
+
+axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} Avoiding(f, u, w, p) ==> Equal(BetweenSet(f[p := q], u, w), BetweenSet(f, u, w)));
+axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} p != w && Avoiding(f, u, p, w) && Avoiding(f, q, w, p) ==> Equal(BetweenSet(f[p := q], u, w), Union(BetweenSet(f, u, p), BetweenSet(f, q, w))));
 axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} Avoiding(f, u, w, p) || (p != w && Avoiding(f, u, p, w) && Avoiding(f, q, w, p)) || Equal(BetweenSet(f[p := q], u, w), Empty()));
\ No newline at end of file
diff --git a/Test/civl/treiber-stack.bpl.expect b/Test/civl/treiber-stack.bpl.expect
index be6b95ba..9823d44a 100644
--- a/Test/civl/treiber-stack.bpl.expect
+++ b/Test/civl/treiber-stack.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 6 verified, 0 errors

+
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl
index f4964258..17f53401 100644
--- a/Test/civl/wsq.bpl
+++ b/Test/civl/wsq.bpl
@@ -1,560 +1,560 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-type Tid;

-const nil: Tid;

-

-function {:builtin "MapConst"} MapConstBool(bool) : [Tid]bool;

-function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool

-{

- MapConstBool(false)[x := true]

-}

-

-

-

-var {:layer 0,3} H: int;

-var {:layer 0,3} T: int;

-var {:layer 0,3} items: [int]int;

-var {:layer 0} status: [int]bool;

-var {:layer 0,3} take_in_cs: bool;

-var {:layer 0,3} put_in_cs: bool;

-var {:layer 0,3} steal_in_cs: [Tid]bool;

-var {:layer 0,3} h_ss: [Tid]int;

-var {:layer 0,3} t_ss: [Tid]int;

-

-const IN_Q: bool;

-const NOT_IN_Q: bool;

-axiom IN_Q == true;

-axiom NOT_IN_Q == false;

-

-const unique EMPTY: int;

-const unique NIL: Tid;

-const unique ptTid: Tid;

-axiom ptTid != NIL;

-

-function {:inline} stealerTid(tid: Tid):(bool) { tid != NIL && tid != ptTid  }

-

-function {:inline} ideasInv(put_in_cs:bool,

-                           items:[int]int,

-                           status: [int]bool,

-                H:int, T:int,

-                take_in_cs:bool,

-                steal_in_cs:[Tid]bool,

-                h_ss:[Tid]int,

-                    t_ss:[Tid]int

-                ):(bool)

-{ 

-   (

-     ( (take_in_cs) && h_ss[ptTid] < t_ss[ptTid] ==> (t_ss[ptTid] == T && H <= T && 

-                                                          items[T] != EMPTY && status[T] == IN_Q) ) &&

-     (put_in_cs ==> !take_in_cs) && (take_in_cs ==> !put_in_cs) &&                            

-     (( (take_in_cs) && H != h_ss[ptTid]) ==> H > h_ss[ptTid]) &&

-     (forall td:Tid :: (stealerTid(td) && steal_in_cs[td] && H == h_ss[td] && H < t_ss[td]) ==> (items[H] != EMPTY && status[H] == IN_Q)) &&

-     (forall td:Tid :: (stealerTid(td) && steal_in_cs[td] && H != h_ss[td]) ==> H > h_ss[td])

-    )

-}

-

-function {:inline} queueInv(steal_in_cs:[Tid]bool,

-                           put_in_cs:bool,

-                take_in_cs:bool,

-                items:[int]int, status: [int]bool, _H:int, _T:int):(bool)

-{ 

-   ( (forall i:int :: (_H <= i && i <= _T) ==> (status[i] == IN_Q && items[i] != EMPTY)) )

-}

-

-function {:inline} emptyInv(put_in_cs:bool, take_in_cs:bool, items:[int]int, status:[int]bool, T:int):(bool)

-{

-	(forall i:int :: (i>=T && !put_in_cs && !take_in_cs) ==> status[i] == NOT_IN_Q && items[i] == EMPTY)

-}

-

-function {:inline} putInv(items:[int]int, status: [int]bool, H:int, T:int):(bool)

-{ 

-   (forall i:int :: (H <= i && i < T) ==> (status[i] == IN_Q && items[i] != EMPTY))

-}

-

-function {:inline} takeInv(items:[int]int, status: [int]bool, H:int, T:int, t:int, h:int):(bool)

-{ 

-   (forall i:int :: (h <= i && i <= t) ==> (status[i] == IN_Q &&

-    items[i] != EMPTY) &&

-    t == T 

-   )

-}

-                 

-procedure {:yields} {:layer 3} put({:linear "tid"} tid:Tid, task: int)

-requires {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && task != EMPTY && !take_in_cs && !put_in_cs;

-requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-requires {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);

-ensures {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;

-ensures {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);

-ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|;

-{

-   var t: int;

-   var {:ghost} oldH:int;

-   var {:ghost} oldT:int;

-   var {:ghost} oldStatusT:bool;

-   

-

-   oldH := H;

-   oldT := T;

-   yield;

-   assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;

-   assert {:layer 3} {:expand} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-   assert {:layer 3} oldH <= H && oldT == T;

-   assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);

-

-   call t := readT_put(tid);

-

-   oldH := H;

-   oldT := T;

-   yield;

-   assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && put_in_cs;

-   assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-   assert {:layer 3} tid == ptTid && t == T;

-   assert {:layer 3} oldH <= H && oldT == T;

-   assert {:layer 3} (forall i:int :: i>=T ==> status[i] == NOT_IN_Q && items[i] == EMPTY);

-   

-   call writeItems_put(tid,t, task);

-

-   oldH := H;

-   oldT := T;

-   oldStatusT := status[T];

-   yield;

-   assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && t == T && tid == ptTid && !take_in_cs && put_in_cs;

-   assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-   assert {:layer 3} items[t] == task;

-   assert {:layer 3} oldH <= H && oldT == T;

-   assert {:layer 3} (forall i:int :: i>T ==> status[i] == NOT_IN_Q && items[i] == EMPTY);

-

-   

-   call writeT_put(tid, t+1);

-

-   oldH := H;

-   oldT := T;

-   yield;

-   assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;

-   assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-   assert {:layer 3} T == t + 1;

-   assert {:layer 3} oldH <= H && oldT == T;

-   assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);

-}

-

-procedure {:yields} {:layer 3} take({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool)

-requires {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;

-requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-ensures {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs && (task != EMPTY ==> taskstatus == IN_Q);

-ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; status[i] := NOT_IN_Q; return true; C: return true;}|;

-{

-   var h, t: int;

-   var chk: bool;

-   var {:ghost} oldH:int;

-   var {:ghost} oldT:int;

-

-   oldH := H;

-   oldT := T;

-   yield;

-   assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;

-   assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-   assert {:layer 3} oldH <= H && oldT == T;

-   

-   LOOP_ENTRY_1:

-

-   while(true) 

-   invariant {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;

-   invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    

-   {

-

-       oldH := H;

-       oldT := T;

-       yield;

-       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;

-    assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-       assert {:layer 3} oldH <= H && oldT == T;

-    

-       call t := readT_take_init(tid);

-

-       oldH := H;

-       oldT := T;

-       yield;

-       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;

-       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    

-       assert {:layer 3} t == T;

-    assert {:layer 3} items[t-1] == EMPTY ==> H > t-1;

-       assert {:layer 3} oldH <= H && oldT == T;

-    

-       t := t-1;

-       call writeT_take(tid, t);

-

-       oldH := H;

-       oldT := T;

-       yield;

-       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !take_in_cs && !put_in_cs && t_ss[tid] == t;

-       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    

-       assert {:layer 3} t == T;

-       assert {:layer 3} items[t] == EMPTY ==> H > t;

-       assert {:layer 3} oldH <= H && oldT == T;

-    

-       call h := readH_take(tid);

-

-       oldH := H;

-       oldT := T;

-       yield;

-       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs  && !put_in_cs && h_ss[tid] == h && t_ss[tid] == t;  

-       assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    

-       assert {:layer 3} t == T;

-       assert {:layer 3} h <= H;

-       assert {:layer 3} items[t] == EMPTY ==> H > t;

-       assert {:layer 3} oldH <= H;

-    assert {:layer 3} oldT == T;

-    assert {:layer 3} h <= H;

-    assert {:layer 3} oldH == h;

-

-       if(t<h) {

-

-           call writeT_take_abort(tid, h);

-           task := EMPTY;

- 

-           oldH := H;

-           oldT := T;

-           yield;

-        assert {:layer 3} h <= H;

-           assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; 

-           assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-        assert {:layer 3} h == T;

-           assert {:layer 3} oldH <= H && oldT == T;

-           return;

-       }

-

-       call task, taskstatus := readItems(tid, t);

-

-       oldH := H;

-       oldT := T;

-       yield;

-    assert {:layer 3} H >= h;

-       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && h_ss[tid] == h && t_ss[tid] == t;  

-       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    

-       assert {:layer 3} t == T && task == items[T];

-    assert {:layer 3} T > H ==> items[T] != EMPTY;

-       assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && take_in_cs;

-

-       if(t>h) {

-        call takeExitCS(tid);

-

-           oldH := H;

-           oldT := T;    

-           yield;

-           assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && h_ss[tid] == h && t_ss[tid] == t;  

-        assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-        assert {:layer 3} t == T && task == items[t] && task != EMPTY && taskstatus == IN_Q;

-           assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && !take_in_cs;

-           return;

-       }

-	   call writeT_take_eq(tid, h+1);

-	   oldH := H;

-       oldT := T;

-	   

-	   yield;

-	   assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;

-       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-	   assert {:layer 3} T == h + 1;

-	   assert {:layer 3} oldH <= H;

-	   assert {:layer 3} oldT == T;

-	   assert {:layer 3} task == items[t];

-	   assert {:layer 3} !put_in_cs;

-	   

-       call chk := CAS_H_take(tid, h,h+1);

-

-

-       oldH := H;

-       oldT := T;    

-       yield;

-	assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == oldH -1 && task != EMPTY);

-       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  

-    assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-       assert {:layer 3} h+1 == T;

-	   assert {:layer 3} task == items[t];

-	   assert {:layer 3} !take_in_cs;

-	   assert {:layer 3} !put_in_cs;

-       assert {:layer 3} oldH <= H && oldT == T;

-

-       if(!chk) {

-    

-          oldH := H;

-          oldT := T;    

-          yield;

-          assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  

-         assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-          assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs;

-          assert {:layer 3} oldH <= H && oldT == T;

-   

-          goto LOOP_ENTRY_1;

-       }

-

-       oldH := H;

-       oldT := T;    

-       yield;

-       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  

-    assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-    assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs;

-       assert {:layer 3} oldH <= H && oldT == T && task != EMPTY && taskstatus == IN_Q;

-

-       return;

-   }

-   

-   oldH := H;

-   oldT := T;

-   yield;

-   assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !put_in_cs;

-   assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-   assert {:layer 3} oldH <= H && oldT == T;

-

-}

-

-

-procedure {:yields}{:layer 3} steal({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool)

-requires {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && stealerTid(tid) &&

-                   !steal_in_cs[tid];

-requires {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-ensures {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) &&

-                   !steal_in_cs[tid] && (task != EMPTY ==> taskstatus == IN_Q);

-ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; status[i] := NOT_IN_Q; return true; C: return true;}|;

-{

-   var h, t: int;

-   var chk: bool;

-   var {:ghost} oldH:int;

-   var {:ghost} oldT:int;

-

-   oldH := H;

-   oldT := T;

-   yield;

-   assert {:layer 3} stealerTid(tid);

-   assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);

-   assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-   assert {:layer 3} oldH <= H;

-   assert {:layer 3} !steal_in_cs[tid];

-

-   LOOP_ENTRY_2:

-   while(true) 

-   invariant {:layer 3} stealerTid(tid);

-   invariant {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);

-   invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-   invariant {:layer 3} !steal_in_cs[tid];

-   {

-       oldH := H;

-       oldT := T;

-       yield;

-    assert {:layer 3} stealerTid(tid);

-       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);

-       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-       assert {:layer 3} oldH <= H;

-       assert {:layer 3} !steal_in_cs[tid];

-    

-       call h := readH_steal(tid);

-

-       oldH := H;

-       oldT := T;

-       yield;

-    assert {:layer 3} H >= h;

-    assert {:layer 3} !steal_in_cs[tid];

-    assert {:layer 3} h_ss[tid] == h; 

-       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);

-       assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-       assert {:layer 3} oldH <= H;

-

-       call t := readT_steal(tid);

-

-

-       oldH := H;

-       oldT := T;

-       yield;

-    assert {:layer 3} steal_in_cs[tid];

-    assert {:layer 3} stealerTid(tid) && H >= h && steal_in_cs[tid] && h_ss[tid] == h;

-       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);

-       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-       assert {:layer 3} oldH <= H && t == t_ss[tid];

-    assert {:layer 3} (h < t && take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && h == H) ==> (H < T);

-    assert {:layer 3} H >= h;

-

-       if( h>= t) {

-

-           task := EMPTY;

-        call stealExitCS(tid);

-

-           oldH := H;

-           oldT := T;

-           yield;

-        assert {:layer 3} !steal_in_cs[tid];

-        assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid] && h_ss[tid] == h;

-           assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);

-           assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-           assert {:layer 3} oldH <= H;

-           return;

-       }

-    

-       call task, taskstatus := readItems(tid, h);

-

-

-       oldH := H;

-       oldT := T;

-       yield;

-    assert {:layer 3} stealerTid(tid) && steal_in_cs[tid] && h_ss[tid] == h;

-       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);

-       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-       assert {:layer 3} oldH <= H;

-    assert {:layer 3} oldH == H && H == h && h_ss[tid] == h ==> task != EMPTY;

-    assert {:layer 3} (take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && h == H) ==> (H < T);

-	assert {:layer 3} h == H ==> status[H] == IN_Q;

-

-       call chk := CAS_H_steal(tid, h,h+1);

-

-       oldH := H;

-       oldT := T;

-       yield;

-    assert {:layer 3} h_ss[tid] == h;

-    assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == h && task != EMPTY && taskstatus == IN_Q);

-    assert {:layer 3} (take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && chk) ==> ((oldH-1) < T);    

-    assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-    assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];

-       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);

-       assert {:layer 3} oldH <= H;

-

-       if(!chk) {

-          goto LOOP_ENTRY_2;

-       }

-

-       oldH := H;

-       oldT := T;

-       yield;

-    assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];

-       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);

-       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);

-       assert {:layer 3} oldH <= H && task != EMPTY;

-       return;

-   }

-   

-   oldH := H;

-   oldT := T;

-   yield;

-   assert {:layer 3} chk && task != EMPTY;

-   assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];

-   assert {:layer 3} oldH <= H;

-}

-

-procedure {:yields}{:layer 0,3} readH_take({:linear "tid"} tid:Tid) returns (y: int);

-ensures {:atomic} |{A:  assert tid == ptTid;

-                       y := H;

-            take_in_cs := true;

-            h_ss[tid] := H;

-            return true;}|;

-

-procedure {:yields}{:layer 0,3} readH_steal({:linear "tid"} tid:Tid) returns (y: int);

-ensures {:atomic} |{A:  assert stealerTid(tid);

-                       assert !steal_in_cs[tid];

-                       y := H;

-            h_ss[tid] := H;

-            return true;}|;

-

-procedure {:yields}{:layer 0,3} readT_take_init({:linear "tid"} tid:Tid) returns (y: int);

-ensures {:atomic} |{A:  assert tid != NIL; assert tid == ptTid; y := T; return true;}|;

-

-procedure {:yields}{:layer 0,3} readT_put({:linear "tid"} tid:Tid) returns (y: int);

-ensures {:atomic} |{A:  assert tid != NIL;

-                       assert tid == ptTid;

-            put_in_cs := true;

-            y := T;

-            return true;}|;

-

-procedure {:yields}{:layer 0,3} readT_steal({:linear "tid"} tid:Tid) returns (y: int);

-ensures {:atomic} |{A:  assert tid != NIL;

-                       assert stealerTid(tid);

-            assert !steal_in_cs[tid];

-                       y := T;

-            t_ss[tid] := T;

-            steal_in_cs[tid] := true;

-            return true;}|;

-

-procedure {:yields}{:layer 0,3} readItems({:linear "tid"} tid:Tid, ind: int) returns (y: int, b:bool);

-ensures {:atomic} |{A: y := items[ind]; b := status[ind]; return true; }|;

-

-procedure {:yields}{:layer 0,3} writeT_put({:linear "tid"} tid:Tid, val: int);

-ensures {:atomic} |{A: assert tid == ptTid; 

-                      T := T+1;

-               put_in_cs := false;

-                      return true; }|;

-

-procedure {:yields}{:layer 0,3} writeT_take({:linear "tid"} tid:Tid, val: int);

-ensures {:atomic} |{A: assert tid == ptTid;

-                      T := val;

-               t_ss[tid] := val;

-                      return true; }|;

-

-procedure {:yields}{:layer 0,3} writeT_take_abort({:linear "tid"} tid:Tid, val: int);

-ensures {:atomic} |{A: assert tid == ptTid;

-                      assert take_in_cs;

-                      T := val;

-               take_in_cs := false;

-                      return true; }|;

-

-procedure {:yields}{:layer 0,3} writeT_take_eq({:linear "tid"} tid:Tid, val: int);

-ensures {:atomic} |{A: assert tid == ptTid;

-                      T := val;

-                      return true; }|;

-

-procedure {:yields}{:layer 0,3} takeExitCS({:linear "tid"} tid:Tid);

-ensures {:atomic} |{A: assert tid == ptTid;

-               take_in_cs := false;

-                      return true; }|;

-

-procedure {:yields}{:layer 0,3} stealExitCS({:linear "tid"} tid:Tid);

-ensures {:atomic} |{A: assert stealerTid(tid);

-                      assert steal_in_cs[tid];

-               steal_in_cs[tid] := false;

-                      return true; }|;

-

-

-procedure {:yields}{:layer 0,3} writeItems({:linear "tid"} tid:Tid, idx: int, val: int);

-ensures {:atomic} |{A: assert tid == ptTid; 

-                      assert val != EMPTY; 

-                      items[idx] := val; 

-                      status[idx] := IN_Q; 

-                      return true; }|;

-

-

-procedure {:yields}{:layer 0,3} writeItems_put({:linear "tid"} tid:Tid, idx: int, val: int);

-ensures {:atomic} |{A: assert tid == ptTid; 

-                      assert val != EMPTY; 

-                      items[idx] := val; 

-                      status[idx] := IN_Q; 

-                      return true; }|;

-

-procedure {:yields}{:layer 0,3} CAS_H_take({:linear "tid"} tid:Tid, prevVal :int, val: int)

-                                          returns (result: bool);

-ensures {:atomic} |{ A: assert tid == ptTid;

-                       goto B, C; 

-                    B: assume H == prevVal; 

-                take_in_cs := false;

-            status[H] := NOT_IN_Q;

-            H := H+1;

-            result := true;

-                return true; 

-                    C: assume H != prevVal; result := false; 

-                take_in_cs := false;

-            return true; 

-}|;

-

-procedure {:yields}{:layer 0,3} CAS_H_steal({:linear "tid"} tid:Tid, prevVal :int, val: int)

-                                           returns (result: bool);

-ensures {:atomic} |{ A: assert stealerTid(tid);

-                       goto B, C; 

-                    B: assume H == prevVal;

-            status[H] := NOT_IN_Q;

-                 H := H+1;

-            result := true;

-                steal_in_cs[tid] := false;

-                return true; 

-                    C: assume H != prevVal;

-                result := false;

-                steal_in_cs[tid] := false;

-                return true; 

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type Tid;
+const nil: Tid;
+
+function {:builtin "MapConst"} MapConstBool(bool) : [Tid]bool;
+function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
+{
+ MapConstBool(false)[x := true]
+}
+
+
+
+var {:layer 0,3} H: int;
+var {:layer 0,3} T: int;
+var {:layer 0,3} items: [int]int;
+var {:layer 0} status: [int]bool;
+var {:layer 0,3} take_in_cs: bool;
+var {:layer 0,3} put_in_cs: bool;
+var {:layer 0,3} steal_in_cs: [Tid]bool;
+var {:layer 0,3} h_ss: [Tid]int;
+var {:layer 0,3} t_ss: [Tid]int;
+
+const IN_Q: bool;
+const NOT_IN_Q: bool;
+axiom IN_Q == true;
+axiom NOT_IN_Q == false;
+
+const unique EMPTY: int;
+const unique NIL: Tid;
+const unique ptTid: Tid;
+axiom ptTid != NIL;
+
+function {:inline} stealerTid(tid: Tid):(bool) { tid != NIL && tid != ptTid  }
+
+function {:inline} ideasInv(put_in_cs:bool,
+                           items:[int]int,
+                           status: [int]bool,
+                H:int, T:int,
+                take_in_cs:bool,
+                steal_in_cs:[Tid]bool,
+                h_ss:[Tid]int,
+                    t_ss:[Tid]int
+                ):(bool)
+{ 
+   (
+     ( (take_in_cs) && h_ss[ptTid] < t_ss[ptTid] ==> (t_ss[ptTid] == T && H <= T && 
+                                                          items[T] != EMPTY && status[T] == IN_Q) ) &&
+     (put_in_cs ==> !take_in_cs) && (take_in_cs ==> !put_in_cs) &&                            
+     (( (take_in_cs) && H != h_ss[ptTid]) ==> H > h_ss[ptTid]) &&
+     (forall td:Tid :: (stealerTid(td) && steal_in_cs[td] && H == h_ss[td] && H < t_ss[td]) ==> (items[H] != EMPTY && status[H] == IN_Q)) &&
+     (forall td:Tid :: (stealerTid(td) && steal_in_cs[td] && H != h_ss[td]) ==> H > h_ss[td])
+    )
+}
+
+function {:inline} queueInv(steal_in_cs:[Tid]bool,
+                           put_in_cs:bool,
+                take_in_cs:bool,
+                items:[int]int, status: [int]bool, _H:int, _T:int):(bool)
+{ 
+   ( (forall i:int :: (_H <= i && i <= _T) ==> (status[i] == IN_Q && items[i] != EMPTY)) )
+}
+
+function {:inline} emptyInv(put_in_cs:bool, take_in_cs:bool, items:[int]int, status:[int]bool, T:int):(bool)
+{
+	(forall i:int :: (i>=T && !put_in_cs && !take_in_cs) ==> status[i] == NOT_IN_Q && items[i] == EMPTY)
+}
+
+function {:inline} putInv(items:[int]int, status: [int]bool, H:int, T:int):(bool)
+{ 
+   (forall i:int :: (H <= i && i < T) ==> (status[i] == IN_Q && items[i] != EMPTY))
+}
+
+function {:inline} takeInv(items:[int]int, status: [int]bool, H:int, T:int, t:int, h:int):(bool)
+{ 
+   (forall i:int :: (h <= i && i <= t) ==> (status[i] == IN_Q &&
+    items[i] != EMPTY) &&
+    t == T 
+   )
+}
+                 
+procedure {:yields} {:layer 3} put({:linear "tid"} tid:Tid, task: int)
+requires {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && task != EMPTY && !take_in_cs && !put_in_cs;
+requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+requires {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
+ensures {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
+ensures {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
+ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|;
+{
+   var t: int;
+   var {:ghost} oldH:int;
+   var {:ghost} oldT:int;
+   var {:ghost} oldStatusT:bool;
+   
+
+   oldH := H;
+   oldT := T;
+   yield;
+   assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
+   assert {:layer 3} {:expand} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+   assert {:layer 3} oldH <= H && oldT == T;
+   assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
+
+   call t := readT_put(tid);
+
+   oldH := H;
+   oldT := T;
+   yield;
+   assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && put_in_cs;
+   assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+   assert {:layer 3} tid == ptTid && t == T;
+   assert {:layer 3} oldH <= H && oldT == T;
+   assert {:layer 3} (forall i:int :: i>=T ==> status[i] == NOT_IN_Q && items[i] == EMPTY);
+   
+   call writeItems_put(tid,t, task);
+
+   oldH := H;
+   oldT := T;
+   oldStatusT := status[T];
+   yield;
+   assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && t == T && tid == ptTid && !take_in_cs && put_in_cs;
+   assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+   assert {:layer 3} items[t] == task;
+   assert {:layer 3} oldH <= H && oldT == T;
+   assert {:layer 3} (forall i:int :: i>T ==> status[i] == NOT_IN_Q && items[i] == EMPTY);
+
+   
+   call writeT_put(tid, t+1);
+
+   oldH := H;
+   oldT := T;
+   yield;
+   assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
+   assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+   assert {:layer 3} T == t + 1;
+   assert {:layer 3} oldH <= H && oldT == T;
+   assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
+}
+
+procedure {:yields} {:layer 3} take({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool)
+requires {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
+requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+ensures {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs && (task != EMPTY ==> taskstatus == IN_Q);
+ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; status[i] := NOT_IN_Q; return true; C: return true;}|;
+{
+   var h, t: int;
+   var chk: bool;
+   var {:ghost} oldH:int;
+   var {:ghost} oldT:int;
+
+   oldH := H;
+   oldT := T;
+   yield;
+   assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
+   assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+   assert {:layer 3} oldH <= H && oldT == T;
+   
+   LOOP_ENTRY_1:
+
+   while(true) 
+   invariant {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
+   invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
+   {
+
+       oldH := H;
+       oldT := T;
+       yield;
+       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
+    assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+       assert {:layer 3} oldH <= H && oldT == T;
+    
+       call t := readT_take_init(tid);
+
+       oldH := H;
+       oldT := T;
+       yield;
+       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
+       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
+       assert {:layer 3} t == T;
+    assert {:layer 3} items[t-1] == EMPTY ==> H > t-1;
+       assert {:layer 3} oldH <= H && oldT == T;
+    
+       t := t-1;
+       call writeT_take(tid, t);
+
+       oldH := H;
+       oldT := T;
+       yield;
+       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !take_in_cs && !put_in_cs && t_ss[tid] == t;
+       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
+       assert {:layer 3} t == T;
+       assert {:layer 3} items[t] == EMPTY ==> H > t;
+       assert {:layer 3} oldH <= H && oldT == T;
+    
+       call h := readH_take(tid);
+
+       oldH := H;
+       oldT := T;
+       yield;
+       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs  && !put_in_cs && h_ss[tid] == h && t_ss[tid] == t;  
+       assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
+       assert {:layer 3} t == T;
+       assert {:layer 3} h <= H;
+       assert {:layer 3} items[t] == EMPTY ==> H > t;
+       assert {:layer 3} oldH <= H;
+    assert {:layer 3} oldT == T;
+    assert {:layer 3} h <= H;
+    assert {:layer 3} oldH == h;
+
+       if(t<h) {
+
+           call writeT_take_abort(tid, h);
+           task := EMPTY;
+ 
+           oldH := H;
+           oldT := T;
+           yield;
+        assert {:layer 3} h <= H;
+           assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; 
+           assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+        assert {:layer 3} h == T;
+           assert {:layer 3} oldH <= H && oldT == T;
+           return;
+       }
+
+       call task, taskstatus := readItems(tid, t);
+
+       oldH := H;
+       oldT := T;
+       yield;
+    assert {:layer 3} H >= h;
+       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && h_ss[tid] == h && t_ss[tid] == t;  
+       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
+       assert {:layer 3} t == T && task == items[T];
+    assert {:layer 3} T > H ==> items[T] != EMPTY;
+       assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && take_in_cs;
+
+       if(t>h) {
+        call takeExitCS(tid);
+
+           oldH := H;
+           oldT := T;    
+           yield;
+           assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && h_ss[tid] == h && t_ss[tid] == t;  
+        assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+        assert {:layer 3} t == T && task == items[t] && task != EMPTY && taskstatus == IN_Q;
+           assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && !take_in_cs;
+           return;
+       }
+	   call writeT_take_eq(tid, h+1);
+	   oldH := H;
+       oldT := T;
+	   
+	   yield;
+	   assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;
+       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+	   assert {:layer 3} T == h + 1;
+	   assert {:layer 3} oldH <= H;
+	   assert {:layer 3} oldT == T;
+	   assert {:layer 3} task == items[t];
+	   assert {:layer 3} !put_in_cs;
+	   
+       call chk := CAS_H_take(tid, h,h+1);
+
+
+       oldH := H;
+       oldT := T;    
+       yield;
+	assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == oldH -1 && task != EMPTY);
+       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  
+    assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+       assert {:layer 3} h+1 == T;
+	   assert {:layer 3} task == items[t];
+	   assert {:layer 3} !take_in_cs;
+	   assert {:layer 3} !put_in_cs;
+       assert {:layer 3} oldH <= H && oldT == T;
+
+       if(!chk) {
+    
+          oldH := H;
+          oldT := T;    
+          yield;
+          assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  
+         assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+          assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs;
+          assert {:layer 3} oldH <= H && oldT == T;
+   
+          goto LOOP_ENTRY_1;
+       }
+
+       oldH := H;
+       oldT := T;    
+       yield;
+       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  
+    assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+    assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs;
+       assert {:layer 3} oldH <= H && oldT == T && task != EMPTY && taskstatus == IN_Q;
+
+       return;
+   }
+   
+   oldH := H;
+   oldT := T;
+   yield;
+   assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !put_in_cs;
+   assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+   assert {:layer 3} oldH <= H && oldT == T;
+
+}
+
+
+procedure {:yields}{:layer 3} steal({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool)
+requires {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && stealerTid(tid) &&
+                   !steal_in_cs[tid];
+requires {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+ensures {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) &&
+                   !steal_in_cs[tid] && (task != EMPTY ==> taskstatus == IN_Q);
+ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; status[i] := NOT_IN_Q; return true; C: return true;}|;
+{
+   var h, t: int;
+   var chk: bool;
+   var {:ghost} oldH:int;
+   var {:ghost} oldT:int;
+
+   oldH := H;
+   oldT := T;
+   yield;
+   assert {:layer 3} stealerTid(tid);
+   assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
+   assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+   assert {:layer 3} oldH <= H;
+   assert {:layer 3} !steal_in_cs[tid];
+
+   LOOP_ENTRY_2:
+   while(true) 
+   invariant {:layer 3} stealerTid(tid);
+   invariant {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
+   invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+   invariant {:layer 3} !steal_in_cs[tid];
+   {
+       oldH := H;
+       oldT := T;
+       yield;
+    assert {:layer 3} stealerTid(tid);
+       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
+       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+       assert {:layer 3} oldH <= H;
+       assert {:layer 3} !steal_in_cs[tid];
+    
+       call h := readH_steal(tid);
+
+       oldH := H;
+       oldT := T;
+       yield;
+    assert {:layer 3} H >= h;
+    assert {:layer 3} !steal_in_cs[tid];
+    assert {:layer 3} h_ss[tid] == h; 
+       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
+       assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+       assert {:layer 3} oldH <= H;
+
+       call t := readT_steal(tid);
+
+
+       oldH := H;
+       oldT := T;
+       yield;
+    assert {:layer 3} steal_in_cs[tid];
+    assert {:layer 3} stealerTid(tid) && H >= h && steal_in_cs[tid] && h_ss[tid] == h;
+       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
+       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+       assert {:layer 3} oldH <= H && t == t_ss[tid];
+    assert {:layer 3} (h < t && take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && h == H) ==> (H < T);
+    assert {:layer 3} H >= h;
+
+       if( h>= t) {
+
+           task := EMPTY;
+        call stealExitCS(tid);
+
+           oldH := H;
+           oldT := T;
+           yield;
+        assert {:layer 3} !steal_in_cs[tid];
+        assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid] && h_ss[tid] == h;
+           assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
+           assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+           assert {:layer 3} oldH <= H;
+           return;
+       }
+    
+       call task, taskstatus := readItems(tid, h);
+
+
+       oldH := H;
+       oldT := T;
+       yield;
+    assert {:layer 3} stealerTid(tid) && steal_in_cs[tid] && h_ss[tid] == h;
+       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
+       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+       assert {:layer 3} oldH <= H;
+    assert {:layer 3} oldH == H && H == h && h_ss[tid] == h ==> task != EMPTY;
+    assert {:layer 3} (take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && h == H) ==> (H < T);
+	assert {:layer 3} h == H ==> status[H] == IN_Q;
+
+       call chk := CAS_H_steal(tid, h,h+1);
+
+       oldH := H;
+       oldT := T;
+       yield;
+    assert {:layer 3} h_ss[tid] == h;
+    assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == h && task != EMPTY && taskstatus == IN_Q);
+    assert {:layer 3} (take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && chk) ==> ((oldH-1) < T);    
+    assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+    assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];
+       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
+       assert {:layer 3} oldH <= H;
+
+       if(!chk) {
+          goto LOOP_ENTRY_2;
+       }
+
+       oldH := H;
+       oldT := T;
+       yield;
+    assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];
+       assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
+       assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+       assert {:layer 3} oldH <= H && task != EMPTY;
+       return;
+   }
+   
+   oldH := H;
+   oldT := T;
+   yield;
+   assert {:layer 3} chk && task != EMPTY;
+   assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];
+   assert {:layer 3} oldH <= H;
+}
+
+procedure {:yields}{:layer 0,3} readH_take({:linear "tid"} tid:Tid) returns (y: int);
+ensures {:atomic} |{A:  assert tid == ptTid;
+                       y := H;
+            take_in_cs := true;
+            h_ss[tid] := H;
+            return true;}|;
+
+procedure {:yields}{:layer 0,3} readH_steal({:linear "tid"} tid:Tid) returns (y: int);
+ensures {:atomic} |{A:  assert stealerTid(tid);
+                       assert !steal_in_cs[tid];
+                       y := H;
+            h_ss[tid] := H;
+            return true;}|;
+
+procedure {:yields}{:layer 0,3} readT_take_init({:linear "tid"} tid:Tid) returns (y: int);
+ensures {:atomic} |{A:  assert tid != NIL; assert tid == ptTid; y := T; return true;}|;
+
+procedure {:yields}{:layer 0,3} readT_put({:linear "tid"} tid:Tid) returns (y: int);
+ensures {:atomic} |{A:  assert tid != NIL;
+                       assert tid == ptTid;
+            put_in_cs := true;
+            y := T;
+            return true;}|;
+
+procedure {:yields}{:layer 0,3} readT_steal({:linear "tid"} tid:Tid) returns (y: int);
+ensures {:atomic} |{A:  assert tid != NIL;
+                       assert stealerTid(tid);
+            assert !steal_in_cs[tid];
+                       y := T;
+            t_ss[tid] := T;
+            steal_in_cs[tid] := true;
+            return true;}|;
+
+procedure {:yields}{:layer 0,3} readItems({:linear "tid"} tid:Tid, ind: int) returns (y: int, b:bool);
+ensures {:atomic} |{A: y := items[ind]; b := status[ind]; return true; }|;
+
+procedure {:yields}{:layer 0,3} writeT_put({:linear "tid"} tid:Tid, val: int);
+ensures {:atomic} |{A: assert tid == ptTid; 
+                      T := T+1;
+               put_in_cs := false;
+                      return true; }|;
+
+procedure {:yields}{:layer 0,3} writeT_take({:linear "tid"} tid:Tid, val: int);
+ensures {:atomic} |{A: assert tid == ptTid;
+                      T := val;
+               t_ss[tid] := val;
+                      return true; }|;
+
+procedure {:yields}{:layer 0,3} writeT_take_abort({:linear "tid"} tid:Tid, val: int);
+ensures {:atomic} |{A: assert tid == ptTid;
+                      assert take_in_cs;
+                      T := val;
+               take_in_cs := false;
+                      return true; }|;
+
+procedure {:yields}{:layer 0,3} writeT_take_eq({:linear "tid"} tid:Tid, val: int);
+ensures {:atomic} |{A: assert tid == ptTid;
+                      T := val;
+                      return true; }|;
+
+procedure {:yields}{:layer 0,3} takeExitCS({:linear "tid"} tid:Tid);
+ensures {:atomic} |{A: assert tid == ptTid;
+               take_in_cs := false;
+                      return true; }|;
+
+procedure {:yields}{:layer 0,3} stealExitCS({:linear "tid"} tid:Tid);
+ensures {:atomic} |{A: assert stealerTid(tid);
+                      assert steal_in_cs[tid];
+               steal_in_cs[tid] := false;
+                      return true; }|;
+
+
+procedure {:yields}{:layer 0,3} writeItems({:linear "tid"} tid:Tid, idx: int, val: int);
+ensures {:atomic} |{A: assert tid == ptTid; 
+                      assert val != EMPTY; 
+                      items[idx] := val; 
+                      status[idx] := IN_Q; 
+                      return true; }|;
+
+
+procedure {:yields}{:layer 0,3} writeItems_put({:linear "tid"} tid:Tid, idx: int, val: int);
+ensures {:atomic} |{A: assert tid == ptTid; 
+                      assert val != EMPTY; 
+                      items[idx] := val; 
+                      status[idx] := IN_Q; 
+                      return true; }|;
+
+procedure {:yields}{:layer 0,3} CAS_H_take({:linear "tid"} tid:Tid, prevVal :int, val: int)
+                                          returns (result: bool);
+ensures {:atomic} |{ A: assert tid == ptTid;
+                       goto B, C; 
+                    B: assume H == prevVal; 
+                take_in_cs := false;
+            status[H] := NOT_IN_Q;
+            H := H+1;
+            result := true;
+                return true; 
+                    C: assume H != prevVal; result := false; 
+                take_in_cs := false;
+            return true; 
+}|;
+
+procedure {:yields}{:layer 0,3} CAS_H_steal({:linear "tid"} tid:Tid, prevVal :int, val: int)
+                                           returns (result: bool);
+ensures {:atomic} |{ A: assert stealerTid(tid);
+                       goto B, C; 
+                    B: assume H == prevVal;
+            status[H] := NOT_IN_Q;
+                 H := H+1;
+            result := true;
+                steal_in_cs[tid] := false;
+                return true; 
+                    C: assume H != prevVal;
+                result := false;
+                steal_in_cs[tid] := false;
+                return true; 
                  }|;
\ No newline at end of file
diff --git a/Test/civl/wsq.bpl.expect b/Test/civl/wsq.bpl.expect
index 5b2909f1..a9949f2e 100644
--- a/Test/civl/wsq.bpl.expect
+++ b/Test/civl/wsq.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 3 verified, 0 errors

+
+Boogie program verifier finished with 3 verified, 0 errors