diff --git a/Test/civl/regression-tests/call-in-yield-proc.bpl b/Test/civl/regression-tests/call-in-yield-proc.bpl
deleted file mode 100644
index 1e1ef5810..000000000
--- a/Test/civl/regression-tests/call-in-yield-proc.bpl
+++ /dev/null
@@ -1,24 +0,0 @@
-// RUN: %parallel-boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-yield procedure {:layer 1} Foo1({:linear_in} x: Lset int) returns (z: Lset int)
-{
-    var y: Lval int;
-    z := x;
-    call {:layer 1} Lval_Split(z, y);
-}
-
-var {:layer 0,1} w: Lset int;
-
-yield procedure {:layer 1} Foo2()
-{
-    var y: Lval int;
-    call {:layer 1} Lval_Split(w, y);
-}
-
-var {:layer 1,2} a: Lset int;
-yield procedure {:layer 2} Foo3()
-{
-    var y: Lval int;
-    call {:layer 1} Lval_Split(a, y);
-}
diff --git a/Test/civl/regression-tests/call-in-yield-proc.bpl.expect b/Test/civl/regression-tests/call-in-yield-proc.bpl.expect
deleted file mode 100644
index fc1d4fbdf..000000000
--- a/Test/civl/regression-tests/call-in-yield-proc.bpl.expect
+++ /dev/null
@@ -1,4 +0,0 @@
-call-in-yield-proc.bpl(8,4): Error: variable must be available only within layers in [1, 1]: z
-call-in-yield-proc.bpl(16,4): Error: variable must be introduced at layer 1: w
-call-in-yield-proc.bpl(23,4): Error: variable must be hidden at layer 1: a
-3 type checking errors detected in call-in-yield-proc.bpl
diff --git a/Test/civl/regression-tests/dir_request.bpl b/Test/civl/regression-tests/dir_request.bpl
deleted file mode 100644
index a17996797..000000000
--- a/Test/civl/regression-tests/dir_request.bpl
+++ /dev/null
@@ -1,24 +0,0 @@
-// RUN: %parallel-boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-var {:layer 0,1} X: Lset int;
-var {:layer 0,1} B: [int]bool;
-
-right action {:layer 1} Lock(i: int) returns (li: Lval int)
-modifies X, B;
-{
-    assume !B[i];
-    li := Lval(i);
-    call Lval_Split(X, li);
-    B[i] := true;
-}
-
-left action {:layer 1} Unlock({:linear_in} li: Lval int)
-modifies X, B;
-{
-    var i: int;
-    i := li->val;
-    assert B[i];
-    call Lval_Put(X, li);
-    B[i] := false;
-}
diff --git a/Test/civl/regression-tests/dir_request.bpl.expect b/Test/civl/regression-tests/dir_request.bpl.expect
deleted file mode 100644
index 76a9a2bfb..000000000
--- a/Test/civl/regression-tests/dir_request.bpl.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/regression-tests/linear-test.bpl b/Test/civl/regression-tests/linear-test.bpl
index 92ad397bb..37d4a7157 100644
--- a/Test/civl/regression-tests/linear-test.bpl
+++ b/Test/civl/regression-tests/linear-test.bpl
@@ -7,21 +7,3 @@ yield procedure {:layer 1} foo1({:linear "A"} x: int, {:linear "A"} y: int)
 {
     assert {:layer 1} x != y;
 }
