diff --git a/Source/Concurrency/LinearDomainCollector.cs b/Source/Concurrency/LinearDomainCollector.cs
index c05d0c501..c54f76a46 100644
--- a/Source/Concurrency/LinearDomainCollector.cs
+++ b/Source/Concurrency/LinearDomainCollector.cs
@@ -140,7 +140,7 @@ private bool ContainsPermissionType(Type type)
         {
           var originalDecl = Monomorphizer.GetOriginalDecl(datatypeTypeCtorDecl);
           var originalDeclName = originalDecl.Name;
-          if (originalDeclName == "Lheap" || originalDeclName == "Lset" || originalDeclName == "Lval")
+          if (CivlPrimitives.LinearTypes.Contains(originalDeclName))
           {
             permissionTypes.Add(type);
             linearTypes.Add(type);
@@ -198,15 +198,13 @@ private Dictionary<Type, LinearDomain> MakeLinearDomains()
         }
         if (!permissionTypeToCollectors[permissionType].ContainsKey(type))
         {
-          var collector = 
-            originalTypeCtorDecl.Name == "Lheap"
-              ? program.monomorphizer.InstantiateFunction("Lheap_Collector",
-                new Dictionary<string, Type> { { "V", actualTypeParams[0] } }) :
-              originalTypeCtorDecl.Name == "Lset" 
-                ? program.monomorphizer.InstantiateFunction("Lset_Collector",
-                  new Dictionary<string, Type> { { "V", actualTypeParams[0] } }) :
-                program.monomorphizer.InstantiateFunction("Lval_Collector",
-                  new Dictionary<string, Type> { { "V", actualTypeParams[0] } });
+          var typeParamInstantiationMap = new Dictionary<string, Type> { { "V", actualTypeParams[0] } };
+          var collector =
+              originalTypeCtorDecl.Name == "Lheap"
+                ? program.monomorphizer.InstantiateFunction("Lheap_Collector", typeParamInstantiationMap) :
+              originalTypeCtorDecl.Name == "Lset"
+                ? program.monomorphizer.InstantiateFunction("Lset_Collector", typeParamInstantiationMap) :
+                program.monomorphizer.InstantiateFunction("Lval_Collector", typeParamInstantiationMap);
           permissionTypeToCollectors[permissionType].Add(type, collector);
         }
       }
diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs
index 9d12ac0e0..76b1bd694 100644
--- a/Source/Concurrency/LinearRewriter.cs
+++ b/Source/Concurrency/LinearRewriter.cs
@@ -18,7 +18,7 @@ public LinearRewriter(CivlTypeChecker civlTypeChecker)
   
   public static bool IsPrimitive(DeclWithFormals decl)
   {
-    return CivlPrimitives.Linear.Contains(Monomorphizer.GetOriginalDecl(decl).Name);
+    return CivlPrimitives.LinearPrimitives.Contains(Monomorphizer.GetOriginalDecl(decl).Name);
   }
 
   public static void Rewrite(CivlTypeChecker civlTypeChecker, Implementation impl)
@@ -52,10 +52,10 @@ public List<Cmd> RewriteCallCmd(CallCmd callCmd)
         return RewriteRefAlloc(callCmd);
       case "Lheap_Empty":
         return RewriteLheapEmpty(callCmd);
-      case "Lheap_Split":
-        return RewriteLheapSplit(callCmd);
-      case "Lheap_Transfer":
-        return RewriteLheapTransfer(callCmd);
+      case "Lheap_Get":
+        return RewriteLheapGet(callCmd);
+      case "Lheap_Put":
+        return RewriteLheapPut(callCmd);
       case "Lheap_Read":
         return RewriteLheapRead(callCmd);
       case "Lheap_Write":
@@ -68,12 +68,16 @@ public List<Cmd> RewriteCallCmd(CallCmd callCmd)
         return RewriteLsetEmpty(callCmd);
       case "Lset_Split":
         return RewriteLsetSplit(callCmd);
-      case "Lset_Transfer":
-        return RewriteLsetTransfer(callCmd);
+      case "Lset_Get":
+        return RewriteLsetGet(callCmd);
+      case "Lset_Put":
+        return RewriteLsetPut(callCmd);
       case "Lval_Split":
         return RewriteLvalSplit(callCmd);
-      case "Lval_Transfer":
-        return RewriteLvalTransfer(callCmd);
+      case "Lval_Get":
+        return RewriteLvalGet(callCmd);
+      case "Lval_Put":
+        return RewriteLvalPut(callCmd);
       default:
         Contract.Assume(false);
         return null;
