diff --git a/Source/Concurrency/CivlCoreTypes.cs b/Source/Concurrency/CivlCoreTypes.cs
index 8ce15a01f..598613278 100644
--- a/Source/Concurrency/CivlCoreTypes.cs
+++ b/Source/Concurrency/CivlCoreTypes.cs
@@ -186,8 +186,8 @@ private Function ComputeInputOutputRelation(CivlTypeChecker civlTypeChecker, Imp
       var existsVars = foroldMap.Values
         .Concat(alwaysMap.Keys.Where(key => key is GlobalVariable).Select(key => alwaysMap[key]))
         .OfType<IdentifierExpr>().Select(ie => ie.Decl).ToList();
-      inputOutputRelation.Body =
-        ExprHelper.ExistsExpr(existsVars, Expr.And(gateExprs.Append(transitionRelationExpr)));
+      var expr = Expr.And(gateExprs.Append(transitionRelationExpr));
+      inputOutputRelation.Body = existsVars.Any() ? ExprHelper.ExistsExpr(existsVars, expr) : expr;
       CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, inputOutputRelation.Body);
       return inputOutputRelation;
     }
diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
index a123a36d6..a7c883c03 100644
--- a/Source/Concurrency/CivlTypeChecker.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -16,7 +16,6 @@ public class CivlTypeChecker
     private Dictionary<ActionDecl, Action> actionDeclToAction;
     private List<Sequentialization> sequentializations;
     private Dictionary<Implementation, Dictionary<CtorType, Variable>> implToPendingAsyncCollectors;
-    private HashSet<ActionDecl> linkActionDecls;
     private string namePrefix;
 
     public CivlTypeChecker(ConcurrencyOptions options, Program program)
@@ -33,7 +32,6 @@ public CivlTypeChecker(ConcurrencyOptions options, Program program)
       this.actionDeclToAction = new Dictionary<ActionDecl, Action>();
       this.sequentializations = new List<Sequentialization>();
       this.implToPendingAsyncCollectors = new Dictionary<Implementation, Dictionary<CtorType, Variable>>();
-      this.linkActionDecls = new HashSet<ActionDecl>();
 
       IEnumerable<string> declNames = program.TopLevelDeclarations.OfType<NamedDeclaration>().Select(x => x.Name);
       IEnumerable<string> localVarNames = VariableNameCollector.Collect(program);
@@ -49,8 +47,8 @@ public CivlTypeChecker(ConcurrencyOptions options, Program program)
         }
       }
 
-      SkipActionDecl = new ActionDecl(Token.NoToken, AddNamePrefix("Skip"), MoverType.Both,
-        new List<Variable>(), new List<Variable>(), new List<ActionDeclRef>(), null, null, new List<ElimDecl>(),
+      SkipActionDecl = new ActionDecl(Token.NoToken, AddNamePrefix("Skip"), MoverType.Both, new List<Variable>(),
+        new List<Variable>(), true, new List<ActionDeclRef>(), null, null, new List<ElimDecl>(),
         new List<IdentifierExpr>(), null, null);
       var skipImplementation = DeclHelper.Implementation(
         SkipActionDecl,
@@ -294,10 +292,6 @@ private void TypeCheckYieldingProcedures()
             }
           }
         }
-        impl.Blocks.ForEach(block =>
-        {
-          block.Cmds.OfType<CallCmd>().Select(callCmd => callCmd.Proc).OfType<ActionDecl>().ForEach(actionDecl => linkActionDecls.Add(actionDecl));
-        });
       }
     }
     
@@ -454,9 +448,6 @@ private void MatchFormals(List<Variable> formals1, List<Variable> formals2, stri
     #region Public access methods
 
     public IEnumerable<Variable> GlobalVariables => program.GlobalVariables;
-    
-    public IEnumerable<Action> LinkActions =>
-      actionDeclToAction.Values.Where(action => linkActionDecls.Contains(action.ActionDecl));
 
     public IEnumerable<Action> MoverActions => actionDeclToAction.Keys
       .Where(actionDecl => actionDecl.HasMoverType).Select(actionDecl => actionDeclToAction[actionDecl]);
diff --git a/Source/Concurrency/LinearDomainCollector.cs b/Source/Concurrency/LinearDomainCollector.cs
index 3543c3e69..c05d0c501 100644
--- a/Source/Concurrency/LinearDomainCollector.cs
+++ b/Source/Concurrency/LinearDomainCollector.cs
@@ -138,7 +138,7 @@ private bool ContainsPermissionType(Type type)
         visitedTypes.Add(type);
         if (type is CtorType ctorType && ctorType.Decl is DatatypeTypeCtorDecl datatypeTypeCtorDecl)
         {
-          var originalDecl = program.monomorphizer.GetOriginalDecl(datatypeTypeCtorDecl);
+          var originalDecl = Monomorphizer.GetOriginalDecl(datatypeTypeCtorDecl);
           var originalDeclName = originalDecl.Name;
           if (originalDeclName == "Lheap" || originalDeclName == "Lset" || originalDeclName == "Lval")
           {
@@ -174,7 +174,7 @@ private bool ContainsPermissionType(Type type)
     private Type GetPermissionType(Type type)
     {
       var typeCtorDecl = type.AsCtor.Decl;
-      var originalTypeCtorDecl = program.monomorphizer.GetOriginalDecl(typeCtorDecl);
+      var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(typeCtorDecl);
       var actualTypeParams = program.monomorphizer.GetTypeInstantiation(typeCtorDecl);
       return 
         originalTypeCtorDecl.Name == "Lheap"
@@ -189,7 +189,7 @@ private Dictionary<Type, LinearDomain> MakeLinearDomains()
       foreach (var type in permissionTypes)
       {
         var typeCtorDecl = type.AsCtor.Decl;
-        var originalTypeCtorDecl = program.monomorphizer.GetOriginalDecl(typeCtorDecl);
+        var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(typeCtorDecl);
         var actualTypeParams = program.monomorphizer.GetTypeInstantiation(typeCtorDecl);
         var permissionType = GetPermissionType(type); 
         if (!permissionTypeToCollectors.ContainsKey(permissionType))
diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs
index d399fb649..9d12ac0e0 100644
--- a/Source/Concurrency/LinearRewriter.cs
+++ b/Source/Concurrency/LinearRewriter.cs
@@ -190,8 +190,8 @@ private List<Cmd> RewriteLheapSplit(CallCmd callCmd)
       out Function lsetConstructor, out Function lvalConstructor);
     
     var cmdSeq = new List<Cmd>();
-    var k = callCmd.Ins[0];
-    var path = callCmd.Ins[1];
+    var path = callCmd.Ins[0];
+    var k = callCmd.Ins[1];
     var l = callCmd.Outs[0].Decl;
     
     var mapImpFunc = MapImp(refType);
@@ -223,16 +223,16 @@ private List<Cmd> RewriteLheapTransfer(CallCmd callCmd)
       out Function lsetConstructor, out Function lvalConstructor);
 
     var cmdSeq = new List<Cmd>();
-    var path1 = callCmd.Ins[0];
-    var path2 = callCmd.Ins[1];
+    var path = callCmd.Ins[0];
+    var path1 = callCmd.Ins[1];
 
     var mapOrFunc = MapOr(refType);
     var mapIteFunc = MapIte(refType, type);
     cmdSeq.Add(CmdHelper.AssignCmd(
-      CmdHelper.ExprToAssignLhs(path2),
+      CmdHelper.ExprToAssignLhs(path),
       ExprHelper.FunctionCall(lheapConstructor,
-        ExprHelper.FunctionCall(mapOrFunc, Dom(path2), Dom(path1)),
-        ExprHelper.FunctionCall(mapIteFunc, Dom(path2), Val(path2), Val(path1)))));
+        ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(path1)),
+        ExprHelper.FunctionCall(mapIteFunc, Dom(path), Val(path), Val(path1)))));
     
     ResolveAndTypecheck(options, cmdSeq);
     return cmdSeq;
@@ -286,7 +286,7 @@ private List<Cmd> CreateAccessAsserts(Expr expr, IToken tok, string msg)
         if (mapExpr is NAryExpr lheapValExpr &&
             lheapValExpr.Fun is FieldAccess &&
             lheapValExpr.Args[0].Type is CtorType ctorType &&
-            monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap")
+            Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap")
         {
           var cmdSeq = CreateAccessAsserts(lheapValExpr.Args[0], tok, msg);
           var lheapContainsFunc = LheapContains(nAryExpr.Type);
@@ -371,9 +371,9 @@ private List<Cmd> RewriteLsetSplit(CallCmd callCmd)
       out Function lsetConstructor, out Function lvalConstructor);
     
     var cmdSeq = new List<Cmd>();
-    var k = callCmd.Ins[0];
-    var path = callCmd.Ins[1];
-    
+    var path = callCmd.Ins[0];
+    var k = callCmd.Ins[1];
+
     var mapConstFunc = MapConst(type, Type.Bool);
     var mapImpFunc = MapImp(type);
     cmdSeq.Add(AssertCmd(callCmd.tok,
@@ -394,13 +394,13 @@ private List<Cmd> RewriteLsetTransfer(CallCmd callCmd)
       out Function lsetConstructor, out Function lvalConstructor);
 
     var cmdSeq = new List<Cmd>();
-    var path1 = callCmd.Ins[0];
-    var path2 = callCmd.Ins[1];
+    var path = callCmd.Ins[0];
+    var path1 = callCmd.Ins[1];
 
     var mapOrFunc = MapOr(type);
     cmdSeq.Add(CmdHelper.AssignCmd(
-      CmdHelper.ExprToAssignLhs(path2),
-      ExprHelper.FunctionCall(lsetConstructor, ExprHelper.FunctionCall(mapOrFunc, Dom(path2), Dom(path1)))));
+      CmdHelper.ExprToAssignLhs(path),
+      ExprHelper.FunctionCall(lsetConstructor, ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(path1)))));
     
     ResolveAndTypecheck(options, cmdSeq);
     return cmdSeq;
@@ -412,9 +412,9 @@ private List<Cmd> RewriteLvalSplit(CallCmd callCmd)
       out Function lsetConstructor, out Function lvalConstructor);
 
     var cmdSeq = new List<Cmd>();
-    var k = callCmd.Ins[0];
-    var path = callCmd.Ins[1];
-    
+    var path = callCmd.Ins[0];
+    var k = callCmd.Ins[1];
+
     var lsetContainsFunc = LsetContains(type);
     cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(lsetContainsFunc, path, Val(k)), "Lval_Split failed"));
 
@@ -434,15 +434,15 @@ private List<Cmd> RewriteLvalTransfer(CallCmd callCmd)
       out Function lsetConstructor, out Function lvalConstructor);
 
     var cmdSeq = new List<Cmd>();
-    var l = callCmd.Ins[0];
-    var path2 = callCmd.Ins[1];
-
+    var path = callCmd.Ins[0];
+    var k = callCmd.Ins[1];
+    
     var mapOneFunc = MapOne(type);
     var mapOrFunc = MapOr(type);
     cmdSeq.Add(CmdHelper.AssignCmd(
-      CmdHelper.ExprToAssignLhs(path2),
+      CmdHelper.ExprToAssignLhs(path),
       ExprHelper.FunctionCall(lsetConstructor,
-        ExprHelper.FunctionCall(mapOrFunc, Dom(path2), ExprHelper.FunctionCall(mapOneFunc, Val(l))))));
+        ExprHelper.FunctionCall(mapOrFunc, Dom(path), ExprHelper.FunctionCall(mapOneFunc, Val(k))))));
     
     ResolveAndTypecheck(options, cmdSeq);
     return cmdSeq;
diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs
index 8e09da6e3..32927bb45 100644
--- a/Source/Concurrency/LinearTypeChecker.cs
+++ b/Source/Concurrency/LinearTypeChecker.cs
@@ -280,7 +280,7 @@ private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b)
               continue;
             }
             var ie = IsPrimitive(callCmd.Proc) && paramKind == LinearKind.LINEAR
-              ? ExtractRootFromAccessPathExpr(callCmd.Ins[i])
+              ? CivlPrimitives.ExtractRootFromAccessPathExpr(callCmd.Ins[i])
               : callCmd.Ins[i] as IdentifierExpr;
             if (start.Contains(ie.Decl))
             {
@@ -393,69 +393,6 @@ private bool SkipCheck(Variable v)
       return enclosingProc is ActionDecl || enclosingProc.IsPure;
     }
 
-    private IdentifierExpr ExtractRootFromAccessPathExpr(Expr expr)
-    {
-      if (expr is IdentifierExpr identifierExpr)
-      {
-        return identifierExpr;
-      }
-      if (expr is NAryExpr nAryExpr)
-      {
-        if (nAryExpr.Fun is FieldAccess)
-        {
-          return ExtractRootFromAccessPathExpr(nAryExpr.Args[0]);
-        }
-        if (nAryExpr.Fun is MapSelect)
-        {
-          var mapExpr = nAryExpr.Args[0];
-          if (mapExpr is NAryExpr lheapValExpr &&
-              lheapValExpr.Fun is FieldAccess &&
-              lheapValExpr.Args[0].Type is CtorType ctorType &&
-              program.monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap")
-          {
-            return ExtractRootFromAccessPathExpr(lheapValExpr.Args[0]);
-          }
-          return ExtractRootFromAccessPathExpr(nAryExpr.Args[0]);
-        }
-      }
-      return null;
-    }
-    
-    private IdentifierExpr ModifiedArgument(CallCmd callCmd)
-    {
-      switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name)
-      {
-        case "Ref_Alloc":
-          return null;
-        case "Lheap_Empty":
-          return null;
-        case "Lheap_Split":
-          return ExtractRootFromAccessPathExpr(callCmd.Ins[1]);
-        case "Lheap_Transfer":
-          return ExtractRootFromAccessPathExpr(callCmd.Ins[1]);
-        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[1]);
-        case "Lset_Transfer":
-          return ExtractRootFromAccessPathExpr(callCmd.Ins[1]);
-        case "Lval_Split":
-          return ExtractRootFromAccessPathExpr(callCmd.Ins[1]);
-        case "Lval_Transfer":
-          return ExtractRootFromAccessPathExpr(callCmd.Ins[1]);
-        default:
-          throw new cce.UnreachableException();
-      }
-    }
-
     public override Cmd VisitAssignCmd(AssignCmd node)
     {
       HashSet<Variable> rhsVars = new HashSet<Variable>();
@@ -606,7 +543,8 @@ public int CheckLinearParameters(CallCmd callCmd, HashSet<Variable> availableLin
     public override Cmd VisitCallCmd(CallCmd node)
     {
       var isPrimitive = IsPrimitive(node.Proc);
-      HashSet<Variable> inVars = new HashSet<Variable>();
+      var inVars = new HashSet<Variable>();
+      var globalInVars = new HashSet<Variable>();
       for (int i = 0; i < node.Proc.InParams.Count; i++)
       {
         var formal = node.Proc.InParams[i];
@@ -616,7 +554,7 @@ public override Cmd VisitCallCmd(CallCmd node)
           continue;
         }
         var isLinearParamInPrimitiveCall = isPrimitive && formalKind == LinearKind.LINEAR;
-        var actual = isLinearParamInPrimitiveCall ? ExtractRootFromAccessPathExpr(node.Ins[i]) : node.Ins[i] as IdentifierExpr;
+        var actual = isLinearParamInPrimitiveCall ? CivlPrimitives.ExtractRootFromAccessPathExpr(node.Ins[i]) : node.Ins[i] as IdentifierExpr;
         if (actual == null)
         {
           if (isLinearParamInPrimitiveCall)
@@ -640,7 +578,7 @@ public override Cmd VisitCallCmd(CallCmd node)
           Error(node, $"The domains of parameter {formal} and argument {actual} must be the same");
           continue;
         }
-        if (actual.Decl is GlobalVariable && !IsPrimitive(node.Proc))
+        if (actual.Decl is GlobalVariable && !node.Proc.IsPure)
         {
           Error(node, $"Only local linear variable can be an argument to a procedure call: {actual}");
           continue;
@@ -651,6 +589,10 @@ public override Cmd VisitCallCmd(CallCmd node)
           continue;
         }
         inVars.Add(actual.Decl);
+        if (actual.Decl is GlobalVariable && actualKind == LinearKind.LINEAR_IN)
+        {
+          globalInVars.Add(actual.Decl);
+        }
       }
 
       for (int i = 0; i < node.Proc.OutParams.Count; i++)
@@ -674,9 +616,15 @@ public override Cmd VisitCallCmd(CallCmd node)
         }
       }
 
+      var globalOutVars = node.Outs.Select(ie => ie.Decl).ToHashSet();
+      globalInVars.Where(v => !globalOutVars.Contains(v)).ForEach(v =>
+      {
+        Error(node, $"Global variable passed as input to pure call but not received as output: {v}");
+      });
+
       if (isPrimitive)
       {
-        var modifiedArgument = ModifiedArgument(node)?.Decl;
+        var modifiedArgument = CivlPrimitives.ModifiedArgument(node)?.Decl;
         if (modifiedArgument != null)
         {
           if (modifiedArgument is Formal formal && formal.InComing)
@@ -687,8 +635,9 @@ public override Cmd VisitCallCmd(CallCmd node)
                    enclosingProc is not YieldProcedureDecl &&
                    enclosingProc.Modifies.All(v => v.Decl != modifiedArgument))
           {
+            var str = enclosingProc is ActionDecl ? "action's" : "procedure's";
             Error(node,
-              $"Primitive assigns to a global variable that is not in the enclosing procedure's modifies clause: {modifiedArgument}");
+              $"Primitive assigns to a global variable that is not in the enclosing {str} modifies clause: {modifiedArgument}");
           }
         }
       }
