renamed :phase to :layer

34 files changed, 573 insertions, 573 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index d98d9e1f..9a2203c3 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -35,9 +35,9 @@ namespace Microsoft.Boogie
             {

                 AtomicActionInfo atomicAction = action as AtomicActionInfo;

                 if (atomicAction == null) continue;

-                foreach (int phaseNum in moverTypeChecker.AllPhaseNums)

+                foreach (int phaseNum in moverTypeChecker.AllLayerNums)

                 {

-                    if (action.phaseNum < phaseNum && phaseNum <= action.availableUptoPhaseNum)

+                    if (action.phaseNum < phaseNum && phaseNum <= action.availableUptoLayerNum)

                     {

                         if (!pools.ContainsKey(phaseNum))

                         {

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 964bf024..f656da57 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -38,12 +38,12 @@ namespace Microsoft.Boogie
 

         private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds)

         {

-            int enclosingProcPhaseNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].phaseNum;

+            int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].phaseNum;

             Procedure originalProc = originalCallCmd.Proc;

             if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))

             {

                 AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo;

-                if (atomicActionInfo != null && atomicActionInfo.thisGate.Count > 0 && phaseNum == enclosingProcPhaseNum)

+                if (atomicActionInfo != null && atomicActionInfo.thisGate.Count > 0 && phaseNum == enclosingProcLayerNum)

                 {

                     newCmds.Add(new HavocCmd(Token.NoToken, new List<IdentifierExpr>(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) })));

                     Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();

@@ -63,14 +63,14 @@ namespace Microsoft.Boogie
 

         private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List<Cmd> newCmds)

         {

-            int maxCalleePhaseNum = 0;

+            int maxCalleeLayerNum = 0;

             foreach (CallCmd iter in originalParCallCmd.CallCmds)

             {

-                int calleePhaseNum = moverTypeChecker.procToActionInfo[iter.Proc].phaseNum;

-                if (calleePhaseNum > maxCalleePhaseNum)

-                    maxCalleePhaseNum = calleePhaseNum;

+                int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].phaseNum;

+                if (calleeLayerNum > maxCalleeLayerNum)

+                    maxCalleeLayerNum = calleeLayerNum;

             }

-            if (phaseNum > maxCalleePhaseNum)

+            if (phaseNum > maxCalleeLayerNum)

             {

                 for (int i = 0; i < parCallCmd.CallCmds.Count; i++) 

                 {

@@ -220,7 +220,7 @@ namespace Microsoft.Boogie
             Requires requires = base.VisitRequires(node);

             if (node.Free)

                 return requires;

-            if (!moverTypeChecker.absyToPhaseNums[node].Contains(phaseNum))

+            if (!moverTypeChecker.absyToLayerNums[node].Contains(phaseNum))

                 requires.Condition = Expr.True;

             return requires;

         }

@@ -232,7 +232,7 @@ namespace Microsoft.Boogie
                 return ensures;

             AtomicActionInfo atomicActionInfo =  moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo;

             bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node;

-            if (isAtomicSpecification || !moverTypeChecker.absyToPhaseNums[node].Contains(phaseNum))

+            if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(phaseNum))

             {

                 ensures.Condition = Expr.True;

                 ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes);

@@ -243,7 +243,7 @@ namespace Microsoft.Boogie
         public override Cmd VisitAssertCmd(AssertCmd node)

         {

             AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node);

-            if (!moverTypeChecker.absyToPhaseNums[node].Contains(phaseNum))

+            if (!moverTypeChecker.absyToLayerNums[node].Contains(phaseNum))

                 assertCmd.Expr = Expr.True;

             return assertCmd;

         }

@@ -742,11 +742,11 @@ namespace Microsoft.Boogie
                 HashSet<Variable> introducedVars = new HashSet<Variable>();

                 foreach (Variable v in program.GlobalVariables)

                 {

-                    if (moverTypeChecker.hidePhaseNums[v] <= actionInfo.phaseNum || moverTypeChecker.introducePhaseNums[v] > actionInfo.phaseNum)

+                    if (moverTypeChecker.hideLayerNums[v] <= actionInfo.phaseNum || moverTypeChecker.introduceLayerNums[v] > actionInfo.phaseNum)

                     {

                         frame.Remove(v);

                     }

-                    if (moverTypeChecker.introducePhaseNums[v] == actionInfo.phaseNum)

+                    if (moverTypeChecker.introduceLayerNums[v] == actionInfo.phaseNum)

                     {

                         introducedVars.Add(v);

                     }

@@ -1159,9 +1159,9 @@ namespace Microsoft.Boogie
         public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

         {

             Program program = linearTypeChecker.program;

-            foreach (int phaseNum in moverTypeChecker.AllPhaseNums.Except(new int[] { 0 }))

+            foreach (int phaseNum in moverTypeChecker.AllLayerNums.Except(new int[] { 0 }))

             {

-                if (CommandLineOptions.Clo.TrustPhasesDownto <= phaseNum || phaseNum <= CommandLineOptions.Clo.TrustPhasesUpto) continue;

+                if (CommandLineOptions.Clo.TrustLayersDownto <= phaseNum || phaseNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;

 

                 MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, phaseNum);

                 foreach (var proc in program.Procedures)

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 657e3b06..be40bbf0 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -21,13 +21,13 @@ namespace Microsoft.Boogie
     {

         public Procedure proc;

         public int phaseNum;

-        public int availableUptoPhaseNum;

+        public int availableUptoLayerNum;

 

-        public ActionInfo(Procedure proc, int phaseNum, int availableUptoPhaseNum)

+        public ActionInfo(Procedure proc, int phaseNum, int availableUptoLayerNum)

         {

             this.proc = proc;

             this.phaseNum = phaseNum;

-            this.availableUptoPhaseNum = availableUptoPhaseNum;

+            this.availableUptoLayerNum = availableUptoLayerNum;

         }

 

         public virtual bool IsRightMover

@@ -77,8 +77,8 @@ namespace Microsoft.Boogie
             get { return moverType == MoverType.Left || moverType == MoverType.Both; }

         }

 

-        public AtomicActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int phaseNum, int availableUptoPhaseNum)

-            : base(proc, phaseNum, availableUptoPhaseNum)

+        public AtomicActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int phaseNum, int availableUptoLayerNum)

+            : base(proc, phaseNum, availableUptoLayerNum)

         {

             CodeExpr codeExpr = ensures.Condition as CodeExpr;

             this.ensures = ensures;

@@ -203,17 +203,17 @@ namespace Microsoft.Boogie
     {

         CheckingContext checkingContext;

         public int errorCount;

-        public Dictionary<Variable, int> introducePhaseNums;

-        public Dictionary<Variable, int> hidePhaseNums;

+        public Dictionary<Variable, int> introduceLayerNums;

+        public Dictionary<Variable, int> hideLayerNums;

         Procedure enclosingProc;

         Implementation enclosingImpl;

         public Dictionary<Procedure, ActionInfo> procToActionInfo;

         public Program program;

         bool canAccessSharedVars;

         bool canAccessAuxVars;

-        int minPhaseNum;

-        int maxPhaseNum;

-        public Dictionary<Absy, HashSet<int>> absyToPhaseNums;

+        int minLayerNum;

+        int maxLayerNum;

+        public Dictionary<Absy, HashSet<int>> absyToLayerNums;

         HashSet<Variable> auxVars;

 

         private static List<int> FindIntAttributes(QKeyValue kv, string name)

@@ -250,20 +250,20 @@ namespace Microsoft.Boogie
             return MoverType.Top;

         }

 

-        private HashSet<int> allPhaseNums;

-        public IEnumerable<int> AllPhaseNums

+        private HashSet<int> allLayerNums;

+        public IEnumerable<int> AllLayerNums

         {

             get

             {

-                if (allPhaseNums == null)

+                if (allLayerNums == null)

                 {

-                    allPhaseNums = new HashSet<int>();

+                    allLayerNums = new HashSet<int>();

                     foreach (ActionInfo actionInfo in procToActionInfo.Values)

                     {

-                        allPhaseNums.Add(actionInfo.phaseNum);

+                        allLayerNums.Add(actionInfo.phaseNum);

                     }

                 }

-                return allPhaseNums;

+                return allLayerNums;

             }

         }

 

@@ -274,8 +274,8 @@ namespace Microsoft.Boogie
                 if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;

 

                 int phaseNum = int.MaxValue;

-                int availableUptoPhaseNum = int.MaxValue;

-                List<int> attrs = FindIntAttributes(proc.Attributes, "phase");

+                int availableUptoLayerNum = int.MaxValue;

+                List<int> attrs = FindIntAttributes(proc.Attributes, "layer");

                 if (attrs.Count == 1)

                 {

                     phaseNum = attrs[0];

@@ -283,7 +283,7 @@ namespace Microsoft.Boogie
                 else if (attrs.Count == 2)

                 {

                     phaseNum = attrs[0];

-                    availableUptoPhaseNum = attrs[1];

+                    availableUptoLayerNum = attrs[1];

                 }

                 else

                 {

@@ -306,14 +306,14 @@ namespace Microsoft.Boogie
                         continue;

                     }

 

-                    minPhaseNum = int.MaxValue;

-                    maxPhaseNum = -1;

+                    minLayerNum = int.MaxValue;

+                    maxLayerNum = -1;

                     canAccessSharedVars = true;

                     enclosingProc = proc;

                     enclosingImpl = null;

                     base.VisitEnsures(e);

                     canAccessSharedVars = false;

-                    if (maxPhaseNum <= phaseNum && availableUptoPhaseNum <= minPhaseNum)

+                    if (maxLayerNum <= phaseNum && availableUptoLayerNum <= minLayerNum)

                     {

                         // ok

                     }

@@ -322,11 +322,11 @@ namespace Microsoft.Boogie
                         Error(e, "A variable being accessed is hidden before this action becomes unavailable");

                     }

 

-                    procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, phaseNum, availableUptoPhaseNum);

+                    procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, phaseNum, availableUptoLayerNum);

                 }

                 if (!procToActionInfo.ContainsKey(proc))

                 {

-                    procToActionInfo[proc] = new ActionInfo(proc, phaseNum, availableUptoPhaseNum);

+                    procToActionInfo[proc] = new ActionInfo(proc, phaseNum, availableUptoLayerNum);

                 }

             }

             if (errorCount > 0) return;