@@ -184,7 +188,7 @@ private List<Cmd> RewriteLheapEmpty(CallCmd callCmd)
     return cmdSeq;
   }
   
-  private List<Cmd> RewriteLheapSplit(CallCmd callCmd)
+  private List<Cmd> RewriteLheapGet(CallCmd callCmd)
   {
     GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
       out Function lsetConstructor, out Function lvalConstructor);
@@ -202,7 +206,7 @@ private List<Cmd> RewriteLheapSplit(CallCmd callCmd)
     
     cmdSeq.Add(AssertCmd(callCmd.tok,
       Expr.Eq(ExprHelper.FunctionCall(mapImpFunc, k, Dom(path)), ExprHelper.FunctionCall(mapConstFunc1, Expr.True)),
-      "Lheap_Split failed"));
+      "Lheap_Get failed"));
     
     cmdSeq.Add(CmdHelper.AssignCmd(l,
       ExprHelper.FunctionCall(lheapConstructor, k,
@@ -217,22 +221,22 @@ private List<Cmd> RewriteLheapSplit(CallCmd callCmd)
     return cmdSeq;
   }
 
-  private List<Cmd> RewriteLheapTransfer(CallCmd callCmd)
+  private List<Cmd> RewriteLheapPut(CallCmd callCmd)
   {
     GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
       out Function lsetConstructor, out Function lvalConstructor);
 
     var cmdSeq = new List<Cmd>();
     var path = callCmd.Ins[0];
-    var path1 = callCmd.Ins[1];
+    var l = callCmd.Ins[1];
 
     var mapOrFunc = MapOr(refType);
     var mapIteFunc = MapIte(refType, type);
     cmdSeq.Add(CmdHelper.AssignCmd(
       CmdHelper.ExprToAssignLhs(path),
       ExprHelper.FunctionCall(lheapConstructor,
-        ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(path1)),
-        ExprHelper.FunctionCall(mapIteFunc, Dom(path), Val(path), Val(path1)))));
+        ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(l)),
+        ExprHelper.FunctionCall(mapIteFunc, Dom(path), Val(path), Val(l)))));
     
     ResolveAndTypecheck(options, cmdSeq);
     return cmdSeq;
@@ -308,16 +312,16 @@ private List<Cmd> RewriteLheapAlloc(CallCmd callCmd)
     var cmdSeq = new List<Cmd>();
     var path = callCmd.Ins[0];
     var v = callCmd.Ins[1];
-    var k = callCmd.Outs[0];
+    var l = callCmd.Outs[0];
 
-    cmdSeq.Add(CmdHelper.HavocCmd(k));
-    cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Neq(Val(k), ExprHelper.FunctionCall(nilFunc))));
-    cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Not(ExprHelper.FunctionCall(new MapSelect(callCmd.tok, 1), Dom(path), Val(k)))));
-    cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Eq(ExprHelper.FunctionCall(new MapSelect(callCmd.tok, 1), Val(path), Val(k)), v)));
+    cmdSeq.Add(CmdHelper.HavocCmd(l));
+    cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Neq(Val(l), ExprHelper.FunctionCall(nilFunc))));
+    cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Not(ExprHelper.FunctionCall(new MapSelect(callCmd.tok, 1), Dom(path), Val(l)))));
+    cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Eq(ExprHelper.FunctionCall(new MapSelect(callCmd.tok, 1), Val(path), Val(l)), v)));
     cmdSeq.Add(CmdHelper.AssignCmd(
       CmdHelper.ExprToAssignLhs(path),
       ExprHelper.FunctionCall(lheapConstructor,
-        ExprHelper.FunctionCall(new MapStore(callCmd.tok, 1), Dom(path), Val(k), Expr.True),
+        ExprHelper.FunctionCall(new MapStore(callCmd.tok, 1), Dom(path), Val(l), Expr.True),
         Val(path))));
     
     ResolveAndTypecheck(options, cmdSeq);
@@ -369,38 +373,64 @@ private List<Cmd> RewriteLsetSplit(CallCmd callCmd)
   {
     GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
       out Function lsetConstructor, out Function lvalConstructor);
-    
+
     var cmdSeq = new List<Cmd>();
     var path = callCmd.Ins[0];