-
-yield procedure {:layer 1} foo2({:layer 1} {:linear_in} x: Lset int, i: int) returns ({:layer 1} y: Lset int)
-requires {:layer 1} x->dom[i];
-{
-    var {:layer 1} v: Lval int;
-    y := x;
-    call {:layer 1} v := Lval_Get(y, i);
-    assert {:layer 1} !Lset_Contains(y, i);
-}
-
-yield procedure {:layer 1} foo3({:layer 1} {:linear_in} x: Lset int, i: [int]bool) returns ({:layer 1} y: Lset int)
-requires {:layer 1} IsSubset(i, x->dom);
-{
-    var {:layer 1} v: Lset int;
-    y := x;
-    call {:layer 1} v := Lset_Get(y, i);
-    assert {:layer 1} IsDisjoint(y->dom, i);
-}
\ No newline at end of file
diff --git a/Test/civl/regression-tests/linear-test.bpl.expect b/Test/civl/regression-tests/linear-test.bpl.expect
index a9949f2e7..37fad75c9 100644
--- a/Test/civl/regression-tests/linear-test.bpl.expect
+++ b/Test/civl/regression-tests/linear-test.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/civl/regression-tests/linear_types.bpl b/Test/civl/regression-tests/linear_types.bpl
deleted file mode 100644
index 2060cb3f0..000000000
--- a/Test/civl/regression-tests/linear_types.bpl
+++ /dev/null
@@ -1,43 +0,0 @@
-// RUN: %parallel-boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-atomic action {:layer 1, 2} A3({:linear_in} path: Lset int, {:linear_out} l: Lset int) returns (path': Lset int) {
-    call path' := Lset_Empty();
-    call Lset_Put(path', path);
-    call Lset_Split(path', l);
-}
-
-atomic action {:layer 1, 2} A4({:linear_in} path: Lset int, l: Lval int) returns (path': Lset int) {
-    call path' := Lset_Empty();
-    call Lset_Put(path', path);
-    call Lval_Put(path', l);
-    call Lval_Split(path', l);
-}
-
-atomic action {:layer 1, 2} A5({:linear_in} path: Lheap int) returns (path': Lheap int) {
-    path' := path;
-}
-
-var {:layer 0, 2} g: Lheap int;
-
-datatype Foo { Foo(f: Lheap int) }
-
-atomic action {:layer 1, 2} A8({:linear_out} l: Lval int, {:linear_in} path: Lset int) returns (path': Lset int)
-{
-    path' := path;
-    call Lval_Split(path', l);
-}
-
-atomic action {:layer 1, 2} A10({:linear_in} a: Foo) returns (b: Foo)
-{
-    var x: Lheap int;
-    Foo(x) := a;
-    b := Foo(x);
-}
-
-datatype Bar { Bar(x: Lval int, y: int) }
-
-atomic action {:layer 1, 2} A11({:linear_in} a: Lval int) returns (b: Bar)
-{
-    b := Bar(a, 3+4);
-}
diff --git a/Test/civl/regression-tests/linear_types_error.bpl b/Test/civl/regression-tests/linear_types_error.bpl
deleted file mode 100644
index 88f607a61..000000000
--- a/Test/civl/regression-tests/linear_types_error.bpl
+++ /dev/null
@@ -1,59 +0,0 @@
-// RUN: %parallel-boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-atomic action {:layer 1, 2} A0(path: Lheap int) returns (l: Lheap int) { }
-
-atomic action {:layer 1, 2} A1(path: Lheap int) returns (path': Lheap int) {
-    path' := path;
-}
-
-atomic action {:layer 1, 2} A2(path: Lheap int) returns (path': Lheap int) { var k: Lset (Ref int);
-    call path' := Lmap_Empty();
-    call k := Lmap_Free(path);
-}
-
-var {:layer 0, 2} g: Lheap int;
-
-datatype Foo { Foo(f: Lheap int) }
-
-atomic action {:layer 1, 2} A5({:linear_out} path: Lheap int) { }
-
-atomic action {:layer 1, 2} A11({:linear_in} a: Foo) returns (b: Foo)
-{
-    var x: Lheap int;
-    Foo(x) := a;
-}
-
-atomic action {:layer 1, 2} A12({:linear_in} a: Foo) returns (b: Foo)
-{
-    var x: Lheap int;
-    b := a;
-    Foo(x) := a;
-}
-
-atomic action {:layer 1, 2} A13({:linear_in} a: Foo) returns (b: Foo)
-{
-    var x: Lheap int;
-    b := Foo(x);
-}
-
-datatype Bar { Bar(x: Lval int, y: int) }
-
-atomic action {:layer 1, 2} A14({:linear_in} a: Lval int) returns (b: Bar)
-{
-    b := Bar(Lval(3), 3+4);
-}
-
-type {:linear "X"} X = int;
-yield procedure {:layer 1} A15({:linear_in "X"} a: Lval int);
-
-yield procedure {:layer 1} Foo1(x: Lheap int)
-{
-  call Lmap_Assume(x, x);
-}
-
-yield procedure {:layer 1} Foo2(x: Foo)
-{
-  call Lmap_Assume(x->f, x->f);
-}
-
diff --git a/Test/civl/regression-tests/linear_types_error.bpl.expect b/Test/civl/regression-tests/linear_types_error.bpl.expect
deleted file mode 100644
index 891e35034..000000000
--- a/Test/civl/regression-tests/linear_types_error.bpl.expect
+++ /dev/null
@@ -1,12 +0,0 @@
-linear_types_error.bpl(48,48): Error: Variable of linear type must not have a domain name
-linear_types_error.bpl(4,73): Error: Output variable l must be available at a return
-linear_types_error.bpl(8,0): Error: Input variable path must be available at a return
-linear_types_error.bpl(13,0): Error: Input variable path must be available at a return
-linear_types_error.bpl(19,64): Error: Input variable path must be available at a return
-linear_types_error.bpl(25,0): Error: Output variable b must be available at a return
-linear_types_error.bpl(31,14): Error: unavailable source for a linear read
-linear_types_error.bpl(37,9): Error: unavailable source for a linear read
-linear_types_error.bpl(44,6): Error: A source of pack of linear type must be a variable
-linear_types_error.bpl(52,2): Error: Linear variable x can occur only once as an input parameter
-linear_types_error.bpl(57,2): Error: Linear variable x can occur only once as an input parameter
-11 type checking errors detected in linear_types_error.bpl
diff --git a/Test/civl/regression-tests/yield-proc-rewrite.bpl b/Test/civl/regression-tests/yield-proc-rewrite.bpl
deleted file mode 100644
index 0c00fb0c5..000000000
--- a/Test/civl/regression-tests/yield-proc-rewrite.bpl
+++ /dev/null
@@ -1,23 +0,0 @@
-// RUN: %parallel-boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-yield procedure {:layer 1} Foo1({:linear_in} x: Lset int) returns ({:layer 1} z: Lset int)
-{
-    var y: Lval int;
-    z := x;
-    call {:layer 1} Lval_Split(z, y);
-}
-
-atomic action {:layer 2} AtomicFoo2({:linear_in} x: Lset int) returns (z: Lset int)
-{
-    var y: Lval int;
-    z := x;
-    call Lval_Split(z, y);
-}
-yield procedure {:layer 1} Foo2({:linear_in} x: Lset int) returns ({:layer 1} z: Lset int)
-refines AtomicFoo2;
-{
-    var y: Lval int;
-    z := x;
-    call {:layer 1} Lval_Split(z, y);
-}
diff --git a/Test/civl/regression-tests/yield-proc-rewrite.bpl.expect b/Test/civl/regression-tests/yield-proc-rewrite.bpl.expect
deleted file mode 100644
index b37a9b950..000000000
--- a/Test/civl/regression-tests/yield-proc-rewrite.bpl.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-yield-proc-rewrite.bpl(8,5): Error: Lval_Split failed
-Execution trace:
-    yield-proc-rewrite.bpl(7,7): anon0
-
-Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/civl/samples/MutexOverFutex.bpl b/Test/civl/samples/MutexOverFutex.bpl
index 80ac9e8b9..9a46c1a7e 100644
--- a/Test/civl/samples/MutexOverFutex.bpl
+++ b/Test/civl/samples/MutexOverFutex.bpl
@@ -1,7 +1,7 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-type Tid; // thread identifiers
+type {:linear "tid"} Tid; // thread identifiers
 
 type Mutex = Option Tid;
 
@@ -13,13 +13,13 @@ var {:layer 0, 1} futex: Futex;           // implementation
 
 /// Implementation of Mutex
 
-atomic action {:layer 2} AtomicLock(tid: Lval Tid)
+atomic action {:layer 2} AtomicLock({:linear "tid"} tid: Tid)
 modifies mutex;
 {
   assume mutex == None();
-  mutex := Some(tid->val);
+  mutex := Some(tid);
 }
-yield procedure {:layer 1} Lock(tid: Lval Tid)
+yield procedure {:layer 1} Lock({:linear "tid"} tid: Tid)
 refines AtomicLock;
 preserves call YieldInv();
 preserves call YieldWait(tid);
@@ -27,7 +27,7 @@ preserves call YieldWait(tid);
   var oldValue, temp: int;
   call oldValue := CmpXchg(0, 1);
   if (oldValue != 0) {
-    call {:layer 1} inSlowPath := Copy(inSlowPath[tid->val := true]);
+    call {:layer 1} inSlowPath := Copy(inSlowPath[tid := true]);
     while (true)
     invariant {:yields} true;
     invariant call YieldInv();
@@ -39,28 +39,28 @@ preserves call YieldWait(tid);
       }
       par YieldInv() | YieldWait(tid) | YieldSlowPath(tid);
       if (oldValue == 2 || temp != 0) {
-        call WaitEnter(tid->val, 2);
+        call WaitEnter(tid, 2);
         par YieldInv() | YieldSlowPath(tid);
-        call WaitExit(tid->val);
+        call WaitExit(tid);
       }
       par YieldInv() | YieldWait(tid) | YieldSlowPath(tid);
       call oldValue := CmpXchg(0, 2);
       if (oldValue == 0) {
-        call {:layer 1} inSlowPath := Copy(inSlowPath[tid->val := false]);
+        call {:layer 1} inSlowPath := Copy(inSlowPath[tid := false]);
         break;
       }
     }
   }
-  call {:layer 1} mutex := Copy(Some(tid->val));
+  call {:layer 1} mutex := Copy(Some(tid));
 }
 
-atomic action {:layer 2} AtomicUnlock(tid: Lval Tid)
+atomic action {:layer 2} AtomicUnlock({:linear "tid"} tid: Tid)
 modifies mutex;
 {
-  assert mutex == Some(tid->val);
+  assert mutex == Some(tid);
   mutex := None();
 }
-yield procedure {:layer 1} Unlock(tid: Lval Tid)
+yield procedure {:layer 1} Unlock({:linear "tid"} tid: Tid)
 refines AtomicUnlock;
 preserves call YieldInv();
 preserves call YieldWait(tid);
@@ -70,13 +70,13 @@ preserves call YieldWait(tid);
   if (oldValue == 1) {
     call {:layer 1} mutex := Copy(None());
   } else {
-    call {:layer 1} inSlowPath := Copy(inSlowPath[tid->val := true]);
+    call {:layer 1} inSlowPath := Copy(inSlowPath[tid := true]);
     par YieldInv() | YieldWait(tid) | YieldSlowPath(tid);
     call Store(0);
     call {:layer 1} mutex := Copy(None());
     par YieldInv() | YieldWait(tid) | YieldSlowPath(tid);
     call Wake();
-    call {:layer 1} inSlowPath := Copy(inSlowPath[tid->val := false]);
+    call {:layer 1} inSlowPath := Copy(inSlowPath[tid := false]);
   }
 }
 
@@ -92,11 +92,11 @@ invariant (forall i: Tid :: futex->waiters[i] ==> inSlowPath[i]);
 invariant futex->word == 2 || futex->waiters == MapConst(false) || (exists i: Tid :: !futex->waiters[i] && inSlowPath[i]);
 invariant mutex == None() <==> futex->word == 0;
 
-yield invariant {:layer 1} YieldWait(tid: Lval Tid);
-invariant !futex->waiters[tid->val];
+yield invariant {:layer 1} YieldWait({:linear "tid"} tid: Tid);
+invariant !futex->waiters[tid];
 
-yield invariant {:layer 1} YieldSlowPath(tid: Lval Tid);
-invariant inSlowPath[tid->val];
+yield invariant {:layer 1} YieldSlowPath({:linear "tid"} tid: Tid);
+invariant inSlowPath[tid];
 
 /// Primitive atomic actions
 
diff --git a/Test/civl/samples/MutexOverFutex.bpl.expect b/Test/civl/samples/MutexOverFutex.bpl.expect
index 41374b000..00ddb38b4 100644
--- a/Test/civl/samples/MutexOverFutex.bpl.expect
+++ b/Test/civl/samples/MutexOverFutex.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/samples/alloc-mem.bpl b/Test/civl/samples/alloc-mem.bpl
index b3a98f59a..4d7f17df0 100644
--- a/Test/civl/samples/alloc-mem.bpl
+++ b/Test/civl/samples/alloc-mem.bpl
@@ -1,15 +1,19 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-function {:inline} PoolInv(unallocated:[int]bool, pool:Lset int) : (bool)
+type {:linear "mem"} X = int;
+function {:inline}{:linear "mem"} SetCollector(x: Set int): [int]bool { x->val }
+function {:inline}{:linear "mem"} MapCollector(x: Map int int): [int]bool { SetCollector(x->dom) }
+
+function {:inline} PoolInv(unallocated:[int]bool, pool:Set int) : (bool)
 {
-  (forall x:int :: unallocated[x] ==> Lset_Contains(pool, x))
+  (forall x:int :: unallocated[x] ==> Set_Contains(pool, x))
 }
 
 yield procedure {:layer 2} Main ()
 preserves call Yield();
 {
-  var {:layer 1,2} l:Lmap int int;
+  var {:layer 1,2} {:linear "mem"} l:Map int int;
   var i:int;
   while (*)
     invariant {:yields} true;
@@ -20,13 +24,13 @@ preserves call Yield();
   }
 }
 
-yield procedure {:layer 2} Thread ({:layer 1,2} {:linear_in} local_in:Lmap int int, i:int)
+yield procedure {:layer 2} Thread ({:layer 1,2} {:linear_in "mem"} local_in:Map int int, i:int)
 preserves call Yield();
-requires {:layer 1,2} Map_Contains(local_in->val, i);
+requires {:layer 1,2} Map_Contains(local_in, i);
 {
   var y, o:int;
-  var {:layer 1,2} local:Lmap int int;
-  var {:layer 1,2} l:Lmap int int;
+  var {:layer 1,2} {:linear "mem"} local:Map int int;
+  var {:layer 1,2} {:linear "mem"} l:Map int int;
 
   call local := Write(local_in, i, 42);
   call o := Read(local, i);
@@ -43,56 +47,55 @@ requires {:layer 1,2} Map_Contains(local_in->val, i);
   }
 }
 