@@ -338,9 +338,9 @@ namespace Microsoft.Boogie
         public MoverTypeChecker(Program program)

         {

             this.auxVars = new HashSet<Variable>();

-            this.absyToPhaseNums = new Dictionary<Absy, HashSet<int>>();

-            this.introducePhaseNums = new Dictionary<Variable, int>();

-            this.hidePhaseNums = new Dictionary<Variable, int>();

+            this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();

+            this.introduceLayerNums = new Dictionary<Variable, int>();

+            this.hideLayerNums = new Dictionary<Variable, int>();

             this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();

             this.errorCount = 0;

             this.checkingContext = new CheckingContext(null);

@@ -349,25 +349,25 @@ namespace Microsoft.Boogie
             this.enclosingImpl = null;

             this.canAccessSharedVars = false;

             this.canAccessAuxVars = false;

-            this.minPhaseNum = int.MaxValue;

-            this.maxPhaseNum = -1;

+            this.minLayerNum = int.MaxValue;

+            this.maxLayerNum = -1;

             foreach (var g in program.GlobalVariables)

             {

-                List<int> phaseNums = FindIntAttributes(g.Attributes, "phase");

-                this.introducePhaseNums[g] = 0;

-                this.hidePhaseNums[g] = int.MaxValue;

+                List<int> phaseNums = FindIntAttributes(g.Attributes, "layer");

+                this.introduceLayerNums[g] = 0;

+                this.hideLayerNums[g] = int.MaxValue;

                 if (phaseNums.Count == 0)

                 {

                     // ok

                 }

                 else if (phaseNums.Count == 1)

                 {

-                    this.hidePhaseNums[g] = phaseNums[0];

+                    this.hideLayerNums[g] = phaseNums[0];

                 }

                 else if (phaseNums.Count == 2)

                 {

-                    this.introducePhaseNums[g] = phaseNums[0];

-                    this.hidePhaseNums[g] = phaseNums[1];

+                    this.introduceLayerNums[g] = phaseNums[0];

+                    this.hideLayerNums[g] = phaseNums[1];

                 }

                 else

                 {

@@ -408,7 +408,7 @@ namespace Microsoft.Boogie
 

         public override Cmd VisitCallCmd(CallCmd node)

         {

-            int enclosingProcPhaseNum = procToActionInfo[enclosingImpl.Proc].phaseNum;

+            int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].phaseNum;

             if (procToActionInfo.ContainsKey(node.Proc))

             {

                 ActionInfo actionInfo = procToActionInfo[node.Proc];

@@ -416,13 +416,13 @@ namespace Microsoft.Boogie
                 {

                     Error(node, "Target of async call cannot be an atomic action");

                 }

-                int calleePhaseNum = procToActionInfo[node.Proc].phaseNum;

-                if (enclosingProcPhaseNum < calleePhaseNum ||

-                    (enclosingProcPhaseNum == calleePhaseNum && actionInfo is AtomicActionInfo))

+                int calleeLayerNum = procToActionInfo[node.Proc].phaseNum;

+                if (enclosingProcLayerNum < calleeLayerNum ||

+                    (enclosingProcLayerNum == calleeLayerNum && actionInfo is AtomicActionInfo))

                 {

                     Error(node, "The phase of the caller procedure must be greater than the phase of the callee");

                 }

-                else if (enclosingProcPhaseNum == calleePhaseNum && enclosingImpl.OutParams.Count > 0)

+                else if (enclosingProcLayerNum == calleeLayerNum && enclosingImpl.OutParams.Count > 0)

                 {

                     HashSet<Variable> outParams = new HashSet<Variable>(enclosingImpl.OutParams);

                     foreach (var x in node.Outs)

@@ -437,7 +437,7 @@ namespace Microsoft.Boogie
                         }

                     }

                 }

-                if (actionInfo.availableUptoPhaseNum < enclosingProcPhaseNum)

+                if (actionInfo.availableUptoLayerNum < enclosingProcLayerNum)

                 {

                     Error(node, "The callee is not available in the phase of the caller procedure");

                 }

@@ -447,30 +447,30 @@ namespace Microsoft.Boogie
 

         public override Cmd VisitParCallCmd(ParCallCmd node)

         {

-            int enclosingProcPhaseNum = procToActionInfo[enclosingImpl.Proc].phaseNum;

+            int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].phaseNum;

             bool isLeftMover = true;

             bool isRightMover = true;

-            int maxCalleePhaseNum = 0;

+            int maxCalleeLayerNum = 0;

             int numAtomicActions = 0;

             foreach (CallCmd iter in node.CallCmds)

             {

                 ActionInfo actionInfo = procToActionInfo[iter.Proc];

                 isLeftMover = isLeftMover && actionInfo.IsLeftMover;

                 isRightMover = isRightMover && actionInfo.IsRightMover;

-                if (actionInfo.phaseNum > maxCalleePhaseNum)

+                if (actionInfo.phaseNum > maxCalleeLayerNum)

                 { 

-                    maxCalleePhaseNum = actionInfo.phaseNum; 

+                    maxCalleeLayerNum = actionInfo.phaseNum; 

                 }

                 if (actionInfo is AtomicActionInfo)

                 {

                     numAtomicActions++;

                 }

             }

-            if (maxCalleePhaseNum < enclosingProcPhaseNum && !isLeftMover && !isRightMover && node.CallCmds.Count > 1)

+            if (maxCalleeLayerNum < enclosingProcLayerNum && !isLeftMover && !isRightMover && node.CallCmds.Count > 1)

             {

                 Error(node, "The callees in the parallel call must be all right movers or all left movers");

             }

-            if (maxCalleePhaseNum == enclosingProcPhaseNum && numAtomicActions > 0)

+            if (maxCalleeLayerNum == enclosingProcLayerNum && numAtomicActions > 0)

             {

                 Error(node, "If some callee in the parallel call has the same phase as the enclosing procedure, then no callee can be an atomic action");

             }

@@ -508,13 +508,13 @@ namespace Microsoft.Boogie
                 }

                 else

                 {

-                    if (hidePhaseNums[node.Decl] < minPhaseNum)

+                    if (hideLayerNums[node.Decl] < minLayerNum)

                     {

-                        minPhaseNum = hidePhaseNums[node.Decl];

+                        minLayerNum = hideLayerNums[node.Decl];

                     }

-                    if (introducePhaseNums[node.Decl] > maxPhaseNum)

+                    if (introduceLayerNums[node.Decl] > maxLayerNum)

                     {

-                        maxPhaseNum = introducePhaseNums[node.Decl];

+                        maxLayerNum = introduceLayerNums[node.Decl];

                     }

                 }

             }