@@ -793,7 +742,7 @@ public IEnumerable<Expr> LheapWellFormedExpressions(IEnumerable<Variable> availa
         return Enumerable.Empty<Expr>();
       }
       return availableVars.Where(v =>
-        v.TypedIdent.Type is CtorType ctorType && monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap").Select(
+        v.TypedIdent.Type is CtorType ctorType && Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap").Select(
         v =>
         {
           var ctorType = (CtorType)v.TypedIdent.Type;
diff --git a/Source/Concurrency/LinearityChecker.cs b/Source/Concurrency/LinearityChecker.cs
index 6f0dd6e0c..ee6b2e19a 100644
--- a/Source/Concurrency/LinearityChecker.cs
+++ b/Source/Concurrency/LinearityChecker.cs
@@ -15,7 +15,7 @@ private LinearityChecker(CivlTypeChecker civlTypeChecker)
     public static void AddCheckers(CivlTypeChecker civlTypeChecker, List<Declaration> decls)
     {
       var linearityChecker = new LinearityChecker(civlTypeChecker);
-      foreach (var action in civlTypeChecker.MoverActions.Concat<Action>(civlTypeChecker.LinkActions))
+      foreach (var action in civlTypeChecker.MoverActions)
       {
         linearityChecker.AddChecker(action, decls);
       }
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 50d8f3db5..28c7d724b 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -82,11 +82,6 @@ where action.LayerRange.Contains(sequentialization.Layer)
       {
         moverChecking.CreateCooperationChecker(action);
       }
-
-      foreach (var action in civlTypeChecker.LinkActions)
-      {
-        moverChecking.CreateCooperationChecker(action);
-      }
     }
 
     private IEnumerable<Requires> DisjointnessAndWellFormedRequires(IEnumerable<Variable> paramVars, HashSet<Variable> frame)
diff --git a/Source/Concurrency/YieldSufficiencyTypeChecker.cs b/Source/Concurrency/YieldSufficiencyTypeChecker.cs
index b89c4ba41..625e004a5 100644
--- a/Source/Concurrency/YieldSufficiencyTypeChecker.cs
+++ b/Source/Concurrency/YieldSufficiencyTypeChecker.cs
@@ -16,7 +16,7 @@ public static class YieldSufficiencyTypeChecker
     private const string L = "L"; // left mover action
     private const string R = "R"; // right mover action
     private const string N = "N"; // non mover action
-    private const string P = "P"; // private access (local variable, link action, pure procedure, ...)
+    private const string P = "P"; // private access (local variable, pure action, pure procedure, ...)
     private const string M = "M"; // modification of global variables
     private const string A = "A"; // async call
     
@@ -318,7 +318,7 @@ private static List<Tuple<Absy, string, Absy>> LabelsToLabeledEdges(Dictionary<T
 
       private string CallCmdLabel(CallCmd callCmd)
       {
-        if (callCmd.Proc is ActionDecl || LinearRewriter.IsPrimitive(callCmd.Proc) || callCmd.Proc.IsPure)
+        if (callCmd.Proc.IsPure)
         {
           return P;
         }
@@ -387,7 +387,7 @@ public static string ModifiesGlobalLabel<T>(IEnumerable<T> modifiedGlobalVars)
 
       private string CallCmdLabelAsync(CallCmd callCmd)
       {
-        if (callCmd.Proc is ActionDecl || LinearRewriter.IsPrimitive(callCmd.Proc) || callCmd.Proc.IsPure)
+        if (callCmd.Proc.IsPure)
         {
           return P;
         }
diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs
index 4589d099b..d0811a142 100644
--- a/Source/Concurrency/YieldingProcDuplicator.cs
+++ b/Source/Concurrency/YieldingProcDuplicator.cs
@@ -248,34 +248,26 @@ public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq)
 
     private void ProcessCallCmd(CallCmd newCall)
     {
-      if (newCall.Proc is ActionDecl actionDecl)
-      {
-        var linkAction = civlTypeChecker.Action(actionDecl);
-        if (linkAction.LowerLayer == layerNum)
-        {
-          newCall.Proc = linkAction.Impl.Proc;
-          InjectGate(linkAction, newCall);
-          newCmdSeq.Add(newCall);
-        }
-        return;
-      }
-
-      if (LinearRewriter.IsPrimitive(newCall.Proc))
-      {
-        var callLayerRange = new LayerRange(newCall.Layers[0],
-          newCall.Layers.Count == 1 ? newCall.Layers[0] : newCall.Layers[1]);
-        if (callLayerRange.Contains(layerNum))
-        {
-          newCmdSeq.AddRange(linearRewriter.RewriteCallCmd(newCall));
-        }
-        return;
-      }
-
       if (newCall.Proc.IsPure)
       {
-        if (newCall.Layers[0] == layerNum)
+        var callLayerRange = newCall.LayerRange;
+        if (callLayerRange.Contains(layerNum))
         {
-          newCmdSeq.Add(newCall);
+          if (newCall.Proc is ActionDecl actionDecl)
+          {
+            var pureAction = civlTypeChecker.Action(actionDecl);
+            newCall.Proc = pureAction.Impl.Proc;
+            InjectGate(pureAction, newCall);
+            newCmdSeq.Add(newCall);
+          }
+          else if (LinearRewriter.IsPrimitive(newCall.Proc))
+          {
+            newCmdSeq.AddRange(linearRewriter.RewriteCallCmd(newCall));
+          }
+          else
+          {
+            newCmdSeq.Add(newCall);
+          }
         }
         return;
       }
diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
index ccb4fa556..4536013c8 100644
--- a/Source/Core/AST/Absy.cs
+++ b/Source/Core/AST/Absy.cs
@@ -2705,7 +2705,7 @@ public override void Resolve(ResolutionContext rc)
       {
         if (IsPure)
         {
-          rc.Error(this, "unnecessary modifies clause for pure procedure");
+          rc.Error(this, "unnecessary modifies clause for pure {0}", this is ActionDecl ? "action" : "procedure");
         }
         else
         {
@@ -2928,12 +2928,12 @@ public class ActionDecl : Procedure
     public LayerRange LayerRange; // set during registration
 
     public ActionDecl(IToken tok, string name, MoverType moverType,
-      List<Variable> inParams, List<Variable> outParams,
+      List<Variable> inParams, List<Variable> outParams, bool isPure,
       List<ActionDeclRef> creates, ActionDeclRef refinedAction, ActionDeclRef invariantAction,
       List<ElimDecl> eliminates,
       List<IdentifierExpr> modifies, DatatypeTypeCtorDecl pendingAsyncCtorDecl, QKeyValue kv) : base(tok, name,
       new List<TypeVariable>(), inParams, outParams,
-      false, new List<Requires>(), modifies, new List<Ensures>(), kv)
+      isPure, new List<Requires>(), modifies, new List<Ensures>(), kv)
     {
       this.MoverType = moverType;
       this.Creates = creates;
@@ -3091,24 +3091,31 @@ public override void Typecheck(TypecheckingContext tc)
 
     protected override void EmitBegin(TokenTextWriter stream, int level)
     {
+      if (IsPure)
+      {
+        stream.Write(this, level, "pure ");
+      }
       if (MaybePendingAsync)
       {
         stream.Write(level, "async ");
       }
-      switch (MoverType)
+      if (!IsPure)
       {
-        case MoverType.Atomic:
-          stream.Write(level, ">-<");
-          break;
-        case MoverType.Both:
-          stream.Write(level, "<->");
-          break;
-        case MoverType.Left:
-          stream.Write(level, "<-");
-          break;
-        case MoverType.Right:
-          stream.Write(level, "->");
-          break;
+        switch (MoverType)
+        {
+          case MoverType.Atomic:
+            stream.Write(level, "atomic");
+            break;
+          case MoverType.Both:
+            stream.Write(level, "both");
+            break;
+          case MoverType.Left:
+            stream.Write(level, "left");
+            break;
+          case MoverType.Right:
+            stream.Write(level, "right");
+            break;
+        }
       }
       stream.Write(level, " action ");
     }
diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs
index 96ed16ad5..b3e00dfbb 100644
--- a/Source/Core/AST/AbsyCmd.cs
+++ b/Source/Core/AST/AbsyCmd.cs
@@ -1584,8 +1584,8 @@ public void CheckAssignments(TypecheckingContext tc)
           if (!tc.Yields && !tc.InFrame(v))
           {
             tc.Error(this,
-              "command assigns to a global variable that is not in the enclosing procedure's modifies clause: {0}",
-              v.Name);
+              "command assigns to a global variable that is not in the enclosing {0} modifies clause: {1}",
+              tc.Proc is ActionDecl ? "action's" : "procedure's", v.Name);
           }
         }
       }
@@ -3281,14 +3281,14 @@ public override void Resolve(ResolutionContext rc)
       }
       if (rc.Proc is YieldProcedureDecl)
       {
-        if (CivlPrimitives.Linear.Contains(Proc.Name) || Proc.IsPure || Proc is YieldProcedureDecl or YieldInvariantDecl or ActionDecl)
+        if (Proc.IsPure || Proc is YieldProcedureDecl or YieldInvariantDecl)
         {
           // call ok
         }
         else
         {
           rc.Error(this,
-            "a yielding procedure may only call primitive procedures, pure procedures, yield procedures, yield invariants, or link actions");
+            "a yielding procedure may only call pure actions, pure procedures, yield procedures, and yield invariants");
         }
       }
       if (IsAsync)
@@ -3437,96 +3437,54 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
           tc.Error(this, "layer of callee must not be more than layer of caller");
         }
       }
-      else if (Proc is ActionDecl actionDecl)
-      {
-        // link call
-        var calleeLayer = actionDecl.LayerRange.LowerLayer;
-        // allowed to execute only on calleeLayer
-        actionDecl.Modifies.ForEach(ie =>
-        {
-          if (ie.Decl.LayerRange.LowerLayer != calleeLayer)
-          {
-            tc.Error(this, $"modified variable of callee must be introduced at layer {calleeLayer}: {ie.Decl.Name}");
-          }
-        });
-        if (calleeLayer > callerDecl.Layer)
-        {
-          tc.Error(this, "layer of callee must not be more than layer of caller");
-        }
-        else if (calleeLayer < callerDecl.Layer)
-        {
-          actionDecl.Modifies.ForEach(ie =>
-          {
-            if (ie.Decl.LayerRange.UpperLayer != calleeLayer)
-            {
-              tc.Error(this, $"modified variable of callee must be hidden at layer {calleeLayer}: {ie.Decl.Name}");
-            }
-          });
-        }
-        else
-        {
-          CheckModifies(actionDecl.ModifiedVars);
-        }
-      }
-      else if (CivlPrimitives.Linear.Contains(Proc.Name))
+      else
       {
+        Debug.Assert(Proc.IsPure);
         if (Layers.Count == 0 || Layers.Count > 2)
         {
           tc.Error(this, "expected layer range");
         }
         else if (Layers[^1] > callerDecl.Layer)
         {
-          tc.Error(this, $"each layer must not be more than {callerDecl.Layer}");
+          tc.Error(this, $"layer must be no more than layer {callerDecl.Layer}");
         }
         else
         {
           var usedVars = VariableCollector.Collect(Ins.Union(Outs));
-          var globalUsedVars = usedVars.OfType<GlobalVariable>();
-          if (globalUsedVars.Any())
+          if (usedVars.OfType<GlobalVariable>().Any())
           {
             if (Layers.Count == 2)
             {
-              tc.Error(this, "expected a singleton layer range");
+              tc.Error(this, "expected singleton layer range");
             }
             else
             {
+              // Check global outputs only; the checking of local outputs is done later
               var calleeLayer = Layers[0];
-              globalUsedVars.ForEach(v =>
+              var globalOutputs = Outs.Select(ie => ie.Decl).OfType<GlobalVariable>().Cast<Variable>();
+              if (CivlPrimitives.Linear.Contains(Proc.Name))
               {
-                if (v.LayerRange.LowerLayer != calleeLayer)
+                var modifiedArgument = CivlPrimitives.ModifiedArgument(this);
+                if (modifiedArgument is { Decl: GlobalVariable })
                 {
-                  tc.Error(this, $"accessed variable must be introduced at layer {calleeLayer}: {v.Name}");
+                  globalOutputs = globalOutputs.Append(modifiedArgument.Decl);
                 }
+              }
+              globalOutputs.Where(v => v.LayerRange.LowerLayer != calleeLayer).ForEach(v =>
+              {
+                tc.Error(this, $"variable must be introduced at layer {calleeLayer}: {v.Name}");
               });
               if (calleeLayer < callerDecl.Layer)
               {
-                globalUsedVars.ForEach(v =>
+                globalOutputs.Where(v => v.LayerRange.UpperLayer != calleeLayer).ForEach(v =>
                 {
-                  if (v.LayerRange.UpperLayer != calleeLayer)
-                  {
-                    tc.Error(this, $"accessed variable must be hidden at layer {calleeLayer}: {v.Name}");
-                  }
+                  tc.Error(this, $"variable must be hidden at layer {calleeLayer}: {v.Name}");
                 });
               }
             }
           }
         }
       }
-      else
-      {
-        Debug.Assert(Proc.IsPure);
-        if (Layers.Count != 1)
-        {
-          tc.Error(this, "call to pure procedure must be annotated with a layer");
-        }
-        else
-        {
-          if (Layers[0] > callerDecl.Layer)
-          {
-            tc.Error(this, "layer of callee must not be more than layer of caller");
-          }
-        }
-      }
     }
 
     private void TypecheckCallCmdInActionDecl(TypecheckingContext tc)
@@ -3570,12 +3528,8 @@ private void TypecheckCallCmdInActionDecl(TypecheckingContext tc)
         }
         if (!callerActionDecl.LayerRange.Subset(calleeActionDecl.LayerRange))
         {
-          tc.Error(this, "caller layer range must be subset of callee layer range");
-        }
-        else if (callerActionDecl.LayerRange.LowerLayer == calleeActionDecl.LayerRange.LowerLayer &&
-                 callerActionDecl.HasMoverType && !calleeActionDecl.HasMoverType)
-        {
-          tc.Error(this, "lower layer of caller must be greater than lower layer of callee");
+          tc.Error(this,
+            $"caller layer range ({callerActionDecl.LayerRange}) must be subset of callee layer range ({calleeActionDecl.LayerRange})");
         }
       }
       else
@@ -3634,7 +3588,10 @@ public override void Typecheck(TypecheckingContext tc)
           var actual = Outs[i];
           if (actual.Decl is GlobalVariable)
           {
-            tc.Error(actual, $"global variable directly modified in a yield procedure: {actual.Decl.Name}");
+            if (!Proc.IsPure) // global outputs of pure calls already checked
+            {
+              tc.Error(actual, $"global variable directly modified in a yield procedure: {actual.Decl.Name}");
+            }
           }
           else
           {
@@ -3645,6 +3602,28 @@ public override void Typecheck(TypecheckingContext tc)
             }
           }
         }
+        // primitive calls have inout parameters that must be checked here
+        if (CivlPrimitives.Linear.Contains(Proc.Name))
+        {
+          var modifiedArgument = CivlPrimitives.ModifiedArgument(this);
+          if (modifiedArgument == null)
+          {
+            // nothing to do
+          }
+          else if (modifiedArgument is { Decl: GlobalVariable })
+          {
+            // already done in TypecheckCallCmdInYieldProcedureDecl
+          }
+          else
+          {
+            var modifiedDecl = modifiedArgument.Decl;
+            var callLayerRange = new LayerRange(Layers[0], Layers.Count > 1 ? Layers[1] : Layers[0]);
+            if (!modifiedDecl.LayerRange.Subset(callLayerRange))
+            {
+              tc.Error(this, $"variable must be available only within layers in {callLayerRange}: {modifiedDecl.Name}");
+            }
+          }
+        }
         expectedLayerRanges = Proc.InParams.Select(formal => FormalLayerRange(callerDecl, formal)).ToList();
       }
 
@@ -3714,6 +3693,9 @@ public override void Typecheck(TypecheckingContext tc)
       TypecheckCallCmdInActionDecl(tc);
     }
 
+    public LayerRange LayerRange => Layers.Count == 0 ? LayerRange.MinMax :
+      Layers.Count == 1 ? new LayerRange(Layers[0]) : new LayerRange(Layers[0], Layers[1]);
+
     private LayerRange FormalLayerRange(YieldProcedureDecl callerDecl, Variable calleeFormal)
     {
       LayerRange formalLayerRange;
@@ -3722,9 +3704,6 @@ private LayerRange FormalLayerRange(YieldProcedureDecl callerDecl, Variable call
         case YieldInvariantDecl yieldInvariantDecl:
           formalLayerRange = new LayerRange(yieldInvariantDecl.Layer);
           break;
-        case ActionDecl actionDecl:
-          formalLayerRange = new LayerRange(actionDecl.LayerRange.LowerLayer);
-          break;
         case YieldProcedureDecl yieldProcedureDecl:
         {
           formalLayerRange = calleeFormal.LayerRange;
@@ -3736,15 +3715,8 @@ private LayerRange FormalLayerRange(YieldProcedureDecl callerDecl, Variable call
         }
         default:
         {
-          if (CivlPrimitives.Linear.Contains(Proc.Name))
-          {
-            formalLayerRange = new LayerRange(Layers[0], Layers.Count > 1 ? Layers[1] : Layers[0]);
-          }
-          else
-          {
-            Debug.Assert(Proc.IsPure);
-            formalLayerRange = new LayerRange(Layers[0]);
-          }
+          Debug.Assert(Proc.IsPure);
+          formalLayerRange = LayerRange;
           break;
         }
       }
diff --git a/Source/Core/AST/AbsyExpr.cs b/Source/Core/AST/AbsyExpr.cs
index 62c108329..2dc0b8911 100644
--- a/Source/Core/AST/AbsyExpr.cs
+++ b/Source/Core/AST/AbsyExpr.cs
@@ -1357,11 +1357,16 @@ public override void Typecheck(TypecheckingContext tc)
           if (Decl is GlobalVariable)
           {
             var globalVarLayerRange = Decl.LayerRange;
-            if (!actionDecl.LayerRange.Subset(globalVarLayerRange) ||
-                // a global variable introduced at layer n is visible to a mover action only at layer n+1 or higher
-                actionDecl.HasMoverType && actionDecl.LayerRange.LowerLayer == globalVarLayerRange.LowerLayer)
+            if (actionDecl.LayerRange.LowerLayer <= globalVarLayerRange.LowerLayer)
             {
-              tc.Error(this, $"variable not available across layers in {actionDecl.LayerRange}: {Decl.Name}");
+              // a global variable introduced at layer n is visible to an action only at layers greater than n
+              tc.Error(this,
+                $"global variable must be introduced below the lower layer {actionDecl.LayerRange.LowerLayer} of action {actionDecl.Name}: {Decl.Name}");
+            }
+            else if (!actionDecl.LayerRange.Subset(globalVarLayerRange))
+            {
+              tc.Error(this,
+                $"global variable must be available across all layers ({actionDecl.LayerRange}) of action {actionDecl.Name}: {Decl.Name}");
             }
           }
         }
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index d0e35bac5..ab76a6c77 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -189,6 +189,7 @@ BoogiePL
      Procedure/*!*/ pr;
      Implementation im;
      Implementation/*!*/ nnim;
+     bool isPure = false;
   .)
   { Consts<out ds>             (. foreach(Bpl.Declaration/*!*/ v in ds){
                                     Contract.Assert(v != null);
@@ -212,14 +213,6 @@ BoogiePL
                                     Pgm.AddTopLevelDeclaration(v);
                                   }
                                .)
-  | ActionDecl<out ac, out im, out dt> (. Pgm.AddTopLevelDeclaration(ac);
-                                          if (im != null) {
-                                            Pgm.AddTopLevelDeclaration(im);
-                                          }
-                                          if (dt != null) {
-                                            Pgm.AddTopLevelDeclaration(dt);
-                                          }
-                                       .)
   | "yield" 
     (
       YieldInvariantDecl<out yi> (. Pgm.AddTopLevelDeclaration(yi); .)
@@ -230,11 +223,26 @@ BoogiePL
                                   }
                                .)
     )
-  | Procedure<out pr, out im>  (. Pgm.AddTopLevelDeclaration(pr);
+  | Pure<ref isPure>
+    (
+      Procedure<isPure, out pr, out im>
+                                (. Pgm.AddTopLevelDeclaration(pr);
                                    if (im != null) {
                                      Pgm.AddTopLevelDeclaration(im);
                                    }
-                               .)
+                                   isPure = false;
+                                .)
+    | ActionDecl<isPure, out ac, out im, out dt>
+                                       (. Pgm.AddTopLevelDeclaration(ac);
+                                          if (im != null) {
+                                            Pgm.AddTopLevelDeclaration(im);
+                                          }
+                                          if (dt != null) {
+                                            Pgm.AddTopLevelDeclaration(dt);
+                                          }
+                                          isPure = false;
+                                       .)
+    )
   | Implementation<out nnim>   (. Pgm.AddTopLevelDeclaration(nnim); .)
   }
   EOF
@@ -649,7 +657,11 @@ Invariant<.List<Requires> invariants.>
   )
   .
 
-ActionDecl<out ActionDecl actionDecl, out Implementation impl, out DatatypeTypeCtorDecl datatypeTypeCtorDecl>
+Pure<ref bool isPure>
+= ["pure" (. isPure = true; .)]
+  .
+
+ActionDecl<bool isPure, out ActionDecl actionDecl, out Implementation impl, out DatatypeTypeCtorDecl datatypeTypeCtorDecl>
 = (. IToken name = null;
      bool isAsync = false;
      MoverType moverType = MoverType.None;
@@ -666,7 +678,7 @@ ActionDecl<out ActionDecl actionDecl, out Implementation impl, out DatatypeTypeC
      impl = null;
    .)
   [ "async" (. isAsync = true; .) ]
-  [ MoverQualifier <ref moverType> ]
+  [ MoverQualifier<ref moverType> ]
   "action"
   { Attribute<ref kv> }
   Ident<out name>
@@ -682,6 +694,16 @@ ActionDecl<out ActionDecl actionDecl, out Implementation impl, out DatatypeTypeC
     .)
   )
   (.
+     if (isPure) {
+       if (moverType == MoverType.None)
+       {
+         moverType = MoverType.Both;
+       }
+       else
+       {
+         this.SemErr("mover type unnecessary for pure action since it is a both mover");
+       }
+     }
      if (isAsync) {
        if (moverType == MoverType.None)
        {
@@ -697,7 +719,7 @@ ActionDecl<out ActionDecl actionDecl, out Implementation impl, out DatatypeTypeC
          datatypeTypeCtorDecl.AddConstructor(name, name.val, ins.Select(v => new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type)).ToList());
        }
      }
-     actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, creates, refinedAction, invariantAction, elims, mods, datatypeTypeCtorDecl, kv);
+     actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, elims, mods, datatypeTypeCtorDecl, kv);
   .)
   .
 
@@ -820,21 +842,19 @@ SpecYieldPrePost<. ref ActionDeclRef refinedAction, List<Requires> pre, List<Ens
   ";"
   .
 
-Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl>
+Procedure<bool isPure, out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl>
 = (. Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;
      List<TypeVariable>/*!*/ typeParams;
      List<Variable>/*!*/ ins, outs;
      List<Requires>/*!*/ pre = new List<Requires>();
      List<IdentifierExpr>/*!*/ mods = new List<IdentifierExpr>();
      List<Ensures>/*!*/ post = new List<Ensures>();
-     bool isPure = false;
      List<Variable>/*!*/ locals = new List<Variable>();
      StmtList/*!*/ stmtList;
      QKeyValue kv = null;
      impl = null;
   .)
 
-  ["pure" (. isPure = true; .)]
   "procedure"
   ProcSignature<true, out x, out typeParams, out ins, out outs, out kv>
   ( ";"
diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs
index 85d3c4279..fd652352e 100644
--- a/Source/Core/CivlAttributes.cs
+++ b/Source/Core/CivlAttributes.cs
@@ -186,6 +186,69 @@ public static class CivlPrimitives
       "Lval_Split", "Lval_Transfer"
     };
 
+    public static IdentifierExpr ExtractRootFromAccessPathExpr(Expr expr)
+    {
+      if (expr is IdentifierExpr identifierExpr)
+      {
+        return identifierExpr;
+      }
+      if (expr is NAryExpr nAryExpr)
+      {
+        if (nAryExpr.Fun is FieldAccess)
+        {
+          return ExtractRootFromAccessPathExpr(nAryExpr.Args[0]);
+        }
+        if (nAryExpr.Fun is MapSelect)
+        {
+          var mapExpr = nAryExpr.Args[0];
+          if (mapExpr is NAryExpr lheapValExpr &&
+              lheapValExpr.Fun is FieldAccess &&
+              lheapValExpr.Args[0].Type is CtorType ctorType &&
+              Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap")
+          {
+            return ExtractRootFromAccessPathExpr(lheapValExpr.Args[0]);
+          }
+          return ExtractRootFromAccessPathExpr(nAryExpr.Args[0]);
+        }
+      }
+      return null;
+    }
+    
+    public static IdentifierExpr ModifiedArgument(CallCmd callCmd)
+    {
+      switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name)
+      {
+        case "Ref_Alloc":
+          return null;
+        case "Lheap_Empty":
+          return null;
+        case "Lheap_Split":
+          return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
+        case "Lheap_Transfer":
+          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":
+          return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
+        case "Lval_Split":
+          return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
+        case "Lval_Transfer":
+          return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
+        default:
+          throw new cce.UnreachableException();
+      }
+    }
+    
     public static HashSet<string> Async = new()
     {
       "create_async", "create_asyncs", "create_multi_asyncs", "set_choice"
diff --git a/Source/Core/Monomorphization.cs b/Source/Core/Monomorphization.cs
index 181744358..bb7674fd1 100644
--- a/Source/Core/Monomorphization.cs
+++ b/Source/Core/Monomorphization.cs
@@ -2050,7 +2050,7 @@ public Dictionary<string, Type> GetTypeInstantiation(DeclWithFormals decl)
       return value;
     }
     