-right action {:layer 2} atomic_Alloc() returns (l:Lmap int int, i:int)
+right action {:layer 2} atomic_Alloc() returns ({:linear "mem"} l:Map int int, i:int)
 modifies pool;
 {
-  assume Lset_Contains(pool, i);
+  assume Set_Contains(pool, i);
   call l, pool := AllocLinear(i, pool);
 }
 
 yield procedure {:layer 1}
-Alloc() returns ({:layer 1} l:Lmap int int, i:int)
+Alloc() returns ({:layer 1} {:linear "mem"} l:Map int int, i:int)
 refines atomic_Alloc;
 preserves call Yield();
-ensures {:layer 1} Map_Contains(l->val, i);
+ensures {:layer 1} Map_Contains(l, i);
 {
   call i := PickAddr();
   call {:layer 1} l, pool := AllocLinear(i, pool);
 }
 
-left action {:layer 2} atomic_Free({:linear_in} l:Lmap int int, i:int)
+left action {:layer 2} atomic_Free({:linear_in "mem"} l:Map int int, i:int)
 modifies pool;
 {
-  var t:Lset int;
-  assert Map_Contains(l->val, i);
-  call t := Lmap_Free(l);
-  call Lset_Put(pool, t);
+  assert Map_Contains(l, i);
+  pool := Set_Union(pool, l->dom);
 }
 
-yield procedure {:layer 1} Free({:layer 1} {:linear_in} l:Lmap int int, i:int)
+yield procedure {:layer 1} Free({:layer 1} {:linear_in "mem"} l:Map int int, i:int)
 refines atomic_Free;
-requires {:layer 1} Map_Contains(l->val, i);
+requires {:layer 1} Map_Contains(l, i);
 preserves call Yield();
 {
   call {:layer 1} pool := FreeLinear(l, i, pool);
   call ReturnAddr(i);
 }
 
-both action {:layer 2} atomic_Read (l:Lmap int int, i:int) returns (o:int)
+both action {:layer 2} atomic_Read ({:linear "mem"} l:Map int int, i:int) returns (o:int)
 {
-  assert Map_Contains(l->val, i);
-  o := l->val->val[i];
+  assert Map_Contains(l, i);
+  o := l->val[i];
 }
 