@@ -528,8 +528,8 @@ namespace Microsoft.Boogie
         

         public override Ensures VisitEnsures(Ensures ensures)

         {

-            minPhaseNum = int.MaxValue;

-            maxPhaseNum = -1;

+            minLayerNum = int.MaxValue;

+            maxLayerNum = -1;

             canAccessSharedVars = true;

             Ensures ret = base.VisitEnsures(ensures);

             canAccessSharedVars = false;

@@ -541,19 +541,19 @@ namespace Microsoft.Boogie
             }

             else

             {

-                CheckAndAddPhases(ensures, ensures.Attributes, actionInfo.phaseNum);

+                CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.phaseNum);

             }

             return ret;

         }

         

         public override Requires VisitRequires(Requires requires)

         {

-            minPhaseNum = int.MaxValue;

-            maxPhaseNum = -1;

+            minLayerNum = int.MaxValue;

+            maxLayerNum = -1;

             canAccessSharedVars = true;

             Requires ret = base.VisitRequires(requires);

             canAccessSharedVars = false;

-            CheckAndAddPhases(requires, requires.Attributes, procToActionInfo[enclosingProc].phaseNum);

+            CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].phaseNum);

             return ret;

         }

 

@@ -561,35 +561,35 @@ namespace Microsoft.Boogie
         {

             if (enclosingImpl == null)

                 return base.VisitAssertCmd(node);

-            minPhaseNum = int.MaxValue;

-            maxPhaseNum = -1;

+            minLayerNum = int.MaxValue;

+            maxLayerNum = -1;

             canAccessSharedVars = true;

             canAccessAuxVars = true;

             Cmd ret = base.VisitAssertCmd(node);

             canAccessAuxVars = false;

             canAccessSharedVars = false;

-            CheckAndAddPhases(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].phaseNum);

+            CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].phaseNum);

             return ret;

         }

 

-        private void CheckAndAddPhases(Absy node, QKeyValue attributes, int enclosingProcPhaseNum)

+        private void CheckAndAddLayers(Absy node, QKeyValue attributes, int enclosingProcLayerNum)

         {

-            List<int> attrs = FindIntAttributes(attributes, "phase");

+            List<int> attrs = FindIntAttributes(attributes, "layer");

             if (attrs.Count == 0)

             {

                 Error(node, "phase not present");

                 return;

             }

-            absyToPhaseNums[node] = new HashSet<int>();

+            absyToLayerNums[node] = new HashSet<int>();

             foreach (int phaseNum in attrs)

             {

-                if (phaseNum > enclosingProcPhaseNum)

+                if (phaseNum > enclosingProcLayerNum)

                 {

                     Error(node, "The phase cannot be greater than the phase of enclosing procedure");

                 }

-                else if (maxPhaseNum < phaseNum && phaseNum <= minPhaseNum)

+                else if (maxLayerNum < phaseNum && phaseNum <= minLayerNum)

                 {

-                    absyToPhaseNums[node].Add(phaseNum);

+                    absyToLayerNums[node].Add(phaseNum);

                 }

                 else

                 {

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 7a037f93..345841aa 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -81,7 +81,7 @@ namespace Microsoft.Boogie
             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();

             if (simulationRelation[initialState].Count == 0)

             {

-                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at phase {1}. An action must be preceded by a yield.\n", impl.Name, currPhaseNum));

+                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at phase {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum));

             }

         }

 

@@ -97,7 +97,7 @@ namespace Microsoft.Boogie
             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();

             if (simulationRelation[initialState].Count == 0)

             {

-                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at phase {1}. An action must be succeeded by a yield.\n", impl.Name, currPhaseNum));

+                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at phase {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum));

             }

         }

 

@@ -115,7 +115,7 @@ namespace Microsoft.Boogie
             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();

             if (simulationRelation[initialState].Count == 0)

             {

-                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at phase {1}. Transactions must be separated by a yield.\n", impl.Name, currPhaseNum));

+                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at phase {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum));

             }

         }

 

@@ -124,7 +124,7 @@ namespace Microsoft.Boogie
             foreach (Cmd cmd in block.Cmds)

             {

                 AssertCmd assertCmd = cmd as AssertCmd;

-                if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && moverTypeChecker.absyToPhaseNums[assertCmd].Contains(currPhaseNum))

+                if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && moverTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum))

                 {

                     return true;

                 }

@@ -140,10 +140,10 @@ namespace Microsoft.Boogie
                 impl.PruneUnreachableBlocks();

                 Graph<Block> implGraph = Program.GraphFromImpl(impl);

                 implGraph.ComputeLoops();

-                int specPhaseNum = moverTypeChecker.procToActionInfo[impl.Proc].phaseNum;

-                foreach (int phaseNum in moverTypeChecker.AllPhaseNums)

+                int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].phaseNum;

+                foreach (int phaseNum in moverTypeChecker.AllLayerNums)

                 {

-                    if (phaseNum > specPhaseNum) continue;

+                    if (phaseNum > specLayerNum) continue;

                     YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, phaseNum, implGraph.Headers);

                 }

             }

@@ -152,7 +152,7 @@ namespace Microsoft.Boogie
         int stateCounter;

         MoverTypeChecker moverTypeChecker;

         Implementation impl;

-        int currPhaseNum;

+        int currLayerNum;

         Dictionary<Absy, int> absyToNode;

         Dictionary<int, Absy> nodeToAbsy;

         int initialState;

@@ -160,11 +160,11 @@ namespace Microsoft.Boogie
         Dictionary<Tuple<int, int>, int> edgeLabels;

         IEnumerable<Block> loopHeaders;

 

-        private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currPhaseNum, IEnumerable<Block> loopHeaders)

+        private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders)

         {

             this.moverTypeChecker = moverTypeChecker;

             this.impl = impl;

-            this.currPhaseNum = currPhaseNum;

+            this.currLayerNum = currLayerNum;

             this.loopHeaders = loopHeaders;

             this.stateCounter = 0;

             this.absyToNode = new Dictionary<Absy, int>();

@@ -227,7 +227,7 @@ namespace Microsoft.Boogie
                         if (callCmd.IsAsync)

                         {

                             ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];

-                            if (currPhaseNum <= actionInfo.phaseNum)

+                            if (currLayerNum <= actionInfo.phaseNum)

                                 edgeLabels[edge] = 'L';

                             else

                                 edgeLabels[edge] = 'B';

@@ -240,7 +240,7 @@ namespace Microsoft.Boogie
                         {

                             MoverType moverType;

                             ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];

-                            if (actionInfo.phaseNum >= currPhaseNum)

+                            if (actionInfo.phaseNum >= currLayerNum)

                             {

                                 moverType = MoverType.Top;

                             }

@@ -280,7 +280,7 @@ namespace Microsoft.Boogie
                         bool isLeftMover = true;

                         foreach (CallCmd callCmd in parCallCmd.CallCmds)

                         {

-                            if (moverTypeChecker.procToActionInfo[callCmd.Proc].phaseNum >= currPhaseNum)

+                            if (moverTypeChecker.procToActionInfo[callCmd.Proc].phaseNum >= currLayerNum)

                             {

                                 isYield = true;

                             }

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index f938b0f8..01212da1 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -505,8 +505,8 @@ namespace Microsoft.Boogie {
     public string OwickiGriesDesugaredOutputFile = null;

     public bool TrustAtomicityTypes = false;

     public bool TrustNonInterference = false;

-    public int TrustPhasesUpto = -1;

-    public int TrustPhasesDownto = int.MaxValue;

+    public int TrustLayersUpto = -1;

+    public int TrustLayersDownto = int.MaxValue;

 

     public enum VCVariety {

       Structured,

@@ -766,17 +766,17 @@ namespace Microsoft.Boogie {
           }

           return true;

 

-        case "trustPhasesUpto":

+        case "trustLayersUpto":

           if (ps.ConfirmArgumentCount(1))

           {

-              ps.GetNumericArgument(ref TrustPhasesUpto);

+              ps.GetNumericArgument(ref TrustLayersUpto);

           }

           return true;

 

-        case "trustPhasesDownto":

+        case "trustLayersDownto":

           if (ps.ConfirmArgumentCount(1))

           {

-              ps.GetNumericArgument(ref TrustPhasesDownto);

+              ps.GetNumericArgument(ref TrustLayersDownto);

           }

           return true;

 

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index ad75f1f9..b74b52c5 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -3,10 +3,10 @@
 type X;

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

 const nil: X;

-var {:phase 1} ghostLock: X;

-var {:phase 1} lock: X;

-var {:phase 1} currsize: int;

-var {:phase 1} newsize: int;

+var {:layer 1} ghostLock: X;

+var {:layer 1} lock: X;

+var {:layer 1} currsize: int;

+var {:layer 1} newsize: int;

 

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

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

@@ -24,27 +24,27 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
     (ghostLock == nil <==> currsize == newsize)

 }

 

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

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

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

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

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

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

 {

    yield;

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

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

 }

 

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

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

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

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

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

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

 {

     yield;

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

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

 }

 

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

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

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

 

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

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

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

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

 {

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

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

@@ -55,24 +55,24 @@ requires {:phase 1} xls' == mapconstbool(true);
     call Init(xls);

     

     yield;

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

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

 

     while (*)

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

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

     {

         call xls, tid := Allocate(xls);

 	yield;

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

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

         async call Thread(tid);

 	yield;

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

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

     }

     yield;

 }

 

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

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

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

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

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

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

 {

     var start, size, bytesRead: int;

 

@@ -81,11 +81,11 @@ requires {:phase 1} Inv(ghostLock, currsize, newsize);
     call bytesRead := Read(tid, start, size);

 }

 

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

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

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

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

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

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

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

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

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

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

 {

     var i, tmp: int;

 

@@ -121,19 +121,19 @@ COPY_TO_BUFFER:
     call ReadCache(tid, start, bytesRead);

 }

 

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

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

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

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

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

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

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

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

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

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

 {

     var j: int;

 

     par YieldToWriteCache(tid);

     call j := ReadCurrsize(tid);

     while (j < index)

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

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

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

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

     {

         par YieldToWriteCache(tid);

         call WriteCacheEntry(tid, j);

@@ -142,12 +142,12 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsiz
     par YieldToWriteCache(tid);

 }

 

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

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

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

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

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

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

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

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

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

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

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

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

 {

     var j: int;

 

@@ -155,11 +155,11 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize);
 

     j := 0;

     while(j < bytesRead)

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

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

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

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

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

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

     {

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

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

         call ReadCacheEntry(tid, start + j);

         j := j + 1;

 	par YieldToReadCache(tid);

@@ -168,29 +168,29 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize);
     par YieldToReadCache(tid);

 }

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 1e98fa6d..9eb11495 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -2,8 +2,8 @@
 // RUN: %diff "%s.expect" "%t"

 type X;

 const nil: X;

-var {:phase 1} l: X;

-var {:phase 1} x: int;

+var {:layer 1} l: X;

+var {:layer 1} x: int;

 

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

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

@@ -12,9 +12,9 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
 }

 

 procedure Allocate() returns ({:linear "tid"} xls: X);

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

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

 

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

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

 {

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

     var val: int;

@@ -29,17 +29,17 @@ procedure {:yields} {:phase 1} main()
     }

     yield;

 }

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

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

 {

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

     tid := tid';

@@ -49,19 +49,19 @@ requires {:phase 1} tid' != nil;
     call tid := Yield(tid);

     call Set(val);

     call tid := Yield(tid);

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

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

     call tid := Yield(tid);

     call Unlock();

     yield;

 }

 

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

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

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

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

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

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

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

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

 {

     tid := tid';

     yield;

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

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

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

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

 }
\ No newline at end of file
diff --git a/Test/og/Program1.bpl b/Test/og/Program1.bpl
index 5a3ba93d..5704b680 100644
--- a/Test/og/Program1.bpl
+++ b/Test/og/Program1.bpl
@@ -1,32 +1,32 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} x:int;