-    public TypeCtorDecl GetOriginalDecl(TypeCtorDecl decl)
+    public static TypeCtorDecl GetOriginalDecl(TypeCtorDecl decl)
     {
       return decl.OriginalTypeCtorDecl ?? decl;
     }
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index d5b432cc6..6eefe668f 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -242,6 +242,7 @@ void BoogiePL() {
 		Procedure/*!*/ pr;
 		Implementation im;
 		Implementation/*!*/ nnim;
+		bool isPure = false;
 		
 		while (StartOf(1)) {
 			switch (la.kind) {
@@ -291,18 +292,6 @@ void BoogiePL() {
 				
 				break;
 			}
-			case 35: case 36: case 41: case 42: case 43: case 44: {
-				ActionDecl(out ac, out im, out dt);
-				Pgm.AddTopLevelDeclaration(ac);
-				if (im != null) {
-				 Pgm.AddTopLevelDeclaration(im);
-				}
-				if (dt != null) {
-				 Pgm.AddTopLevelDeclaration(dt);
-				}
-				
-				break;
-			}
 			case 8: {
 				Get();
 				if (la.kind == 34) {
@@ -318,13 +307,28 @@ void BoogiePL() {
 				} else SynErr(120);
 				break;
 			}
-			case 45: case 50: {
-				Procedure(out pr, out im);
-				Pgm.AddTopLevelDeclaration(pr);
-				if (im != null) {
-				  Pgm.AddTopLevelDeclaration(im);
-				}
-				
+			case 35: case 36: case 37: case 42: case 43: case 44: case 45: case 46: {
+				Pure(ref isPure);
+				if (la.kind == 46) {
+					Procedure(isPure, out pr, out im);
+					Pgm.AddTopLevelDeclaration(pr);
+					if (im != null) {
+					 Pgm.AddTopLevelDeclaration(im);
+					}
+					isPure = false;
+					
+				} else if (StartOf(3)) {
+					ActionDecl(isPure, out ac, out im, out dt);
+					Pgm.AddTopLevelDeclaration(ac);
+					if (im != null) {
+					 Pgm.AddTopLevelDeclaration(im);
+					}
+					if (dt != null) {
+					 Pgm.AddTopLevelDeclaration(dt);
+					}
+					isPure = false;
+					
+				} else SynErr(121);
 				break;
 			}
 			case 51: {
@@ -363,7 +367,7 @@ void Consts(out List<Declaration>/*!*/ ds) {
 				axioms.Add(axiom); ds.Add(axiom); 
 			}
 			Expect(27);
-		} else SynErr(121);
+		} else SynErr(122);
 		foreach(TypedIdent/*!*/ x in xs){
 		 Contract.Assert(x != null);
 		 var constant = new Constant(y, x, u, kv, axioms);
@@ -397,7 +401,7 @@ void Function(out List<Declaration>/*!*/ ds) {
 			TypeParams(out typeParamTok, out typeParams);
 		}
 		Expect(11);
-		if (StartOf(3)) {
+		if (StartOf(4)) {
 			VarOrType(out tyd, out argKv);
 			arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); 
 			while (la.kind == 14) {
@@ -417,7 +421,7 @@ void Function(out List<Declaration>/*!*/ ds) {
 			Get();
 			Type(out retTy);
 			retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); 
-		} else SynErr(122);
+		} else SynErr(123);
 		if (la.kind == 26) {
 			Get();
 			Expression(out tmp);
@@ -442,7 +446,7 @@ void Function(out List<Declaration>/*!*/ ds) {
 			Expect(27);
 		} else if (la.kind == 10) {
 			Get();
-		} else SynErr(123);
+		} else SynErr(124);
 		if (retTyd == null) {
 		 // construct a dummy type for the case of syntax error
 		 retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));
@@ -564,72 +568,6 @@ void GlobalVars(out List<Variable>/*!*/ ds) {
 		Expect(10);
 	}
 
-	void ActionDecl(out ActionDecl actionDecl, out Implementation impl, out DatatypeTypeCtorDecl datatypeTypeCtorDecl) {
-		IToken name = null;
-		bool isAsync = false;
-		MoverType moverType = MoverType.None;
-		List<Variable> ins, outs = new List<Variable>();
-		List<IdentifierExpr> mods = new List<IdentifierExpr>();
-		List<ActionDeclRef> creates = new List<ActionDeclRef>();
-		ActionDeclRef refinedAction = null;
-		ActionDeclRef invariantAction = null;
-		List<ElimDecl> elims = new List<ElimDecl>();
-		List<Variable> locals;
-		StmtList stmtList;
-		QKeyValue kv = null;
-		datatypeTypeCtorDecl = null;
-		impl = null;
-		
-		if (la.kind == 35) {
-			Get();
-			isAsync = true; 
-		}
-		if (StartOf(4)) {
-			MoverQualifier(ref moverType);
-		}
-		Expect(36);
-		while (la.kind == 26) {
-			Attribute(ref kv);
-		}
-		Ident(out name);
-		ProcFormals(true, true, out ins);
-		if (la.kind == 29) {
-			Get();
-			ProcFormals(false, true, out outs);
-		}
-		if (la.kind == 10) {
-			Get();
-			while (StartOf(5)) {
-				SpecAction(ref refinedAction, ref invariantAction, mods, creates, elims);
-			}
-		} else if (StartOf(6)) {
-			while (StartOf(5)) {
-				SpecAction(ref refinedAction, ref invariantAction, mods, creates, elims);
-			}
-			ImplBody(out locals, out stmtList);
-			impl = new Implementation(name, name.val, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
-			                              locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
-			
-		} else SynErr(124);
-		if (isAsync) {
-		 if (moverType == MoverType.None)
-		 {
-		   this.SemErr("async action must have a mover type");
-		 }
-		 else if (outs.Count > 0)
-		 {
-		   this.SemErr("async action must not have output parameters");
-		 }
-		 else
-		 {
-		   datatypeTypeCtorDecl = new DatatypeTypeCtorDecl(name, name.val, new List<TypeVariable>(), null);
-		   datatypeTypeCtorDecl.AddConstructor(name, name.val, ins.Select(v => new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type)).ToList());
-		 }
-		}
-		actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, creates, refinedAction, invariantAction, elims, mods, datatypeTypeCtorDecl, kv);
-		
-	}
-
 	void YieldInvariantDecl(out YieldInvariantDecl yieldInvariant) {
 		List<Requires> invariants = new List<Requires>(); QKeyValue kv = null; IToken name = null; List<Variable> ins; 
 		Expect(34);
@@ -661,10 +599,10 @@ void YieldProcedureDecl(out YieldProcedureDecl ypDecl, out Implementation impl)
 		QKeyValue kv = null;
 		impl = null;
 		
-		if (StartOf(4)) {
+		if (StartOf(5)) {
 			MoverQualifier(ref moverType);
 		}
-		Expect(45);
+		Expect(46);
 		while (la.kind == 26) {
 			Attribute(ref kv);
 		}
@@ -676,11 +614,11 @@ void YieldProcedureDecl(out YieldProcedureDecl ypDecl, out Implementation impl)
 		}
 		if (la.kind == 10) {
 			Get();
-			while (StartOf(7)) {
+			while (StartOf(6)) {
 				SpecYieldPrePost(ref refinedAction, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods);
 			}
-		} else if (StartOf(8)) {
-			while (StartOf(7)) {
+		} else if (StartOf(7)) {
+			while (StartOf(6)) {
 				SpecYieldPrePost(ref refinedAction, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods);
 			}
 			ImplBody(out locals, out stmtList);
@@ -691,32 +629,34 @@ void YieldProcedureDecl(out YieldProcedureDecl ypDecl, out Implementation impl)
 		ypDecl = new YieldProcedureDecl(name, name.val, moverType, ins, outs, pre, mods, post, yieldRequires, yieldEnsures, yieldPreserves, refinedAction, kv); 
 	}
 
-	void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) {
+	void Pure(ref bool isPure) {
+		if (la.kind == 35) {
+			Get();
+			isPure = true; 
+		}
+	}
+
+	void Procedure(bool isPure, out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) {
 		Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;
 		List<TypeVariable>/*!*/ typeParams;
 		List<Variable>/*!*/ ins, outs;
 		List<Requires>/*!*/ pre = new List<Requires>();
 		List<IdentifierExpr>/*!*/ mods = new List<IdentifierExpr>();
 		List<Ensures>/*!*/ post = new List<Ensures>();
-		bool isPure = false;
 		List<Variable>/*!*/ locals = new List<Variable>();
 		StmtList/*!*/ stmtList;
 		QKeyValue kv = null;
 		impl = null;
 		
-		if (la.kind == 50) {
-			Get();
-			isPure = true; 
-		}
-		Expect(45);
+		Expect(46);
 		ProcSignature(true, out x, out typeParams, out ins, out outs, out kv);
 		if (la.kind == 10) {
 			Get();
-			while (StartOf(9)) {
+			while (StartOf(8)) {
 				Spec(pre, mods, post);
 			}
-		} else if (StartOf(10)) {
-			while (StartOf(9)) {
+		} else if (StartOf(9)) {
+			while (StartOf(8)) {
 				Spec(pre, mods, post);
 			}
 			ImplBody(out locals, out stmtList);
@@ -727,6 +667,82 @@ void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl)
 		proc = new Procedure(x, x.val, typeParams, ins, outs, isPure, pre, mods, post, kv); 
 	}
 
+	void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl, out DatatypeTypeCtorDecl datatypeTypeCtorDecl) {
+		IToken name = null;
+		bool isAsync = false;
+		MoverType moverType = MoverType.None;
+		List<Variable> ins, outs = new List<Variable>();
+		List<IdentifierExpr> mods = new List<IdentifierExpr>();
+		List<ActionDeclRef> creates = new List<ActionDeclRef>();
+		ActionDeclRef refinedAction = null;
+		ActionDeclRef invariantAction = null;
+		List<ElimDecl> elims = new List<ElimDecl>();
+		List<Variable> locals;
+		StmtList stmtList;
+		QKeyValue kv = null;
+		datatypeTypeCtorDecl = null;
+		impl = null;
+		
+		if (la.kind == 36) {
+			Get();
+			isAsync = true; 
+		}
+		if (StartOf(5)) {
+			MoverQualifier(ref moverType);
+		}
+		Expect(37);
+		while (la.kind == 26) {
+			Attribute(ref kv);
+		}
+		Ident(out name);
+		ProcFormals(true, true, out ins);
+		if (la.kind == 29) {
+			Get();
+			ProcFormals(false, true, out outs);
+		}
+		if (la.kind == 10) {
+			Get();
+			while (StartOf(10)) {
+				SpecAction(ref refinedAction, ref invariantAction, mods, creates, elims);
+			}
+		} else if (StartOf(11)) {
+			while (StartOf(10)) {
+				SpecAction(ref refinedAction, ref invariantAction, mods, creates, elims);
+			}
+			ImplBody(out locals, out stmtList);
+			impl = new Implementation(name, name.val, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
+			                              locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
+			
+		} else SynErr(127);
+		if (isPure) {
+		 if (moverType == MoverType.None)
+		 {
+		   moverType = MoverType.Both;
+		 }
+		 else
+		 {
+		   this.SemErr("mover type unnecessary for pure action since it is a both mover");
+		 }
+		}
+		if (isAsync) {
+		 if (moverType == MoverType.None)
+		 {
+		   this.SemErr("async action must have a mover type");
+		 }
+		 else if (outs.Count > 0)
+		 {
+		   this.SemErr("async action must not have output parameters");
+		 }
+		 else
+		 {
+		   datatypeTypeCtorDecl = new DatatypeTypeCtorDecl(name, name.val, new List<TypeVariable>(), null);
+		   datatypeTypeCtorDecl.AddConstructor(name, name.val, ins.Select(v => new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type)).ToList());
+		 }
+		}
+		actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, elims, mods, datatypeTypeCtorDecl, kv);
+		
+	}
+
 	void Implementation(out Implementation/*!*/ impl) {
 		Contract.Ensures(Contract.ValueAtReturn(out impl) != null); IToken/*!*/ x;
 		List<TypeVariable>/*!*/ typeParams;
@@ -774,7 +790,7 @@ void ProcFormals(bool incoming, bool allowWhereClauses, out List<Variable>/*!*/
 		var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals";
 		
 		Expect(11);
-		if (StartOf(11)) {
+		if (StartOf(12)) {
 			AttrsIdsTypeWheres(allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); });
 		}
 		Expect(12);
@@ -823,18 +839,18 @@ void Idents(out List<IToken>/*!*/ xs) {
 
 	void Type(out Bpl.Type/*!*/ ty) {
 		Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; ty = dummyType; 
-		if (StartOf(12)) {
+		if (StartOf(13)) {
 			TypeAtom(out ty);
-		} else if (StartOf(13)) {
+		} else if (StartOf(14)) {
 			Ident(out tok);
 			List<Bpl.Type>/*!*/ args = new List<Bpl.Type> (); 
-			if (StartOf(14)) {
+			if (StartOf(15)) {
 				TypeArgs(args);
 			}
 			ty = new UnresolvedTypeIdentifier (tok, tok.val, args); 
 		} else if (la.kind == 19 || la.kind == 21) {
 			MapType(out ty);
-		} else SynErr(127);
+		} else SynErr(128);
 	}
 
 	void AttributesIdsTypeWhere(bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
@@ -893,26 +909,26 @@ void TypeAtom(out Bpl.Type/*!*/ ty) {
 			Get();
 			Type(out ty);
 			Expect(12);
-		} else SynErr(128);
+		} else SynErr(129);
 	}
 
 	void Ident(out IToken/*!*/ x) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null);
 		if (la.kind == 1) {
 			Get();
-		} else if (la.kind == 44) {
+		} else if (la.kind == 45) {
 			Get();
 			t.kind = _ident; 
-		} else if (la.kind == 43) {
+		} else if (la.kind == 44) {
 			Get();
 			t.kind = _ident; 
-		} else if (la.kind == 41) {
+		} else if (la.kind == 42) {
 			Get();
 			t.kind = _ident; 
-		} else if (la.kind == 42) {
+		} else if (la.kind == 43) {
 			Get();
 			t.kind = _ident; 
-		} else SynErr(129);
+		} else SynErr(130);
 		x = t;
 		if (x.val.StartsWith("\\"))
 		 x.val = x.val.Substring(1);
@@ -921,23 +937,23 @@ void Ident(out IToken/*!*/ x) {
 
 	void TypeArgs(List<Bpl.Type>/*!*/ ts) {
 		Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty; 
-		if (StartOf(12)) {
+		if (StartOf(13)) {
 			TypeAtom(out ty);
 			ts.Add(ty); 
-			if (StartOf(14)) {
+			if (StartOf(15)) {
 				TypeArgs(ts);
 			}
-		} else if (StartOf(13)) {
+		} else if (StartOf(14)) {
 			Ident(out tok);
 			List<Bpl.Type>/*!*/ args = new List<Bpl.Type> ();
 			ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); 
-			if (StartOf(14)) {
+			if (StartOf(15)) {
 				TypeArgs(ts);
 			}
 		} else if (la.kind == 19 || la.kind == 21) {
 			MapType(out ty);
 			ts.Add(ty); 
-		} else SynErr(130);
+		} else SynErr(131);
 	}
 
 	void MapType(out Bpl.Type/*!*/ ty) {
@@ -953,7 +969,7 @@ void MapType(out Bpl.Type/*!*/ ty) {
 		}
 		Expect(19);
 		if (tok == null) tok = t;  
-		if (StartOf(14)) {
+		if (StartOf(15)) {
 			Types(arguments);
 		}
 		Expect(20);
@@ -1021,7 +1037,7 @@ void UserDefinedType(out Declaration/*!*/ decl, QKeyValue kv) {
 		Contract.Ensures(Contract.ValueAtReturn(out decl) != null); IToken/*!*/ id; List<IToken>/*!*/ paramTokens = new List<IToken> ();
 		Bpl.Type/*!*/ body = dummyType; bool synonym = false; 
 		Ident(out id);
-		if (StartOf(13)) {
+		if (StartOf(14)) {
 			WhiteSpaceIdents(out paramTokens);
 		}
 		if (la.kind == 32) {
@@ -1045,7 +1061,7 @@ void WhiteSpaceIdents(out List<IToken>/*!*/ xs) {
 		Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>(); 
 		Ident(out id);
 		xs.Add(id); 
-		while (StartOf(13)) {
+		while (StartOf(14)) {
 			Ident(out id);
 			xs.Add(id); 
 		}
@@ -1063,7 +1079,7 @@ void Constructor(DatatypeTypeCtorDecl datatypeTypeCtorDecl) {
 		IToken name; List<TypedIdent> fields = new List<TypedIdent>(); 
 		Ident(out name);
 		Expect(11);
-		if (StartOf(13)) {
+		if (StartOf(14)) {
 			IdsTypeWheres(false, "datatype constructor", delegate(TypedIdent ti) { fields.Add(ti); });
 		}
 		Expect(12);
@@ -1086,31 +1102,31 @@ void Invariant(List<Requires> invariants) {
 	}
 
 	void MoverQualifier(ref MoverType moverType) {
-		if (la.kind == 41) {
+		if (la.kind == 42) {
 			Get();
 			moverType = MoverType.Left; 
-		} else if (la.kind == 42) {
+		} else if (la.kind == 43) {
 			Get();
 			moverType = MoverType.Right; 
-		} else if (la.kind == 43) {
+		} else if (la.kind == 44) {
 			Get();
 			moverType = MoverType.Both; 
-		} else if (la.kind == 44) {
+		} else if (la.kind == 45) {
 			Get();
 			moverType = MoverType.Atomic; 
-		} else SynErr(131);
+		} else SynErr(132);
 	}
 
 	void SpecAction(ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction, List<IdentifierExpr> mods, List<ActionDeclRef> creates, List<ElimDecl> elims) {
-		if (la.kind == 40) {
+		if (la.kind == 41) {
 			SpecRefinedAction(ref refinedAction, ref invariantAction);
-		} else if (la.kind == 49) {
+		} else if (la.kind == 50) {
 			SpecModifies(mods);
-		} else if (la.kind == 37) {
+		} else if (la.kind == 38) {
 			SpecCreates(creates);
-		} else if (la.kind == 39) {
+		} else if (la.kind == 40) {
 			SpecEliminates(elims);
-		} else SynErr(132);
+		} else SynErr(133);
 	}
 
 	void ImplBody(out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) {
@@ -1123,7 +1139,7 @@ void ImplBody(out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) {
 	}
 
 	void SpecCreates(List<ActionDeclRef> creates) {
-		Expect(37);
+		Expect(38);
 		List<IToken> cs; 
 		Idents(out cs);
 		foreach(IToken c in cs) { creates.Add(new ActionDeclRef(c, c.val)); } 
@@ -1134,7 +1150,7 @@ void SpecUsing(List<ElimDecl> elims) {
 		IToken name, tok; ActionDeclRef target, abstraction; 
 		Ident(out name);
 		target = new ActionDeclRef(name, name.val); 
-		Expect(38);
+		Expect(39);
 		tok = t; 
 		Ident(out name);
 		abstraction = new ActionDeclRef(name, name.val); 
@@ -1142,7 +1158,7 @@ void SpecUsing(List<ElimDecl> elims) {
 	}
 
 	void SpecEliminates(List<ElimDecl> elims) {
-		Expect(39);
+		Expect(40);
 		SpecUsing(elims);
 		while (la.kind == 14) {
 			Get();
@@ -1152,7 +1168,7 @@ void SpecEliminates(List<ElimDecl> elims) {
 	}
 
 	void SpecRefinedAction(ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction) {
-		Expect(40);
+		Expect(41);
 		IToken m; 
 		Ident(out m);
 		if (refinedAction == null) {
@@ -1161,7 +1177,7 @@ void SpecRefinedAction(ref ActionDeclRef refinedAction, ref ActionDeclRef invari
 		 this.SemErr("a refines specification already exists");
 		}
 		
-		if (la.kind == 38) {
+		if (la.kind == 39) {
 			Get();
 			Ident(out m);
 			invariantAction = new ActionDeclRef(m, m.val); 
@@ -1171,8 +1187,8 @@ void SpecRefinedAction(ref ActionDeclRef refinedAction, ref ActionDeclRef invari
 
 	void SpecModifies(List<IdentifierExpr> mods) {
 		List<IToken> ms; 
-		Expect(49);
-		if (StartOf(13)) {
+		Expect(50);
+		if (StartOf(14)) {
 			Idents(out ms);
 			foreach(IToken m in ms) { mods.Add(new IdentifierExpr(m, m.val)); } 
 		}
@@ -1181,7 +1197,7 @@ void SpecModifies(List<IdentifierExpr> mods) {
 
 	void SpecYieldPrePost(ref ActionDeclRef refinedAction, List<Requires> pre, List<Ensures> post, List<CallCmd> yieldRequires, List<CallCmd> yieldEnsures, List<CallCmd> yieldPreserves, List<IdentifierExpr> mods) {
 		Expr e; Cmd cmd; Token tok = null; QKeyValue kv = null; 
-		if (la.kind == 40) {
+		if (la.kind == 41) {
 			Get();
 			IToken m; 
 			Ident(out m);
@@ -1191,45 +1207,45 @@ void SpecYieldPrePost(ref ActionDeclRef refinedAction, List<Requires> pre, List<
 			 this.SemErr("a refines specification already exists");
 			}
 			
-		} else if (la.kind == 46) {
+		} else if (la.kind == 47) {
 			Get();
 			tok = t; 
-			if (StartOf(15)) {
+			if (StartOf(16)) {
 				while (la.kind == 26) {
 					Attribute(ref kv);
 				}
 				Proposition(out e);
 				pre.Add(new Requires(tok, false, e, null, kv)); 
-			} else if (la.kind == 35 || la.kind == 52 || la.kind == 65) {
+			} else if (la.kind == 36 || la.kind == 52 || la.kind == 65) {
 				CallCmd(out cmd);
 				yieldRequires.Add((CallCmd)cmd); 
-			} else SynErr(133);
-		} else if (la.kind == 47) {
+			} else SynErr(134);
+		} else if (la.kind == 48) {
 			Get();
 			tok = t; 
-			if (StartOf(15)) {
+			if (StartOf(16)) {
 				while (la.kind == 26) {
 					Attribute(ref kv);
 				}
 				Proposition(out e);
 				post.Add(new Ensures(tok, false, e, null, kv)); 
-			} else if (la.kind == 35 || la.kind == 52 || la.kind == 65) {
+			} else if (la.kind == 36 || la.kind == 52 || la.kind == 65) {
 				CallCmd(out cmd);
 				yieldEnsures.Add((CallCmd)cmd); 
-			} else SynErr(134);
-		} else if (la.kind == 48) {
+			} else SynErr(135);
+		} else if (la.kind == 49) {
 			Get();
 			tok = t; 
 			CallCmd(out cmd);
 			yieldPreserves.Add((CallCmd)cmd); 
-		} else if (la.kind == 49) {
+		} else if (la.kind == 50) {
 			Get();
 			List<IToken> ms; 
-			if (StartOf(13)) {
+			if (StartOf(14)) {
 				Idents(out ms);
 				foreach(IToken m in ms) { mods.Add(new IdentifierExpr(m, m.val)); } 
 			}
-		} else SynErr(135);
+		} else SynErr(136);
 		Expect(10);
 	}
 
@@ -1240,7 +1256,7 @@ void CallCmd(out Cmd c) {
 		bool isFree = false;
 		c = null;
 		
-		if (la.kind == 35) {
+		if (la.kind == 36) {
 			Get();
 			isAsync = true; 
 		}
@@ -1274,19 +1290,19 @@ void ProcSignature(bool allowWhereClausesOnFormals, out IToken/*!*/ name, out Li
 	}
 
 	void Spec(List<Requires> pre, List<IdentifierExpr> mods, List<Ensures> post) {
-		if (la.kind == 49) {
+		if (la.kind == 50) {
 			SpecModifies(mods);
 		} else if (la.kind == 52) {
 			Get();
 			SpecPrePost(true, pre, post);
-		} else if (la.kind == 46 || la.kind == 47) {
+		} else if (la.kind == 47 || la.kind == 48) {
 			SpecPrePost(false, pre, post);
-		} else SynErr(136);
+		} else SynErr(137);
 	}
 
 	void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
 		Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; 
-		if (la.kind == 46) {
+		if (la.kind == 47) {
 			Get();
 			tok = t; 
 			while (la.kind == 26) {
@@ -1295,7 +1311,7 @@ void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
 			Proposition(out e);
 			Expect(10);
 			pre.Add(new Requires(tok, free, e, null, kv)); 
-		} else if (la.kind == 47) {
+		} else if (la.kind == 48) {
 			Get();
 			tok = t; 
 			while (la.kind == 26) {
@@ -1304,7 +1320,7 @@ void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
 			Proposition(out e);
 			Expect(10);
 			post.Add(new Ensures(tok, free, e, null, kv)); 
-		} else SynErr(137);
+		} else SynErr(138);
 	}
 
 	void StmtList(out StmtList/*!*/ stmtList) {
@@ -1317,8 +1333,8 @@ void StmtList(out StmtList/*!*/ stmtList) {
 		StructuredCmd ec = null;  StructuredCmd/*!*/ ecn;
 		TransferCmd tc = null;  TransferCmd/*!*/ tcn;
 		
-		while (StartOf(16)) {
-			if (StartOf(17)) {
+		while (StartOf(17)) {
+			if (StartOf(18)) {
 				LabelOrCmd(out c, out label);
 				Contract.Assert(c == null || label == null);
 				if (c != null) {
@@ -1384,7 +1400,7 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 		QKeyValue kv = null;
 		
 		switch (la.kind) {
-		case 1: case 41: case 42: case 43: case 44: {
+		case 1: case 42: case 43: case 44: case 45: {
 			LabelOrAssign(out c, out label);
 			break;
 		}
@@ -1424,7 +1440,7 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 			
 			break;
 		}
-		case 35: case 52: case 65: {
+		case 36: case 52: case 65: {
 			CallCmd(out cn);
 			Expect(10);
 			c = cn; 
@@ -1435,7 +1451,7 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 			c = cn; 
 			break;
 		}
-		default: SynErr(138); break;
+		default: SynErr(139); break;
 		}
 	}
 
@@ -1452,7 +1468,7 @@ void StructuredCmd(out StructuredCmd/*!*/ ec) {
 		} else if (la.kind == 59) {
 			BreakCmd(out bcmd);
 			ec = bcmd; 
-		} else SynErr(139);
+		} else SynErr(140);
 	}
 
 	void TransferCmd(out TransferCmd/*!*/ tc) {
@@ -1472,7 +1488,7 @@ void TransferCmd(out TransferCmd/*!*/ tc) {
 		} else if (la.kind == 54) {
 			Get();
 			tc = new ReturnCmd(t); 
-		} else SynErr(140);
+		} else SynErr(141);
 		Expect(10);
 	}
 
@@ -1497,7 +1513,7 @@ void IfCmd(out IfCmd/*!*/ ifcmd) {
 				Get();
 				StmtList(out els);
 				elseOption = els; 
-			} else SynErr(141);
+			} else SynErr(142);
 		}
 		ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); 
 	}
@@ -1524,7 +1540,7 @@ void WhileCmd(out WhileCmd wcmd) {
 			while (la.kind == 26) {
 				Attribute(ref kv);
 			}
-			if (StartOf(18)) {
+			if (StartOf(19)) {
 				Expression(out e);
 				if (isFree) {
 				 invariants.Add(new AssumeCmd(z, e, kv));
@@ -1533,10 +1549,10 @@ void WhileCmd(out WhileCmd wcmd) {
 				}
 				kv = null;
 				
-			} else if (la.kind == 35 || la.kind == 52 || la.kind == 65) {
+			} else if (la.kind == 36 || la.kind == 52 || la.kind == 65) {
 				CallCmd(out cmd);
 				yields.Add((CallCmd)cmd); 
-			} else SynErr(142);
+			} else SynErr(143);
 			Expect(10);
 		}
 		Expect(26);
@@ -1550,7 +1566,7 @@ void BreakCmd(out BreakCmd/*!*/ bcmd) {
 		
 		Expect(59);
 		x = t; 
-		if (StartOf(13)) {
+		if (StartOf(14)) {
 			Ident(out y);
 			breakLabel = y.val; 
 		}
@@ -1564,10 +1580,10 @@ void Guard(out Expr e) {
 		if (la.kind == 58) {
 			Get();
 			e = null; 
-		} else if (StartOf(18)) {
+		} else if (StartOf(19)) {
 			Expression(out ee);
 			e = ee; 
-		} else SynErr(143);
+		} else SynErr(144);
 		Expect(12);
 	}
 
@@ -1602,7 +1618,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
 			Expect(10);
 			c = new UnpackCmd(x, lhsExpr, e0, kv);
 			
-		} else if (StartOf(19)) {
+		} else if (StartOf(20)) {
 			lhss = new List<AssignLhs/*!*/>(); 
 			lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); 
 			while (la.kind == 19 || la.kind == 64) {
@@ -1645,7 +1661,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
 			}
 			Expect(10);
 			c = new AssignCmd(x, lhss, rhss, kv); 
-		} else SynErr(144);
+		} else SynErr(145);
 	}
 
 	void ParCallCmd(out Cmd d) {
@@ -1673,7 +1689,7 @@ void MapAssignIndex(out IToken/*!*/ x, out List<Expr/*!*/>/*!*/ indexes) {
 		
 		Expect(19);
 		x = t; 
-		if (StartOf(18)) {
+		if (StartOf(19)) {
 			Expression(out e);
 			indexes.Add(e); 
 			while (la.kind == 14) {
@@ -1708,7 +1724,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) {
 		Ident(out first);
 		if (la.kind == 11) {
 			Get();
-			if (StartOf(18)) {
+			if (StartOf(19)) {
 				Expression(out en);
 				es.Add(en); 
 				while (la.kind == 14) {
@@ -1734,7 +1750,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) {
 			Expect(63);
 			Ident(out first);
 			Expect(11);
-			if (StartOf(18)) {
+			if (StartOf(19)) {
 				Expression(out en);
 				es.Add(en); 
 				while (la.kind == 14) {
@@ -1745,7 +1761,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) {
 			}
 			Expect(12);
 			c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; 
-		} else SynErr(145);
+		} else SynErr(146);
 	}
 
 	void Expressions(out List<Expr>/*!*/ es) {
@@ -1762,7 +1778,7 @@ void Expressions(out List<Expr>/*!*/ es) {
 	void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		LogicalExpression(out e0);
-		if (StartOf(20)) {
+		if (StartOf(21)) {
 			if (la.kind == 70 || la.kind == 71) {
 				ImpliesOp();
 				x = t; 
@@ -1790,13 +1806,13 @@ void EquivOp() {
 			Get();
 		} else if (la.kind == 69) {
 			Get();
-		} else SynErr(146);
+		} else SynErr(147);
 	}
 
 	void LogicalExpression(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		RelationalExpression(out e0);
-		if (StartOf(21)) {
+		if (StartOf(22)) {
 			if (la.kind == 74 || la.kind == 75) {
 				AndOp();
 				x = t; 
@@ -1828,7 +1844,7 @@ void ImpliesOp() {
 			Get();
 		} else if (la.kind == 71) {
 			Get();
-		} else SynErr(147);
+		} else SynErr(148);
 	}
 
 	void ExpliesOp() {
@@ -1836,13 +1852,13 @@ void ExpliesOp() {
 			Get();
 		} else if (la.kind == 73) {
 			Get();
-		} else SynErr(148);
+		} else SynErr(149);
 	}
 
 	void RelationalExpression(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; 
 		BvTerm(out e0);
-		if (StartOf(22)) {
+		if (StartOf(23)) {
 			RelOp(out x, out op);
 			BvTerm(out e1);
 			e0 = Expr.Binary(x, op, e0, e1); 
@@ -1854,7 +1870,7 @@ void AndOp() {
 			Get();
 		} else if (la.kind == 75) {
 			Get();
-		} else SynErr(149);
+		} else SynErr(150);
 	}
 
 	void OrOp() {
@@ -1862,7 +1878,7 @@ void OrOp() {
 			Get();
 		} else if (la.kind == 77) {
 			Get();
-		} else SynErr(150);
+		} else SynErr(151);
 	}
 
 	void BvTerm(out Expr/*!*/ e0) {
@@ -1924,7 +1940,7 @@ void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 			x = t; op=BinaryOperator.Opcode.Ge; 
 			break;
 		}
-		default: SynErr(151); break;
+		default: SynErr(152); break;
 		}
 	}
 
@@ -1941,7 +1957,7 @@ void Term(out Expr/*!*/ e0) {
 	void Factor(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; 
 		Power(out e0);
-		while (StartOf(23)) {
+		while (StartOf(24)) {
 			MulOp(out x, out op);
 			Power(out e1);
 			e0 = Expr.Binary(x, op, e0, e1); 
@@ -1956,7 +1972,7 @@ void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 		} else if (la.kind == 87) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Sub; 
-		} else SynErr(152);
+		} else SynErr(153);
 	}
 
 	void Power(out Expr/*!*/ e0) {
@@ -1984,7 +2000,7 @@ void MulOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 		} else if (la.kind == 90) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.RealDiv; 
-		} else SynErr(153);
+		} else SynErr(154);
 	}
 
 	void IsConstructor(out Expr/*!*/ e0) {
@@ -2014,9 +2030,9 @@ void UnaryExpression(out Expr/*!*/ e) {
 			x = t; 
 			UnaryExpression(out e);
 			e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); 
-		} else if (StartOf(24)) {
+		} else if (StartOf(25)) {
 			CoercionExpression(out e);
-		} else SynErr(154);
+		} else SynErr(155);
 	}
 
 	void NegOp() {
@@ -2024,7 +2040,7 @@ void NegOp() {
 			Get();
 		} else if (la.kind == 94) {
 			Get();
-		} else SynErr(155);
+		} else SynErr(156);
 	}
 
 	void CoercionExpression(out Expr/*!*/ e) {
@@ -2036,7 +2052,7 @@ void CoercionExpression(out Expr/*!*/ e) {
 		while (la.kind == 13) {
 			Get();
 			x = t; 
-			if (StartOf(14)) {
+			if (StartOf(15)) {
 				Type(out coercedTo);
 				e = Expr.CoerceType(x, e, coercedTo); 
 			} else if (la.kind == 3) {
@@ -2048,7 +2064,7 @@ void CoercionExpression(out Expr/*!*/ e) {
 				 e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
 				}
 				
-			} else SynErr(156);
+			} else SynErr(157);
 		}
 	}
 
@@ -2066,8 +2082,8 @@ void ArrayExpression(out Expr/*!*/ e) {
 				x = t; allArgs = new List<Expr> ();
 				allArgs.Add(e);
 				store = false; bvExtract = false; 
-				if (StartOf(25)) {
-					if (StartOf(18)) {
+				if (StartOf(26)) {
+					if (StartOf(19)) {
 						Expression(out index0);
 						if (index0 is BvBounds)
 						 bvExtract = true;
@@ -2109,7 +2125,7 @@ void ArrayExpression(out Expr/*!*/ e) {
 			} else {
 				Get();
 				x = t; 
-				if (StartOf(13)) {
+				if (StartOf(14)) {
 					Ident(out id);
 					e = new NAryExpr(x, new FieldAccess(id, id.val), new List<Expr> { e }); 
 				} else if (la.kind == 11) {
@@ -2120,7 +2136,7 @@ void ArrayExpression(out Expr/*!*/ e) {
 					Expression(out e1);
 					Expect(12);
 					e = new NAryExpr(x, new FieldUpdate(id, id.val), new List<Expr> { e, e1 }); 
-				} else SynErr(157);
+				} else SynErr(158);
 			}
 		}
 	}
@@ -2227,17 +2243,17 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new LiteralExpr(t, t.val.Trim('"')); 
 			break;
 		}
-		case 1: case 41: case 42: case 43: case 44: {
+		case 1: case 42: case 43: case 44: case 45: {
 			Ident(out x);
 			id = new IdentifierExpr(x, x.val);  e = id; 
 			if (la.kind == 11) {
 				Get();
-				if (StartOf(18)) {
+				if (StartOf(19)) {
 					Expressions(out es);
 					e = new NAryExpr(x, new FunctionCall(id), es); 
 				} else if (la.kind == 12) {
 					e = new NAryExpr(x, new FunctionCall(id), new List<Expr>()); 
-				} else SynErr(158);
+				} else SynErr(159);
 				Expect(12);
 			}
 			break;
@@ -2271,7 +2287,7 @@ void AtomExpression(out Expr/*!*/ e) {
 		}
 		case 11: {
 			Get();
-			if (StartOf(18)) {
+			if (StartOf(19)) {
 				Expression(out e);
 				if (e is BvBounds)
 				 this.SemErr("parentheses around bitvector bounds are not allowed"); 
@@ -2297,7 +2313,7 @@ void AtomExpression(out Expr/*!*/ e) {
 				 e = new LambdaExpr(x, typeParams, ds, kv, e); 
 			} else if (la.kind == 9) {
 				LetExpr(out e);
-			} else SynErr(159);
+			} else SynErr(160);
 			Expect(12);
 			break;
 		}
@@ -2310,7 +2326,7 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new CodeExpr(locals, blocks); 
 			break;
 		}
-		default: SynErr(160); break;
+		default: SynErr(161); break;
 		}
 	}
 
@@ -2322,7 +2338,7 @@ void Dec(out BigDec n) {
 		} else if (la.kind == 6) {
 			Get();
 			s = t.val; 
-		} else SynErr(161);
+		} else SynErr(162);
 		try {
 		 n = BigDec.FromString(s);
 		} catch (FormatException) {
@@ -2366,7 +2382,7 @@ void Forall() {
 			Get();
 		} else if (la.kind == 112) {
 			Get();
-		} else SynErr(162);
+		} else SynErr(163);
 	}
 
 	void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds,
@@ -2379,12 +2395,12 @@ void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out L
 		
 		if (la.kind == 21) {
 			TypeParams(out tok, out typeParams);
-			if (StartOf(11)) {
+			if (StartOf(12)) {
 				BoundVars(out ds);
 			}
-		} else if (StartOf(11)) {
+		} else if (StartOf(12)) {
 			BoundVars(out ds);
-		} else SynErr(163);
+		} else SynErr(164);
 		QSep();
 		while (la.kind == 26) {
 			AttributeOrTrigger(ref kv, ref trig);
@@ -2397,7 +2413,7 @@ void Exists() {
 			Get();
 		} else if (la.kind == 114) {
 			Get();
-		} else SynErr(164);
+		} else SynErr(165);
 	}
 
 	void Lambda() {
@@ -2405,7 +2421,7 @@ void Lambda() {
 			Get();
 		} else if (la.kind == 116) {
 			Get();
-		} else SynErr(165);
+		} else SynErr(166);
 	}
 
 	void LetExpr(out Expr/*!*/ letexpr) {
@@ -2467,7 +2483,7 @@ void CodeExpression(out List<Variable>/*!*/ locals, out List<Block/*!*/>/*!*/ bl
 		}
 		SpecBlock(out b);
 		blocks.Add(b); 
-		while (StartOf(13)) {
+		while (StartOf(14)) {
 			SpecBlock(out b);
 			blocks.Add(b); 
 		}
@@ -2485,7 +2501,7 @@ void SpecBlock(out Block/*!*/ b) {
 		
 		Ident(out x);
 		Expect(13);
-		while (StartOf(17)) {
+		while (StartOf(18)) {
 			LabelOrCmd(out c, out label);
 			Contract.Assert(c == null || label == null);
 			if (c != null) {
@@ -2508,7 +2524,7 @@ void SpecBlock(out Block/*!*/ b) {
 			Get();
 			Expression(out e);
 			b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); 
-		} else SynErr(166);
+		} else SynErr(167);
 		Expect(10);
 	}
 
@@ -2523,7 +2539,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
 			Get();
 			Expect(1);
 			key = t.val;  parameters = new List<object/*!*/>(); 
-			if (StartOf(18)) {
+			if (StartOf(19)) {
 				AttributeParameter(out param);
 				parameters.Add(param); 
 				while (la.kind == 14) {
@@ -2551,7 +2567,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
 			 }
 			}
 			
-		} else if (StartOf(18)) {
+		} else if (StartOf(19)) {
 			Expression(out e);
 			es = new List<Expr> { e }; 
 			while (la.kind == 14) {
@@ -2565,7 +2581,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
 			 trig.AddLast(new Trigger(tok, true, es, null));
 			}
 			
-		} else SynErr(167);
+		} else SynErr(168);
 		Expect(27);
 	}
 
@@ -2577,10 +2593,10 @@ void AttributeParameter(out object/*!*/ o) {
 		if (la.kind == 4) {
 			Get();
 			o = t.val.Substring(1, t.val.Length-2); 
-		} else if (StartOf(18)) {
+		} else if (StartOf(19)) {
 			Expression(out e);
 			o = e; 
-		} else SynErr(168);
+		} else SynErr(169);
 	}
 
 	void QSep() {
@@ -2588,7 +2604,7 @@ void QSep() {
 			Get();
 		} else if (la.kind == 118) {
 			Get();
-		} else SynErr(169);
+		} else SynErr(170);
 	}
 
 	void LetVar(out Variable/*!*/ v) {
@@ -2618,31 +2634,32 @@ public void Parse() {
 
 	static readonly bool[,]/*!*/ set = {
 		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_T,_T, _x,_T,_x,_T, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_T,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_T,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_T,_T, _x,_T,_x,_T, _T,_T,_x,_x, _x,_x,_T,_T, _T,_T,_T,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_T, _T,_T,_T,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_T, _T,_T,_T,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}
+		{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}
 
 	};
 } // end Parser
@@ -2702,22 +2719,22 @@ string GetSyntaxErrorString(int n) {
 			case 32: s = "\"=\" expected"; break;
 			case 33: s = "\"datatype\" expected"; break;
 			case 34: s = "\"invariant\" expected"; break;
-			case 35: s = "\"async\" expected"; break;
-			case 36: s = "\"action\" expected"; break;
-			case 37: s = "\"creates\" expected"; break;
-			case 38: s = "\"using\" expected"; break;
-			case 39: s = "\"eliminates\" expected"; break;
-			case 40: s = "\"refines\" expected"; break;
-			case 41: s = "\"left\" expected"; break;
-			case 42: s = "\"right\" expected"; break;
-			case 43: s = "\"both\" expected"; break;
-			case 44: s = "\"atomic\" expected"; break;
-			case 45: s = "\"procedure\" expected"; break;
-			case 46: s = "\"requires\" expected"; break;
-			case 47: s = "\"ensures\" expected"; break;
-			case 48: s = "\"preserves\" expected"; break;
-			case 49: s = "\"modifies\" expected"; break;
-			case 50: s = "\"pure\" expected"; break;
+			case 35: s = "\"pure\" expected"; break;
+			case 36: s = "\"async\" expected"; break;
+			case 37: s = "\"action\" expected"; break;
+			case 38: s = "\"creates\" expected"; break;
+			case 39: s = "\"using\" expected"; break;
+			case 40: s = "\"eliminates\" expected"; break;
+			case 41: s = "\"refines\" expected"; break;
+			case 42: s = "\"left\" expected"; break;
+			case 43: s = "\"right\" expected"; break;
+			case 44: s = "\"both\" expected"; break;
+			case 45: s = "\"atomic\" expected"; break;
+			case 46: s = "\"procedure\" expected"; break;
+			case 47: s = "\"requires\" expected"; break;
+			case 48: s = "\"ensures\" expected"; break;
+			case 49: s = "\"preserves\" expected"; break;
+			case 50: s = "\"modifies\" expected"; break;
 			case 51: s = "\"implementation\" expected"; break;
 			case 52: s = "\"free\" expected"; break;
 			case 53: s = "\"goto\" expected"; break;
@@ -2788,55 +2805,56 @@ string GetSyntaxErrorString(int n) {
 			case 118: s = "\"\\u2022\" expected"; break;
 			case 119: s = "??? expected"; break;
 			case 120: s = "invalid BoogiePL"; break;
-			case 121: s = "invalid Consts"; break;
-			case 122: s = "invalid Function"; break;
+			case 121: s = "invalid BoogiePL"; break;
+			case 122: s = "invalid Consts"; break;
 			case 123: s = "invalid Function"; break;
-			case 124: s = "invalid ActionDecl"; break;
+			case 124: s = "invalid Function"; break;
 			case 125: s = "invalid YieldProcedureDecl"; break;
 			case 126: s = "invalid Procedure"; break;
-			case 127: s = "invalid Type"; break;
-			case 128: s = "invalid TypeAtom"; break;
-			case 129: s = "invalid Ident"; break;
-			case 130: s = "invalid TypeArgs"; break;
-			case 131: s = "invalid MoverQualifier"; break;
-			case 132: s = "invalid SpecAction"; break;
-			case 133: s = "invalid SpecYieldPrePost"; break;
+			case 127: s = "invalid ActionDecl"; break;
+			case 128: s = "invalid Type"; break;
+			case 129: s = "invalid TypeAtom"; break;
+			case 130: s = "invalid Ident"; break;
+			case 131: s = "invalid TypeArgs"; break;
+			case 132: s = "invalid MoverQualifier"; break;
+			case 133: s = "invalid SpecAction"; break;
 			case 134: s = "invalid SpecYieldPrePost"; break;
 			case 135: s = "invalid SpecYieldPrePost"; break;
-			case 136: s = "invalid Spec"; break;
-			case 137: s = "invalid SpecPrePost"; break;
-			case 138: s = "invalid LabelOrCmd"; break;
-			case 139: s = "invalid StructuredCmd"; break;
-			case 140: s = "invalid TransferCmd"; break;
-			case 141: s = "invalid IfCmd"; break;
-			case 142: s = "invalid WhileCmd"; break;
-			case 143: s = "invalid Guard"; break;
-			case 144: s = "invalid LabelOrAssign"; break;
-			case 145: s = "invalid CallParams"; break;
-			case 146: s = "invalid EquivOp"; break;
-			case 147: s = "invalid ImpliesOp"; break;
-			case 148: s = "invalid ExpliesOp"; break;
-			case 149: s = "invalid AndOp"; break;
-			case 150: s = "invalid OrOp"; break;
-			case 151: s = "invalid RelOp"; break;
-			case 152: s = "invalid AddOp"; break;
-			case 153: s = "invalid MulOp"; break;
-			case 154: s = "invalid UnaryExpression"; break;
-			case 155: s = "invalid NegOp"; break;
-			case 156: s = "invalid CoercionExpression"; break;
-			case 157: s = "invalid ArrayExpression"; break;
-			case 158: s = "invalid AtomExpression"; break;
+			case 136: s = "invalid SpecYieldPrePost"; break;
+			case 137: s = "invalid Spec"; break;
+			case 138: s = "invalid SpecPrePost"; break;
+			case 139: s = "invalid LabelOrCmd"; break;
+			case 140: s = "invalid StructuredCmd"; break;
+			case 141: s = "invalid TransferCmd"; break;
+			case 142: s = "invalid IfCmd"; break;
+			case 143: s = "invalid WhileCmd"; break;
+			case 144: s = "invalid Guard"; break;
+			case 145: s = "invalid LabelOrAssign"; break;
+			case 146: s = "invalid CallParams"; break;
+			case 147: s = "invalid EquivOp"; break;
+			case 148: s = "invalid ImpliesOp"; break;
+			case 149: s = "invalid ExpliesOp"; break;
+			case 150: s = "invalid AndOp"; break;
+			case 151: s = "invalid OrOp"; break;
+			case 152: s = "invalid RelOp"; break;
+			case 153: s = "invalid AddOp"; break;
+			case 154: s = "invalid MulOp"; break;
+			case 155: s = "invalid UnaryExpression"; break;
+			case 156: s = "invalid NegOp"; break;
+			case 157: s = "invalid CoercionExpression"; break;
+			case 158: s = "invalid ArrayExpression"; break;
 			case 159: s = "invalid AtomExpression"; break;
 			case 160: s = "invalid AtomExpression"; break;
-			case 161: s = "invalid Dec"; break;
-			case 162: s = "invalid Forall"; break;
-			case 163: s = "invalid QuantifierBody"; break;
-			case 164: s = "invalid Exists"; break;
-			case 165: s = "invalid Lambda"; break;
-			case 166: s = "invalid SpecBlock"; break;
-			case 167: s = "invalid AttributeOrTrigger"; break;
-			case 168: s = "invalid AttributeParameter"; break;
-			case 169: s = "invalid QSep"; break;
+			case 161: s = "invalid AtomExpression"; break;
+			case 162: s = "invalid Dec"; break;
+			case 163: s = "invalid Forall"; break;
+			case 164: s = "invalid QuantifierBody"; break;
+			case 165: s = "invalid Exists"; break;
+			case 166: s = "invalid Lambda"; break;
+			case 167: s = "invalid SpecBlock"; break;
+			case 168: s = "invalid AttributeOrTrigger"; break;
+			case 169: s = "invalid AttributeParameter"; break;
+			case 170: s = "invalid QSep"; break;
 
 			default: s = "error " + n; break;
 		}
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index 484eb98c4..6f2bcdabc 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -528,22 +528,22 @@ void CheckLiteral() {
 			case "type": t.kind = 31; break;
 			case "datatype": t.kind = 33; break;
 			case "invariant": t.kind = 34; break;
-			case "async": t.kind = 35; break;
-			case "action": t.kind = 36; break;
-			case "creates": t.kind = 37; break;
-			case "using": t.kind = 38; break;
-			case "eliminates": t.kind = 39; break;
-			case "refines": t.kind = 40; break;
-			case "left": t.kind = 41; break;
-			case "right": t.kind = 42; break;
-			case "both": t.kind = 43; break;
-			case "atomic": t.kind = 44; break;
-			case "procedure": t.kind = 45; break;
-			case "requires": t.kind = 46; break;
-			case "ensures": t.kind = 47; break;
-			case "preserves": t.kind = 48; break;
-			case "modifies": t.kind = 49; break;
-			case "pure": t.kind = 50; break;
+			case "pure": t.kind = 35; break;
+			case "async": t.kind = 36; break;
+			case "action": t.kind = 37; break;
+			case "creates": t.kind = 38; break;
+			case "using": t.kind = 39; break;
+			case "eliminates": t.kind = 40; break;
+			case "refines": t.kind = 41; break;
+			case "left": t.kind = 42; break;
+			case "right": t.kind = 43; break;
+			case "both": t.kind = 44; break;
+			case "atomic": t.kind = 45; break;
+			case "procedure": t.kind = 46; break;
+			case "requires": t.kind = 47; break;
+			case "ensures": t.kind = 48; break;
+			case "preserves": t.kind = 49; break;
+			case "modifies": t.kind = 50; break;
 			case "implementation": t.kind = 51; break;
 			case "free": t.kind = 52; break;
 			case "goto": t.kind = 53; break;
diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl
index 0489673df..bd248ef1e 100644
--- a/Source/Core/base.bpl
+++ b/Source/Core/base.bpl
@@ -246,7 +246,7 @@ function {:inline} Map_Swap<T,U>(a: Map T U, t1: T, t2: T): Map T U
     (var u1, u2 := Map_At(a, t1), Map_At(a, t2); Map_Update(Map_Update(a, t1, u2), t2, u1))
 }
 
-/// linear maps
+/// linear heaps
 type Ref _;
 procedure Ref_Alloc<V>() returns (k: Lval (Ref V));
 
@@ -265,13 +265,13 @@ function {:inline} Lheap_Contains<V>(l: Lheap V, k: Ref V): bool {
 function {:inline} Lheap_Deref<V>(l: Lheap V, k: Ref V): V {
     l->val[k]
 }
-procedure Lheap_Empty<V>() returns (l: Lheap V);
-procedure Lheap_Split<V>(k: [Ref V]bool, path: Lheap V) returns (l: Lheap V);
-procedure Lheap_Transfer<V>({:linear_in} path1: Lheap V, path2: Lheap V);
-procedure Lheap_Read<V>(path: V) returns (v: V);
-procedure Lheap_Write<V>(path: V, v: V);
-procedure Lheap_Alloc<V>(path: Lheap V, v: V) returns (k: Lval (Ref V));
-procedure Lheap_Remove<V>(path: Lheap V, k: Ref V) returns (v: V);
+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_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_Remove<V>(path: Lheap V, k: Ref V) returns (v: V);
 
 /// linear sets
 datatype Lset<V> { Lset(dom: [V]bool) }
@@ -282,9 +282,9 @@ function {:inline} Lset_Collector<V>(l: Lset V): [V]bool {
 function {:inline} Lset_Contains<V>(l: Lset V, k: V): bool {
     l->dom[k]
 }
-procedure Lset_Empty<V>() returns (l: Lset V);
-procedure Lset_Split<V>({:linear_out} k: Lset V, path: Lset V);
-procedure Lset_Transfer<V>({:linear_in} path1: Lset V, path2: Lset V);
+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);
 
 /// linear vals
 datatype Lval<V> { Lval(val: V) }
@@ -292,10 +292,15 @@ datatype Lval<V> { Lval(val: V) }
 function {:inline} Lval_Collector<V>(l: Lval V): [V]bool {
     MapConst(false)[l->val := true]
 }
-procedure Lval_Split<V>({:linear_out} k: Lval V, path: Lset V);
-procedure Lval_Transfer<V>({:linear_in} l: Lval V, path: Lset V);
+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);
 
 procedure create_async<T>(PA: T);
 procedure create_asyncs<T>(PAs: [T]bool);
 procedure create_multi_asyncs<T>(PAs: [T]int);
 procedure set_choice<T>(choice: T);
+
+pure procedure {:inline 1} Copy<T>(v: T) returns (copy_v: T)
+{
+  copy_v := v;
+}
diff --git a/Test/civl/async/2pc.bpl b/Test/civl/async/2pc.bpl
index c611da537..530092718 100644
--- a/Test/civl/async/2pc.bpl
+++ b/Test/civl/async/2pc.bpl
@@ -180,16 +180,6 @@ requires call YieldConsistent_10();
 // ###########################################################################
 // Event Handlers
 
-action {:layer 8} GhostRead_8() returns (snapshot: GState)
-{
-   snapshot := state;
-}
-
-action {:layer 10} GhostRead_10() returns (snapshot: GState)
-{
-   snapshot := state;
-}
-
 atomic action {:layer 11} atomic_Coordinator_TransactionReq () returns (xid: Xid)
 modifies state;
 {
@@ -211,7 +201,7 @@ preserves call YieldConsistent_10();
   var i : Mid;
 
   call xid, pairs := AllocateXid();
-  call snapshot := GhostRead_10();
+  call {:layer 10} snapshot := Copy(state);
   i := 1;
   while (i <= numParticipants)
   invariant {:layer 8} Inv_8(state, B, votes);
@@ -287,7 +277,7 @@ requires call YieldUndecidedOrCommitted_8(xid, mid, pair);
   var i : Mid;
   var {:layer 8} snapshot: GState;
 
-  call snapshot := GhostRead_8();
+  call {:layer 8} snapshot := Copy(state);
   call {:layer 8} Lemma_add_to_set(B, pair);
   call {:layer 8} Lemma_all_in_set(B, xid);
   call commit := StateUpdateOnVoteYes(xid, mid, pair);
@@ -332,7 +322,7 @@ requires call YieldAborted_8(xid, mid, pair);
   var i : int;
   var {:layer 8} snapshot: GState;
 
-  call snapshot := GhostRead_8();
+  call {:layer 8} snapshot := Copy(state);
   call abort := StateUpdateOnVoteNo(xid, mid);
 
   if (abort)
diff --git a/Test/civl/async/inc-dec-2.bpl b/Test/civl/async/inc-dec-2.bpl
index 95835389c..7b5753df2 100644
--- a/Test/civl/async/inc-dec-2.bpl
+++ b/Test/civl/async/inc-dec-2.bpl
@@ -16,7 +16,7 @@ refines skip;
 {
   var {:layer 1} old_x: int;
 
-  call old_x := snapshot_x();
+  call {:layer 1} old_x := Copy(x);
   while (*)
   invariant {:layer 1} x == old_x;
   {
@@ -25,11 +25,6 @@ refines skip;
   }
 }
 
-action {:layer 1} snapshot_x() returns (snapshot: int)
-{
-   snapshot := x;
-}
-
 // ###########################################################################
 // Low level atomic actions
 
diff --git a/Test/civl/async/tds.bpl b/Test/civl/async/tds.bpl
index 9153c57e8..8e5b9902e 100644
--- a/Test/civl/async/tds.bpl
+++ b/Test/civl/async/tds.bpl
@@ -61,11 +61,6 @@ refines atomic_main;
     call master3(id);
 }
 
-action {:layer 3} StatusSnapshot() returns (snapshot: [int]int)
-{
-  snapshot := status;
-}
-
 yield procedure {:layer 2} Alloc(i: int, {:linear_in "tid"} tidq: [int]bool) returns ({:linear "tid"} id: int, {:linear "tid"} tidq':[int]bool);
 refines AtomicAlloc;
 both action {:layer 3} AtomicAlloc(i: int, {:linear_in "tid"} tidq: [int]bool) returns ({:linear "tid"} id: int, {:linear "tid"} tidq':[int]bool)
@@ -80,7 +75,7 @@ refines atomic_server;
     var {:linear "tid"} tid: int;
 
     i := 0;
-    call snapshot := StatusSnapshot();
+    call {:layer 3} snapshot := Copy(status);
     tids' := tids;
     while (i < n)
     invariant {:layer 3} 0 <= i && i <= n;
diff --git a/Test/civl/async/tds2.bpl b/Test/civl/async/tds2.bpl
index 61f9f39a8..45243bede 100644
--- a/Test/civl/async/tds2.bpl
+++ b/Test/civl/async/tds2.bpl
@@ -40,11 +40,6 @@ modifies status;
 yield procedure {:layer 0} FinishTask({:linear "tid"} tid: int);
 refines AtomicFinishTask;
 
-action {:layer 1} StatusSnapshot() returns (snapshot: [int]int)
-{
-  snapshot := status;
-}
-
 yield procedure {:layer 0} Alloc(i: int, {:linear_in "tid"} tidq: [int]bool) returns ({:linear "tid"} id: int, {:linear "tid"} tidq':[int]bool);
 refines AtomicAlloc;
 both action {:layer 1} AtomicAlloc(i: int, {:linear_in "tid"} tidq: [int]bool) returns ({:linear "tid"} id: int, {:linear "tid"} tidq':[int]bool)
@@ -68,7 +63,7 @@ refines AtomicMain;
 
     i := 0;
     tids' := tids;
-    call snapshot := StatusSnapshot();
+    call {:layer 1} snapshot := Copy(status);
     while (i < n)
     invariant {:layer 1} 0 <= i && i <= n;
     invariant {:layer 1} (forall j: int :: i <= j && j < n <==> tids'[j]);
diff --git a/Test/civl/inductive-sequentialization/2PC.bpl b/Test/civl/inductive-sequentialization/2PC.bpl
index 2c0cea813..fbab78705 100644
--- a/Test/civl/inductive-sequentialization/2PC.bpl
+++ b/Test/civl/inductive-sequentialization/2PC.bpl
@@ -299,7 +299,7 @@ requires call YieldCoordinator();
   var i:int;
   var {:layer 1} old_RequestChannel:[int]int;
 
-  call old_RequestChannel := Snapshot_RequestChannel();
+  call {:layer 1} old_RequestChannel := Copy(RequestChannel);
   i := 1;
   while (i <= n)
   invariant {:layer 1} 1 <= i && i <= n+1;
@@ -322,8 +322,8 @@ requires call YieldCoordinator();
   var {:layer 1} old_VoteChannel:[vote]int;
   var {:layer 1} old_DecisionChannel:[int][decision]int;
 
-  call old_VoteChannel := Snapshot_VoteChannel();
-  call old_DecisionChannel := Snapshot_DecisionChannel();
+  call {:layer 1} old_VoteChannel := Copy(VoteChannel);
+  call {:layer 1} old_DecisionChannel := Copy(DecisionChannel);
   i := 0;
   d := COMMIT();
   while (i < n)
@@ -351,21 +351,6 @@ requires call YieldCoordinator();
   }
 }
 
-action {:layer 1} Snapshot_RequestChannel() returns (snapshot:[int]int)
-{
-  snapshot := RequestChannel;
-}
-
-action {:layer 1} Snapshot_VoteChannel() returns (snapshot:[vote]int)
-{
-  snapshot := VoteChannel;
-}
-
-action {:layer 1} Snapshot_DecisionChannel() returns (snapshot:[int][decision]int)
-{
-  snapshot := DecisionChannel;
-}
-
 ////////////////////////////////////////////////////////////////////////////////
 
 both action {:layer 1} SET_VOTE({:linear "pid"} pid:int, v:vote)
diff --git a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl
index afb69cd59..4d04b75ff 100644
--- a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl
+++ b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl
@@ -193,19 +193,13 @@ function {:inline} Inv(CH_low:[pid][val]int, CH:[val]int) : bool
   (forall i:pid :: MultisetSubsetEq(MultisetEmpty, CH_low[i]) && MultisetSubsetEq(CH_low[i], CH))
 }
 
-action {:layer 1} intro (i:pid)
-modifies CH;
+pure procedure {:inline 1} add_to_multiset (CH:[val]int, x: val) returns (CH':[val]int)
 {
-  CH := CH[value[i] := CH[value[i]] + 1];
+  CH' := CH[x := CH[x] + 1];
 }
 
 ////////////////////////////////////////////////////////////////////////////////
 
-action {:layer 1} Snapshot() returns (snapshot:[pid][val]int)
-{
-  snapshot := CH_low;
-}
-
 yield invariant {:layer 1}
 YieldInit({:linear "broadcast"} pidsBroadcast:[pid]bool, {:linear "collect"} pidsCollect:[pid]bool);
 invariant pidsBroadcast == (lambda ii:pid :: pid(ii)) && pidsCollect == pidsBroadcast;
@@ -251,7 +245,7 @@ requires {:layer 1} pid(i);
   var v: val;
   var {:layer 1} old_CH_low: [pid][val]int;
 
-  call old_CH_low := Snapshot();
+  call {:layer 1} old_CH_low := Copy(CH_low);
   call v := get_value(i);
   j := 1;
   while (j <= n)
@@ -261,7 +255,7 @@ requires {:layer 1} pid(i);
     call send(v, j);
     j := j + 1;
   }
-  call intro(i);
+  call {:layer 1} CH := add_to_multiset(CH, value[i]);
 }
 
 yield procedure {:layer 1}
@@ -276,7 +270,7 @@ requires {:layer 1} pid(i);
   var {:layer 1} received_values: [val]int;
   var {:layer 1} old_CH_low: [pid][val]int;
 
-  call old_CH_low := Snapshot();
+  call {:layer 1} old_CH_low := Copy(CH_low);
   call d := receive(i);
   received_values := MultisetSingleton(d);
   j := 2;
diff --git a/Test/civl/inductive-sequentialization/ChangRoberts.bpl b/Test/civl/inductive-sequentialization/ChangRoberts.bpl
index 68cae8ac1..b3f7fbe02 100644
--- a/Test/civl/inductive-sequentialization/ChangRoberts.bpl
+++ b/Test/civl/inductive-sequentialization/ChangRoberts.bpl
@@ -250,7 +250,7 @@ requires {:layer 1} Pid(pid);
   if (m == i)
   {
     call set_leader(pid);
-    call set_terminated(pid);
+    call {:layer 1} terminated := set_terminated(terminated, pid);
   }
   else
   {
@@ -262,10 +262,9 @@ requires {:layer 1} Pid(pid);
   }
 }
 
-action {:layer 1} set_terminated(pid:int)
-modifies terminated;
+pure procedure {:inline 1} set_terminated(terminated:[int]bool, pid:int) returns (terminated':[int]bool)
 {
-  terminated[pid] := true;
+  terminated' := terminated[pid := true];
 }
 
 ////////////////////////////////////////////////////////////////////////////////
diff --git a/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl b/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl
index 1706ab014..664592ab8 100644
--- a/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl
+++ b/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl
@@ -77,9 +77,9 @@ requires call YieldInit(rs);
   var {:layer 1}{:linear "perm"} rs': [Round]bool;
   var {:layer 1}{:pending_async} PAs:[A_StartRound]int;
 
-  call InitJoinedNodes();
-  call InitVoteInfo();
-  call InitDecision();
+  call {:layer 1} joinedNodes := Copy((lambda r: Round:: NoNodes()));
+  call {:layer 1} voteInfo := Copy((lambda r: Round:: None()));
+  call {:layer 1} decision := Copy((lambda r: Round :: None()));
   r := 0;
   rs' := rs;
   while (*)
@@ -88,7 +88,7 @@ requires call YieldInit(rs);
   invariant {:layer 1} PAs == ToMultiset((lambda pa: A_StartRound :: pa->r == pa->r_lin && Round(pa->r) && pa->r <= r));
   {
     r := r + 1;
-    call rs', r_lin := ExtractRoundPermission(rs', r);
+    call {:layer 1} rs', r_lin := ExtractRoundPermission(rs', r);
     async call StartRound(r, r_lin);
   }
 }
@@ -106,14 +106,14 @@ requires call YieldInvChannels();
   var {:layer 1}{:linear "perm"} ps': [Permission]bool;
   var {:layer 1}{:pending_async} PAs:[A_Join]int;
 
-  call ps, ps' := SplitPermissions(r_lin);
+  call {:layer 1} ps, ps' := SplitPermissions(r_lin);
   n := 1;
   while (n <= numNodes)
   invariant {:layer 1} 1 <= n && n <= numNodes+1;
   invariant {:layer 1} (forall n': Node :: n <= n' && n' <= numNodes ==> ps[JoinPerm(r, n')]);
   invariant {:layer 1} PAs == ToMultiset((lambda pa: A_Join :: pa->r == r && 1 <= pa->n && pa->n < n && pa->p == JoinPerm(pa->r, pa->n)));
   {
-    call ps, p := ExtractJoinPermission(ps, r, n);
+    call {:layer 1} ps, p := ExtractJoinPermission(ps, r, n);
     async call Join(r, n, p);
     n := n + 1;
   }
@@ -136,8 +136,8 @@ ensures {:layer 1} InvChannels(joinChannel, permJoinChannel, voteChannel, permVo
   var {:layer 1}{:linear "perm"} receivedPermissions: [Permission]bool;
   var {:layer 1}{:linear "perm"} receivedPermission: Permission;
 
-  call {:layer 1} ns := InitializeQuorum();
-  call receivedPermissions := InitializePermissions();
+  call {:layer 1} ns := Copy(NoNodes());
+  call {:layer 1} receivedPermissions := InitializePermissions();
   count := 0;
   maxRound := 0;
   while (true)
@@ -151,10 +151,10 @@ ensures {:layer 1} InvChannels(joinChannel, permJoinChannel, voteChannel, permVo
   invariant {:layer 1} InvChannels(joinChannel, permJoinChannel, voteChannel, permVoteChannel);
   {
     call joinResponse := ReceiveJoinResponse(r);
-    call receivedPermission := ReceiveJoinResponseIntro(r, joinResponse);
+    call {:layer 1} receivedPermission, permJoinChannel := ReceiveJoinResponseIntro(r, joinResponse, permJoinChannel);
     call {:layer 1} MaxRoundLemma(voteInfo, r, ns, SingletonNode(receivedPermission->n));
     call {:layer 1} ns := AddToQuorum(ns, receivedPermission->n);
-    call receivedPermissions := AddPermission(receivedPermissions, receivedPermission);
+    call {:layer 1} receivedPermissions := AddPermission(receivedPermissions, receivedPermission);
     count := count + 1;
     if (joinResponse->lastVoteRound > maxRound) {
       maxRound := joinResponse->lastVoteRound;
@@ -184,19 +184,19 @@ requires call YieldInvChannels();
 
   call maxRound, maxValue, ns := ProposeHelper(r);
   assume {:add_to_pool "NodeSet", ns} {:add_to_pool "MaxValue", maxValue} true;
-  call ps', cp := SplitConcludePermission(r, ps);
+  call {:layer 1} ps', cp := SplitConcludePermission(r, ps);
   n := 1;
   while (n <= numNodes)
   invariant {:layer 1} 1 <= n && n <= numNodes+1;
   invariant {:layer 1} (forall n': Node :: n <= n' && n' <= numNodes ==> ps'[VotePerm(r, n')]);
   invariant {:layer 1} PAs == ToMultiset((lambda pa: A_Vote :: pa->r == r && 1 <= pa->n && pa->n < n && pa->v == maxValue && pa->p == VotePerm(pa->r, pa->n)));
   {
-    call ps', p := ExtractVotePermission(ps', r, n);
+    call {:layer 1} ps', p := ExtractVotePermission(ps', r, n);
     async call Vote(r, n, maxValue, p);
     n := n + 1;
   }
   async call Conclude(r, maxValue, cp);
-  call SetVoteInfoInPropose(r, maxValue);
+  call {:layer 1} voteInfo := Copy(voteInfo[r := Some(VoteInfo(maxValue, NoNodes()))]);
 }
 
 yield procedure {:layer 1}
@@ -212,8 +212,8 @@ requires call YieldInvChannels();
   var {:linear "perm"} {:layer 1} receivedPermissions: [Permission]bool;
   var {:linear "perm"} {:layer 1} receivedPermission: Permission;
 
-  call {:layer 1} q := InitializeQuorum();
-  call receivedPermissions := InitializePermissions();
+  call {:layer 1} q := Copy(NoNodes());
+  call {:layer 1} receivedPermissions := InitializePermissions();
   count := 0;
   while (true)
   invariant {:layer 1} count == Cardinality(q);
@@ -224,12 +224,12 @@ requires call YieldInvChannels();
   invariant {:layer 1} InvChannels(joinChannel, permJoinChannel, voteChannel, permVoteChannel);
   {
     call voteResponse := ReceiveVoteResponse(r);
-    call receivedPermission := ReceiveVoteResponseIntro(r, voteResponse);
+    call {:layer 1} receivedPermission, permVoteChannel := ReceiveVoteResponseIntro(r, voteResponse, permVoteChannel);
     call {:layer 1} q := AddToQuorum(q, receivedPermission->n);
-    call receivedPermissions := AddPermission(receivedPermissions, receivedPermission);
+    call {:layer 1} receivedPermissions := AddPermission(receivedPermissions, receivedPermission);
     count := count + 1;
     if (2 * count > numNodes) {
-      call SetDecision(r, v);
+      call {:layer 1} decision := Copy(decision[r := Some(v)]);
       assume {:add_to_pool "NodeSet", q} true;
       break;
     }
@@ -249,8 +249,8 @@ requires call YieldInv();
   call doJoin, lastVoteRound, lastVoteValue := JoinUpdate(r, n);
   if (doJoin) {
     call SendJoinResponse(r, n, lastVoteRound, lastVoteValue);
-    call SendJoinResponseIntro(r, n, lastVoteRound, lastVoteValue, p);
-    call SetJoinedNodes(r, n);
+    call {:layer 1} permJoinChannel := SendJoinResponseIntro(JoinResponse(n, lastVoteRound, lastVoteValue), p, permJoinChannel);
+    call {:layer 1} joinedNodes := Copy(joinedNodes[r := joinedNodes[r][n := true]]);
   }
 }
 
@@ -265,56 +265,14 @@ requires call YieldInv();
   call doVote := VoteUpdate(r, n, v);
   if (doVote) {
     call SendVoteResponse(r, n);
-    call SendVoteResponseIntro(r, n, p);
-    call SetJoinedNodes(r, n);
-    call SetVoteInfoInVote(r, n);
+    call {:layer 1} permVoteChannel := SendVoteResponseIntro(VoteResponse(n), p, permVoteChannel);
+    call {:layer 1} joinedNodes := Copy(joinedNodes[r := joinedNodes[r][n := true]]);
+    call {:layer 1} voteInfo := Copy(voteInfo[r := Some(VoteInfo(voteInfo[r]->t->value, voteInfo[r]->t->ns[n := true]))]);
   }
 }
 
 ////////////////////////////////////////////////////////////////////////////////
 
-action {:layer 1} InitJoinedNodes()
-modifies joinedNodes;
-{
-  joinedNodes := (lambda r: Round:: NoNodes());
-}
-
-action {:layer 1} SetJoinedNodes(r: Round, n: Node)
-modifies joinedNodes;
-{
-  joinedNodes[r][n] := true;
-}
-
-action {:layer 1} InitVoteInfo()
-modifies voteInfo;
-{
-  voteInfo := (lambda r: Round:: None());
-}
-
-action {:layer 1} SetVoteInfoInPropose(r: Round, v: Value)
-modifies voteInfo;
-{
-  voteInfo[r] := Some(VoteInfo(v, NoNodes()));
-}
-
-action {:layer 1} SetVoteInfoInVote(r: Round, n: Node)
-modifies voteInfo;
-{
-  voteInfo[r] := Some(VoteInfo(voteInfo[r]->t->value, voteInfo[r]->t->ns[n := true]));
-}
-
-action {:layer 1} InitDecision()
-modifies decision;
-{
-  decision := (lambda r: Round :: None());
-}
-
-action {:layer 1} SetDecision(round: Round, value: Value)
-modifies decision;
-{
-  decision[round] := Some(value);
-}
-
 // Trusted lemmas for the proof of Propose and Conclude
 pure procedure AddToQuorum(q: NodeSet, n: Node) returns (q': NodeSet);
 requires !q[n];
@@ -412,62 +370,56 @@ yield procedure {:layer 0}
 ReceiveVoteResponse(round: Round) returns (voteResponse: VoteResponse);
 refines A_ReceiveVoteResponse;
 
-//// Introduction procedure for quorum
-action {:layer 1} InitializeQuorum() returns (q: NodeSet) {
-  q := NoNodes();
-}
-
 //// Introduction procedures to make send/receive more abstract
 
-action {:layer 1} SendJoinResponseIntro(round: Round, from: Node, lastVoteRound: Round, lastVoteValue: Value, {:linear_in "perm"} p: Permission)
-modifies permJoinChannel;
+pure action SendJoinResponseIntro(joinResponse: JoinResponse, {:linear_in "perm"} p: Permission, {:linear_in "perm"} permJoinChannel: JoinResponseChannel)
+returns ({:linear "perm"} permJoinChannel': JoinResponseChannel)
 {
-  permJoinChannel := JoinResponseChannel(
+  permJoinChannel' := JoinResponseChannel(
     permJoinChannel->domain[p := true],
-    permJoinChannel->contents[p := JoinResponse(from, lastVoteRound, lastVoteValue)]);
+    permJoinChannel->contents[p := joinResponse]);
 }
 
-action {:layer 1} ReceiveJoinResponseIntro(round: Round, joinResponse: JoinResponse) returns ({:linear "perm"} receivedPermission: Permission)
-modifies permJoinChannel;
+pure action ReceiveJoinResponseIntro(round: Round, joinResponse: JoinResponse, {:linear_in "perm"} permJoinChannel: JoinResponseChannel)
+returns ({:linear "perm"} receivedPermission: Permission, {:linear "perm"} permJoinChannel': JoinResponseChannel)
 {
   assert permJoinChannel->domain[JoinPerm(round, joinResponse->from)];
   receivedPermission := JoinPerm(round, joinResponse->from);
-  permJoinChannel := JoinResponseChannel(permJoinChannel->domain[receivedPermission := false], permJoinChannel->contents);
+  permJoinChannel' := JoinResponseChannel(permJoinChannel->domain[receivedPermission := false], permJoinChannel->contents);
 }
 
-action {:layer 1} SendVoteResponseIntro(round: Round, from: Node, {:linear_in "perm"} p: Permission)
-modifies permVoteChannel;
+pure action SendVoteResponseIntro(voteResponse: VoteResponse, {:linear_in "perm"} p: Permission, {:linear_in "perm"} permVoteChannel: VoteResponseChannel)
+returns ({:linear "perm"} permVoteChannel': VoteResponseChannel)
 {
-  permVoteChannel := VoteResponseChannel(
+  permVoteChannel' := VoteResponseChannel(
     permVoteChannel->domain[p := true],
-    permVoteChannel->contents[p := VoteResponse(from)]);
+    permVoteChannel->contents[p := voteResponse]);
 }
 
-action {:layer 1} ReceiveVoteResponseIntro(round: Round, voteResponse: VoteResponse)
-returns ({:linear "perm"} receivedPermission: Permission)
-modifies permVoteChannel;
+pure action ReceiveVoteResponseIntro(round: Round, voteResponse: VoteResponse, {:linear_in "perm"} permVoteChannel: VoteResponseChannel)
+returns ({:linear "perm"} receivedPermission: Permission, {:linear "perm"} permVoteChannel': VoteResponseChannel)
 {
   assert permVoteChannel->domain[VotePerm(round, voteResponse->from)];
   receivedPermission := VotePerm(round, voteResponse->from);
-  permVoteChannel := VoteResponseChannel(permVoteChannel->domain[receivedPermission := false], permVoteChannel->contents);
+  permVoteChannel' := VoteResponseChannel(permVoteChannel->domain[receivedPermission := false], permVoteChannel->contents);
 }
 
 //// Permission accounting
 
-action {:layer 1} ExtractRoundPermission({:linear_in "perm"} rs: [Round]bool, r: Round)
+pure action ExtractRoundPermission({:linear_in "perm"} rs: [Round]bool, r: Round)
 returns ({:linear "perm"} rs': [Round]bool, {:linear "perm"} r_lin: Round)
 {
   assert rs[r];
   rs', r_lin := rs[r := false], r;
 }
 
-action {:layer 1} SplitPermissions({:linear_in "perm"} r_lin: Round)
+pure action SplitPermissions({:linear_in "perm"} r_lin: Round)
 returns ({:linear "perm"} ps: [Permission]bool, {:linear "perm"} ps': [Permission]bool)
 {
   ps, ps' := JoinPermissions(r_lin), ProposePermissions(r_lin);
 }
 
-action {:layer 1} ExtractJoinPermission({:linear_in "perm"} ps: [Permission]bool, r: Round, n: Node)
+pure action ExtractJoinPermission({:linear_in "perm"} ps: [Permission]bool, r: Round, n: Node)
 returns ({:linear "perm"} ps': [Permission]bool, {:linear "perm"} p: Permission)
 {
   assert ps[JoinPerm(r, n)];
@@ -475,14 +427,14 @@ returns ({:linear "perm"} ps': [Permission]bool, {:linear "perm"} p: Permission)
   ps' := ps[p := false];
 }
 
-action {:layer 1} SplitConcludePermission(r: Round, {:linear_in "perm"} ps: [Permission]bool)
+pure action SplitConcludePermission(r: Round, {:linear_in "perm"} ps: [Permission]bool)
 returns ({:linear "perm"} ps': [Permission]bool, {:linear "perm"} cp: Permission)
 {
   assert ps == ProposePermissions(r);
   ps', cp := VotePermissions(r), ConcludePerm(r);
 }
 
-action {:layer 1} ExtractVotePermission({:linear_in "perm"} ps: [Permission]bool, r: Round, n: Node)
+pure action ExtractVotePermission({:linear_in "perm"} ps: [Permission]bool, r: Round, n: Node)
 returns ({:linear "perm"} ps': [Permission]bool, {:linear "perm"} p: Permission)
 {
   assert ps[VotePerm(r, n)];
@@ -490,13 +442,13 @@ returns ({:linear "perm"} ps': [Permission]bool, {:linear "perm"} p: Permission)
   ps' := ps[p := false];
 }
 
-action {:layer 1} InitializePermissions()
+pure action InitializePermissions()
 returns ({:linear "perm"} receivedPermissions: [Permission]bool)
 {
   receivedPermissions := MapConst(false);
 }
 
-action {:layer 1} AddPermission({:linear_in "perm"} receivedPermissions: [Permission]bool, {:linear_in "perm"} p: Permission)
+pure action AddPermission({:linear_in "perm"} receivedPermissions: [Permission]bool, {:linear_in "perm"} p: Permission)
 returns ({:linear "perm"}receivedPermissions': [Permission]bool)
 {
   receivedPermissions' := receivedPermissions[p := true];
diff --git a/Test/civl/regression-tests/Pure1.bpl b/Test/civl/regression-tests/Pure1.bpl
new file mode 100644
index 000000000..29ab6054e
--- /dev/null
+++ b/Test/civl/regression-tests/Pure1.bpl
@@ -0,0 +1,11 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+var x: int;
+
+pure action E()
+modifies x;
+{
+    var c: int;
+    c := x;
+}
diff --git a/Test/civl/regression-tests/Pure1.bpl.expect b/Test/civl/regression-tests/Pure1.bpl.expect
new file mode 100644
index 000000000..145041b4f
--- /dev/null
+++ b/Test/civl/regression-tests/Pure1.bpl.expect
@@ -0,0 +1,3 @@
+Pure1.bpl(6,12): Error: unnecessary modifies clause for pure action
+Pure1.bpl(10,9): Error: cannot refer to a global variable in this context: x
+2 name resolution errors detected in Pure1.bpl
diff --git a/Test/civl/regression-tests/Pure2.bpl b/Test/civl/regression-tests/Pure2.bpl
new file mode 100644
index 000000000..709989049
--- /dev/null
+++ b/Test/civl/regression-tests/Pure2.bpl
@@ -0,0 +1,10 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+var {:layer 0,1} g:int;
+
+action {:layer 1} F(d: int)
+{
+    var c: int;
+    g := c;
+}
diff --git a/Test/civl/regression-tests/Pure2.bpl.expect b/Test/civl/regression-tests/Pure2.bpl.expect
new file mode 100644
index 000000000..7abd8bcb6
--- /dev/null
+++ b/Test/civl/regression-tests/Pure2.bpl.expect
@@ -0,0 +1,2 @@
+Pure2.bpl(9,6): Error: command assigns to a global variable that is not in the enclosing action's modifies clause: g
+1 type checking errors detected in Pure2.bpl
diff --git a/Test/civl/regression-tests/call-in-yield-proc.bpl b/Test/civl/regression-tests/call-in-yield-proc.bpl
new file mode 100644
index 000000000..1e1ef5810
--- /dev/null
+++ b/Test/civl/regression-tests/call-in-yield-proc.bpl
@@ -0,0 +1,24 @@
+// 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
new file mode 100644
index 000000000..fc1d4fbdf
--- /dev/null
+++ b/Test/civl/regression-tests/call-in-yield-proc.bpl.expect
@@ -0,0 +1,4 @@
+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/chris5.bpl b/Test/civl/regression-tests/chris5.bpl
index c29c48a52..06a9c4ebc 100644
--- a/Test/civl/regression-tests/chris5.bpl
+++ b/Test/civl/regression-tests/chris5.bpl
@@ -2,13 +2,13 @@
 // RUN: %diff "%s.expect" "%t"
 var {:layer 1,1} g:int;
 
-action {:layer 1} P(x:int)
+pure procedure {:inline 1} P(x:int)
 {
   assert x == 0;
 }
 
 yield procedure {:layer 1} Y(x:int)
 {
-  call P(x);
-  assert{:layer 1} x == 0;
+  call {:layer 1} P(x);
+  assert {:layer 1} x == 0;
 }
diff --git a/Test/civl/regression-tests/chris5.bpl.expect b/Test/civl/regression-tests/chris5.bpl.expect
index 7e545bd34..7d1f3dd2a 100644
--- a/Test/civl/regression-tests/chris5.bpl.expect
+++ b/Test/civl/regression-tests/chris5.bpl.expect
@@ -1,5 +1,6 @@
-chris5.bpl(7,3): Error: this gate of P could not be proved
+chris5.bpl(7,3): Error: this assertion could not be proved
 Execution trace:
     chris5.bpl(12,3): anon0
+    chris5.bpl(7,3): inline$P$0$anon0
 
 Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/civl/regression-tests/dir_request.bpl b/Test/civl/regression-tests/dir_request.bpl
index 915f157c7..ce37c9bd7 100644
--- a/Test/civl/regression-tests/dir_request.bpl
+++ b/Test/civl/regression-tests/dir_request.bpl
@@ -9,7 +9,7 @@ modifies X, B;
 {
     assume !B[i];
     li := Lval(i);
-    call Lval_Split(li, X);
+    call Lval_Split(X, li);
     B[i] := true;
 }
 
@@ -19,6 +19,6 @@ modifies X, B;
     var i: int;
     i := li->val;
     assert B[i];
-    call Lval_Transfer(li, X);
+    call Lval_Transfer(X, li);
     B[i] := false;
 }
diff --git a/Test/civl/regression-tests/ghost.bpl b/Test/civl/regression-tests/ghost.bpl
index 9f9e067fb..d42da58ad 100644
--- a/Test/civl/regression-tests/ghost.bpl
+++ b/Test/civl/regression-tests/ghost.bpl
@@ -9,7 +9,7 @@ modifies x;
 yield procedure {:layer 0} Incr();
 refines AtomicIncr;
 
-action {:layer 1} ghost(y: int) returns (z: int)
+pure procedure {:inline 1} ghost(y: int) returns (z: int)
 {
   z := y + 1;
 }
@@ -23,24 +23,19 @@ refines AtomicIncr2;
 {
   var {:layer 1} a: int;
 
-  call a := ghost(1);
+  call {:layer 1} a := ghost(1);
   assert {:layer 1} a == 2;
   par Incr() | Incr();
 }
 
-action {:layer 1} ghost'() returns (z: int)
-{
-  z := x;
-}
-
 yield procedure {:layer 1} Incr2'()
 refines AtomicIncr2;
 {
   var {:layer 1} a: int;
   var {:layer 1} b: int;
 
-  call a := ghost'();
+  call {:layer 1} a := Copy(x);
   par Incr() | Incr();
-  call b := ghost'();
+  call {:layer 1} b := Copy(x);
   assert {:layer 1} b == a + 2;
 }
diff --git a/Test/civl/regression-tests/intro-inline-check.bpl b/Test/civl/regression-tests/intro-inline-check.bpl
index c1b533dc7..26c1410b2 100644
--- a/Test/civl/regression-tests/intro-inline-check.bpl
+++ b/Test/civl/regression-tests/intro-inline-check.bpl
@@ -2,8 +2,8 @@
 // RUN: %diff "%s.expect" "%t"
 
 var {:layer 1} g: int;
-
-atomic action {:layer 1} A()
+var {:layer 0} h: int;
+action {:layer 1} A()
 modifies g;
 {
     call I();
@@ -12,5 +12,13 @@ modifies g;
 action {:layer 1} I()
 modifies g;
 {
-    g := g  + 1;
+    var x: int;
+    g := 1;
+    x := h;
+}
+
+action {:layer 1,2} B()
+modifies g;
+{
+    call I();
 }
diff --git a/Test/civl/regression-tests/intro-inline-check.bpl.expect b/Test/civl/regression-tests/intro-inline-check.bpl.expect
index 4910bdb0a..6cbbdeb09 100644
--- a/Test/civl/regression-tests/intro-inline-check.bpl.expect
+++ b/Test/civl/regression-tests/intro-inline-check.bpl.expect
@@ -1,2 +1,4 @@
-intro-inline-check.bpl(9,4): Error: lower layer of caller must be greater than lower layer of callee
-1 type checking errors detected in intro-inline-check.bpl
+intro-inline-check.bpl(16,4): Error: global variable must be introduced below the lower layer 1 of action I: g
+intro-inline-check.bpl(17,9): Error: global variable must be available across all layers ([1, 1]) of action I: h
+intro-inline-check.bpl(23,4): Error: caller layer range ([1, 2]) must be subset of callee layer range ([1, 1])
+3 type checking errors detected in intro-inline-check.bpl
diff --git a/Test/civl/regression-tests/intro-nonblocking.bpl b/Test/civl/regression-tests/intro-nonblocking.bpl
index ad24178dd..02a1a5750 100644
--- a/Test/civl/regression-tests/intro-nonblocking.bpl
+++ b/Test/civl/regression-tests/intro-nonblocking.bpl
@@ -1,12 +1,7 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-action {:layer 1} intro (x:int)
+pure action intro (x:int)
 {
   assume x == 0;
 }
-
-yield procedure {:layer 1} p (x:int)
-{
-  call intro(x);
-}
diff --git a/Test/civl/regression-tests/intro-nonblocking.bpl.expect b/Test/civl/regression-tests/intro-nonblocking.bpl.expect
index 71f101b83..1a747e1d9 100644
--- a/Test/civl/regression-tests/intro-nonblocking.bpl.expect
+++ b/Test/civl/regression-tests/intro-nonblocking.bpl.expect
@@ -1,5 +1,5 @@
-intro-nonblocking.bpl(4,19): Error: Cooperation check for intro failed
+intro-nonblocking.bpl(4,13): Error: Cooperation check for intro failed
 Execution trace:
     (0,0): init
 
-Boogie program verifier finished with 1 verified, 1 error
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/civl/regression-tests/intro.bpl b/Test/civl/regression-tests/intro.bpl
index 2c8e43f57..a9c1a2e41 100644
--- a/Test/civl/regression-tests/intro.bpl
+++ b/Test/civl/regression-tests/intro.bpl
@@ -23,13 +23,7 @@ refines atomic_write_y;
 requires call Yield_xy();
 {
   call write_x(y');
-  call set_y_to_x();
-}
-
-action {:layer 1} set_y_to_x ()
-modifies y;
-{
-  y := x;
+  call {:layer 1} y := Copy(x);
 }
 
 atomic action {:layer 1,1} atomic_read_x () returns (v:int)
@@ -42,21 +36,14 @@ modifies x;
 yield procedure {:layer 0} read_x () returns ({:layer 0} v:int)
 refines atomic_read_x;
 {
-  call v := intro_read_x();
+  call {:layer 0} v := Copy(x);
 }
 
 yield procedure {:layer 0} write_x (x':int)
 refines atomic_write_x;
 {
-  call intro_write_x(x');
+  call {:layer 0} x := Copy(x');
 }
 
-action {:layer 0} intro_read_x () returns (v:int)
-{ v := x; }
-
-action {:layer 0} intro_write_x (x':int)
-modifies x;
-{ x := x'; }
-
 yield invariant {:layer 1} Yield_xy();
 invariant x == y;
diff --git a/Test/civl/regression-tests/linear_types.bpl b/Test/civl/regression-tests/linear_types.bpl
index 63cbc6cbe..163f59baf 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(k, path');
+    call Lheap_Transfer(path', path);
+    call l := Lheap_Split(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_Transfer(path', path);
     call Lheap_Write(path'->val[k], v);
     call v' := Lheap_Read(path'->val[k]);
 }
@@ -23,15 +23,15 @@ 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_Split(l, path');
+    call Lset_Transfer(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(l, path');
-    call Lval_Split(l, path');
+    call Lset_Transfer(path', path);
+    call Lval_Transfer(path', l);
+    call Lval_Split(path', l);
 }
 
 atomic action {:layer 1, 2} A5({:linear_in} path: Lheap int) returns (path': Lheap int) {
@@ -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(g, path');
+    call Lheap_Transfer(path', g);
     call g := Lheap_Empty();
 }
 
@@ -54,19 +54,19 @@ 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(MapOne(y), path'->val[x]->f);
+    call l := Lheap_Split(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)
 {
     path' := path;
-    call Lval_Split(l, path');
+    call Lval_Split(path', l);
 }
 
 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(path1, path2->val[x]->f);
+    call Lheap_Transfer(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 92ef2a722..02c931886 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_Transfer(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(g, path');
+    call Lheap_Transfer(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(path'->val[x]->f, l');
+    call Lheap_Transfer(l', path'->val[x]->f);
 }
 
 atomic action {:layer 1, 2} A5({:linear_out} path: Lheap int) { }
@@ -41,22 +41,22 @@ atomic action {:layer 1, 2} A6({:linear_in} path: Lheap int) returns (path': Lhe
 atomic action {:layer 1, 2} A7(path1: Lheap int, {:linear_in} path2: Lheap int) returns (path': Lheap int)
 {
     path' := path2;
-    call Lheap_Transfer(path1, path');
+    call Lheap_Transfer(path', path1);
 }
 
 atomic action {:layer 1, 2} A8({:linear_in} path1: Lheap int, x: Ref Foo) returns (path2: Lheap Foo)
 {
-    call Lheap_Transfer(path1, path2->val[x]->f);
+    call Lheap_Transfer(path2->val[x]->f, path1);
 }
 
 atomic action {:layer 1, 2} A9({:linear_in} l: Lheap int)
 {
-    call Lheap_Transfer(l, g);
+    call Lheap_Transfer(g, l);
 }
 
 atomic action {:layer 1, 2} A10({:linear_in} l: Lheap int, l': Lheap int)
 {
-    call Lheap_Transfer(l, l');
+    call Lheap_Transfer(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 752f5cc53..d738b7e58 100644
--- a/Test/civl/regression-tests/linear_types_error.bpl.expect
+++ b/Test/civl/regression-tests/linear_types_error.bpl.expect
@@ -7,9 +7,9 @@ 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,31): Error: unavailable source path2 for linear parameter at position 1
+linear_types_error.bpl(49,24): 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 procedure's modifies clause: g
+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'
 linear_types_error.bpl(66,0): Error: Output variable b must be available at a return
 linear_types_error.bpl(72,14): Error: unavailable source for a linear read
diff --git a/Test/civl/regression-tests/yield-proc-rewrite.bpl b/Test/civl/regression-tests/yield-proc-rewrite.bpl
index adc9434b3..0c00fb0c5 100644
--- a/Test/civl/regression-tests/yield-proc-rewrite.bpl
+++ b/Test/civl/regression-tests/yield-proc-rewrite.bpl
@@ -1,23 +1,23 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-yield procedure {:layer 1} Foo1({:linear_in} x: Lset int) returns (z: Lset int)
+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(y, z);
+    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(y, z);
+    call Lval_Split(z, y);
 }
-yield procedure {:layer 1} Foo2({:linear_in} x: Lset int) returns (z: Lset int)
+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(y, z);
+    call {:layer 1} Lval_Split(z, y);
 }
diff --git a/Test/civl/samples/GC.bpl b/Test/civl/samples/GC.bpl
index 59c2b5154..5649be258 100644
--- a/Test/civl/samples/GC.bpl
+++ b/Test/civl/samples/GC.bpl
@@ -467,7 +467,7 @@ ensures call YieldSweepEnd(tid);
     call ClearToAbsWhite(tid);
     par YieldSweepBegin(tid, true, Color) | Yield_MsWellFormed(tid, 0) | Yield_RootScanBarrierInv() | Yield_Iso();
 
-    call snapColor := GhostReadColor100();
+    call {:layer 100} snapColor := Copy(Color);
     while (localSweepPtr < memHi)
     invariant {:yields} {:layer 96} true;
     invariant {:layer 98} MsWellFormed(MarkStack, MarkStackPtr, Color, 0);
@@ -573,7 +573,7 @@ preserves call Yield_RootScanBarrierInv();
 
     par Yield_MsWellFormed(tid, 0) | Yield_CollectorPhase_98(tid, old(collectorPhase)) | Yield_RootScanBarrierInv() | Yield_RootScanOn(tid, true) | Yield_97();
 
-    call snapColor := GhostReadColor99();
+    call {:layer 99} snapColor := Copy(Color);
     call CollectorRootScanBarrierWait(tid);
 
     i := 0;
@@ -614,7 +614,7 @@ requires {:layer 98} mutatorTidWhole(tid);
     call valx := ReadRoot(tid, x);
     call valy := ReadRoot(tid, y);
     call WriteFieldGeneral(tid, valx, f, valy);
-    call SetMemAbs1(x, f, y);
+    call {:layer 99} memAbs := Copy((var a, b := rootAbs[x], rootAbs[y]; memAbs[a := memAbs[a][f := b]]));
 }
 
 atomic action {:layer 100} AtomicReadFieldRaw({:linear "tid"} tid:Tid, x: idx, f: fld, y: idx)
@@ -634,7 +634,7 @@ refines AtomicReadFieldRaw;
     call valx := ReadRoot(tid, x);
     call valy := ReadFieldGeneral(tid, valx, f);
     call WriteRoot(tid, y, valy);
-    call SetRootAbs1(x, f, y);
+    call {:layer 99} rootAbs := Copy((var a := rootAbs[x]; rootAbs[y := memAbs[a][f]]));
 }
 
 atomic action {:layer 100} AtomicEqRaw({:linear "tid"} tid:Tid, x: idx, y:idx) returns (isEqual:bool)
@@ -673,8 +673,8 @@ refines AtomicAllocRaw;
     call absPtr := PrimitiveFindFreePtrAbs();
     call ptr := FindFreePtr(tid, absPtr);
     call WriteRoot(tid, y, ptr);
-    call SetMemAbs2(absPtr);
-    call SetRootAbs2(y, absPtr);
+    call {:layer 99} memAbs := Copy(memAbs[absPtr := (lambda z: int :: if (fieldAddr(z)) then absPtr else memAbs[absPtr][z])]);
+    call {:layer 99} rootAbs := Copy(rootAbs[y := absPtr]);
 }
 
 atomic action {:layer 100} AtomicWriteBarrier({:linear "tid"} tid:Tid, y:idx)
@@ -1371,7 +1371,7 @@ refines AtomicAllocIfPtrFree;
                 color := WHITE();
             }
 
-            call snapMem := GhostReadMem();
+            call {:layer 96} snapMem := Copy(mem);
             fldIter := 0;
             while (fldIter < numFields)
             invariant {:yields} {:layer 95} true;
@@ -1430,7 +1430,7 @@ modifies toAbs;
 yield procedure {:layer 95} LockedClearToAbsWhite({:linear "tid"} tid:Tid)
 refines AtomicLockedClearToAbsWhite;
 {
-    call SetToAbs1();
+    call {:layer 95} toAbs := Copy((lambda x: int :: if memAddr(x) && White(Color[x]) then nil else toAbs[x]));
 }
 
 both action {:layer 96,99} AtomicInitField({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool, x: int, f: int)
@@ -1854,7 +1854,7 @@ yield procedure {:layer 95} SetColor3({:linear "tid"} tid:Tid, i: int, val: int,
 refines AtomicSetColor3;
 {
     call PrimitiveSetColor(i, val);
-    call SetToAbs2(i, o);
+    call {:layer 95} toAbs := Copy(toAbs[i := o]);
 }
 
 both action {:layer 96,99} AtomicInitToAbs({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool)
@@ -1867,7 +1867,7 @@ modifies toAbs;
 yield procedure {:layer 95} InitToAbs({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool)
 refines AtomicInitToAbs;
 {
-    call SetToAbs3();
+    call {:layer 95} toAbs := Copy((lambda i:int :: if memAddr(i) then nil else Int(i)));
 }
 
 right action {:layer 96} AtomicLockAcquire({:linear "tid"} tid: Tid)
@@ -1899,21 +1899,6 @@ refines AtomicLockRelease;
     call PrimitiveLockZero();
 }
 
-action {:layer 96} GhostReadMem() returns (snapMem: [int][fld]int)
-{
-    snapMem := mem;
-}
-
-action {:layer 99} GhostReadColor99() returns (snapColor: [int]int)
-{
-    snapColor := Color;
-}
-
-action {:layer 100} GhostReadColor100() returns (snapColor: [int]int)
-{
-    snapColor := Color;
-}
-
 //////////////////////////////////////////////////////////////////////////////
 // ATOMIC PRIMITIVES
 //   The action specifications, linearity specifications, and requires/ensures below here are trusted.
@@ -2087,45 +2072,3 @@ modifies lock;
 { lock := 0; }
 yield procedure {:layer 0} PrimitiveLockZero();
 refines AtomicPrimitiveLockZero;
-
-action {:layer 99} SetMemAbs1(x: idx, f: fld, y: idx)
-modifies memAbs;
-{
-    memAbs[rootAbs[x]][f] := rootAbs[y];
-}
-
-action {:layer 99} SetRootAbs1(x: idx, f: fld, y: idx)
-modifies rootAbs;
-{
-    rootAbs[y] := memAbs[rootAbs[x]][f];
-}
-
-action {:layer 99} SetMemAbs2(absPtr: obj)
-modifies memAbs;
-{
-    memAbs[absPtr] := (lambda z: int :: if (fieldAddr(z)) then absPtr else memAbs[absPtr][z]);
-}
-
-action {:layer 99} SetRootAbs2(y: idx, absPtr: obj)
-modifies rootAbs;
-{
-    rootAbs[y] := absPtr;
-}
-
-action {:layer 95} SetToAbs1()
-modifies toAbs;
-{
-    toAbs := (lambda x: int :: if memAddr(x) && White(Color[x]) then nil else toAbs[x]);
-}
-
-action {:layer 95} SetToAbs2(i: int, o: obj)
-modifies toAbs;
-{
-    toAbs[i] := o;
-}
-
-action {:layer 95} SetToAbs3()
-modifies toAbs;
-{
-    toAbs := (lambda i:int :: if memAddr(i) then nil else Int(i));
-}
diff --git a/Test/civl/samples/MutexOverFutex.bpl b/Test/civl/samples/MutexOverFutex.bpl
index f28b5344c..80ac9e8b9 100644
--- a/Test/civl/samples/MutexOverFutex.bpl
+++ b/Test/civl/samples/MutexOverFutex.bpl
@@ -27,7 +27,7 @@ preserves call YieldWait(tid);
   var oldValue, temp: int;
   call oldValue := CmpXchg(0, 1);
   if (oldValue != 0) {
-    call EnterSlowPath(tid);
+    call {:layer 1} inSlowPath := Copy(inSlowPath[tid->val := true]);
     while (true)
     invariant {:yields} true;
     invariant call YieldInv();
@@ -46,12 +46,12 @@ preserves call YieldWait(tid);
       par YieldInv() | YieldWait(tid) | YieldSlowPath(tid);
       call oldValue := CmpXchg(0, 2);
       if (oldValue == 0) {
-        call ExitSlowPath(tid);
+        call {:layer 1} inSlowPath := Copy(inSlowPath[tid->val := false]);
         break;
       }
     }
   }
-  call SetMutex(Some(tid->val));
+  call {:layer 1} mutex := Copy(Some(tid->val));
 }
 
 atomic action {:layer 2} AtomicUnlock(tid: Lval Tid)
@@ -68,15 +68,15 @@ preserves call YieldWait(tid);
   var oldValue: int;
   call oldValue := FetchSub(1);
   if (oldValue == 1) {
-    call SetMutex(None());
+    call {:layer 1} mutex := Copy(None());
   } else {
-    call EnterSlowPath(tid);
+    call {:layer 1} inSlowPath := Copy(inSlowPath[tid->val := true]);
     par YieldInv() | YieldWait(tid) | YieldSlowPath(tid);
     call Store(0);
-    call SetMutex(None());
+    call {:layer 1} mutex := Copy(None());
     par YieldInv() | YieldWait(tid) | YieldSlowPath(tid);
     call Wake();
-    call ExitSlowPath(tid);
+    call {:layer 1} inSlowPath := Copy(inSlowPath[tid->val := false]);
   }
 }
 
@@ -98,28 +98,6 @@ invariant !futex->waiters[tid->val];
 yield invariant {:layer 1} YieldSlowPath(tid: Lval Tid);
 invariant inSlowPath[tid->val];
 
-/// Linking action for mutex
-
-action {:layer 1, 1} SetMutex(x: Mutex)
-modifies mutex;
-{
-  mutex := x;
-}
-
-/// Linking actions for inSlowPath
-
-action {:layer 1, 1} EnterSlowPath(tid: Lval Tid)
-modifies inSlowPath;
-{
-  inSlowPath[tid->val] := true;
-}
-
-action {:layer 1, 1} ExitSlowPath(tid: Lval Tid)
-modifies inSlowPath;
-{
-  inSlowPath[tid->val] := false;
-}
-
 /// Primitive atomic actions
 
 atomic action {:layer 1} AtomicCmpXchg(expected: int, newValue: int) returns (oldValue: int)
diff --git a/Test/civl/samples/Siddharth-queue.bpl b/Test/civl/samples/Siddharth-queue.bpl
index 4925d870e..6240714b1 100644
--- a/Test/civl/samples/Siddharth-queue.bpl
+++ b/Test/civl/samples/Siddharth-queue.bpl
@@ -20,21 +20,15 @@ type Key;
 
 // ---------- Primitives for manipulating logical/abstract state
 
-action {:layer 1} intro_readLin() returns (s: SetInvoc)
+pure procedure {:inline 1} intro_write_vis(vis: [Invoc]SetInvoc, n: Invoc, s: SetInvoc)
+  returns (vis': [Invoc]SetInvoc)
 {
-  s := Set_ofSeq(lin);
+  vis' := vis[n := s];
 }
 
-action {:layer 1} intro_write_vis(n: Invoc, s: SetInvoc)
-  modifies vis;
+pure procedure {:inline 1} intro_writeLin(lin: SeqInvoc, n: Invoc) returns (lin': SeqInvoc)
 {
-  vis[n] := s;
-}
-
-action {:layer 1} intro_writeLin(n: Invoc)
-  modifies lin;
-{
-  lin := Seq_append(lin, n);
+  lin' := Seq_append(lin, n);
 }
 
 // ---------- Specification program:
@@ -57,8 +51,8 @@ refines pop_atomic;
 {
   var {:layer 1} my_vis: SetInvoc;
 
-  call intro_writeLin(this);
-  call my_vis := intro_readLin();
-  call intro_write_vis(this, my_vis);
+  call {:layer 1} lin := intro_writeLin(lin, this);
+  call {:layer 1} my_vis := Copy(Set_ofSeq(lin));
+  call {:layer 1} vis := intro_write_vis(vis, this, my_vis);
   assert {:layer 1} my_vis == Set_ofSeq(lin);  // Despite this assertion passing
 }
diff --git a/Test/civl/samples/alloc-mem.bpl b/Test/civl/samples/alloc-mem.bpl
index f0e358eee..0a3d6076a 100644
--- a/Test/civl/samples/alloc-mem.bpl
+++ b/Test/civl/samples/alloc-mem.bpl
@@ -78,7 +78,7 @@ requires call Yield();
 ensures call YieldMem(l, i);
 {
   call i := PickAddr();
-  call l := AllocLinear(i);
+  call {:layer 1} l, pool := AllocLinear(i, Add(Empty(mem), i), pool);
 }
 
 left action {:layer 2} atomic_Free({:linear_in "mem"} l:lmap, i:int)
@@ -93,7 +93,7 @@ refines atomic_Free;
 requires {:layer 1} dom(l)[i];
 preserves call Yield();
 {
-  call FreeLinear(l, i);
+  call {:layer 1} pool := FreeLinear(l, i, pool);
   call ReturnAddr(i);
 }
 
@@ -125,25 +125,23 @@ requires call YieldMem(l, i);
 ensures call YieldMem(l', i);
 {
   call WriteLow(i, o);
-  call l' := WriteLinear(l, i, o);
+  call {:layer 1} l' := WriteLinear(l, i, o);
 }
 
-action {:layer 1} AllocLinear (i:int) returns ({:linear "mem"} l:lmap)
-modifies pool;
+pure action AllocLinear (i:int, _l:lmap, {:linear_in "mem"} pool:lmap) returns ({:linear "mem"} l:lmap, {:linear "mem"} pool':lmap)
 {
-  assert dom(pool)[i];
-  pool := Remove(pool, i);
-  l := Add(Empty(mem), i);
+  assert dom(pool)[i] && dom(_l) == MapConst(false)[i := true];
+  pool' := Remove(pool, i);
+  l := _l;
 }
 
-action {:layer 1} FreeLinear ({:linear_in "mem"} l:lmap, i:int)
-modifies pool;
+pure action FreeLinear ({:linear_in "mem"} l:lmap, i:int, {:linear_in "mem"} pool:lmap) returns ({:linear "mem"} pool':lmap)
 {
   assert dom(l)[i];
-  pool := Add(pool, i);
+  pool' := Add(pool, i);
 }
 
-action {:layer 1} WriteLinear ({:layer 1} {:linear_in "mem"} l:lmap, i:int, o:int) returns ({:layer 1} {:linear "mem"} l':lmap)
+pure action WriteLinear ({:layer 1} {:linear_in "mem"} l:lmap, i:int, o:int) returns ({:layer 1} {:linear "mem"} l':lmap)
 {
   assert dom(l)[i];
   l' := cons(dom(l), map(l)[i := o]);
diff --git a/Test/civl/samples/alloc-tid.bpl b/Test/civl/samples/alloc-tid.bpl
index 4a415f9ad..b39ea0fa5 100644
--- a/Test/civl/samples/alloc-tid.bpl
+++ b/Test/civl/samples/alloc-tid.bpl
@@ -55,7 +55,7 @@ ensures {:layer 1} tid == i;
 preserves call Yield1();
 {
   call i := AllocateLow();
-  call tid := MakeLinear(i);
+  call {:layer 1} tid, unallocated := MakeLinear(i, unallocated);
 }
 
 atomic action {:layer 2,2} AtomicRead({:linear "tid"} tid: int, i: int) returns (val: int)
@@ -121,10 +121,10 @@ refines AtomicAllocateLow;
 
 // We can prove that this primitive procedure preserves the permission invariant locally.
 // We only need to use its specification and the definitions of TidCollector and TidSetCollector.
-action {:layer 1} MakeLinear(i: int) returns ({:linear "tid"} tid: int)
-modifies unallocated;
+pure action MakeLinear(i: int, {:linear_in "tid"} unallocated: [int]bool)
+returns ({:linear "tid"} tid: int, {:linear "tid"} unallocated': [int]bool)
 {
   assert unallocated[i];
   tid := i;
-  unallocated := unallocated[i := false];
+  unallocated' := unallocated[i := false];
 }
diff --git a/Test/civl/samples/array-insert.bpl b/Test/civl/samples/array-insert.bpl
index b7d8d9409..a47a1aa56 100644
--- a/Test/civl/samples/array-insert.bpl
+++ b/Test/civl/samples/array-insert.bpl
@@ -45,7 +45,7 @@ requires {:layer 1} tid != nil;
   var c:int;   // value read from count
   var {:layer 1} _A:[int]int;
 
-  call _A := snapshot();
+  call {:layer 1} _A := Copy(A);
   call acquire(tid);
 
   idx := 0;
@@ -79,11 +79,6 @@ requires {:layer 1} tid != nil;
   call release(tid);
 }
 
-action {:layer 1} snapshot () returns (snapshot: [int]int)
-{
-   snapshot := A;
-}
-
 // =============================================================================
 
 both action {:layer 1} READ_A ({:linear "tid"} tid:Tid, i:int) returns (v:int)
diff --git a/Test/civl/samples/bluetooth.bpl b/Test/civl/samples/bluetooth.bpl
index 6c8128522..d66bbbebf 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 AddToBarrier(i, l);
+    call Lval_Transfer(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 AddToBarrier(i, l);
+    call {:layer 1} Lval_Transfer(usersInDriver, l);
 }
 
 left action {:layer 2} AtomicCheckAssert#1(i: int, r: Lval Perm)
@@ -90,7 +90,7 @@ left action {:layer 2} AtomicExit(i: int, {:linear_out} l: Lval Perm, r: Lval Pe
 modifies usersInDriver;
 {
     assert l->val == Left(i) && r->val == Right(i);
-    call RemoveFromBarrier(i, l);
+    call Lval_Split(usersInDriver, l);
 }
 yield procedure {:layer 1}
 Exit(i: int, {:layer 1} {:linear_out} l: Lval Perm, {:layer 1} r: Lval Perm)
@@ -99,7 +99,7 @@ preserves call Inv1();
 {
     call DeleteReference();
     call {:layer 1} SizeLemma(usersInDriver->dom, Left(i));
-    call RemoveFromBarrier(i, l);
+    call {:layer 1} Lval_Split(usersInDriver, l);
     call {:layer 1} SubsetSizeRelationLemma(MapConst(false), usersInDriver->dom);
 }
 
@@ -137,20 +137,6 @@ preserves call Inv1();
     call SetStopped();
 }
 
-/// introduction actions
-
-action {:layer 1, 2} AddToBarrier(i: int, {:linear_in} l: Lval Perm)
-modifies usersInDriver;
-{
-    call Lval_Transfer(l, usersInDriver);
-}
-
-action {:layer 1, 2} RemoveFromBarrier(i: int, {:linear_out} l: Lval Perm)
-modifies usersInDriver;
-{
-    call Lval_Split(l, usersInDriver);
-}
-
 /// primitive actions
 
 atomic action {:layer 1} AtomicEnter()
diff --git a/Test/civl/samples/cav2020-2.bpl b/Test/civl/samples/cav2020-2.bpl
index 1e21bb8c3..8840ddc25 100644
--- a/Test/civl/samples/cav2020-2.bpl
+++ b/Test/civl/samples/cav2020-2.bpl
@@ -41,7 +41,7 @@ preserves call LockInv();
 
     call t := CAS(false, true);
     if (t) {
-        call set_l(Some(tid));
+        call {:layer 1} l := Copy(Some(tid));
     } else {
         call {:mark} Acquire(tid);
     }
@@ -60,7 +60,7 @@ preserves call LockInv();
     var t: bool;
 
     call t := CAS(true, false);
-    call set_l(None());
+    call {:layer 1} l := Copy(None());
 }
 
 both action {:layer 2,2} ReadSpec({:linear "tid"} tid: Tid) returns (v: int)
@@ -111,9 +111,3 @@ modifies count;
 }
 yield procedure {:layer 0} WRITE(v: int);
 refines atomic_WRITE;
-
-action {:layer 1} set_l(v: Option Tid)
-modifies l;
-{
-    l := v;
-}
diff --git a/Test/civl/samples/lamport.bpl b/Test/civl/samples/lamport.bpl
index 99f022e82..b27efad50 100644
--- a/Test/civl/samples/lamport.bpl
+++ b/Test/civl/samples/lamport.bpl
@@ -46,14 +46,7 @@ preserves call yield_ind_inv();
   call update_x(i);
   call Yield(i);
   call update_y(i);
-  call mark_done(i);
-}
-
-// Introduction action that gives meaning to the introduced variable done
-action {:layer 1} mark_done(i: int)
-modifies done;
-{
-  done := done[i:=true];
+  call {:layer 1} done := Copy(done[i:=true]);
 }
 
 // #############################################################################
diff --git a/Test/civl/samples/lock-introduced.bpl b/Test/civl/samples/lock-introduced.bpl
index 68c12c179..0d445d69b 100644
--- a/Test/civl/samples/lock-introduced.bpl
+++ b/Test/civl/samples/lock-introduced.bpl
@@ -61,7 +61,7 @@ refines AtomicLowerEnter;
   {
     call status := CAS(false, true);
     if (status) {
-      call SetLock(tid);
+      call {:layer 1} lock := Copy(tid);
       return;
     }
   }
@@ -75,13 +75,9 @@ yield procedure {:layer 1} LowerLeave()
 refines AtomicLowerLeave;
 {
   call SET(false);
-  call SetLock(nil);
+  call {:layer 1} lock := Copy(nil);
 }
 
-action {:layer 1} SetLock(v: X)
-modifies lock;
-{ lock := v; }
-
 atomic action {:layer 1} AtomicCAS(prev: bool, next: bool) returns (status: bool)
 modifies b;
 {
diff --git a/Test/civl/samples/reserve.bpl b/Test/civl/samples/reserve.bpl
index cad8a2070..ad42492d6 100644
--- a/Test/civl/samples/reserve.bpl
+++ b/Test/civl/samples/reserve.bpl
@@ -79,30 +79,29 @@ preserves call YieldInvariant#1();
     }
 }
 
-action {:layer 1,2} Alloc(tid: Tid, ptr: int)
-modifies allocMap;
+pure action Alloc(tid: Tid, ptr: int, allocMap: Bijection) returns (allocMap': Bijection)
 {
     var tid': Tid;
     var ptr': int;
     assert Map_Contains(allocMap->tidToPtr, tid);
-    if (Map_Contains(allocMap->ptrToTid, ptr)) {
+    allocMap' := allocMap;
+    if (Map_Contains(allocMap'->ptrToTid, ptr)) {
         // swap
-        tid' := Map_At(allocMap->ptrToTid, ptr);
-        ptr' := Map_At(allocMap->tidToPtr, tid);
-        allocMap := Bijection(Map_Swap(allocMap->tidToPtr, tid, tid'), Map_Swap(allocMap->ptrToTid, ptr, ptr'));
+        tid' := Map_At(allocMap'->ptrToTid, ptr);
+        ptr' := Map_At(allocMap'->tidToPtr, tid);
+        allocMap' := Bijection(Map_Swap(allocMap'->tidToPtr, tid, tid'), Map_Swap(allocMap'->ptrToTid, ptr, ptr'));
     }
     // alloc
-    ptr' := Map_At(allocMap->tidToPtr, tid);
-    allocMap := Bijection(Map_Remove(allocMap->tidToPtr, tid), Map_Remove(allocMap->ptrToTid, ptr'));
+    ptr' := Map_At(allocMap'->tidToPtr, tid);
+    allocMap' := Bijection(Map_Remove(allocMap'->tidToPtr, tid), Map_Remove(allocMap'->ptrToTid, ptr'));
 }
 
-action {:layer 1,2} PreAlloc({:linear "tid"} tid: Tid, set: Set int)
-modifies allocMap;
+pure action PreAlloc({:linear "tid"} tid: Tid, set: Set int, allocMap: Bijection) returns (allocMap': Bijection)
 {
     var ptr: int;
     assert set != Set_Empty();
     ptr := Set_Choose(set);
-    allocMap := Bijection(Map_Update(allocMap->tidToPtr, tid, ptr), Map_Update(allocMap->ptrToTid, ptr, tid));
+    allocMap' := Bijection(Map_Update(allocMap->tidToPtr, tid, ptr), Map_Update(allocMap->ptrToTid, ptr, tid));
 }
 
 atomic action {:layer 2} AtomicDecrementFreeSpace#1({:linear "tid"} tid: Tid)
@@ -110,14 +109,14 @@ modifies freeSpace, allocMap;
 {
     assert !Map_Contains(allocMap->tidToPtr, tid);
     call AtomicDecrementFreeSpace#0(tid);
-    call PreAlloc(tid, Set_Difference(isFreeSet, allocMap->ptrToTid->dom));
+    call allocMap := PreAlloc(tid, Set_Difference(isFreeSet, allocMap->ptrToTid->dom), allocMap);
 }
 yield procedure {:layer 1} DecrementFreeSpace#1({:linear "tid"} tid: Tid)
 refines AtomicDecrementFreeSpace#1;
 preserves call YieldInvariant#1();
 {
     call DecrementFreeSpace#0(tid);
-    call PreAlloc(tid, Set_Difference(isFreeSet, allocMap->ptrToTid->dom));
+    call {:layer 1} allocMap := PreAlloc(tid, Set_Difference(isFreeSet, allocMap->ptrToTid->dom), allocMap);
 }
 
 atomic action {:layer 1,2} AtomicDecrementFreeSpace#0({:linear "tid"} tid: Tid)
@@ -137,7 +136,7 @@ modifies isFreeSet, allocMap;
     spaceFound := Set_Contains(isFreeSet, ptr);
     if (spaceFound) {
         isFreeSet := Set_Remove(isFreeSet, ptr);
-        call Alloc(tid, ptr);
+        call allocMap := Alloc(tid, ptr, allocMap);
     }
 }
 yield procedure {:layer 1} AllocIfPtrFree#1({:linear "tid"} tid: Tid, ptr: int) returns (spaceFound:bool)
@@ -146,8 +145,8 @@ preserves call YieldInvariant#1();
 {
     call spaceFound := AllocIfPtrFree#0(tid, ptr);
     if (spaceFound) {
-        call IsFreeSetRemove(ptr);
-        call Alloc(tid, ptr);
+        call {:layer 1} isFreeSet := Copy(Set_Remove(isFreeSet, ptr));
+        call {:layer 1} allocMap := Alloc(tid, ptr, allocMap);
     }
 }
 
@@ -163,18 +162,6 @@ modifies isFree;
 yield procedure {:layer 0} AllocIfPtrFree#0({:linear "tid"} tid: Tid, ptr: int) returns (spaceFound:bool);
 refines AtomicAllocIfPtrFree#0;
 
-action {:layer 1,2} IsFreeSetAdd(ptr: int)
-modifies isFreeSet;
-{
-    isFreeSet := Set_Add(isFreeSet, ptr);
-}
-
-action {:layer 1,2} IsFreeSetRemove(ptr: int)
-modifies isFreeSet;
-{
-    isFreeSet := Set_Remove(isFreeSet, ptr);
-}
-
 atomic action {:layer 2} AtomicReclaim#1() returns (ptr: int)
 modifies freeSpace, isFreeSet;
 {
@@ -187,7 +174,7 @@ refines AtomicReclaim#1;
 preserves call YieldInvariant#1();
 {
     call ptr := Reclaim#0();
-    call IsFreeSetAdd(ptr);
+    call {:layer 1} isFreeSet := Copy(Set_Add(isFreeSet, ptr));
 }
 
 atomic action {:layer 1} AtomicReclaim#0() returns (ptr: int)
diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl
index 45e49fd58..18116b21b 100644
--- a/Test/civl/samples/treiber-stack.bpl
+++ b/Test/civl/samples/treiber-stack.bpl
@@ -31,7 +31,7 @@ yield procedure {:layer 4} Alloc() returns (ref_t: Lval (RefTreiber X))
 refines AtomicAlloc;
 {
   call ref_t := Alloc#0();
-  call AddStack(ref_t->val);
+  call {:layer 4} Stack := Copy(Stack[ref_t->val := Vec_Empty()]);
   call {:layer 4} AbsDefinition(ts->val[ref_t->val]->top, ts->val[ref_t->val]->stack->val);
 }
 
@@ -49,7 +49,7 @@ preserves call YieldInv#4(ref_t);
 {
   call success := PushIntermediate(ref_t, x);
   if (success) {
-    call PushStack(ref_t, x);
+    call {:layer 4} Stack := Copy(Stack[ref_t := Vec_Append(Stack[ref_t], x)]);
   }
   call {:layer 4} AbsDefinition(ts->val[ref_t]->top, ts->val[ref_t]->stack->val);
 }
@@ -74,7 +74,8 @@ preserves call YieldInv#4(ref_t);
   call {:layer 4} AbsDefinition(ts->val[ref_t]->top, ts->val[ref_t]->stack->val);
   call success, x := PopIntermediate(ref_t);
   if (success) {
-    call PopStack(ref_t);
+    assert {:layer 4} Vec_Len(Stack[ref_t]) > 0;
+    call {:layer 4} Stack := Copy(Stack[ref_t := Vec_Remove(Stack[ref_t])]);
   }
 }
 
@@ -133,7 +134,9 @@ preserves call YieldInv#2(ref_t);
   call new_ref_n := AllocInStack(ref_t, Node(ref_n, x));
   call success := WriteTopOfStack(ref_t, ref_n, new_ref_n->val);
   assume {:add_to_pool "A", Lval(ref_n), new_ref_n} true;
-  call AddToUnusedNodes(success, ref_t, new_ref_n->val);
+  if (!success) {
+    call {:layer 2} unused := Copy((var a := unused[ref_t]; unused[ref_t := a[new_ref_n->val := true]]));
+  }
 }
 
 right action {:layer 3} AtomicReadTopOfStack#Pop(ref_t: RefTreiber X) returns (ref_n: RefNode X)
@@ -226,33 +229,6 @@ modifies ts;
 yield procedure {:layer 0} Alloc#0() returns (ref_t: Lval (RefTreiber X));
 refines AtomicAlloc#0;
 
-action {:layer 4} AddStack(ref_t: RefTreiber X)
-modifies Stack;
-{
-  Stack[ref_t] := Vec_Empty();
-}
-
-action {:layer 4} PushStack(ref_t: RefTreiber X, x: X)
-modifies Stack;
-{
-  Stack[ref_t] := Vec_Append(Stack[ref_t], x);
-}
-
-action {:layer 4} PopStack(ref_t: RefTreiber X)
-modifies Stack;
-{
-  assert Vec_Len(Stack[ref_t]) > 0;
-  Stack[ref_t] := Vec_Remove(Stack[ref_t]);
-}
-
-action {:layer 2} AddToUnusedNodes(success: bool, ref_t: RefTreiber X, ref_n: RefNode X)
-modifies unused;
-{
-  if (!success) {
-    unused[ref_t][ref_n] := true;
-  }
-}
-
 function {:inline} Domain(ts: Lheap (Treiber X), ref_t: RefTreiber X, unused: [RefTreiber X][RefNode X]bool): [RefNode X]bool {
   Difference(ts->val[ref_t]->stack->dom, unused[ref_t])
 }
diff --git a/Test/civl/samples/treiber-stack.bpl.expect b/Test/civl/samples/treiber-stack.bpl.expect
index a099146bd..d996ab7ab 100644
--- a/Test/civl/samples/treiber-stack.bpl.expect
+++ b/Test/civl/samples/treiber-stack.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 44 verified, 0 errors
+Boogie program verifier finished with 43 verified, 0 errors
diff --git a/Test/civl/samples/verified-ft.bpl b/Test/civl/samples/verified-ft.bpl
index 2758ed3c5..ae6b9a357 100644
--- a/Test/civl/samples/verified-ft.bpl
+++ b/Test/civl/samples/verified-ft.bpl
@@ -414,7 +414,8 @@ ensures call Yield_VCPreserved_10(tid, v1, v1, old(shadow.Lock), old(shadow.VC))
   var {:layer 10} oldVC : [Shadowable] [Tid]Epoch;
   var {:layer 10} oldLock : [Shadowable] Tid;
 
-  call oldLock, oldVC := GhostRead();
+  call {:layer 10} oldLock := Copy(shadow.Lock);
+  call {:layer 10} oldVC := Copy(shadow.VC);
 
   call len1 := VCGetSize(tid, v1);
   call len2 := VCGetSize(tid, v2);
@@ -470,7 +471,8 @@ ensures call Yield_VCPreserved_10(tid, v1, v1, old(shadow.Lock), old(shadow.VC))
   var {:layer 10} oldVC : [Shadowable] [Tid]Epoch;
   var {:layer 10} oldLock : [Shadowable] Tid;
 
-  call oldLock, oldVC := GhostRead();
+  call {:layer 10} oldLock := Copy(shadow.Lock);
+  call {:layer 10} oldVC := Copy(shadow.VC);
 
   call len1 := VCGetSize(tid, v1);
   call len2 := VCGetSize(tid, v2);
@@ -494,13 +496,6 @@ ensures call Yield_VCPreserved_10(tid, v1, v1, old(shadow.Lock), old(shadow.VC))
   assume {:add_to_pool "A", shadow.VC[v1]} true;
 }
 
-
-action {:layer 10} GhostRead() returns (lock : [Shadowable]Tid, data : [Shadowable] [Tid]Epoch)
-{
-  lock := shadow.Lock;
-  data := shadow.VC;
-}
-
 both action {:layer 11,20} AtomicVC.Inc({:linear "tid" } tid: Tid, v: Shadowable, i: int)
 modifies shadow.VC;
 {
diff --git a/Test/civl/samples/wilcox.bpl b/Test/civl/samples/wilcox.bpl
index 5e6ac1845..f6f7e5202 100644
--- a/Test/civl/samples/wilcox.bpl
+++ b/Test/civl/samples/wilcox.bpl
@@ -1,11 +1,6 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-action {:layer 1} GhostRead() returns (oldx: int)
-{
-   oldx := x;
-}
-
 var {:layer 0,2} x: int;
 
 yield procedure {:layer 0} IncX();
@@ -22,7 +17,7 @@ requires {:layer 1} n >= 0;
     var i: int;
     var {:layer 1} oldx: int;
 
-    call oldx := GhostRead();
+    call {:layer 1} oldx := Copy(x);
     i := 0;
     while (i < n)
     invariant {:layer 1} i <= n;