-both action {:layer 2} atomic_Write ({:linear_in} l:Lmap int int, i:int, o:int) returns (l':Lmap int int)
+both action {:layer 2} atomic_Write ({:linear_in "mem"} l:Map int int, i:int, o:int)
+  returns ({:linear "mem"} l':Map int int)
 {
-  assert Map_Contains(l->val, i);
+  assert Map_Contains(l, i);
   l' := l;
-  l'->val->val[i] := o;
+  l'->val[i] := o;
 }
 
 yield procedure {:layer 1}
-Read ({:layer 1} l:Lmap int int, i:int) returns (o:int)
+Read ({:layer 1} {:linear "mem"} l:Map int int, i:int) returns (o:int)
 refines atomic_Read;
 requires call YieldMem(l, i);
 ensures call Yield();
@@ -101,50 +104,49 @@ ensures call Yield();
 }
 
 yield procedure {:layer 1}
-Write ({:layer 1} {:linear_in} l:Lmap int int, i:int, o:int) returns ({:layer 1} l':Lmap int int)
+Write ({:layer 1} {:linear_in "mem"} l:Map int int, i:int, o:int)
+  returns ({:layer 1} {:linear "mem"} l':Map int int)
 refines atomic_Write;
 requires call Yield();
-requires {:layer 1} Map_Contains(l->val, i);
+requires {:layer 1} Map_Contains(l, i);
 ensures call YieldMem(l', i);
 {
   call WriteLow(i, o);
   call {:layer 1} l' := WriteLinear(l, i, o);
 }
 
-pure action AllocLinear (i:int, {:linear_in} pool:Lset int) returns (l:Lmap int int, pool':Lset int)
+pure action AllocLinear (i:int, {:linear_in "mem"} pool:Set int)
+  returns ({:linear "mem"} l:Map int int, {:linear "mem"} pool':Set int)
 {
   var m:[int]int;
-  var t:Lset int;
-  assert Lset_Contains(pool, i);
-  pool' := pool;
-  call t := Lset_Get(pool', MapOne(i));
-  call l := Lmap_Create(t, m);
+  assert Set_Contains(pool, i);
+  pool' := Set_Remove(pool, i);
+  l := Map(Set_Singleton(i), m);
 }
 
-pure action FreeLinear ({:linear_in} l:Lmap int int, i:int, {:linear_in} pool:Lset int) returns (pool':Lset int)
+pure action FreeLinear ({:linear_in "mem"} l:Map int int, i:int, {:linear_in "mem"} pool:Set int)
+  returns ({:linear "mem"} pool':Set int)
 {
-  var t: Lset int;
-  assert Map_Contains(l->val, i);
-  call t := Lmap_Free(l);
-  pool' := pool;
-  call Lset_Put(pool', t);
+  assert Map_Contains(l, i);
+  pool' := Set_Union(pool, l->dom);
 }
 
-pure action WriteLinear ({:layer 1} {:linear_in} l:Lmap int int, i:int, o:int) returns ({:layer 1} l':Lmap int int)
+pure action WriteLinear ({:layer 1} {:linear_in "mem"} l:Map int int, i:int, o:int)
+  returns ({:layer 1} {:linear "mem"} l':Map int int)
 {
-  assert Map_Contains(l->val, i);
+  assert Map_Contains(l, i);
   l' := l;
-  l'->val->val[i] := o;
+  l'->val[i] := o;
 }
 
 yield invariant {:layer 1} Yield ();
 invariant PoolInv(unallocated, pool);
 
-yield invariant {:layer 1} YieldMem ({:layer 1} l:Lmap int int, i:int);
+yield invariant {:layer 1} YieldMem ({:layer 1} {:linear "mem"} l:Map int int, i:int);
 invariant PoolInv(unallocated, pool);
-invariant Map_Contains(l->val, i) && Map_At(l->val, i) == mem[i];
+invariant Map_Contains(l, i) && Map_At(l, i) == mem[i];
 
-var {:layer 1, 2} pool:Lset int;
+var {:layer 1, 2} {:linear "mem"} pool:Set int;
 var {:layer 0, 1} mem:[int]int;
 var {:layer 0, 1} unallocated:[int]bool;
 
diff --git a/Test/civl/samples/alloc-mem.bpl.expect b/Test/civl/samples/alloc-mem.bpl.expect
index 0999d9ead..0c0d03d71 100644
--- a/Test/civl/samples/alloc-mem.bpl.expect
+++ b/Test/civl/samples/alloc-mem.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 13 verified, 0 errors
+Boogie program verifier finished with 20 verified, 0 errors
diff --git a/Test/civl/samples/bluetooth.bpl b/Test/civl/samples/bluetooth.bpl
index 13e91357c..5dd71c065 100644
--- a/Test/civl/samples/bluetooth.bpl
+++ b/Test/civl/samples/bluetooth.bpl
@@ -12,10 +12,12 @@ see cav2020-3.bpl for another example inspired by a concurrent
 garbage collector.
 */
 
-datatype Perm { Left(i: int), Right(i: int) }
+datatype {:linear "perm"} Perm { Left(i: int), Right(i: int) }
+
+function {:inline}{:linear "perm"} PermCollector(x: Set Perm): [Perm]bool { x->val }
 
 function Size<T>(set: [T]bool): int;
-axiom {:ctor "Lset"} (forall<T> set: [T]bool :: Size(set) >= 0);
+axiom (forall<T> set: [T]bool :: Size(set) >= 0);
 
 pure procedure SizeLemma<T>(X: [T]bool, x: T);
 ensures Size(X[x := false]) + 1 == Size(X[x := true]);
@@ -26,7 +28,7 @@ ensures X == Y || Size(X) < Size(Y);
 
 var {:layer 0,3} stoppingFlag: bool;
 var {:layer 0,2} stopped: bool;
-var {:layer 1,2} usersInDriver: Lset Perm;
+var {:layer 1,2} {:linear "perm"} usersInDriver: Set Perm;
 var {:layer 0,1} pendingIo: int;
 var {:layer 0,1} stoppingEvent: bool;
 
@@ -34,16 +36,16 @@ yield invariant {:layer 2} Inv2();
 invariant stopped ==> stoppingFlag;
 
 yield invariant {:layer 1} Inv1();
-invariant stoppingEvent ==> stoppingFlag && usersInDriver->dom == MapConst(false);
-invariant pendingIo == Size(usersInDriver->dom) + (if stoppingFlag then 0 else 1);
+invariant stoppingEvent ==> stoppingFlag && usersInDriver->val == MapConst(false);
+invariant pendingIo == Size(usersInDriver->val) + (if stoppingFlag then 0 else 1);
 
 // user code
 
 yield procedure {:layer 2}
-User(i: int, {:layer 1,2} l: Lval Perm, {:layer 1,2} r: Lval Perm)
+User(i: int, {:layer 1,2} {:linear "perm"} l: Set Perm, {:linear "perm"} {:layer 1,2} r: Set Perm)
 preserves call Inv2();
 preserves call Inv1();
-requires {:layer 1, 2} l->val == Left(i) && r->val == Right(i);
+requires {:layer 1, 2} l->val == MapOne(Left(i)) && r->val == MapOne(Right(i));
 {
     while (*)
     invariant {:yields} true;
@@ -56,56 +58,70 @@ requires {:layer 1, 2} l->val == Left(i) && r->val == Right(i);
     }
 }
 
-atomic action {:layer 2} AtomicEnter#1(i: int, {:linear_in} l: Lval Perm, r: Lval Perm)
+atomic action {:layer 2} AtomicEnter#1(i: int, {:linear_in "perm"} l: Set Perm, {:linear "perm"} r: Set Perm)
 modifies usersInDriver;
 {
     assume !stoppingFlag;
-    call Lval_Put(usersInDriver, l);
+    usersInDriver := Set_Union(usersInDriver, l);
 }
 yield procedure {:layer 1}
-Enter#1(i: int, {:layer 1} {:linear_in} l: Lval Perm, {:layer 1} r: Lval Perm)
+Enter#1(i: int, {:layer 1} {:linear_in "perm"} l: Set Perm, {:layer 1} {:linear "perm"} r: Set Perm)
 refines AtomicEnter#1;
 preserves call Inv1();
-requires {:layer 1} l->val == Left(i) && r->val == Right(i);
+requires {:layer 1} l->val == MapOne(Left(i)) && r->val == MapOne(Right(i));
 {
     call Enter();
-    call {:layer 1} SizeLemma(usersInDriver->dom, Left(i));
-    call {:layer 1} Lval_Put(usersInDriver, l);
+    call {:layer 1} SizeLemma(usersInDriver->val, Left(i));
+    call {:layer 1} usersInDriver := A(usersInDriver, l);
+}
+
+pure action A({:linear_in "perm"} usersInDriver: Set Perm, {:linear_in "perm"} l: Set Perm)
+  returns ({:linear "perm"} usersInDriver': Set Perm)
+{
+    usersInDriver' := Set_Union(usersInDriver, l);
 }
 
-left action {:layer 2} AtomicCheckAssert#1(i: int, r: Lval Perm)
+left action {:layer 2} AtomicCheckAssert#1(i: int, {:linear "perm"} r: Set Perm)
 {
-    assert r->val == Right(i) && usersInDriver->dom[Left(i)];
+    assert r->val == MapOne(Right(i)) && usersInDriver->val[Left(i)];
     assert !stopped;
 }
 yield procedure {:layer 1}
-CheckAssert#1(i: int, {:layer 1} r: Lval Perm)
+CheckAssert#1(i: int, {:layer 1} {:linear "perm"} r: Set Perm)
 refines AtomicCheckAssert#1;
 preserves call Inv1();
 {
     call CheckAssert();
 }
 
-left action {:layer 2} AtomicExit(i: int, {:linear_out} l: Lval Perm, r: Lval Perm)
+left action {:layer 2} AtomicExit(i: int, {:linear_out "perm"} l: Set Perm, {:linear "perm"} r: Set Perm)
 modifies usersInDriver;
 {
-    assert l->val == Left(i) && r->val == Right(i);
-    call Lval_Split(usersInDriver, l);
+    assert l->val == MapOne(Left(i)) && r->val == MapOne(Right(i));
+    call usersInDriver := B(usersInDriver, l);
 }
 yield procedure {:layer 1}
-Exit(i: int, {:layer 1} {:linear_out} l: Lval Perm, {:layer 1} r: Lval Perm)
+Exit(i: int, {:layer 1} {:linear_out "perm"} l: Set Perm, {:layer 1} {:linear "perm"} r: Set Perm)
 refines AtomicExit;
 preserves call Inv1();
 {
     call DeleteReference();
-    call {:layer 1} SizeLemma(usersInDriver->dom, Left(i));
-    call {:layer 1} Lval_Split(usersInDriver, l);
-    call {:layer 1} SubsetSizeRelationLemma(MapConst(false), usersInDriver->dom);
+    call {:layer 1} SizeLemma(usersInDriver->val, Left(i));
+    call {:layer 1} usersInDriver := B(usersInDriver, l);
+    call {:layer 1} SubsetSizeRelationLemma(MapConst(false), usersInDriver->val);
+}
+
+pure action B({:linear_in "perm"} usersInDriver: Set Perm, {:linear_out "perm"} l: Set Perm)
+  returns ({:linear "perm"} usersInDriver': Set Perm)
+{
+    assert Set_IsSubset(l, usersInDriver);
+    usersInDriver' := Set_Difference(usersInDriver, l);
 }
 
 // stopper code
+type {:linear "stopper"} X = int;
 
-yield procedure {:layer 2} Stopper(i: Lval int)
+yield procedure {:layer 2} Stopper({:linear "stopper"} i: int)
 refines AtomicSetStoppingFlag;
 preserves call Inv2();
 preserves call Inv1();
@@ -114,19 +130,19 @@ preserves call Inv1();
     call WaitAndStop();
 }
 
-yield procedure {:layer 1} Close(i: Lval int)
+yield procedure {:layer 1} Close({:linear "stopper"} i: int)
 refines AtomicSetStoppingFlag;
 preserves call Inv1();
 {
     call SetStoppingFlag(i);
     call DeleteReference();
-    call {:layer 1} SubsetSizeRelationLemma(MapConst(false), usersInDriver->dom);
+    call {:layer 1} SubsetSizeRelationLemma(MapConst(false), usersInDriver->val);
 }
 
 atomic action {:layer 2} AtomicWaitAndStop()
 modifies stopped;
 {
-    assume usersInDriver->dom == MapConst(false);
+    assume usersInDriver->val == MapConst(false);
     stopped := true;
 }
 yield procedure {:layer 1} WaitAndStop()
@@ -155,16 +171,16 @@ atomic action {:layer 1} AtomicCheckAssert()
 yield procedure {:layer 0} CheckAssert();
 refines AtomicCheckAssert;
 
-right action {:layer 1,3} AtomicSetStoppingFlag(i: Lval int)
+right action {:layer 1,3} AtomicSetStoppingFlag({:linear "stopper"} i: int)
 modifies stoppingFlag;
 {
     // The first assertion ensures that there is at most one stopper.
     // Otherwise AtomicSetStoppingFlag does not commute with itself.
-    assert i->val == 0;
+    assert i == 0;
     assert !stoppingFlag;
     stoppingFlag := true;
 }
-yield procedure {:layer 0} SetStoppingFlag(i: Lval int);
+yield procedure {:layer 0} SetStoppingFlag({:linear "stopper"} i: int);
 refines AtomicSetStoppingFlag;
 
 atomic action {:layer 1} AtomicDeleteReference()
diff --git a/Test/civl/samples/bluetooth.bpl.expect b/Test/civl/samples/bluetooth.bpl.expect
index dc45a0eee..c4cf5ccf4 100644
--- a/Test/civl/samples/bluetooth.bpl.expect
+++ b/Test/civl/samples/bluetooth.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 24 verified, 0 errors
+Boogie program verifier finished with 30 verified, 0 errors
diff --git a/Test/civl/samples/civl-paper.bpl b/Test/civl/samples/civl-paper.bpl
index ab7cd87f4..1c788662e 100644
--- a/Test/civl/samples/civl-paper.bpl
+++ b/Test/civl/samples/civl-paper.bpl
@@ -1,10 +1,14 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-type X;
+type {:linear "tid"} X;
 const nil: X;
 
-var {:layer 0,3} g: Lmap int int;
+type {:linear "mem"} Y = int;
+function {:inline}{:linear "mem"} SetCollector(x: Set int): [int]bool { x->val }
+function {:inline}{:linear "mem"} MapCollector(x: Map int int): [int]bool { SetCollector(x->dom) }
+
+var {:layer 0,3} {:linear "mem"} g: Map int int;
 var {:layer 0,3} lock: X;
 var {:layer 0,1} b: bool;
 
@@ -14,15 +18,15 @@ yield invariant {:layer 1} InvLock();
 invariant lock != nil <==> b;
 
 yield invariant {:layer 3} InvMem();
-invariant Map_Contains(g->val, p) && Map_Contains(g->val, p+4) && Map_At(g->val, p) == Map_At(g->val, p+4);
+invariant Map_Contains(g, p) && Map_Contains(g, p+4) && Map_At(g, p) == Map_At(g, p+4);
 
-yield procedure {:layer 3} P(tid: Lval X)
-requires {:layer 1,3} tid->val != nil;
+yield procedure {:layer 3} P({:linear "tid"} tid: X)
+requires {:layer 1,3} tid != nil;
 preserves call InvLock();
 preserves call InvMem();
 {
     var t: int;
-    var l: Lmap int int;
+    var {:linear "mem"} l: Map int int;
 
     call AcquireProtected(tid);
     call l := TransferFromGlobalProtected(tid);
@@ -34,60 +38,60 @@ preserves call InvMem();
     call ReleaseProtected(tid);
 }
 
-both action {:layer 3} AtomicTransferToGlobalProtected(tid: Lval X, {:linear_in} l: Lmap int int)
+both action {:layer 3} AtomicTransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: Map int int)
 modifies g;
-{ assert tid->val != nil && lock == tid->val; g := l; }
+{ assert tid != nil && lock == tid; g := l; }
 
 yield procedure {:layer 2}
-TransferToGlobalProtected(tid: Lval X, {:linear_in} l: Lmap int int)
+TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: Map int int)
 refines AtomicTransferToGlobalProtected;
 preserves call InvLock();
 {
   call TransferToGlobal(tid, l);
 }
 
-both action {:layer 3} AtomicTransferFromGlobalProtected(tid: Lval X) returns (l: Lmap int int)
+both action {:layer 3} AtomicTransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: Map int int)
 modifies g;
-{ assert tid->val != nil && lock == tid->val; l := g; call g := Lmap_Empty(); }
+{ assert tid != nil && lock == tid; l := g; g := Map_Empty(); }
 
 yield procedure {:layer 2}
-TransferFromGlobalProtected(tid: Lval X) returns (l: Lmap int int)
+TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: Map int int)
 refines AtomicTransferFromGlobalProtected;
 preserves call InvLock();
 {
   call l := TransferFromGlobal(tid);
 }
 
-right action {:layer 3} AtomicAcquireProtected(tid: Lval X)
+right action {:layer 3} AtomicAcquireProtected({:linear "tid"} tid: X)
 modifies lock;
-{ assert tid->val != nil; assume lock == nil; lock := tid->val; }
+{ assert tid != nil; assume lock == nil; lock := tid; }
 
-yield procedure {:layer 2} AcquireProtected(tid: Lval X)
+yield procedure {:layer 2} AcquireProtected({:linear "tid"} tid: X)
 refines AtomicAcquireProtected;
-requires {:layer 1} tid->val != nil;
+requires {:layer 1} tid != nil;
 preserves call InvLock();
 {
   call Acquire(tid);
 }
 
-left action {:layer 3} AtomicReleaseProtected(tid: Lval X)
+left action {:layer 3} AtomicReleaseProtected({:linear "tid"} tid: X)
 modifies lock;
-{ assert tid->val != nil && lock == tid->val; lock := nil; }
+{ assert tid != nil && lock == tid; lock := nil; }
 
-yield procedure {:layer 2} ReleaseProtected(tid: Lval X)
+yield procedure {:layer 2} ReleaseProtected({:linear "tid"} tid: X)
 refines AtomicReleaseProtected;
 preserves call InvLock();
 {
   call Release(tid);
 }
 
-atomic action {:layer 2} AtomicAcquire(tid: Lval X)
+atomic action {:layer 2} AtomicAcquire({:linear "tid"} tid: X)
 modifies lock;
-{ assume lock == nil; lock := tid->val; }
+{ assume lock == nil; lock := tid; }
 
-yield procedure {:layer 1} Acquire(tid: Lval X)
+yield procedure {:layer 1} Acquire({:linear "tid"} tid: X)
 refines AtomicAcquire;
-requires {:layer 1} tid->val != nil;
+requires {:layer 1} tid != nil;
 preserves call InvLock();
 {
     var status: bool;
@@ -97,48 +101,49 @@ preserves call InvLock();
     invariant {:yields} true;
     invariant call InvLock();
     {
-        call status := CAS(tid->val, false, true);
+        call status := CAS(tid, false, true);
         if (status) {
             return;
         }
     }
 }
 
-atomic action {:layer 2} AtomicRelease(tid: Lval X)
+atomic action {:layer 2} AtomicRelease({:linear "tid"} tid: X)
 modifies lock;
 { lock := nil; }
 
-yield procedure {:layer 1} Release(tid: Lval X)
+yield procedure {:layer 1} Release({:linear "tid"} tid: X)
 refines AtomicRelease;
 preserves call InvLock();
 {
-  call CLEAR(tid->val, false);
+  call CLEAR(tid, false);
 }
 
-atomic action {:layer 1,2} AtomicTransferToGlobal(tid: Lval X, {:linear_in} l: Lmap int int)
+atomic action {:layer 1,2} AtomicTransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: Map int int)
 modifies g;
 { g := l; }
 
-yield procedure {:layer 0} TransferToGlobal(tid: Lval X, {:linear_in} l: Lmap int int);
+yield procedure {:layer 0} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: Map int int);
 refines AtomicTransferToGlobal;
 
-atomic action {:layer 1,2} AtomicTransferFromGlobal(tid: Lval X) returns (l: Lmap int int)
+atomic action {:layer 1,2} AtomicTransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: Map int int)
 modifies g;
-{ l := g; call g := Lmap_Empty(); }
+{ l := g; g := Map_Empty(); }
 
-yield procedure {:layer 0} TransferFromGlobal(tid: Lval X) returns (l: Lmap int int);
+yield procedure {:layer 0} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: Map int int);
 refines AtomicTransferFromGlobal;
 
-both action {:layer 1,3} AtomicLoad(l: Lmap int int, a: int) returns (v: int)
-{ v := l->val->val[a]; }
+both action {:layer 1,3} AtomicLoad({:linear "mem"} l: Map int int, a: int) returns (v: int)
+{ v := l->val[a]; }
 
-yield procedure {:layer 0} Load(l: Lmap int int, a: int) returns (v: int);
+yield procedure {:layer 0} Load({:linear "mem"} l: Map int int, a: int) returns (v: int);
 refines AtomicLoad;
 
-both action {:layer 1,3} AtomicStore({:linear_in} l_in: Lmap int int, a: int, v: int) returns (l_out: Lmap int int)
-{ l_out := l_in; l_out->val->val[a] := v; }
+both action {:layer 1,3} AtomicStore({:linear_in "mem"} l_in: Map int int, a: int, v: int)
+  returns ({:linear "mem"} l_out: Map int int)
+{ l_out := l_in; l_out->val[a] := v; }
 
-yield procedure {:layer 0} Store({:linear_in} l_in: Lmap int int, a: int, v: int) returns (l_out: Lmap int int);
+yield procedure {:layer 0} Store({:linear_in "mem"} l_in: Map int int, a: int, v: int) returns ({:linear "mem"} l_out: Map int int);
 refines AtomicStore;
 
 atomic action {:layer 1} AtomicCAS(tid: X, prev: bool, next: bool) returns (status: bool)
diff --git a/Test/civl/samples/civl-paper.bpl.expect b/Test/civl/samples/civl-paper.bpl.expect
index 42111ae0b..129e60e25 100644
--- a/Test/civl/samples/civl-paper.bpl.expect
+++ b/Test/civl/samples/civl-paper.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 29 verified, 0 errors
+Boogie program verifier finished with 39 verified, 0 errors
diff --git a/Test/civl/samples/ticket.bpl b/Test/civl/samples/ticket.bpl
index cc21f0312..5a056e1e5 100644
--- a/Test/civl/samples/ticket.bpl
+++ b/Test/civl/samples/ticket.bpl
@@ -1,7 +1,7 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-type Tid;
+type {:linear "tid"} Tid;
 
 var {:layer 0,1} t: int;           // next ticket to issue
 var {:layer 0,2} s: int;           // current ticket permitted to critical section
@@ -24,8 +24,8 @@ function {:inline} Inv2 (tickets: [int]bool, ticket: int, lock: Option Tid): (bo
 // ###########################################################################
 // Yield invariants
 
-yield invariant {:layer 2} YieldSpec (tid: Lval Tid);
-invariant cs is Some && cs->t == tid->val;
+yield invariant {:layer 2} YieldSpec ({:linear "tid"} tid: Tid);
+invariant cs is Some && cs->t == tid;
 
 yield invariant {:layer 1} Yield1 ();
 invariant Inv1(T, t);
@@ -33,38 +33,10 @@ invariant Inv1(T, t);
 yield invariant {:layer 2} Yield2 ();
 invariant Inv2(T, s, cs);
 
-// ###########################################################################
-// Test driver
-
-yield procedure {:layer 2} main ({:layer 1,2} {:linear_in} _tids: Lset Tid)
-requires call Yield1();
-requires call Yield2();
-{
-  var {:layer 1,2} tid: Lval Tid;
-  var {:layer 1,2} tids: Lset Tid;
-
-  tids := _tids;
-  while (*)
-  invariant {:yields} true;
-  invariant call Yield1();
-  invariant call Yield2();
-  {
-    call {:layer 1,2} tid, tids := Allocate(tids);
-    async call Customer(tid);
-  }
-}
-
-pure procedure {:inline 1} Allocate({:linear_in} _tids: Lset Tid) returns (tid: Lval Tid, tids: Lset Tid)
-{
-  tids := _tids;
-  assume {:layer 1,2} tids->dom != MapConst(false);
-  call {:layer 1,2} tid := Lval_Get(tids, Choice(tids->dom));
-}
-
 // ###########################################################################
 // Procedures and actions
 
-yield procedure {:layer 2} Customer ({:layer 1,2} tid: Lval Tid)
+yield procedure {:layer 2} Customer ({:layer 1,2} {:linear "tid"} tid: Tid)
 requires call Yield1();
 requires call Yield2();
 {
@@ -79,7 +51,7 @@ requires call Yield2();
   }
 }
 
-yield procedure {:layer 2} Enter ({:layer 1,2} tid: Lval Tid)
+yield procedure {:layer 2} Enter ({:layer 1,2} {:linear "tid"} tid: Tid)
 preserves call Yield1();
 preserves call Yield2();
 ensures   call YieldSpec(tid);
@@ -90,10 +62,10 @@ ensures   call YieldSpec(tid);
   call WaitAndEnter(tid, m);
 }
 
-right action {:layer 2} AtomicGetTicket (tid: Lval Tid) returns (m: int)
+right action {:layer 2} AtomicGetTicket ({:linear "tid"} tid: Tid) returns (m: int)
 modifies T;
 { assume !T[m]; T[m] := true; }
-yield procedure {:layer 1} GetTicket ({:layer 1} tid: Lval Tid) returns (m: int)
+yield procedure {:layer 1} GetTicket ({:layer 1} {:linear "tid"} tid: Tid) returns (m: int)
 refines AtomicGetTicket;
 preserves call Yield1();
 {
@@ -107,15 +79,15 @@ modifies t;
 yield procedure {:layer 0} GetTicket#0 () returns (m: int);
 refines AtomicGetTicket#0;
 
-atomic action {:layer 2} AtomicWaitAndEnter (tid: Lval Tid, m:int)
+atomic action {:layer 2} AtomicWaitAndEnter ({:linear "tid"} tid: Tid, m:int)
 modifies cs;
-{ assume m == s; cs := Some(tid->val); }
-yield procedure {:layer 1} WaitAndEnter ({:layer 1} tid: Lval Tid, m:int)
+{ assume m == s; cs := Some(tid); }
+yield procedure {:layer 1} WaitAndEnter ({:layer 1} {:linear "tid"} tid: Tid, m:int)
 refines AtomicWaitAndEnter;
 preserves call Yield1();
 {
   call WaitAndEnter#0(m);
-  call {:layer 1} cs := Copy(Some(tid->val));
+  call {:layer 1} cs := Copy(Some(tid));
 }
 
 atomic action {:layer 1} AtomicWaitAndEnter#0 (m:int)
@@ -123,10 +95,10 @@ atomic action {:layer 1} AtomicWaitAndEnter#0 (m:int)
 yield procedure {:layer 0} WaitAndEnter#0 (m:int);
 refines AtomicWaitAndEnter#0;
 
-atomic action {:layer 2} AtomicLeave (tid: Lval Tid)
+atomic action {:layer 2} AtomicLeave ({:linear "tid"} tid: Tid)
 modifies cs, s;
-{ assert cs == Some(tid->val); s := s + 1; cs := None(); }
-yield procedure {:layer 1} Leave ({:layer 1} tid: Lval Tid)
+{ assert cs == Some(tid); s := s + 1; cs := None(); }
+yield procedure {:layer 1} Leave ({:layer 1} {:linear "tid"} tid: Tid)
 refines AtomicLeave;
 preserves call Yield1();
 {
diff --git a/Test/civl/samples/ticket.bpl.expect b/Test/civl/samples/ticket.bpl.expect
index 12041afe1..cccffe05d 100644
--- a/Test/civl/samples/ticket.bpl.expect
+++ b/Test/civl/samples/ticket.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 10 verified, 0 errors
+Boogie program verifier finished with 11 verified, 0 errors
diff --git a/Test/civl/samples/zeldovich.bpl b/Test/civl/samples/zeldovich.bpl
index 4959c6906..8bf80829a 100644
--- a/Test/civl/samples/zeldovich.bpl
+++ b/Test/civl/samples/zeldovich.bpl
@@ -1,7 +1,7 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-type Tid;
+type {:linear "tid"} Tid;
 const nil: Tid;
 
 var {:layer 0,1} lock_x: Tid;
@@ -9,30 +9,30 @@ var {:layer 0,1} lock_y: Tid;
 var {:layer 0,2} x: int;
 var {:layer 0,2} y: int;
 
-atomic action {:layer 2} GET_X (tid: Lval Tid) returns (v: int)
+atomic action {:layer 2} GET_X ({:linear "tid"} {:linear "tid"} tid: Tid) returns (v: int)
 {
   v := x;
 }
 
-atomic action {:layer 2} SET_BOTH (tid: Lval Tid, v: int, w: int)
+atomic action {:layer 2} SET_BOTH ({:linear "tid"} tid: Tid, v: int, w: int)
 modifies x, y;
 {
   x := v;
   y := w;
 }
 
-yield procedure {:layer 1} get_x (tid: Lval Tid) returns (v: int)
+yield procedure {:layer 1} get_x ({:linear "tid"} tid: Tid) returns (v: int)
 refines GET_X;
-requires {:layer 1} tid->val != nil;
+requires {:layer 1} tid != nil;
 {
   call acquire_x(tid);
   call v := read_x(tid);
   call release_x(tid);
 }
 
-yield procedure {:layer 1} set_both (tid: Lval Tid, v: int, w: int)
+yield procedure {:layer 1} set_both ({:linear "tid"} tid: Tid, v: int, w: int)
 refines SET_BOTH;
-requires {:layer 1} tid->val != nil;
+requires {:layer 1} tid != nil;
 {
   call acquire_x(tid);
   call acquire_y(tid);
@@ -42,73 +42,73 @@ requires {:layer 1} tid->val != nil;
   call release_y(tid);
 }
 
-right action {:layer 1} ACQUIRE_X (tid: Lval Tid)
+right action {:layer 1} ACQUIRE_X ({:linear "tid"} tid: Tid)
 modifies lock_x;
 {
-  assert tid->val != nil;
+  assert tid != nil;
   assume lock_x == nil;
-  lock_x := tid->val;
+  lock_x := tid;
 }
 
-left action {:layer 1} RELEASE_X (tid: Lval Tid)
+left action {:layer 1} RELEASE_X ({:linear "tid"} tid: Tid)
 modifies lock_x;
 {
-  assert tid->val != nil && lock_x == tid->val;
+  assert tid != nil && lock_x == tid;
   lock_x := nil;
 }
 
-right action {:layer 1} ACQUIRE_Y (tid: Lval Tid)
+right action {:layer 1} ACQUIRE_Y ({:linear "tid"} tid: Tid)
 modifies lock_y;
 {
-  assert tid->val != nil;
+  assert tid != nil;
   assume lock_y == nil;
-  lock_y := tid->val;
+  lock_y := tid;
 }
 
-left action {:layer 1} RELEASE_Y (tid: Lval Tid)
+left action {:layer 1} RELEASE_Y ({:linear "tid"} tid: Tid)
 modifies lock_y;
 {
-  assert tid->val != nil && lock_y == tid->val;
+  assert tid != nil && lock_y == tid;
   lock_y := nil;
 }
 
-both action {:layer 1} WRITE_X (tid: Lval Tid, v: int)
+both action {:layer 1} WRITE_X ({:linear "tid"} tid: Tid, v: int)
 modifies x;
 {
-  assert tid->val != nil && lock_x == tid->val;
+  assert tid != nil && lock_x == tid;
   x := v;
 }
 
-both action {:layer 1} WRITE_Y (tid: Lval Tid, v: int)
+both action {:layer 1} WRITE_Y ({:linear "tid"} tid: Tid, v: int)
 modifies y;
 {
-  assert tid->val != nil && lock_y == tid->val;
+  assert tid != nil && lock_y == tid;
   y := v;
 }
 
-both action {:layer 1} READ_X (tid: Lval Tid) returns (r: int)
+both action {:layer 1} READ_X ({:linear "tid"} tid: Tid) returns (r: int)
 {
-  assert tid->val != nil && lock_x == tid->val;
+  assert tid != nil && lock_x == tid;
   r := x;
 }
 
-yield procedure {:layer 0} acquire_x (tid: Lval Tid);
+yield procedure {:layer 0} acquire_x ({:linear "tid"} tid: Tid);
 refines ACQUIRE_X;
 
-yield procedure {:layer 0} acquire_y (tid: Lval Tid);
+yield procedure {:layer 0} acquire_y ({:linear "tid"} tid: Tid);
 refines ACQUIRE_Y;
 
-yield procedure {:layer 0} release_x (tid: Lval Tid);
+yield procedure {:layer 0} release_x ({:linear "tid"} tid: Tid);
 refines RELEASE_X;
 
-yield procedure {:layer 0} release_y (tid: Lval Tid);
+yield procedure {:layer 0} release_y ({:linear "tid"} tid: Tid);
 refines RELEASE_Y;
 
-yield procedure {:layer 0} write_x (tid: Lval Tid, v: int);
+yield procedure {:layer 0} write_x ({:linear "tid"} tid: Tid, v: int);
 refines WRITE_X;
 
-yield procedure {:layer 0} write_y (tid: Lval Tid, v: int);
+yield procedure {:layer 0} write_y ({:linear "tid"} tid: Tid, v: int);
 refines WRITE_Y;
 
-yield procedure {:layer 0} read_x (tid: Lval Tid) returns (r: int);
+yield procedure {:layer 0} read_x ({:linear "tid"} tid: Tid) returns (r: int);
 refines READ_X;
diff --git a/Test/civl/samples/zeldovich.bpl.expect b/Test/civl/samples/zeldovich.bpl.expect
index 1931ffd2c..bf98dae4d 100644
--- a/Test/civl/samples/zeldovich.bpl.expect
+++ b/Test/civl/samples/zeldovich.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 27 verified, 0 errors
+Boogie program verifier finished with 36 verified, 0 errors