+var {:layer 1} x:int;

 

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

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

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

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

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

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

 { 

     yield;

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

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

     call Incr(1); 

     yield;

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

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

     call Incr(1); 

     yield;

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

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

     call Incr(1); 

     yield;

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

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

 }

 

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

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

 { 

     yield;

     call Incr(3); 

     yield;

 }

 

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

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

 ensures {:atomic}

 |{A:

   x := x + val; return true;

diff --git a/Test/og/Program2.bpl b/Test/og/Program2.bpl
index a3fbf231..f9d28a5d 100644
--- a/Test/og/Program2.bpl
+++ b/Test/og/Program2.bpl
@@ -1,18 +1,18 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} x:int;

+var {:layer 1} x:int;

 

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

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

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

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

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

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

 {

     yield;

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

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

 }

 

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

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

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

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

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

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

 { 

     call yield_x(5);

     call Incr(1); 

@@ -23,14 +23,14 @@ ensures {:phase 1} x >= 8;
     call yield_x(8);

 }

 

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

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

 { 

     yield;

     call Incr(3); 

     yield;

 }

 

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

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

 ensures {:atomic}

 |{A:

   x := x + val; return true;

diff --git a/Test/og/Program3.bpl b/Test/og/Program3.bpl
index 0933afe8..ae8c6eed 100644
--- a/Test/og/Program3.bpl
+++ b/Test/og/Program3.bpl
@@ -1,17 +1,17 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} x:int;

+var {:layer 1} x:int;

 

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

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

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

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

 {

     yield;

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

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

 }

 

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

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

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

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

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

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

 { 

     call yield_x();

     call Incr(1); 

@@ -22,14 +22,14 @@ ensures {:phase 1} x >= 8;
     call yield_x();

 }

 

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

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

 { 

     yield;

     call Incr(3); 

     yield;

 }

 

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

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

 ensures {:atomic}

 |{A:

   x := x + val; return true;

diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl
index 5005f77c..61d4fcdc 100644
--- a/Test/og/Program4.bpl
+++ b/Test/og/Program4.bpl
@@ -13,11 +13,11 @@ function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
   x

 }

 

-var {:phase 1} a:[Tid]int;

+var {:layer 1} a:[Tid]int;

 

 procedure Allocate() returns ({:linear "tid"} tid:Tid); 

 

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

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

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

 

     yield;