-    var k = callCmd.Ins[1];
+    var l = callCmd.Ins[1];
 
     var mapConstFunc = MapConst(type, Type.Bool);
     var mapImpFunc = MapImp(type);
     cmdSeq.Add(AssertCmd(callCmd.tok,
-      Expr.Eq(ExprHelper.FunctionCall(mapImpFunc, Dom(k), Dom(path)), ExprHelper.FunctionCall(mapConstFunc, Expr.True)),
+      Expr.Eq(ExprHelper.FunctionCall(mapImpFunc, Dom(l), Dom(path)), ExprHelper.FunctionCall(mapConstFunc, Expr.True)),
       "Lset_Split failed"));
 
     var mapDiffFunc = MapDiff(type);
     cmdSeq.Add(
-      CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(path, "dom"),ExprHelper.FunctionCall(mapDiffFunc, Dom(path), Dom(k))));
-    
+      CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(path, "dom"),ExprHelper.FunctionCall(mapDiffFunc, Dom(path), Dom(l))));
+
+    ResolveAndTypecheck(options, cmdSeq);
+    return cmdSeq;
+  }
+
+  private List<Cmd> RewriteLsetGet(CallCmd callCmd)
+  {
+    GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
+      out Function lsetConstructor, out Function lvalConstructor);
+
+    var cmdSeq = new List<Cmd>();
+    var path = callCmd.Ins[0];
+    var k = callCmd.Ins[1];
+    var l = callCmd.Outs[0];
+
+    var mapConstFunc = MapConst(type, Type.Bool);
+    var mapImpFunc = MapImp(type);
+    cmdSeq.Add(AssertCmd(callCmd.tok,
+      Expr.Eq(ExprHelper.FunctionCall(mapImpFunc, k, Dom(path)), ExprHelper.FunctionCall(mapConstFunc, Expr.True)),
+      "Lset_Get failed"));
+
+    var mapDiffFunc = MapDiff(type);
+    cmdSeq.Add(
+      CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(path, "dom"),ExprHelper.FunctionCall(mapDiffFunc, Dom(path), k)));
+
+    cmdSeq.Add(CmdHelper.AssignCmd(l.Decl, ExprHelper.FunctionCall(lsetConstructor, k)));
+
     ResolveAndTypecheck(options, cmdSeq);
     return cmdSeq;
   }
 
-  private List<Cmd> RewriteLsetTransfer(CallCmd callCmd)
+  private List<Cmd> RewriteLsetPut(CallCmd callCmd)
   {
     GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
       out Function lsetConstructor, out Function lvalConstructor);
 
     var cmdSeq = new List<Cmd>();
     var path = callCmd.Ins[0];
-    var path1 = callCmd.Ins[1];
+    var l = callCmd.Ins[1];
 
     var mapOrFunc = MapOr(type);
     cmdSeq.Add(CmdHelper.AssignCmd(
       CmdHelper.ExprToAssignLhs(path),
-      ExprHelper.FunctionCall(lsetConstructor, ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(path1)))));
+      ExprHelper.FunctionCall(lsetConstructor, ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(l)))));
     
     ResolveAndTypecheck(options, cmdSeq);
     return cmdSeq;
@@ -413,22 +443,22 @@ private List<Cmd> RewriteLvalSplit(CallCmd callCmd)
 
     var cmdSeq = new List<Cmd>();
     var path = callCmd.Ins[0];
-    var k = callCmd.Ins[1];
+    var l = callCmd.Ins[1];
 
     var lsetContainsFunc = LsetContains(type);
-    cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(lsetContainsFunc, path, Val(k)), "Lval_Split failed"));
+    cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(lsetContainsFunc, path, Val(l)), "Lval_Split failed"));
 
     var mapOneFunc = MapOne(type);
     var mapDiffFunc = MapDiff(type);
     cmdSeq.Add(
       CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(path, "dom"),
-        ExprHelper.FunctionCall(mapDiffFunc, Dom(path), ExprHelper.FunctionCall(mapOneFunc, Val(k)))));
+        ExprHelper.FunctionCall(mapDiffFunc, Dom(path), ExprHelper.FunctionCall(mapOneFunc, Val(l)))));
     
     ResolveAndTypecheck(options, cmdSeq);
     return cmdSeq;
   }
   
-  private List<Cmd> RewriteLvalTransfer(CallCmd callCmd)
+  private List<Cmd> RewriteLvalGet(CallCmd callCmd)
   {
     GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
       out Function lsetConstructor, out Function lvalConstructor);
@@ -436,13 +466,38 @@ private List<Cmd> RewriteLvalTransfer(CallCmd callCmd)
     var cmdSeq = new List<Cmd>();
     var path = callCmd.Ins[0];
     var k = callCmd.Ins[1];
