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..63170a0f9 100644
--- a/Test/civl/regression-tests/linear-test.bpl
+++ b/Test/civl/regression-tests/linear-test.bpl
@@ -8,15 +8,6 @@ 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);
 {
diff --git a/Test/civl/regression-tests/linear-test.bpl.expect b/Test/civl/regression-tests/linear-test.bpl.expect
index a9949f2e7..41374b000 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 2 verified, 0 errors
diff --git a/Test/civl/regression-tests/linear_types.bpl b/Test/civl/regression-tests/linear_types.bpl
index 2060cb3f0..ac148f18b 100644
--- a/Test/civl/regression-tests/linear_types.bpl
+++ b/Test/civl/regression-tests/linear_types.bpl
@@ -7,13 +7,6 @@ atomic action {:layer 1, 2} A3({:linear_in} path: Lset int, {:linear_out} l: Lse
     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;
 }
@@ -22,22 +15,9 @@ 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
index 88f607a61..a8891f09a 100644
--- a/Test/civl/regression-tests/linear_types_error.bpl
+++ b/Test/civl/regression-tests/linear_types_error.bpl
@@ -37,16 +37,6 @@ atomic action {:layer 1, 2} A13({:linear_in} a: Foo) returns (b: Foo)
     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);
diff --git a/Test/civl/regression-tests/linear_types_error.bpl.expect b/Test/civl/regression-tests/linear_types_error.bpl.expect
index 891e35034..e6d2f50df 100644
--- a/Test/civl/regression-tests/linear_types_error.bpl.expect
+++ b/Test/civl/regression-tests/linear_types_error.bpl.expect
@@ -1,4 +1,3 @@
-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
@@ -6,7 +5,6 @@ linear_types_error.bpl(19,64): Error: Input variable path must be available at a
 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
+linear_types_error.bpl(42,2): Error: Linear variable x can occur only once as an input parameter
+linear_types_error.bpl(47,2): Error: Linear variable x can occur only once as an input parameter
+9 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/bluetooth.bpl b/Test/civl/samples/bluetooth.bpl
index 13e91357c..b74205853 100644
--- a/Test/civl/samples/bluetooth.bpl
+++ b/Test/civl/samples/bluetooth.bpl
@@ -40,10 +40,10 @@ invariant pendingIo == Size(usersInDriver->dom) + (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} l: Lset Perm, {:layer 1,2} r: Lset Perm)
 preserves call Inv2();
 preserves call Inv1();
-requires {:layer 1, 2} l->val == Left(i) && r->val == Right(i);
+requires {:layer 1, 2} l->dom == MapOne(Left(i)) && r->dom == MapOne(Right(i));
 {
     while (*)
     invariant {:yields} true;
@@ -56,56 +56,57 @@ 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} l: Lset Perm, r: Lset Perm)
 modifies usersInDriver;
 {
     assume !stoppingFlag;
-    call Lval_Put(usersInDriver, l);
+    call Lset_Put(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} l: Lset Perm, {:layer 1} r: Lset Perm)
 refines AtomicEnter#1;
 preserves call Inv1();
-requires {:layer 1} l->val == Left(i) && r->val == Right(i);
+requires {:layer 1} l->dom == MapOne(Left(i)) && r->dom == MapOne(Right(i));
 {
     call Enter();
     call {:layer 1} SizeLemma(usersInDriver->dom, Left(i));
-    call {:layer 1} Lval_Put(usersInDriver, l);
+    call {:layer 1} Lset_Put(usersInDriver, l);
 }
 
-left action {:layer 2} AtomicCheckAssert#1(i: int, r: Lval Perm)
+left action {:layer 2} AtomicCheckAssert#1(i: int, r: Lset Perm)
 {
-    assert r->val == Right(i) && usersInDriver->dom[Left(i)];
+    assert r->dom == MapOne(Right(i)) && usersInDriver->dom[Left(i)];
     assert !stopped;
 }
 yield procedure {:layer 1}
-CheckAssert#1(i: int, {:layer 1} r: Lval Perm)
+CheckAssert#1(i: int, {:layer 1} r: Lset 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} l: Lset Perm, r: Lset Perm)
 modifies usersInDriver;
 {
-    assert l->val == Left(i) && r->val == Right(i);
-    call Lval_Split(usersInDriver, l);
+    assert l->dom == MapOne(Left(i)) && r->dom == MapOne(Right(i));
+    call Lset_Split(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} l: Lset Perm, {:layer 1} r: Lset 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} Lset_Split(usersInDriver, l);
     call {:layer 1} SubsetSizeRelationLemma(MapConst(false), usersInDriver->dom);
 }
 
 // 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,7 +115,7 @@ 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();
 {
@@ -155,16 +156,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..d4fb07c44 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 25 verified, 0 errors
diff --git a/Test/civl/samples/civl-paper.bpl b/Test/civl/samples/civl-paper.bpl
index ab7cd87f4..83019099b 100644
--- a/Test/civl/samples/civl-paper.bpl
+++ b/Test/civl/samples/civl-paper.bpl
@@ -1,7 +1,7 @@
 // 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;
@@ -16,8 +16,8 @@ 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);
 
-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();
 {
@@ -34,60 +34,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} l: Lmap 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} l: Lmap 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 (l: Lmap int int)
 modifies g;
-{ assert tid->val != nil && lock == tid->val; l := g; call g := Lmap_Empty(); }
+{ assert tid != nil && lock == tid; l := g; call g := Lmap_Empty(); }
 
 yield procedure {:layer 2}
-TransferFromGlobalProtected(tid: Lval X) returns (l: Lmap int int)
+TransferFromGlobalProtected({:linear "tid"} tid: X) returns (l: Lmap 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,36 +97,36 @@ 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} l: Lmap 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} l: Lmap 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 (l: Lmap int int)
 modifies g;
 { l := g; call g := Lmap_Empty(); }
 
-yield procedure {:layer 0} TransferFromGlobal(tid: Lval X) returns (l: Lmap int int);
+yield procedure {:layer 0} TransferFromGlobal({:linear "tid"} tid: X) returns (l: Lmap int int);
 refines AtomicTransferFromGlobal;
 
 both action {:layer 1,3} AtomicLoad(l: Lmap int int, a: int) returns (v: int)
diff --git a/Test/civl/samples/civl-paper.bpl.expect b/Test/civl/samples/civl-paper.bpl.expect
index 42111ae0b..103f21a1e 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 37 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