@@ -29,28 +29,28 @@ procedure {:yields} {:phase 1} main() {
     yield;

 }

 

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

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

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

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

 { 

     var t:int;

 

     yield;

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

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

     call t := Read(tid); 

     yield;

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

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

     call Write(tid, t + 1); 

     yield;

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

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

 }

 

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

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

 ensures {:atomic}

 |{A:

   val := a[tid]; return true;

 }|;

 

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

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

 ensures {:atomic}

 |{A:

   a[tid] := val; return true;

diff --git a/Test/og/Program5.bpl b/Test/og/Program5.bpl
index 51d5fe3c..af87eac5 100644
--- a/Test/og/Program5.bpl
+++ b/Test/og/Program5.bpl
@@ -5,8 +5,8 @@ const unique nil: Tid;
 function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;

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

 

-var {:phase 0,3} Color:int;

-var {:phase 0,3} lock:Tid;

+var {:layer 0,3} Color:int;

+var {:layer 0,3} lock:Tid;

 

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

 {

@@ -26,14 +26,14 @@ function {:inline} White(i:int) returns(bool) { i == 1 }
 function {:inline} Gray(i:int) returns(bool) { i == 2 }

 function {:inline} Black(i:int) returns(bool) { i >= 3 }

 

-procedure {:yields} {:phase 2} YieldColorOnlyGetsDarker()

-ensures {:phase 2} Color >= old(Color);

+procedure {:yields} {:layer 2} YieldColorOnlyGetsDarker()

+ensures {:layer 2} Color >= old(Color);

 {

   yield;

-  assert {:phase 2} Color >= old(Color);

+  assert {:layer 2} Color >= old(Color);

 }

 

-procedure {:yields} {:phase 2,3} TopWriteBarrier({:linear "tid"} tid:Tid)

+procedure {:yields} {:layer 2,3} TopWriteBarrier({:linear "tid"} tid:Tid)

 ensures {:atomic} |{ A: assert tid != nil; goto B, C; 

                      B: assume White(Color); Color := GRAY(); return true; 

                      C: return true;}|;

@@ -46,7 +46,7 @@ ensures {:atomic} |{ A: assert tid != nil; goto B, C;
   yield;

 }

 

-procedure {:yields} {:phase 1,2} MidWriteBarrier({:linear "tid"} tid:Tid)

+procedure {:yields} {:layer 1,2} MidWriteBarrier({:linear "tid"} tid:Tid)

 ensures {:atomic} |{ A: assert tid != nil; goto B, C; 

                      B: assume White(Color); Color := GRAY(); return true; 

                      C: return true; }|;

@@ -60,18 +60,18 @@ ensures {:atomic} |{ A: assert tid != nil; goto B, C;
        yield;

 }

 

-procedure {:yields} {:phase 0,1} AcquireLock({:linear "tid"} tid: Tid);

+procedure {:yields} {:layer 0,1} AcquireLock({:linear "tid"} tid: Tid);

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

 

-procedure {:yields} {:phase 0,1} ReleaseLock({:linear "tid"} tid: Tid);

+procedure {:yields} {:layer 0,1} ReleaseLock({:linear "tid"} tid: Tid);

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

 

-procedure {:yields} {:phase 0,1} SetColorLocked({:linear "tid"} tid:Tid, newCol:int); 

+procedure {:yields} {:layer 0,1} SetColorLocked({:linear "tid"} tid:Tid, newCol:int); 

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

 

-procedure {:yields} {:phase 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns (col:int);

+procedure {:yields} {:layer 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns (col:int);

   ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|;

 

-procedure {:yields} {:phase 1,2} GetColorNoLock() returns (col:int);

+procedure {:yields} {:layer 1,2} GetColorNoLock() returns (col:int);

   ensures {:atomic} |{A: col := Color; return true;}|;

 

diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl
index f3a4235e..f5d71caa 100644
--- a/Test/og/akash.bpl
+++ b/Test/og/akash.bpl
@@ -19,24 +19,24 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool
 }

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

-ensures {:phase 1} xls != 0;

+ensures {:layer 1} xls != 0;

 

 procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);

-ensures {:phase 1} xls == mapconstbool(true);

+ensures {:layer 1} xls == mapconstbool(true);

 

 procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);

-ensures {:phase 1} xls == mapconstbool(true);

+ensures {:layer 1} xls == mapconstbool(true);

 

-var {:phase 1} g: int;

-var {:phase 1} h: int;

+var {:layer 1} g: int;

+var {:layer 1} h: int;

 

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

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

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

 

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

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

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

 

-procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

 {

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

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

@@ -48,7 +48,7 @@ procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:line
     yield;

     call SetG(0);

     yield;

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

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

 

     yield;

     call tid_child := Allocate();

@@ -58,7 +58,7 @@ procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:line
     call SetH(0);

 

     yield;

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

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

 

     yield;

     call tid_child := Allocate();

@@ -67,8 +67,8 @@ procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:line
     yield;

 }

 

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

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

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

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

 {

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

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

@@ -86,8 +86,8 @@ requires {:phase 1} x_in != mapconstbool(false);
     yield;

 }

 

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

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

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

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

 {

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

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

diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl
index 1d2c9a03..ac2ec1b6 100644
--- a/Test/og/bar.bpl
+++ b/Test/og/bar.bpl
@@ -1,47 +1,47 @@
 // RUN: %boogie -noinfer "%s" > "%t"

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

-var {:phase 1} g:int;

+var {:layer 1} g:int;

 

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

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

 {

   yield;

   call Incr();

   yield;

 }

 

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

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

 ensures {:atomic}

 |{A:

   g := g + 1; return true;

 }|;

 

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

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

 ensures {:atomic}

 |{A:

   g := v; return true;

 }|;

 

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

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

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

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

 {

   yield;

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

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

 }

 

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

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

 {

   call PC();

 }

 

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

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

 {

   yield;

   call Set(3);

   call PC();

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

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

 }

 

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

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

 {

   yield;

   while (*)

diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index be519470..e6a673d8 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -15,18 +15,18 @@ function map(lmap): [int]int;
 function cons([int]bool, [int]int) : lmap;

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

 

-var {:phase 3} {:linear "mem"} g: lmap;

-var {:phase 3} lock: X;

-var {:phase 1} b: bool;

+var {:layer 3} {:linear "mem"} g: lmap;

+var {:layer 3} lock: X;

+var {:layer 1} b: bool;

 

 const p: int;

 

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

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

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

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

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

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

 {

     yield;

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

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

 }

 

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

@@ -34,17 +34,17 @@ function {:inline} InvLock(lock: X, b: bool) : bool
     lock != nil <==> b

 }

 

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

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

 {

     yield;

 }

 

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

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

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

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

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

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

 {

     yield;

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

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

 }

 

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

@@ -52,11 +52,11 @@ function {:inline} Inv(g: lmap) : bool
     dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4]

 }

 

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

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

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

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

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

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

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

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

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

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

 {

     var t: int;

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

@@ -74,49 +74,49 @@ ensures {:phase 3} Inv(g);
 }

 

 

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

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

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

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

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

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

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

 {

   par Yield1() | Yield2();

   call TransferToGlobal(tid, l);

   par Yield1() | Yield2();

 }

 

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

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

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

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

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

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

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

 {

   par Yield1() | Yield2();

   call l := TransferFromGlobal(tid);

   par Yield1() | Yield2();

 }

 

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

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

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

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

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

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

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

 {

   par Yield1() | Yield2();

   call Acquire(tid);

   par Yield1() | Yield2();

 }

 

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

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

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

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

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

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

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

 {

   par Yield1() | Yield2();

   call Release(tid);

   par Yield1() | Yield2();

 }

 

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

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

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

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

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

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

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

 {

     var status: bool;

@@ -124,7 +124,7 @@ ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|;
 

     par Yield1();

     L: 

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

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

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

 	par Yield1();

         goto A, B;

@@ -139,36 +139,36 @@ ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|;
 	goto L;

 }

 

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

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

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

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

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

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

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

 {

     par Yield1();

     call CLEAR(tid, false);

     par Yield1();

 }

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

 ensures {:atomic} |{ 

 A: goto B, C; 

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

 C: status := false; return true; 

 }|;

 

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

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

 ensures {:atomic} |{ 

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

 }|;

diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index eae47e12..bd8c6ef7 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.bpl
@@ -1,47 +1,47 @@
 // RUN: %boogie -noinfer "%s" > "%t"

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

-var {:phase 1} g:int;

+var {:layer 1} g:int;

 

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

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

 {

   yield;

   call Incr();

   yield;

 }

 

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

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

 ensures {:atomic}

 |{A:

   g := g + 1; return true;

 }|;

 

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

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

 ensures {:atomic}

 |{A:

   g := v; return true;

 }|;

 

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

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

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

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

 {

   yield;

   call Set(3);

   yield;

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

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

 }

 

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

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

 {

   call PC();

 }

 

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

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

 {

   call PC();

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

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

 }

 

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

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

 {

   yield;

   while (*)

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index 228062a3..4b6692c5 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -20,26 +20,26 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
   xs

 }

 

-var {:phase 1} x: int;

-var {:phase 1} l: [X]bool;

+var {:layer 1} x: int;

+var {:layer 1} l: [X]bool;

 

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

 ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();

 

 procedure Allocate() returns ({:linear "tid"} xls: [X]bool);

 

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

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

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

 

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

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

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

 

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

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

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

 

 

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

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

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

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

 {

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

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

@@ -52,8 +52,8 @@ requires {:phase 1} tidls' != None() && xls' == All();
     yield;

     call Set(42);

     yield;

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

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

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

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

     call xls1, xls2 := Split(xls);

     call lsChild := Allocate();

     assume (lsChild != None());

@@ -66,8 +66,8 @@ requires {:phase 1} tidls' != None() && xls' == All();
     yield;

 }

 

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

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

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

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

 {

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

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

@@ -78,12 +78,12 @@ requires {:phase 1} tidls' != None() && xls' != None();
     yield;

     call Lock(tidls);

     yield;

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

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

     call Set(0);

     yield;

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

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

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

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

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

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

     call Unlock();

     yield;

 }

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index 11d24605..93ede868 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -20,8 +20,8 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
   xs

 }

 

-var {:phase 1} x: int;

-var {:phase 1} l: X;

+var {:layer 1} x: int;

+var {:layer 1} l: X;

 const nil: X;

 

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

@@ -30,17 +30,17 @@ ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
 procedure Allocate() returns ({:linear "tid"} xls: X);

 ensures xls != nil;

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

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

 {

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

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

@@ -54,8 +54,8 @@ requires {:phase 1} tidls' != nil && xls' == All();
     yield;

     call Set(42);

     yield;

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

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

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

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

     call xls1, xls2 := Split(xls);

     call lsChild := Allocate();

     yield;

@@ -66,8 +66,8 @@ requires {:phase 1} tidls' != nil && xls' == All();
     yield;

 }

 

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

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

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

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

 {

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

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

@@ -78,13 +78,13 @@ requires {:phase 1} tidls' != nil && xls' != None();
     yield;

     call Lock(tidls);

     yield;

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

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

     call Set(0);

     yield;

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

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

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

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

     yield;

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

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

     call Unlock();

     yield;

 }

diff --git a/Test/og/lock-introduced.bpl b/Test/og/lock-introduced.bpl
index 1f576c42..c9650215 100644
--- a/Test/og/lock-introduced.bpl
+++ b/Test/og/lock-introduced.bpl
@@ -8,26 +8,26 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
 

 type X;

 const nil: X;

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

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

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

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

 

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

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

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

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

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

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

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

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

 {

     yield;

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

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

     while (*) 

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

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

     {

         call Enter(tid);

     	call Leave(tid);

         yield;

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

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

     }    

     yield;

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

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

 }

 

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