+    var l = callCmd.Outs[0];
+
+    var lsetContainsFunc = LsetContains(type);
+    cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(lsetContainsFunc, path, k), "Lval_Get failed"));
+
+    var mapOneFunc = MapOne(type);
+    var mapDiffFunc = MapDiff(type);
+    cmdSeq.Add(
+      CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(path, "dom"),
+        ExprHelper.FunctionCall(mapDiffFunc, Dom(path), ExprHelper.FunctionCall(mapOneFunc, k))));
+
+    cmdSeq.Add(CmdHelper.AssignCmd(l.Decl, ExprHelper.FunctionCall(lvalConstructor, k)));
+
+    ResolveAndTypecheck(options, cmdSeq);
+    return cmdSeq;
+  }
+
+  private List<Cmd> RewriteLvalPut(CallCmd callCmd)
+  {
+    GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
+      out Function lsetConstructor, out Function lvalConstructor);
+
+    var cmdSeq = new List<Cmd>();
+    var path = callCmd.Ins[0];
+    var l = callCmd.Ins[1];
     
     var mapOneFunc = MapOne(type);
     var mapOrFunc = MapOr(type);
     cmdSeq.Add(CmdHelper.AssignCmd(
       CmdHelper.ExprToAssignLhs(path),
       ExprHelper.FunctionCall(lsetConstructor,
-        ExprHelper.FunctionCall(mapOrFunc, Dom(path), ExprHelper.FunctionCall(mapOneFunc, Val(k))))));
+        ExprHelper.FunctionCall(mapOrFunc, Dom(path), ExprHelper.FunctionCall(mapOneFunc, Val(l))))));
     
     ResolveAndTypecheck(options, cmdSeq);
     return cmdSeq;
diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
index 11ce98984..e7a44037f 100644
--- a/Source/Core/AST/Absy.cs
+++ b/Source/Core/AST/Absy.cs
@@ -3273,10 +3273,9 @@ public override void Register(ResolutionContext rc)
 
     public override void Resolve(ResolutionContext rc)
     {
+      rc.Proc = this;
       base.Resolve(rc);
-
       var oldStateMode = rc.StateMode;
-      rc.Proc = this;
       rc.StateMode = ResolutionContext.State.Two;
       rc.PushVarContext();
       RegisterFormals(InParams, rc);
diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs
index b3e00dfbb..12a681e1b 100644
--- a/Source/Core/AST/AbsyCmd.cs
+++ b/Source/Core/AST/AbsyCmd.cs
@@ -3462,7 +3462,7 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
               // Check global outputs only; the checking of local outputs is done later
               var calleeLayer = Layers[0];
               var globalOutputs = Outs.Select(ie => ie.Decl).OfType<GlobalVariable>().Cast<Variable>();
-              if (CivlPrimitives.Linear.Contains(Proc.Name))
+              if (CivlPrimitives.LinearPrimitives.Contains(Proc.Name))
               {
                 var modifiedArgument = CivlPrimitives.ModifiedArgument(this);
                 if (modifiedArgument is { Decl: GlobalVariable })
@@ -3494,7 +3494,7 @@ private void TypecheckCallCmdInActionDecl(TypecheckingContext tc)
         return;
       }
 
-      if (CivlPrimitives.Linear.Contains(Proc.Name))
+      if (CivlPrimitives.LinearPrimitives.Contains(Proc.Name))
       {
         // ok
       }
@@ -3603,7 +3603,7 @@ public override void Typecheck(TypecheckingContext tc)
           }
         }
         // primitive calls have inout parameters that must be checked here