@@ -35,32 +35,32 @@ function {:inline} InvLock(lock: X, b: bool) : bool
     lock != nil <==> b

 }

 

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

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

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

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

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

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

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

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

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

 {

     yield;

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

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

     call LowerEnter(tid);

     yield;

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

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

 }

 

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

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

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

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

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

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

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

 {

     yield;

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

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

     call LowerLeave();

     yield;

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

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

 }

 

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

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

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

 {

     var status: bool;

@@ -80,7 +80,7 @@ ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|;
 	goto L;

 }

 

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

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

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

 {

     yield;

@@ -88,13 +88,13 @@ ensures {:atomic} |{ A: b := false; lock := nil; return true; }|;
     yield;

 }

 

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

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

 ensures {:atomic} |{ 

 A: goto B, C; 

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

 C: status := false; return true; 

 }|;

 

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

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

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

 

diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index 86c382d8..db563cce 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -1,8 +1,8 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 2} b: bool;

+var {:layer 2} b: bool;

 

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

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

 {

     yield;

     while (*)

@@ -13,7 +13,7 @@ procedure {:yields} {:phase 2} main()
     yield;

 }

 

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

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

 {

     yield;

     while (*) 

@@ -26,7 +26,7 @@ procedure {:yields} {:phase 2} Customer()
     yield;

 }

 

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

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

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

 {

     var status: bool;

@@ -46,12 +46,12 @@ ensures {:atomic} |{ A: assume !b; b := true; return true; }|;
 	goto L;

 }

 

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

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

 ensures {:atomic} |{ 

 A: goto B, C; 

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

 C: status := false; return true; 

 }|;

 

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

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

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

diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index 354821e7..7f0dde84 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -1,8 +1,8 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 2} b: int;

+var {:layer 2} b: int;

 

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

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

 {

     yield;

     while (*)

@@ -13,7 +13,7 @@ procedure {:yields} {:phase 2} main()
     yield;

 }

 

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

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

 {

     yield;

     while (*) 

@@ -26,7 +26,7 @@ procedure {:yields} {:phase 2} Customer()
     yield;

 }

 

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

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

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

 {

     var _old, curr: int;

@@ -49,15 +49,15 @@ ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|;
     yield;

 }

 

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

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

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

 

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

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

 ensures {:atomic} |{ 

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

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

 C: assume _old != prev; return true; 

 }|;

 

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

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

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

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index a522f304..0f56dd7e 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -20,7 +20,7 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
 

 axiom (max > 0);

 

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

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

 ensures {:right} |{ A: 

                       assert 0 <= i && i < max;

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

@@ -30,7 +30,7 @@ ensures {:right} |{ A:
                     }|;

 

 

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

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

 ensures {:left} |{ A: 

                      assert 0 <= i && i < max;

                      assert lock[i] == tid;

@@ -40,7 +40,7 @@ ensures {:left} |{ A:
                     }|;

 

 

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

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

 ensures {:both} |{ A: 

                      assert 0 <= j && j < max;

                      assert lock[j] == tid;

@@ -50,7 +50,7 @@ ensures {:both} |{ A:
                     }|;

 

 

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

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

 ensures {:both} |{ A: 

                      assert x != null;

                      assert owner[j] == nil;

@@ -63,7 +63,7 @@ ensures {:both} |{ A:
                     }|;

 

 

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

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

 ensures {:left} |{ A: 

                      assert owner[j] == tid;

                      assert 0 <= j && j < max;

@@ -75,7 +75,7 @@ ensures {:left} |{ A:
                      return true;

                     }|;

 

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

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

 ensures {:both} |{ A: 

                      assert 0 <= j && j < max;

                      assert lock[j] == tid;

@@ -86,7 +86,7 @@ ensures {:both} |{ A:
                      return true;

                     }|;

 

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

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

 ensures {:both} |{ A: 

                        assert 0 <= j && j < max;

                        assert lock[j] == tid;

@@ -95,9 +95,9 @@ ensures {:both} |{ A:
                        return true;

                     }|;

 

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

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

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

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

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

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

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

                           assert x != null; 

 			  goto B, C;

@@ -118,8 +118,8 @@ ensures {:right}  |{   A: assert tid != nil && tid != done;
 

 	j := 0;

 	while(j < max)

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

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

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

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

 	{

                 call acquire(j, tid);

                 call elt_j := getElt(j, tid);

@@ -144,11 +144,11 @@ ensures {:right}  |{   A: assert tid != nil && tid != done;
 	return;

 }

 

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

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

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

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

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

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

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

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

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

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

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

                         A: goto B, C;

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

@@ -171,11 +171,11 @@ ensures {:atomic}  |{ var r:int;
 		return;

 	}

         par Yield1();

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

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

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

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

 	call acquire(i, tid);

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

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

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

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

         call setValid(i, tid);   

 	call release(i, tid);

 	result := true; 

@@ -183,11 +183,11 @@ ensures {:atomic}  |{ var r:int;
 	return;

 }

 

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

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

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

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

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

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

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

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

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

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

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

                         var ry:int;

                         A: goto B, C;

@@ -234,13 +234,13 @@ ensures {:atomic}  |{ var rx:int;
 	}

 

         par Yield1();

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

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

 	call acquire(i, tid);

 	call acquire(j, tid);

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

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

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

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

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

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

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

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

         call setValid(i, tid);   

         call setValid(j, tid);   

 	call release(j, tid);

@@ -250,11 +250,11 @@ ensures {:atomic}  |{ var rx:int;
 	return;

 }

 

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

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

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

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

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

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

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

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

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

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

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

                           assert x != null;

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

@@ -270,10 +270,10 @@ ensures {:atomic}  |{ A: assert tid != nil && tid != done;
 	j := 0;

 

 	while(j < max)

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

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

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

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

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

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

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

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

 	{

                 call acquire(j, tid);

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

@@ -294,20 +294,20 @@ ensures {:atomic}  |{ A: assert tid != nil && tid != done;
 	return;

 }

 

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

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

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

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

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

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

 {

 	yield;

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

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

 }

 

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

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

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

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

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

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

 {

         yield;

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

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

 }

 

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

@@ -315,10 +315,10 @@ function {:inline} Inv(valid: [int]bool, elt: [int]int, owner: [int]X): (bool)
    (forall i:int :: 0 <= i && i < max ==> (elt[i] == null <==> (!valid[i] && owner[i] == nil)))

 }

 

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

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

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

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

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

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

 {

     yield;

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

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

 }

diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index 537a5f4b..3faa9156 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -2,7 +2,7 @@
 // RUN: %diff "%s.expect" "%t"

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

 

-var {:phase 1} g:int;

+var {:layer 1} g:int;

 

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

 {

@@ -13,25 +13,25 @@ procedure Allocate_Perm({:linear_in "Perm"} Permissions: [int]bool) returns ({:l
 requires Permissions == mapconstbool(true);

 ensures xls == mapconstbool(true);

 

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

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

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

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

 {

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

   permVar_out := permVar_in;

 

   yield;

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

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

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

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

 

   call IncrG();

 

   yield;

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

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

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

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

 }

 

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

-requires {:phase 0,1} Permissions == mapconstbool(true);

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

+requires {:layer 0,1} Permissions == mapconstbool(true);

 {

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

 

@@ -42,8 +42,8 @@ requires {:phase 0,1} Permissions == mapconstbool(true);
   yield;

 }

 

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

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

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

 

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

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

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

diff --git a/Test/og/one.bpl b/Test/og/one.bpl
index 2da898d6..45cbbda3 100644
--- a/Test/og/one.bpl
+++ b/Test/og/one.bpl
@@ -1,18 +1,18 @@
 // RUN: %boogie -noinfer "%s" > "%t"

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

-var {:phase 1} x:int;

+var {:layer 1} x:int;

 

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

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

 ensures {:atomic}

 |{A:

   x := v; return true;

 }|;

 

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

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

 {

   yield;

   call Set(5);

   yield;

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

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

 }

 

diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
index 6b2ea3a8..96231f5b 100644
--- a/Test/og/parallel1.bpl
+++ b/Test/og/parallel1.bpl
@@ -1,43 +1,43 @@
 // RUN: %boogie -noinfer "%s" > "%t"

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

-var {:phase 1} g:int;

+var {:layer 1} g:int;

 

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

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

 {

   yield;

   call Incr();

   yield;

 }

 

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

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

 ensures {:atomic}

 |{A:

   g := g + 1; return true;

 }|;

 

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

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

 ensures {:atomic}

 |{A:

   g := v; return true;

 }|;

 

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

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

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

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

 {

   yield;

   call Set(3);

   yield;

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

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

 }

 

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

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

 {

   call PC();

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

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

   yield;

 }

 

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

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

 {

   yield;

   while (*)

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 1906d00b..20de0875 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} a:[int]int;

+var {:layer 1} a:[int]int;

 

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

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

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

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

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

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

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

 

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

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

 {

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

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

@@ -23,29 +23,29 @@ procedure {:yields} {:phase 1} main()
     par i := u(i) | j := u(j);

 }

 

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

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

 {

     i := i';

 

     yield;

     call Write(i, 42);

     call Yield(i);

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

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

 }

 

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

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

 {

     i := i';

 

     yield;

     call Write(i, 42);

     yield;

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

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

 }

 

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

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

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

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

 {

     yield;

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

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

 }
\ No newline at end of file
diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index f061f8be..bb9c631b 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} a:int;

+var {:layer 1} a:int;

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

@@ -10,7 +10,7 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
   MapConstBool(false)[x := true]

 }

 

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

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

 {

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

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

@@ -19,19 +19,19 @@ procedure {:yields} {:phase 1} main()
   par i := t(i) | j := t(j);

 }

 

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

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

 {

   i := i';

   call Yield();

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

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

   call Incr();

   yield;

 }

 

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

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

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

 

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

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

 {

   yield;

 }

diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index 751cc666..7ef565e1 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} a:[int]int;

+var {:layer 1} a:[int]int;

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

@@ -10,10 +10,10 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
   MapConstBool(false)[x := true]

 }

 

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

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

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

 

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

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

 {

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

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

@@ -23,29 +23,29 @@ procedure {:yields} {:phase 1} main()
     par i := u(i) | j := u(j);

 }

 

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

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

 {

     i := i';

 

     yield;

     call Write(i, 42);

     call Yield(i);

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

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

 }

 

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

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

 {

     i := i';

 

     yield;

     call Write(i, 42);

     yield;

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

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

 }

 

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

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

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

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

 {

     yield;

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

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

 }
\ No newline at end of file
diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index 4df74778..66ae5285 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 1} x: int;

+var {:layer 1} x: int;

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

 

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

@@ -14,10 +14,10 @@ procedure Split({:linear_in "Perm"} xls: [int]bool) returns ({:linear "Perm"} xl
   ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);

 

 

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

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

-   free requires {:phase 1} permVar_in[0];

-   free requires {:phase 1} x == 0;

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

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

+   free requires {:layer 1} permVar_in[0];

+   free requires {:layer 1} x == 0;

 {

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

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

@@ -25,33 +25,33 @@ procedure {:yields} {:phase 1} mainE({:linear_in "Perm"} permVar_in: [int]bool)
     permVar_out := permVar_in;

 

     yield;

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

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

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

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

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

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

 

     call permVar_out, permVarOut2 := Split(permVar_out);

     async call foo(permVarOut2);

     yield;

 }

 

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

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

-  free requires {:phase 1} permVar_in[1];

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

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

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

+  free requires {:layer 1} permVar_in[1];

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

 {

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

   permVar_out := permVar_in;

   

   yield;

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

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

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

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

 

   call Incr();

 

   yield;

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

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

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

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

 }

 

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

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

 ensures {:atomic} |{A: x := x + 1; return true; }|;
\ No newline at end of file
diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index 3730d490..305f1ed1 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -19,24 +19,24 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool
 }

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

-ensures {:phase 1} xls != 0;

+ensures {:layer 1} xls != 0;

 

 procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);

-ensures {:phase 1} xls == mapconstbool(true);

+ensures {:layer 1} xls == mapconstbool(true);

 

 procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);

-ensures {:phase 1} xls == mapconstbool(true);

+ensures {:layer 1} xls == mapconstbool(true);

 

-var {:phase 1} g: int;

-var {:phase 1} h: int;

+var {:layer 1} g: int;

+var {:layer 1} h: int;

 

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

+procedure {:yields} {:layer 0,1} SetG(val:int);

 ensures {:atomic} |{A: g := val; return true; }|;

 

-procedure {:yields} {:phase 0,1} SetH(val:int);

+procedure {:yields} {:layer 0,1} SetH(val:int);

 ensures {:atomic} |{A: h := val; return true; }|;

 

-procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

 {

     var {:linear "1"} x: [int]bool;

     var {:linear "2"} y: [int]bool;

@@ -48,22 +48,22 @@ procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:line
     yield;

     call SetG(0);

     yield;

-    assert {:phase 1} x == mapconstbool(true);    

-    assert {:phase 1} g == 0;    

+    assert {:layer 1} x == mapconstbool(true);    

+    assert {:layer 1} g == 0;    

 

     yield;

     call tid_child := Allocate();

     async call B(tid_child, x);

 

     yield;

-    assert {:phase 1} x == mapconstbool(true);    

-    assert {:phase 1} g == 0;

+    assert {:layer 1} x == mapconstbool(true);    

+    assert {:layer 1} g == 0;

 

     yield;

     call SetH(0);

 

     yield;

-    assert {:phase 1} h == 0 && y == mapconstbool(true);    

+    assert {:layer 1} h == 0 && y == mapconstbool(true);    

 

     yield;

     call tid_child := Allocate();

@@ -72,8 +72,8 @@ procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:line
     yield;

 }

 

-procedure {:yields} {:phase 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) 

-requires {:phase 1} x_in != mapconstbool(false);

+procedure {:yields} {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) 

+requires {:layer 1} x_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "1"} x: [int]bool;

@@ -85,8 +85,8 @@ requires {:phase 1} x_in != mapconstbool(false);
     yield;

 }

 

-procedure {:yields} {:phase 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) 

-requires {:phase 1} y_in != mapconstbool(false);

+procedure {:yields} {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) 

+requires {:layer 1} y_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "2"} y: [int]bool;

diff --git a/Test/og/termination.bpl b/Test/og/termination.bpl
index 35064f77..2d5542dd 100644
--- a/Test/og/termination.bpl
+++ b/Test/og/termination.bpl
@@ -1,12 +1,12 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

-procedure {:yields} {:phase 0} X();

+procedure {:yields} {:layer 0} X();

 ensures {:atomic} |{ A: return true; }|;

 

-procedure {:yields} {:phase 0} Y();

+procedure {:yields} {:layer 0} Y();

 ensures {:left} |{ A: return true; }|;

 

-procedure {:yields} {:phase 1} main() {

+procedure {:yields} {:layer 1} main() {

   yield;

   call X();

   while (*)

@@ -14,5 +14,5 @@ procedure {:yields} {:phase 1} main() {
     call Y();

   }

   yield;

-  assert {:phase 1} true;

+  assert {:layer 1} true;

 }

diff --git a/Test/og/termination2.bpl b/Test/og/termination2.bpl
index d0d88a22..840c27c1 100644
--- a/Test/og/termination2.bpl
+++ b/Test/og/termination2.bpl
@@ -1,19 +1,19 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

-procedure {:yields} {:phase 0} X();

+procedure {:yields} {:layer 0} X();

 ensures {:atomic} |{ A: return true; }|;

 

-procedure {:yields} {:phase 0} Y();

+procedure {:yields} {:layer 0} Y();

 ensures {:left} |{ A: return true; }|;

 

-procedure {:yields} {:phase 1} main() {

+procedure {:yields} {:layer 1} main() {

   yield;

   call X();

   while (*)

-  invariant {:terminates} {:phase 1} true;

+  invariant {:terminates} {:layer 1} true;

   {

     call Y();

   }

   yield;

-  assert {:phase 1} true;

+  assert {:layer 1} true;

 }

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 9c1b7c9a..70fe1d4c 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -8,10 +8,10 @@ axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
 type X;

 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;

 const nil: X;

-var {:phase 2} t: int;

-var {:phase 2} s: int;

-var {:phase 2} cs: X;

-var {:phase 2} T: [int]bool;

+var {:layer 2} t: int;

+var {:layer 2} s: int;

+var {:layer 2} cs: X;

+var {:layer 2} T: [int]bool;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

@@ -34,10 +34,10 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)
 }

 

 procedure Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

-ensures {:phase 1} {:phase 2} xl != nil;

+ensures {:layer 1} {:layer 2} xl != nil;

 

-procedure {:yields} {:phase 2} main({:linear_in "tid"} xls':[X]bool)

-requires {:phase 2} xls' == mapconstbool(true);

+procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)

+requires {:layer 2} xls' == mapconstbool(true);

 {

     var {:linear "tid"} tid: X;

     var {:linear "tid"} xls: [X]bool;

@@ -50,8 +50,8 @@ requires {:phase 2} xls' == mapconstbool(true);
     par Yield1() | Yield2();

 

     while (*)

-    invariant {:phase 1} Inv1(T, t);

-    invariant {:phase 2} Inv2(T, s, cs);

+    invariant {:layer 1} Inv1(T, t);

+    invariant {:layer 2} Inv2(T, s, cs);

     {

         call xls, tid := Allocate(xls);

         async call Customer(tid);

@@ -60,14 +60,14 @@ requires {:phase 2} xls' == mapconstbool(true);
     par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 2} Customer({:linear_in "tid"} tid: X)

-requires {:phase 1} Inv1(T, t);

-requires {:phase 2} tid != nil && Inv2(T, s, cs);

+procedure {:yields} {:layer 2} Customer({:linear_in "tid"} tid: X)

+requires {:layer 1} Inv1(T, t);

+requires {:layer 2} tid != nil && Inv2(T, s, cs);

 {

     par Yield1() | Yield2();    

     while (*) 

-    invariant {:phase 1} Inv1(T, t);

-    invariant {:phase 2} Inv2(T, s, cs);

+    invariant {:layer 1} Inv1(T, t);

+    invariant {:layer 2} Inv2(T, s, cs);

     {

         call Enter(tid);

         par Yield1() | Yield2() | YieldSpec(tid);

@@ -77,11 +77,11 @@ requires {:phase 2} tid != nil && Inv2(T, s, cs);
     par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 2} Enter({:linear "tid"} tid: X)

-requires {:phase 1} Inv1(T, t);

-ensures {:phase 1} Inv1(T,t);

-requires {:phase 2} tid != nil && Inv2(T, s, cs);

-ensures {:phase 2} Inv2(T, s, cs) && cs == tid;

+procedure {:yields} {:layer 2} Enter({:linear "tid"} tid: X)

+requires {:layer 1} Inv1(T, t);

+ensures {:layer 1} Inv1(T,t);

+requires {:layer 2} tid != nil && Inv2(T, s, cs);

+ensures {:layer 2} Inv2(T, s, cs) && cs == tid;

 {

     var m: int;

 

@@ -92,9 +92,9 @@ ensures {:phase 2} Inv2(T, s, cs) && cs == tid;
     par Yield1() | Yield2() | YieldSpec(tid);

 }

 

-procedure {:yields} {:phase 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int)

-requires {:phase 1} Inv1(T, t);

-ensures {:phase 1} Inv1(T, t);

+procedure {:yields} {:layer 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int)

+requires {:layer 1} Inv1(T, t);

+ensures {:layer 1} Inv1(T, t);

 ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|;

 {

     par Yield1();

@@ -102,39 +102,39 @@ ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|;
     par Yield1();

 }

 

-procedure {:yields} {:phase 2} YieldSpec({:linear "tid"} tid: X)

-requires {:phase 2} tid != nil && cs == tid;

-ensures {:phase 2} cs == tid;

+procedure {:yields} {:layer 2} YieldSpec({:linear "tid"} tid: X)

+requires {:layer 2} tid != nil && cs == tid;

+ensures {:layer 2} cs == tid;

 {

     yield;

-    assert {:phase 2} tid != nil && cs == tid;

+    assert {:layer 2} tid != nil && cs == tid;

 }

 

-procedure {:yields} {:phase 2} Yield2()

-requires {:phase 2} Inv2(T, s, cs);

-ensures {:phase 2} Inv2(T, s, cs);

+procedure {:yields} {:layer 2} Yield2()

+requires {:layer 2} Inv2(T, s, cs);

+ensures {:layer 2} Inv2(T, s, cs);

 {

     yield;

-    assert {:phase 2} Inv2(T, s, cs);

+    assert {:layer 2} Inv2(T, s, cs);

 }

 

-procedure {:yields} {:phase 1} Yield1()

-requires {:phase 1} Inv1(T, t);

-ensures {:phase 1} Inv1(T,t);

+procedure {:yields} {:layer 1} Yield1()

+requires {:layer 1} Inv1(T, t);

+ensures {:layer 1} Inv1(T,t);

 {

     yield;

-    assert {:phase 1} Inv1(T,t);

+    assert {:layer 1} Inv1(T,t);

 }

 

-procedure {:yields} {:phase 0,2} Init({:linear "tid"} xls:[X]bool);

+procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool);

 ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

 

-procedure {:yields} {:phase 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);

+procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);

 ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|;

 

-procedure {:yields} {:phase 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int);

+procedure {:yields} {:layer 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int);

 ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|;

 

-procedure {:yields} {:phase 0,2} Leave({:linear "tid"} tid: X);

+procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X);

 ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|;

 

diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl
index 72dc4181..47dcc515 100644
--- a/Test/og/treiber-stack.bpl
+++ b/Test/og/treiber-stack.bpl
@@ -16,24 +16,24 @@ axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true]
 function Remove(x: lmap, i: Node): (lmap);

 axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));

 