-        if (CivlPrimitives.Linear.Contains(Proc.Name))
+        if (CivlPrimitives.LinearPrimitives.Contains(Proc.Name))
         {
           var modifiedArgument = CivlPrimitives.ModifiedArgument(this);
           if (modifiedArgument == null)
diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs
index fd652352e..3dc7f1ddc 100644
--- a/Source/Core/CivlAttributes.cs
+++ b/Source/Core/CivlAttributes.cs
@@ -178,12 +178,14 @@ public static bool IsCallMarked(CallCmd callCmd)
 
   public static class CivlPrimitives
   {
-    public static HashSet<string> Linear = new()
+    public static HashSet<string> LinearTypes = new() { "Lheap", "Lset", "Lval" };
+
+    public static HashSet<string> LinearPrimitives = new()
     {
       "Ref_Alloc",
-      "Lheap_Empty", "Lheap_Split", "Lheap_Transfer", "Lheap_Read", "Lheap_Write", "Lheap_Alloc", "Lheap_Remove",
-      "Lset_Empty", "Lset_Split", "Lset_Transfer",
-      "Lval_Split", "Lval_Transfer"
+      "Lheap_Empty", "Lheap_Get", "Lheap_Put", "Lheap_Read", "Lheap_Write", "Lheap_Alloc", "Lheap_Remove",
+      "Lset_Empty", "Lset_Split", "Lset_Get", "Lset_Put",
+      "Lval_Split", "Lval_Get", "Lval_Put"
     };
 
     public static IdentifierExpr ExtractRootFromAccessPathExpr(Expr expr)
@@ -222,27 +224,24 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd)
           return null;
         case "Lheap_Empty":
           return null;
-        case "Lheap_Split":
-          return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
-        case "Lheap_Transfer":
+        case "Lheap_Get":
+        case "Lheap_Put":
           return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
         case "Lheap_Read":
           return null;
         case "Lheap_Write":
-          return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
         case "Lheap_Alloc":
-          return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
         case "Lheap_Remove":
           return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
         case "Lset_Empty":
           return null;
         case "Lset_Split":
-          return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
-        case "Lset_Transfer":
+        case "Lset_Get":
+        case "Lset_Put":
           return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
         case "Lval_Split":
-          return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
-        case "Lval_Transfer":
+        case "Lval_Get":
+        case "Lval_Put":
           return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
         default:
           throw new cce.UnreachableException();
diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl
index bd248ef1e..bc0a14644 100644
--- a/Source/Core/base.bpl
+++ b/Source/Core/base.bpl
@@ -266,11 +266,11 @@ function {:inline} Lheap_Deref<V>(l: Lheap V, k: Ref V): V {
     l->val[k]
 }
 pure procedure Lheap_Empty<V>() returns (l: Lheap V);
-pure procedure Lheap_Split<V>(path: Lheap V, k: [Ref V]bool) returns (l: Lheap V);
-pure procedure Lheap_Transfer<V>(path: Lheap V, {:linear_in} path1: Lheap V);
+pure procedure Lheap_Get<V>(path: Lheap V, k: [Ref V]bool) returns (l: Lheap V);
+pure procedure Lheap_Put<V>(path: Lheap V, {:linear_in} l: Lheap V);
 pure procedure Lheap_Read<V>(path: V) returns (v: V);
 pure procedure Lheap_Write<V>(path: V, v: V);
-pure procedure Lheap_Alloc<V>(path: Lheap V, v: V) returns (k: Lval (Ref V));
+pure procedure Lheap_Alloc<V>(path: Lheap V, v: V) returns (l: Lval (Ref V));
 pure procedure Lheap_Remove<V>(path: Lheap V, k: Ref V) returns (v: V);
 
 /// linear sets
@@ -282,9 +282,13 @@ function {:inline} Lset_Collector<V>(l: Lset V): [V]bool {
 function {:inline} Lset_Contains<V>(l: Lset V, k: V): bool {
     l->dom[k]
 }
+function {:inline} Lset_IsSubset<V>(k: Lset V, l: Lset V): bool {
+    IsSubset(k->dom, l->dom)
+}
 pure procedure Lset_Empty<V>() returns (l: Lset V);
-pure procedure Lset_Split<V>(path: Lset V, {:linear_out} k: Lset V);
-pure procedure Lset_Transfer<V>(path: Lset V, {:linear_in} path1: Lset V);
+pure procedure Lset_Split<V>(path: Lset V, {:linear_out} l: Lset V);
+pure procedure Lset_Get<V>(path: Lset V, k: [V]bool) returns (l: Lset V);
+pure procedure Lset_Put<V>(path: Lset V, {:linear_in} l: Lset V);
 
 /// linear vals
 datatype Lval<V> { Lval(val: V) }
@@ -292,8 +296,9 @@ datatype Lval<V> { Lval(val: V) }
 function {:inline} Lval_Collector<V>(l: Lval V): [V]bool {
     MapConst(false)[l->val := true]
 }
-pure procedure Lval_Split<V>(path: Lset V, {:linear_out} k: Lval V);
-pure procedure Lval_Transfer<V>(path: Lset V, {:linear_in} k: Lval V);
+pure procedure Lval_Split<V>(path: Lset V, {:linear_out} l: Lval V);
+pure procedure Lval_Get<V>(path: Lset V, k: V) returns (l: Lval V);
+pure procedure Lval_Put<V>(path: Lset V, {:linear_in} l: Lval V);
 
 procedure create_async<T>(PA: T);
 procedure create_asyncs<T>(PAs: [T]bool);
diff --git a/Test/civl/regression-tests/assert-layers.bpl b/Test/civl/regression-tests/assert-layers.bpl
new file mode 100644
index 000000000..45700d2bd
--- /dev/null
+++ b/Test/civl/regression-tests/assert-layers.bpl
@@ -0,0 +1,9 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+yield procedure {:layer 1} foo()
+requires false;
+ensures false;
+{
+  assert false;
+}
\ No newline at end of file
diff --git a/Test/civl/regression-tests/assert-layers.bpl.expect b/Test/civl/regression-tests/assert-layers.bpl.expect
new file mode 100644
index 000000000..bcb2c6cd7
--- /dev/null
+++ b/Test/civl/regression-tests/assert-layers.bpl.expect
@@ -0,0 +1,4 @@
+assert-layers.bpl(5,0): Error: expected layers
+assert-layers.bpl(6,0): Error: expected layers
+assert-layers.bpl(8,2): Error: expected layers
+3 name resolution errors detected in assert-layers.bpl
diff --git a/Test/civl/regression-tests/dir_request.bpl b/Test/civl/regression-tests/dir_request.bpl
index ce37c9bd7..a17996797 100644
--- a/Test/civl/regression-tests/dir_request.bpl
+++ b/Test/civl/regression-tests/dir_request.bpl
@@ -19,6 +19,6 @@ modifies X, B;
     var i: int;
     i := li->val;
     assert B[i];
-    call Lval_Transfer(X, li);
+    call Lval_Put(X, li);
     B[i] := false;
 }
diff --git a/Test/civl/regression-tests/linear-test.bpl b/Test/civl/regression-tests/linear-test.bpl
index 75c112dd1..92ad397bb 100644
--- a/Test/civl/regression-tests/linear-test.bpl
+++ b/Test/civl/regression-tests/linear-test.bpl
@@ -3,7 +3,25 @@
 
 type {:linear "A"} A = int;
 
-yield procedure {:layer 1} foo({:linear "A"} x: int, {:linear "A"} y: int)
+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 37fad75c9..a9949f2e7 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 1 verified, 0 errors
+Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/civl/regression-tests/linear_types.bpl b/Test/civl/regression-tests/linear_types.bpl
index 163f59baf..85a2cdf30 100644
--- a/Test/civl/regression-tests/linear_types.bpl
+++ b/Test/civl/regression-tests/linear_types.bpl
@@ -3,13 +3,13 @@
 
 atomic action {:layer 1, 2} A0({:linear_in} path: Lheap int, k: [Ref int]bool) returns (path': Lheap int, l: Lheap int) {
     call path' := Lheap_Empty();
-    call Lheap_Transfer(path', path);
-    call l := Lheap_Split(path', k);
+    call Lheap_Put(path', path);
+    call l := Lheap_Get(path', k);
 }
 
 atomic action {:layer 1, 2} A1({:linear_in} path: Lheap int, k: Ref int, v: int) returns (path': Lheap int, v': int) {
     call path' := Lheap_Empty();
-    call Lheap_Transfer(path', path);
+    call Lheap_Put(path', path);
     call Lheap_Write(path'->val[k], v);
     call v' := Lheap_Read(path'->val[k]);
 }
@@ -23,14 +23,14 @@ atomic action {:layer 1, 2} A2(v: int) returns (path': Lheap int, v': int) {
 
 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_Transfer(path', path);
+    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_Transfer(path', path);
-    call Lval_Transfer(path', l);
+    call Lset_Put(path', path);
+    call Lval_Put(path', l);
     call Lval_Split(path', l);
 }
 
@@ -44,7 +44,7 @@ atomic action {:layer 1, 2} A6({:linear_in} path: Lheap int) returns (path': Lhe
 modifies g;
 {
     path' := path;
-    call Lheap_Transfer(path', g);
+    call Lheap_Put(path', g);
     call g := Lheap_Empty();
 }
 
@@ -54,7 +54,7 @@ atomic action {:layer 1, 2} A7({:linear_in} path: Lheap Foo, x: Ref Foo, y: Ref
 {
     var l: Lheap int;
     path' := path;
-    call l := Lheap_Split(path'->val[x]->f, MapOne(y));
+    call l := Lheap_Get(path'->val[x]->f, MapOne(y));
 }
 
 atomic action {:layer 1, 2} A8({:linear_out} l: Lval int, {:linear_in} path: Lset int) returns (path': Lset int)
@@ -66,7 +66,7 @@ atomic action {:layer 1, 2} A8({:linear_out} l: Lval int, {:linear_in} path: Lse
 atomic action {:layer 1, 2} A9({:linear_in} path1: Lheap int, x: Ref Foo) returns (path2: Lheap Foo)
 {
     call path2 := Lheap_Empty();
-    call Lheap_Transfer(path2->val[x]->f, path1);
+    call Lheap_Put(path2->val[x]->f, path1);
 }
 
 atomic action {:layer 1, 2} A10({:linear_in} a: Foo) returns (b: Foo)
diff --git a/Test/civl/regression-tests/linear_types_error.bpl b/Test/civl/regression-tests/linear_types_error.bpl
index 02c931886..23e158117 100644
--- a/Test/civl/regression-tests/linear_types_error.bpl
+++ b/Test/civl/regression-tests/linear_types_error.bpl
@@ -9,7 +9,7 @@ atomic action {:layer 1, 2} A1(path: Lheap int) returns (path': Lheap int) {
 
 atomic action {:layer 1, 2} A2(path: Lheap int) returns (path': Lheap int) {
     call path' := Lheap_Empty();
-    call Lheap_Transfer(path', path);
+    call Lheap_Put(path', path);
 }
 
 var {:layer 0, 2} g: Lheap int;
@@ -17,7 +17,7 @@ var {:layer 0, 2} g: Lheap int;
 atomic action {:layer 1, 2} A3({:linear_in} path: Lheap int) returns (path': Lheap int)
 {
     path' := path;
-    call Lheap_Transfer(path', g);
+    call Lheap_Put(path', g);
 }
 
 datatype Foo { Foo(f: Lheap int) }
@@ -27,7 +27,7 @@ atomic action {:layer 1, 2} A4({:linear_in} path: Lheap Foo, x: Ref Foo, {:linea
 {
     path' := path;
     l' := l;
-    call Lheap_Transfer(l', path'->val[x]->f);
+    call Lheap_Put(l', path'->val[x]->f);
 }
 
 atomic action {:layer 1, 2} A5({:linear_out} path: Lheap int) { }
@@ -35,28 +35,28 @@ atomic action {:layer 1, 2} A5({:linear_out} path: Lheap int) { }
 atomic action {:layer 1, 2} A6({:linear_in} path: Lheap int) returns (path': Lheap int)
 {
     path' := path;
-    call Lheap_Transfer(path', path');
+    call Lheap_Put(path', path');
 }
 
 atomic action {:layer 1, 2} A7(path1: Lheap int, {:linear_in} path2: Lheap int) returns (path': Lheap int)
 {
     path' := path2;
-    call Lheap_Transfer(path', path1);
+    call Lheap_Put(path', path1);
 }
 
 atomic action {:layer 1, 2} A8({:linear_in} path1: Lheap int, x: Ref Foo) returns (path2: Lheap Foo)
 {
-    call Lheap_Transfer(path2->val[x]->f, path1);
+    call Lheap_Put(path2->val[x]->f, path1);
 }
 
 atomic action {:layer 1, 2} A9({:linear_in} l: Lheap int)
 {
-    call Lheap_Transfer(g, l);
+    call Lheap_Put(g, l);
 }
 
 atomic action {:layer 1, 2} A10({:linear_in} l: Lheap int, l': Lheap int)
 {
-    call Lheap_Transfer(l', l);
+    call Lheap_Put(l', l);
 }
 
 atomic action {:layer 1, 2} A11({:linear_in} a: Foo) returns (b: Foo)
diff --git a/Test/civl/regression-tests/linear_types_error.bpl.expect b/Test/civl/regression-tests/linear_types_error.bpl.expect
index d738b7e58..ac64bcea0 100644
--- a/Test/civl/regression-tests/linear_types_error.bpl.expect
+++ b/Test/civl/regression-tests/linear_types_error.bpl.expect
@@ -7,7 +7,7 @@ linear_types_error.bpl(30,4): Error: Only variable can be passed to linear param
 linear_types_error.bpl(33,64): Error: Input variable path must be available at a return
 linear_types_error.bpl(38,4): Error: Linear variable path' can occur only once as an input parameter
 linear_types_error.bpl(45,0): Error: Input variable path1 must be available at a return
-linear_types_error.bpl(49,24): Error: unavailable source path2 for linear parameter at position 0
+linear_types_error.bpl(49,19): Error: unavailable source path2 for linear parameter at position 0
 linear_types_error.bpl(50,0): Error: Output variable path2 must be available at a return
 linear_types_error.bpl(54,4): Error: Primitive assigns to a global variable that is not in the enclosing action's modifies clause: g
 linear_types_error.bpl(59,4): Error: Primitive assigns to input variable: l'
diff --git a/Test/civl/samples/alloc-mem.bpl b/Test/civl/samples/alloc-mem.bpl
index 0a3d6076a..67e735f4b 100644
--- a/Test/civl/samples/alloc-mem.bpl
+++ b/Test/civl/samples/alloc-mem.bpl
@@ -10,9 +10,6 @@ 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);
 axiom (forall x: lmap :: {dom(x)} {map(x)} cons(dom(x), map(x)) == x);
 
-function Empty(m:[int]int) : lmap;
-axiom (forall m: [int]int :: Empty(m) == cons(MapConst(false), m));
-
 function Add(x:lmap, i:int): lmap;
 axiom (forall x:lmap, i:int :: dom(Add(x, i)) == dom(x)[i:=true] && map(Add(x, i)) == map(x));
 
@@ -39,9 +36,8 @@ preserves call Yield();
 }
 
 yield procedure {:layer 2} Thread ({:layer 1,2} {:linear_in "mem"} local_in:lmap, i:int)
-requires call YieldMem(local_in, i);
-ensures call Yield();
-requires {:layer 2} dom(local_in)[i];
+preserves call Yield();
+requires {:layer 1,2} dom(local_in)[i];
 {
   var y, o:int;
   var {:layer 1,2} {:linear "mem"} local:lmap;
@@ -65,20 +61,18 @@ requires {:layer 2} dom(local_in)[i];
 right action {:layer 2} atomic_Alloc() returns ({:linear "mem"} l:lmap, i:int)
 modifies pool;
 {
-  var m:[int]int;
   assume dom(pool)[i];
-  pool := Remove(pool, i);
-  l := Add(Empty(m), i);
+  call l, pool := AllocLinear(i, pool);
 }
 
 yield procedure {:layer 1}
 Alloc() returns ({:layer 1} {:linear "mem"} l:lmap, i:int)
 refines atomic_Alloc;
-requires call Yield();
-ensures call YieldMem(l, i);
+preserves call Yield();
+ensures {:layer 1} dom(l)[i];
 {
   call i := PickAddr();
-  call {:layer 1} l, pool := AllocLinear(i, Add(Empty(mem), i), pool);
+  call {:layer 1} l, pool := AllocLinear(i, pool);
 }
 
 left action {:layer 2} atomic_Free({:linear_in "mem"} l:lmap, i:int)
@@ -121,18 +115,20 @@ ensures call Yield();
 yield procedure {:layer 1}
 Write ({:layer 1} {:linear_in "mem"} l:lmap, i:int, o:int) returns ({:layer 1} {:linear "mem"} l':lmap)
 refines atomic_Write;
-requires call YieldMem(l, i);
+requires call Yield();
+requires {:layer 1} dom(l)[i];
 ensures call YieldMem(l', i);
 {
   call WriteLow(i, o);
   call {:layer 1} l' := WriteLinear(l, i, o);
 }
 
-pure action AllocLinear (i:int, _l:lmap, {:linear_in "mem"} pool:lmap) returns ({:linear "mem"} l:lmap, {:linear "mem"} pool':lmap)
+pure action AllocLinear (i:int, {:linear_in "mem"} pool:lmap) returns ({:linear "mem"} l:lmap, {:linear "mem"} pool':lmap)
 {
-  assert dom(pool)[i] && dom(_l) == MapConst(false)[i := true];
+  var m:[int]int;
+  assert dom(pool)[i];
   pool' := Remove(pool, i);
-  l := _l;
+  l := cons(MapConst(false)[i := true], m);
 }
 
 pure action FreeLinear ({:linear_in "mem"} l:lmap, i:int, {:linear_in "mem"} pool:lmap) returns ({:linear "mem"} pool':lmap)
diff --git a/Test/civl/samples/alloc-mem.bpl.expect b/Test/civl/samples/alloc-mem.bpl.expect
index fde7e7129..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 18 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 d66bbbebf..13e91357c 100644
--- a/Test/civl/samples/bluetooth.bpl
+++ b/Test/civl/samples/bluetooth.bpl
@@ -60,7 +60,7 @@ atomic action {:layer 2} AtomicEnter#1(i: int, {:linear_in} l: Lval Perm, r: Lva
 modifies usersInDriver;
 {
     assume !stoppingFlag;
-    call Lval_Transfer(usersInDriver, l);
+    call Lval_Put(usersInDriver, l);
 }
 yield procedure {:layer 1}
 Enter#1(i: int, {:layer 1} {:linear_in} l: Lval Perm, {:layer 1} r: Lval Perm)
@@ -70,7 +70,7 @@ requires {:layer 1} l->val == Left(i) && r->val == Right(i);
 {
     call Enter();
     call {:layer 1} SizeLemma(usersInDriver->dom, Left(i));
-    call {:layer 1} Lval_Transfer(usersInDriver, l);
+    call {:layer 1} Lval_Put(usersInDriver, l);
 }
 
 left action {:layer 2} AtomicCheckAssert#1(i: int, r: Lval Perm)