-procedure {:yields} {:phase 0} ReadTopOfStack() returns (v:Node);

+procedure {:yields} {:layer 0} ReadTopOfStack() returns (v:Node);

 ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|;

 

-procedure {:yields} {:phase 0} Load(i:Node) returns (v:Node);

+procedure {:yields} {:layer 0} Load(i:Node) returns (v:Node);

 ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C;

 	            B: assume dom(Stack)[i]; v := map(Stack)[i]; return true; 

 		    C: assume !dom(Stack)[i]; return true; }|;

 

-procedure {:yields} {:phase 0} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);

+procedure {:yields} {:layer 0} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);

 ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|;

 

-procedure {:yields} {:phase 0} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);

+procedure {:yields} {:layer 0} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);

 ensures {:atomic} |{ A: assert dom(l_in)[newVal];

 		        goto B,C;

                         B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true;

 			C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|;

 

-procedure {:yields} {:phase 0} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);

+procedure {:yields} {:layer 0} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);

 ensures {:atomic} |{ A: goto B,C;

                         B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true;

 		        C: assume oldVal != TopOfStack; r := false; return true; }|;

@@ -50,10 +50,10 @@ function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool)
 

 var {:linear "Node"} Used: lmap;

 

-procedure {:yields} {:phase 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)

-requires {:phase 1} dom(x_lmap)[x];

-requires {:phase 1} Inv(TopOfStack, Stack);

-ensures {:phase 1} Inv(TopOfStack, Stack);

+procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)

+requires {:layer 1} dom(x_lmap)[x];

+requires {:layer 1} Inv(TopOfStack, Stack);

+ensures {:layer 1} Inv(TopOfStack, Stack);

 ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; return true; }|;

 {

   var t: Node;

@@ -61,30 +61,30 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret
   var {:linear "Node"} t_lmap: lmap;

 

   yield;

-  assert {:phase 1} Inv(TopOfStack, Stack);

+  assert {:layer 1} Inv(TopOfStack, Stack);

   t_lmap := x_lmap;

   while (true)

-  invariant {:phase 1} dom(t_lmap) == dom(x_lmap);

-  invariant {:phase 1} Inv(TopOfStack, Stack);

+  invariant {:layer 1} dom(t_lmap) == dom(x_lmap);

+  invariant {:layer 1} Inv(TopOfStack, Stack);

   {

     call t := ReadTopOfStack();

     call t_lmap := Store(t_lmap, x, t);

     call g, t_lmap := TransferToStack(t, x, t_lmap); 

     if (g) {

-      assert {:phase 1} map(Stack)[x] == t;

+      assert {:layer 1} map(Stack)[x] == t;

       break;

     }

     yield; 

-    assert {:phase 1} dom(t_lmap) == dom(x_lmap);

-    assert {:phase 1} Inv(TopOfStack, Stack);

+    assert {:layer 1} dom(t_lmap) == dom(x_lmap);

+    assert {:layer 1} Inv(TopOfStack, Stack);

   }

   yield; 

-  assert {:expand} {:phase 1} Inv(TopOfStack, Stack);

+  assert {:expand} {:layer 1} Inv(TopOfStack, Stack);

 }

 

-procedure {:yields} {:phase 1} pop()

-requires {:phase 1} Inv(TopOfStack, Stack);

-ensures {:phase 1} Inv(TopOfStack, Stack);

+procedure {:yields} {:layer 1} pop()

+requires {:layer 1} Inv(TopOfStack, Stack);

+ensures {:layer 1} Inv(TopOfStack, Stack);

 ensures {:atomic} |{ var t: Node; 

                      A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;

 {

@@ -93,9 +93,9 @@ ensures {:atomic} |{ var t: Node;
   var t: Node;

 

   yield;

-  assert {:phase 1} Inv(TopOfStack, Stack);

+  assert {:layer 1} Inv(TopOfStack, Stack);

   while (true)

-  invariant {:phase 1} Inv(TopOfStack, Stack);

+  invariant {:layer 1} Inv(TopOfStack, Stack);

   {

     call t := ReadTopOfStack();

     if (t != null) {

@@ -106,10 +106,10 @@ ensures {:atomic} |{ var t: Node;
       }

     }

     yield;

-    assert {:phase 1} Inv(TopOfStack, Stack);

+    assert {:layer 1} Inv(TopOfStack, Stack);

   }

   yield;

-  assert {:phase 1} Inv(TopOfStack, Stack);

+  assert {:layer 1} Inv(TopOfStack, Stack);

 }

 

 function Equal([int]bool, [int]bool) returns (bool);