Merge branch 'dfsg_free'

137 files changed, 3101 insertions, 607 deletions

diff --git a/.travis.yml b/.travis.yml
index c5d0c21d..41ee569f 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -6,16 +6,18 @@ env:
   - BOOGIE_CONFIG=Debug
   - BOOGIE_CONFIG=Release
 install:
-  - sudo apt-key adv --recv-keys --keyserver keyserver.ubuntu.com C504E590
-  # FIXME: We should not be using GPUVerify's repo for Z3
-  - sudo sh -c 'echo "deb http://ppa.launchpad.net/delcypher/gpuverify-smt/ubuntu precise main" > /etc/apt/sources.list.d/smt.list'
+  - wget http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_12.04/Release.key
+  - sudo apt-key add - < Release.key
+  # Use Z3 package built by the OpenSUSE build service https://build.opensuse.org/package/show/home:delcypher:z3/z3
+  - sudo sh -c "echo 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_12.04/ /' >> /etc/apt/sources.list.d/z3.list"
   - sudo apt-get update
-  - nuget restore ${TRAVIS_SOLUTION}
-  # Install Z3
-  - sudo apt-get -y install z3=4.3.2-0~precise2
+  # NuGet is a little flakey in legacy TravisCI, use travis_retry command to retry the command if it fails
+  - travis_retry nuget restore ${TRAVIS_SOLUTION}
+  # Install Z3 executable
+  - sudo apt-get -y install 'z3=4.4.1-*'
   # Install needed python tools
   - sudo pip install lit OutputCheck pyyaml
-  - mkdir -p Source/packages && cd Source/packages && nuget install NUnit.Runners -Version 2.6.3
+  - mkdir -p Source/packages && cd Source/packages && travis_retry nuget install NUnit.Runners -Version 2.6.3
   - cd ../../
 script:
   - xbuild /p:Configuration=${BOOGIE_CONFIG} ${TRAVIS_SOLUTION}
diff --git a/Build/CodePlex.Tools.MsBuild.dll b/Build/CodePlex.Tools.MsBuild.dll
deleted file mode 100644
index 2e400e8e..00000000
--- a/Build/CodePlex.Tools.MsBuild.dll
+++ /dev/null
diff --git a/Build/CodePlex.Tools.Wiki.dll b/Build/CodePlex.Tools.Wiki.dll
deleted file mode 100644
index 9ea2bea8..00000000
--- a/Build/CodePlex.Tools.Wiki.dll
+++ /dev/null
diff --git a/Build/updateVersionFile.xml b/Build/updateVersionFile.xml
deleted file mode 100644
index cb083c7a..00000000
--- a/Build/updateVersionFile.xml
+++ /dev/null
@@ -1,19 +0,0 @@
-<Project xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
-  <UsingTask AssemblyFile="CodePlex.Tools.MsBuild.dll" TaskName="CreateAssemblyInfo" />
-    
-  <Target Name="CreateAssemblyInfo">
-    <CreateAssemblyInfo
-      Version="$(CCNetLabel)"
-      CreateVersionFile="true"
-      ForceReadOnly="true"
-      VersionFileName="..\Source\version.ssc"
-    />
-    <CreateAssemblyInfo
-      Version="$(CCNetLabel)"
-      CreateVersionFile="true"
-      ForceReadOnly="true"
-      VersionFileName="..\Source\version.cs"
-    />
-  </Target>
-</Project>
-
diff --git a/README.md b/README.md
index a976b249..1dd0ba5a 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@
 |-------------------------------|---------------------------------|
 | [![linux build status][1]][2] | [![windows_build_status][3]][4] |
 
-[1]: https://travis-ci.org/boogie-org/boogie.svg
+[1]: https://travis-ci.org/boogie-org/boogie.svg?branch=master
 [2]: https://travis-ci.org/boogie-org/boogie
 [3]: https://pmbuilds.inf.ethz.ch/buildStatus/icon?job=boogie
 [4]: #FIXME
@@ -48,7 +48,7 @@ You can also report issues on our [issue tracker](https://github.com/boogie-org/
 ### Requirements
 
 - [NuGet](https://www.nuget.org/)
-- [Z3](https://github.com/Z3Prover/z3) 4.3.2 or [CVC4](http://cvc4.cs.nyu.edu/web/) **FIXME_VERSION** (note
+- [Z3](https://github.com/Z3Prover/z3) 4.4.1 or [CVC4](http://cvc4.cs.nyu.edu/web/) **FIXME_VERSION** (note
   CVC4 support is experimental)
 
 #### Windows specific
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 0d2676f2..2fd37463 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -698,9 +698,13 @@ namespace Microsoft.Boogie.AbstractInterpretation
             lo = Lo; hi = Hi;
             if (hi != null) {
               Lo = node.Type.IsReal ? -hi : 1 - hi;
+            } else {
+              Lo = null;
             }
             if (lo != null) {
               Hi = node.Type.IsReal ? -lo : 1 - lo;
+            } else {
+              Hi = null;
             }
           }
           else if (op.Op == UnaryOperator.Opcode.Not) {
@@ -880,6 +884,10 @@ namespace Microsoft.Boogie.AbstractInterpretation
               if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
                 Lo = BigInteger.Zero;
                 Hi = hi1;
+                if (lo0 < lo1 && hi0 != null && hi0 < lo1) {
+                  Lo = lo0;
+                  Hi = hi0;
+                }
               }
               break;
             case BinaryOperator.Opcode.RealDiv:
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/CivlRefinement.cs
index 2ad08024..75ff2358 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/CivlRefinement.cs
@@ -13,7 +13,7 @@ namespace Microsoft.Boogie
 {
     public class MyDuplicator : Duplicator
     {
-        MoverTypeChecker moverTypeChecker;
+        CivlTypeChecker civlTypeChecker;
         public int layerNum;
         Procedure enclosingProc;
         Implementation enclosingImpl;
@@ -23,9 +23,9 @@ namespace Microsoft.Boogie
         public HashSet<Procedure> yieldingProcs;
         public List<Implementation> impls;
 
-        public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum)
+        public MyDuplicator(CivlTypeChecker civlTypeChecker, int layerNum)
         {
-            this.moverTypeChecker = moverTypeChecker;
+            this.civlTypeChecker = civlTypeChecker;
             this.layerNum = layerNum;
             this.enclosingProc = null;
             this.enclosingImpl = null;
@@ -38,11 +38,19 @@ namespace Microsoft.Boogie
 
         private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds)
         {
-            int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;
+            int enclosingProcLayerNum = civlTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;
             Procedure originalProc = originalCallCmd.Proc;
-            if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))
+            
+            if (civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(originalProc))
+            {
+                if (civlTypeChecker.CallExists(originalCallCmd, enclosingProcLayerNum, layerNum))
+                {
+                    newCmds.Add(callCmd);
+                }
+            }
+            else if (civlTypeChecker.procToActionInfo.ContainsKey(originalProc))
             {
-                AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo;
+                AtomicActionInfo atomicActionInfo = civlTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo;
                 if (atomicActionInfo != null && atomicActionInfo.gate.Count > 0 && layerNum == enclosingProcLayerNum)
                 {
                     newCmds.Add(new HavocCmd(Token.NoToken, new List<IdentifierExpr>(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) })));
@@ -57,8 +65,12 @@ namespace Microsoft.Boogie
                         newCmds.Add(Substituter.Apply(subst, assertCmd));
                     }
                 }
+                newCmds.Add(callCmd);
+            }
+            else
+            {
+                Debug.Assert(false);
             }
-            newCmds.Add(callCmd);
         }
 
         private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List<Cmd> newCmds)
@@ -66,7 +78,7 @@ namespace Microsoft.Boogie
             int maxCalleeLayerNum = 0;
             foreach (CallCmd iter in originalParCallCmd.CallCmds)
             {
-                int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum;
+                int calleeLayerNum = civlTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum;
                 if (calleeLayerNum > maxCalleeLayerNum)
                     maxCalleeLayerNum = calleeLayerNum;
             }
@@ -144,7 +156,7 @@ namespace Microsoft.Boogie
 
         public override Procedure VisitProcedure(Procedure node)
         {
-            if (!moverTypeChecker.procToActionInfo.ContainsKey(node))
+            if (!civlTypeChecker.procToActionInfo.ContainsKey(node))
                 return node;
             if (!procMap.ContainsKey(node))
             {
@@ -155,7 +167,7 @@ namespace Microsoft.Boogie
                 proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies);
                 proc.OutParams = this.VisitVariableSeq(node.OutParams);
 
-                ActionInfo actionInfo = moverTypeChecker.procToActionInfo[node];
+                ActionInfo actionInfo = civlTypeChecker.procToActionInfo[node];
                 if (actionInfo.createdAtLayerNum < layerNum)
                 {
                     proc.Requires = new List<Requires>();
@@ -198,7 +210,7 @@ namespace Microsoft.Boogie
                 }
                 procMap[node] = proc;
                 proc.Modifies = new List<IdentifierExpr>();
-                moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));
+                civlTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));
             }
             return procMap[node];
         }
@@ -220,7 +232,7 @@ namespace Microsoft.Boogie
             Requires requires = base.VisitRequires(node);
             if (node.Free)
                 return requires;
-            if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
+            if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum))
                 requires.Condition = Expr.True;
             return requires;
         }
@@ -230,12 +242,12 @@ namespace Microsoft.Boogie
             Ensures ensures = base.VisitEnsures(node);
             if (node.Free)
                 return ensures;
-            AtomicActionInfo atomicActionInfo =  moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo;
+            AtomicActionInfo atomicActionInfo =  civlTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo;
             bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node;
-            if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
+            if (isAtomicSpecification || !civlTypeChecker.absyToLayerNums[node].Contains(layerNum))
             {
                 ensures.Condition = Expr.True;
-                ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes);
+                ensures.Attributes = CivlRefinement.RemoveMoverAttribute(ensures.Attributes);
             }
             return ensures;
         }
@@ -243,16 +255,16 @@ namespace Microsoft.Boogie
         public override Cmd VisitAssertCmd(AssertCmd node)
         {
             AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node);
-            if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
+            if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum))
                 assertCmd.Expr = Expr.True;
             return assertCmd;
         }
     }
 
-    public class OwickiGries
+    public class CivlRefinement
     {
         LinearTypeChecker linearTypeChecker;
-        MoverTypeChecker moverTypeChecker;
+        CivlTypeChecker civlTypeChecker;
         Dictionary<Absy, Absy> absyMap;
         Dictionary<Implementation, Implementation> implMap;
         HashSet<Procedure> yieldingProcs;
@@ -269,17 +281,17 @@ namespace Microsoft.Boogie
         Expr beta;
         HashSet<Variable> frame;
 
-        public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator)
+        public CivlRefinement(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, MyDuplicator duplicator)
         {
             this.linearTypeChecker = linearTypeChecker;
-            this.moverTypeChecker = moverTypeChecker;
+            this.civlTypeChecker = civlTypeChecker;
             this.absyMap = duplicator.absyMap;
             this.layerNum = duplicator.layerNum;
             this.implMap = duplicator.implMap;
             this.yieldingProcs = duplicator.yieldingProcs;
             Program program = linearTypeChecker.program;
             globalMods = new List<IdentifierExpr>();
-            foreach (Variable g in moverTypeChecker.SharedVariables)
+            foreach (Variable g in civlTypeChecker.SharedVariables)
             {
                 globalMods.Add(Expr.Ident(g));
             }
@@ -291,7 +303,24 @@ namespace Microsoft.Boogie
 
         private IEnumerable<Variable> AvailableLinearVars(Absy absy)
         {
-            return linearTypeChecker.AvailableLinearVars(absyMap[absy]);
+            HashSet<Variable> availableVars = new HashSet<Variable>(linearTypeChecker.AvailableLinearVars(absyMap[absy]));
+            foreach (var g in civlTypeChecker.globalVarToSharedVarInfo.Keys)
+            {
+                SharedVariableInfo info = civlTypeChecker.globalVarToSharedVarInfo[g];
+                if (!(info.introLayerNum <= layerNum && layerNum <= info.hideLayerNum))
+                {
+                    availableVars.Remove(g);
+                }
+            }
+            foreach (var v in civlTypeChecker.localVarToLocalVariableInfo.Keys)
+            {
+                LocalVariableInfo info = civlTypeChecker.localVarToLocalVariableInfo[v];
+                if (layerNum < info.layer)
+                {
+                    availableVars.Remove(v);
+                }
+            }
+            return availableVars;
         }
 
         private CallCmd CallToYieldProc(IToken tok, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
@@ -715,7 +744,7 @@ namespace Microsoft.Boogie
             }
 
             Procedure originalProc = implMap[impl].Proc;
-            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];
+            ActionInfo actionInfo = civlTypeChecker.procToActionInfo[originalProc];
             if (actionInfo.createdAtLayerNum == this.layerNum)
             {
                 pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool));
@@ -738,19 +767,14 @@ namespace Microsoft.Boogie
                     foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);
                 }
                 Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);
-                frame = new HashSet<Variable>(moverTypeChecker.SharedVariables);
-                HashSet<Variable> introducedVars = new HashSet<Variable>();
-                foreach (Variable v in moverTypeChecker.SharedVariables)
+                frame = new HashSet<Variable>(civlTypeChecker.SharedVariables);
+                foreach (Variable v in civlTypeChecker.SharedVariables)
                 {
-                    if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || 
-                        moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)
+                    if (civlTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || 
+                        civlTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)
                     {
                         frame.Remove(v);
                     }
-                    if (moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum == actionInfo.createdAtLayerNum)
-                    {
-                        introducedVars.Add(v);
-                    }
                 }
                 AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
                 if (atomicActionInfo == null)
@@ -764,7 +788,7 @@ namespace Microsoft.Boogie
                 }
                 else
                 {
-                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, introducedVars)).TransitionRelationCompute(true);
+                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(civlTypeChecker.program, atomicActionInfo, frame, new HashSet<Variable>())).TransitionRelationCompute(true);
                     beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);
                     Expr alphaExpr = Expr.True;
                     foreach (AssertCmd assertCmd in atomicActionInfo.gate)
@@ -1175,31 +1199,31 @@ namespace Microsoft.Boogie
             return decls;
         }
 
-        public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
+        public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls)
         {
             Program program = linearTypeChecker.program;
-            foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))
+            foreach (int layerNum in civlTypeChecker.AllLayerNums)
             {
                 if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;
 
-                MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, layerNum);
+                MyDuplicator duplicator = new MyDuplicator(civlTypeChecker, layerNum);
                 foreach (var proc in program.Procedures)
                 {
-                    if (!moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue;
+                    if (!civlTypeChecker.procToActionInfo.ContainsKey(proc)) continue;
                     Procedure duplicateProc = duplicator.VisitProcedure(proc);
                     decls.Add(duplicateProc);
                 }
                 decls.AddRange(duplicator.impls);
-                OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator);
+                CivlRefinement civlTransform = new CivlRefinement(linearTypeChecker, civlTypeChecker, duplicator);
                 foreach (var impl in program.Implementations)
                 {
-                    if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum)
+                    if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum)
                         continue;
                     Implementation duplicateImpl = duplicator.VisitImplementation(impl);
-                    ogTransform.TransformImpl(duplicateImpl);
+                    civlTransform.TransformImpl(duplicateImpl);
                     decls.Add(duplicateImpl);
                 }
-                decls.AddRange(ogTransform.Collect());
+                decls.AddRange(civlTransform.Collect());
             }
         }
     }
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/CivlTypeChecker.cs
index c821117a..b426d9ed 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -280,22 +280,111 @@ namespace Microsoft.Boogie
         }
     }
 
-    public class MoverTypeChecker : ReadOnlyVisitor
+    public class LayerRange
+    {
+        public int lowerLayerNum;
+        public int upperLayerNum;
+        public LayerRange(int layer)
+        {
+            this.lowerLayerNum = layer;
+            this.upperLayerNum = layer;
+        }
+        public LayerRange(int lower, int upper)
+        {
+            this.lowerLayerNum = lower;
+            this.upperLayerNum = upper;
+        }
+        public LayerRange(IEnumerable<int> layerNums)
+        {
+            int min = int.MaxValue;
+            int max = int.MinValue;
+            foreach (var layerNum in layerNums)
+            {
+                if (layerNum < min)
+                {
+                    min = layerNum;
+                }
+                if (max < layerNum)
+                {
+                    max = layerNum;
+                }
+            }
+            this.lowerLayerNum = min;
+            this.upperLayerNum = max;
+        }
+        public bool Contains(int layerNum)
+        {
+            return lowerLayerNum <= layerNum && layerNum <= upperLayerNum;
+        }
+        public bool Subset(int lower, int upper)
+        {
+            return lower <= lowerLayerNum && upperLayerNum <= upper;
+        }
+        public bool Equal(int lower, int upper)
+        {
+            return lower == lowerLayerNum && upperLayerNum == upper;
+        }
+        public bool Subset(LayerRange info)
+        {
+            return info.lowerLayerNum <= lowerLayerNum && upperLayerNum <= info.upperLayerNum;
+        }
+    }
+
+    public class AtomicProcedureInfo
+    {
+        public bool isPure;
+        public LayerRange layerRange;
+        public AtomicProcedureInfo()
+        {
+            this.isPure = true;
+            this.layerRange = null;
+        }
+        public AtomicProcedureInfo(LayerRange layerRange)
+        {
+            this.isPure = false;
+            this.layerRange = layerRange;
+        }
+    }
+
+    public class LocalVariableInfo
+    {
+        public int layer;
+        public LocalVariableInfo(int layer)
+        {
+            this.layer = layer;
+        }
+    }
+
+    public class CivlTypeChecker : ReadOnlyVisitor
     {
         CheckingContext checkingContext;
-        public int errorCount;
-        public Dictionary<Variable, SharedVariableInfo> globalVarToSharedVarInfo;
         Procedure enclosingProc;
         Implementation enclosingImpl;
-        public Dictionary<Procedure, ActionInfo> procToActionInfo;
+        HashSet<Variable> sharedVarsAccessed;
+        int introducedLocalVarsUpperBound;
+
         public Program program;
-        bool canAccessSharedVars;
-        bool canAccessGhostVars;
-        int minLayerNum;
-        int maxLayerNum;
+        public int errorCount;
+        public Dictionary<Variable, SharedVariableInfo> globalVarToSharedVarInfo;
+        public Dictionary<Procedure, ActionInfo> procToActionInfo;
+        public Dictionary<Procedure, AtomicProcedureInfo> procToAtomicProcedureInfo;
         public Dictionary<Absy, HashSet<int>> absyToLayerNums;
-        HashSet<Variable> ghostVars;
-        public int leastUnimplementedLayerNum;
+        public Dictionary<Variable, LocalVariableInfo> localVarToLocalVariableInfo;
+        Dictionary<CallCmd, int> pureCallLayer;
+
+        public bool CallExists(CallCmd callCmd, int enclosingProcLayerNum, int layerNum)
+        {
+            Debug.Assert(procToAtomicProcedureInfo.ContainsKey(callCmd.Proc));
+            var atomicProcedureInfo = procToAtomicProcedureInfo[callCmd.Proc];
+            if (atomicProcedureInfo.isPure)
+            {
+                return pureCallLayer[callCmd] <= layerNum;
+            }
+            else
+            {
+                return enclosingProcLayerNum == layerNum;
+            }
+        }
 
         private static List<int> FindLayers(QKeyValue kv)
         {
@@ -316,6 +405,19 @@ namespace Microsoft.Boogie
             return layers;
         }
 
+        private static int Least(IEnumerable<int> layerNums)
+        {
+            int least = int.MaxValue;
+            foreach (var layer in layerNums)
+            {
+                if (layer < least)
+                {
+                    least = layer;
+                }
+            }
+            return least;
+        }
+
         private static MoverType GetMoverType(Ensures e)
         {
             if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
@@ -329,28 +431,29 @@ namespace Microsoft.Boogie
             return MoverType.Top;
         }
 
-        public MoverTypeChecker(Program program)
+        public CivlTypeChecker(Program program)
         {
-            this.ghostVars = new HashSet<Variable>();
-            this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();
-            this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();
-            this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
             this.errorCount = 0;
             this.checkingContext = new CheckingContext(null);
             this.program = program;
             this.enclosingProc = null;
             this.enclosingImpl = null;
-            this.canAccessSharedVars = false;
-            this.canAccessGhostVars = false;
-            this.minLayerNum = int.MaxValue;
-            this.maxLayerNum = -1;
-            this.leastUnimplementedLayerNum = int.MaxValue;
+            this.sharedVarsAccessed = null;
+            this.introducedLocalVarsUpperBound = int.MinValue;
+
+            this.localVarToLocalVariableInfo = new Dictionary<Variable, LocalVariableInfo>();
+            this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();
+            this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();
+            this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
+            this.procToAtomicProcedureInfo = new Dictionary<Procedure, AtomicProcedureInfo>();
+            this.pureCallLayer = new Dictionary<CallCmd, int>();
+            
             foreach (var g in program.GlobalVariables)
             {
                 List<int> layerNums = FindLayers(g.Attributes);
                 if (layerNums.Count == 0)
                 {
-                    // Cannot access atomic actions
+                    // Inaccessible from  yielding and atomic procedures
                 }
                 else if (layerNums.Count == 1)
                 {
@@ -366,28 +469,137 @@ namespace Microsoft.Boogie
                 }
             }
         }
-        
-        private HashSet<int> allCreatedLayerNums;
-        public IEnumerable<int> AllCreatedLayerNums
+
+        private HashSet<int> allLayerNums;
+        public IEnumerable<int> AllLayerNums
         {
             get
             {
-                if (allCreatedLayerNums == null)
+                if (allLayerNums == null)
                 {
-                    allCreatedLayerNums = new HashSet<int>();
+                    allLayerNums = new HashSet<int>();
                     foreach (ActionInfo actionInfo in procToActionInfo.Values)
                     {
-                        allCreatedLayerNums.Add(actionInfo.createdAtLayerNum);
+                        allLayerNums.Add(actionInfo.createdAtLayerNum);
+                    }
+                    foreach (var layerNums in absyToLayerNums.Values)
+                    {
+                        foreach (var layer in layerNums)
+                        {
+                            allLayerNums.Add(layer);
+                        }
                     }
                 }
-                return allCreatedLayerNums;
+                return allLayerNums;
+            }
+        }
+
+        private LayerRange FindLayerRange()
+        {
+            int maxIntroLayerNum = int.MinValue;
+            int minHideLayerNum = int.MaxValue;
+            foreach (var g in sharedVarsAccessed)
+            {
+                if (globalVarToSharedVarInfo[g].introLayerNum > maxIntroLayerNum)
+                {
+                    maxIntroLayerNum = globalVarToSharedVarInfo[g].introLayerNum;
+                }
+                if (globalVarToSharedVarInfo[g].hideLayerNum < minHideLayerNum)
+                {
+                    minHideLayerNum = globalVarToSharedVarInfo[g].hideLayerNum;
+                }
             }
+            return new LayerRange(maxIntroLayerNum, minHideLayerNum);
         }
 
         public void TypeCheck()
         {
             foreach (var proc in program.Procedures)
             {
+                if (!QKeyValue.FindBoolAttribute(proc.Attributes, "pure")) continue;
+                if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
+                {
+                    Error(proc, "Pure procedure must not yield");
+                    continue;
+                }
+                if (QKeyValue.FindBoolAttribute(proc.Attributes, "layer"))
+                {
+                    Error(proc, "Pure procedure must not have layers");
+                    continue;
+                }
+                if (proc.Modifies.Count > 0)
+                {
+                    Error(proc, "Pure procedure must not modify a global variable");
+                    continue;
+                }
+                procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo();
+            }
+            foreach (var proc in program.Procedures)
+            {
+                if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
+                var procLayerNums = FindLayers(proc.Attributes);
+                if (procLayerNums.Count == 0) continue;
+                foreach (IdentifierExpr ie in proc.Modifies)
+                {
+                    if (!globalVarToSharedVarInfo.ContainsKey(ie.Decl))
+                    {
+                        Error(proc, "Atomic procedure cannot modify a global variable without layer numbers");
+                        continue;
+                    }
+                }
+                int lower, upper;
+                if (procLayerNums.Count == 1)
+                {
+                    lower = procLayerNums[0];
+                    upper = procLayerNums[0];
+                }
+                else if (procLayerNums.Count == 2)
+                {
+                    lower = procLayerNums[0];
+                    upper = procLayerNums[1];
+                    if (lower >= upper)
+                    {
+                        Error(proc, "Lower layer must be less than upper layer");
+                        continue;
+                    }
+                }
+                else
+                {
+                    Error(proc, "Atomic procedure must specify a layer range");
+                    continue;
+                }
+                LayerRange layerRange = new LayerRange(lower, upper);
+                procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(layerRange);
+            }
+            if (errorCount > 0) return;
+
+            foreach (Implementation impl in program.Implementations)
+            {
+                if (!procToAtomicProcedureInfo.ContainsKey(impl.Proc)) continue;
+                var atomicProcedureInfo = procToAtomicProcedureInfo[impl.Proc];
+                if (atomicProcedureInfo.isPure)
+                {
+                    this.enclosingImpl = impl;
+                    (new PurityChecker(this)).VisitImplementation(impl);
+                }
+                else 
+                {
+                    this.enclosingImpl = impl;
+                    this.sharedVarsAccessed = new HashSet<Variable>();
+                    (new PurityChecker(this)).VisitImplementation(impl);
+                    LayerRange upperBound = FindLayerRange();
+                    LayerRange lowerBound = atomicProcedureInfo.layerRange;
+                    if (!lowerBound.Subset(upperBound))
+                    {
+                        Error(impl, "Atomic procedure cannot access global variable");
+                    }
+                    this.sharedVarsAccessed = null;
+                }
+            }
+            if (errorCount > 0) return; 
+            
+            foreach (var proc in program.Procedures)
+            {
                 if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
 
                 int createdAtLayerNum;  // must be initialized by the following code, otherwise it is an error
@@ -428,25 +640,21 @@ namespace Microsoft.Boogie
                         continue;
                     }
 
-                    minLayerNum = int.MaxValue;
-                    maxLayerNum = -1;
-                    canAccessSharedVars = true;
+                    sharedVarsAccessed = new HashSet<Variable>();
                     enclosingProc = proc;
                     enclosingImpl = null;
                     base.VisitEnsures(e);
-                    canAccessSharedVars = false;
-                    if (maxLayerNum > createdAtLayerNum)
-                    {
-                        Error(e, "A variable being accessed is introduced after this action is created");
-                    }
-                    else if (availableUptoLayerNum > minLayerNum)
+                    LayerRange upperBound = FindLayerRange();
+                    LayerRange lowerBound = new LayerRange(createdAtLayerNum, availableUptoLayerNum);
+                    if (lowerBound.Subset(upperBound))
                     {
-                        Error(e, "A variable being accessed is hidden before this action becomes unavailable");
+                        procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum);
                     }
                     else
                     {
-                        procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum);
+                        Error(e, "A variable being accessed in this action is unavailable");
                     }
+                    sharedVarsAccessed = null;
                 }
                 if (errorCount > 0) continue;
                 if (!procToActionInfo.ContainsKey(proc))
@@ -463,52 +671,63 @@ namespace Microsoft.Boogie
                 }
             }
             if (errorCount > 0) return;
+            
             foreach (var impl in program.Implementations)
             {
                 if (!procToActionInfo.ContainsKey(impl.Proc)) continue;
+                ActionInfo actionInfo = procToActionInfo[impl.Proc];
                 procToActionInfo[impl.Proc].hasImplementation = true;
-            }
-            foreach (var proc in procToActionInfo.Keys)
-            {
-                ActionInfo actionInfo = procToActionInfo[proc];
-                if (actionInfo.isExtern && actionInfo.hasImplementation)
+                if (actionInfo.isExtern)
                 {
-                    Error(proc, "Extern procedure cannot have an implementation");
-                    continue;
+                    Error(impl.Proc, "Extern procedure cannot have an implementation");
                 }
-                if (actionInfo.isExtern || actionInfo.hasImplementation) continue;
-                if (leastUnimplementedLayerNum == int.MaxValue)
+            }
+            if (errorCount > 0) return;
+
+            foreach (Procedure proc in procToActionInfo.Keys)
+            {
+                for (int i = 0; i < proc.InParams.Count; i++)
                 {
-                    leastUnimplementedLayerNum = actionInfo.createdAtLayerNum;
+                    Variable v = proc.InParams[i];
+                    var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum);
+                    if (layer == int.MinValue) continue;
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
                 }
-                else if (leastUnimplementedLayerNum != actionInfo.createdAtLayerNum)
+                for (int i = 0; i < proc.OutParams.Count; i++)
                 {
-                    Error(proc, "All unimplemented atomic actions must be created at the same layer");
+                    Variable v = proc.OutParams[i];
+                    var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum);
+                    if (layer == int.MinValue) continue;
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
                 }
             }
-            foreach (var g in this.globalVarToSharedVarInfo.Keys)
+            foreach (Implementation node in program.Implementations)
             {
-                var info = globalVarToSharedVarInfo[g];
-                if (!this.AllCreatedLayerNums.Contains(info.introLayerNum))
+                if (!procToActionInfo.ContainsKey(node.Proc)) continue;
+                foreach (Variable v in node.LocVars)
                 {
-                    Error(g, "Variable must be introduced with creation of some atomic action");
+                    var layer = FindLocalVariableLayer(node, v, procToActionInfo[node.Proc].createdAtLayerNum);
+                    if (layer == int.MinValue) continue;
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
                 }
-                if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum))
+                for (int i = 0; i < node.Proc.InParams.Count; i++)
                 {
-                    Error(g, "Variable must be hidden with creation of some atomic action");
+                    Variable v = node.Proc.InParams[i];
+                    if (!localVarToLocalVariableInfo.ContainsKey(v)) continue;
+                    var layer = localVarToLocalVariableInfo[v].layer;
+                    localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(layer);
                 }
-            }
-            if (errorCount > 0) return;
-            this.VisitProgram(program);
-            foreach (Procedure proc in program.Procedures)
-            {
-                if (procToActionInfo.ContainsKey(proc)) continue;
-                foreach (var ie in proc.Modifies)
+                for (int i = 0; i < node.Proc.OutParams.Count; i++)
                 {
-                    if (!SharedVariables.Contains(ie.Decl)) continue;
-                    Error(proc, "A ghost procedure must not modify a global variable with layer annotation");
+                    Variable v = node.Proc.OutParams[i];
+                    if (!localVarToLocalVariableInfo.ContainsKey(v)) continue;
+                    var layer = localVarToLocalVariableInfo[v].layer;
+                    localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(layer);
                 }
             }
+            if (errorCount > 0) return; 
+            
+            this.VisitProgram(program);
             if (errorCount > 0) return;
             YieldTypeChecker.PerformYieldSafeCheck(this);
             new LayerEraser().VisitProgram(program);
@@ -516,9 +735,26 @@ namespace Microsoft.Boogie
 
         public IEnumerable<Variable> SharedVariables
         {
-            get { return this.globalVarToSharedVarInfo.Keys;  }
+            get { return this.globalVarToSharedVarInfo.Keys; }
         }
-        
+
+        private int FindLocalVariableLayer(Declaration decl, Variable v, int enclosingProcLayerNum)
+        {
+            var layers = FindLayers(v.Attributes);
+            if (layers.Count == 0) return int.MinValue;
+            if (layers.Count > 1)
+            {
+                Error(decl, "Incorrect number of layers");
+                return int.MinValue;
+            }
+            if (layers[0] > enclosingProcLayerNum)
+            {
+                Error(decl, "Layer of local variable cannot be greater than the creation layer of enclosing procedure");
+                return int.MinValue;
+            }
+            return layers[0];
+        }
+
         public override Implementation VisitImplementation(Implementation node)
         {
             if (!procToActionInfo.ContainsKey(node.Proc))
@@ -527,17 +763,9 @@ namespace Microsoft.Boogie
             }
             this.enclosingImpl = node;
             this.enclosingProc = null;
-            ghostVars = new HashSet<Variable>();
-            foreach (Variable v in node.LocVars)
-            {
-                if (QKeyValue.FindBoolAttribute(v.Attributes, "ghost"))
-                {
-                    ghostVars.Add(v);
-                }
-            }
             return base.VisitImplementation(node);
         }
-        
+
         public override Procedure VisitProcedure(Procedure node)
         {
             if (!procToActionInfo.ContainsKey(node))
@@ -584,23 +812,117 @@ namespace Microsoft.Boogie
                 {
                     Error(node, "The callee is not available in the caller procedure");
                 }
-                return base.VisitCallCmd(node);
+                for (int i = 0; i < node.Ins.Count; i++)
+                {
+                    Visit(node.Ins[i]);
+                    if (introducedLocalVarsUpperBound != int.MinValue)
+                    {
+                        var formal = node.Proc.InParams[i];
+                        if (!localVarToLocalVariableInfo.ContainsKey(formal) ||
+                            introducedLocalVarsUpperBound > localVarToLocalVariableInfo[formal].layer)
+                        {
+                            Error(node, "An introduced local variable is accessed but not available");
+                        }
+                        introducedLocalVarsUpperBound = int.MinValue;
+                    }
+                }
+                for (int i = 0; i < node.Outs.Count; i++)
+                {
+                    var formal = node.Proc.OutParams[i];
+                    if (!localVarToLocalVariableInfo.ContainsKey(formal)) continue;
+                    var actual = node.Outs[i].Decl;
+                    if (localVarToLocalVariableInfo.ContainsKey(actual) && 
+                        localVarToLocalVariableInfo[formal].layer <= localVarToLocalVariableInfo[actual].layer)
+                        continue;
+                    Error(node, "Formal parameter of call must be introduced no later than the actual parameter");
+                }
+                return node;
             }
-            else
+            else if (procToAtomicProcedureInfo.ContainsKey(node.Proc))
             {
-                foreach (var ie in node.Outs)
+                var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc];                
+                if (atomicProcedureInfo.isPure)
                 {
-                    if (ghostVars.Contains(ie.Decl)) continue;
-                    Error(node, "The output of a ghost procedure must be assigned to a ghost variable");
+                    if (node.Outs.Count > 0)
+                    {
+                        int inferredLayer = int.MinValue;
+                        foreach (var ie in node.Outs)
+                        {
+                            if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl)) continue;
+                            if (inferredLayer < localVarToLocalVariableInfo[ie.Decl].layer)
+                            {
+                                inferredLayer = localVarToLocalVariableInfo[ie.Decl].layer;
+                            }
+                        }
+                        pureCallLayer[node] = inferredLayer;
+                        if (inferredLayer != int.MinValue)
+                        {
+                            foreach (var ie in node.Outs)
+                            {
+                                if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl))
+                                {
+                                    Error(node, "Output variable must be introduced");
+                                }
+                                else if (inferredLayer != localVarToLocalVariableInfo[ie.Decl].layer)
+                                {
+                                    Error(node, "All output variables must be introduced at the same layer");
+                                }
+                            }
+                        }
+                        Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+                        foreach (var e in node.Ins)
+                        {
+                            Visit(e);
+                            if (inferredLayer < introducedLocalVarsUpperBound)
+                            {
+                                Error(node, "An introduced local variable is not accessible");
+                            }
+                            introducedLocalVarsUpperBound = int.MinValue;
+                        }
+                    }
+                    else
+                    {
+                        Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+                        int inferredLayer = int.MinValue;
+                        foreach (var e in node.Ins)
+                        {
+                            Visit(e);
+                            if (inferredLayer < introducedLocalVarsUpperBound)
+                            {
+                                inferredLayer = introducedLocalVarsUpperBound;
+                            }
+                            introducedLocalVarsUpperBound = int.MinValue;
+                        }
+                        pureCallLayer[node] = inferredLayer;
+                    }
                 }
-                bool savedCanAccessSharedVars = canAccessSharedVars;
-                bool savedCanAccessAuxVars = canAccessGhostVars;
-                canAccessSharedVars = true;
-                canAccessGhostVars = true;
-                var retVal = base.VisitCallCmd(node);
-                canAccessSharedVars = savedCanAccessSharedVars;
-                canAccessGhostVars = savedCanAccessAuxVars;
-                return retVal;
+                else
+                {
+                    if (enclosingProcLayerNum != atomicProcedureInfo.layerRange.upperLayerNum)
+                    {
+                        Error(node, "Creation layer of caller must be the upper bound of the layer range of callee");
+                    }
+                    foreach (var ie in node.Proc.Modifies)
+                    {
+                        if (enclosingProcLayerNum != globalVarToSharedVarInfo[ie.Decl].introLayerNum)
+                        {
+                            Error(node, "Creation layer of caller must be identical to the introduction layer of modified variable");
+                        }
+                    }
+                    foreach (var ie in node.Outs)
+                    {
+                        if (localVarToLocalVariableInfo.ContainsKey(ie.Decl) &&
+                            enclosingProcLayerNum == localVarToLocalVariableInfo[ie.Decl].layer)
+                            continue;
+                        Error(node, "Output variable must be introduced at the creation layer of caller");
+                    }
+                }
+                return node;
+            }
+            else  
+            {
+                Error(node, "A yielding procedure can call only atomic or yielding procedures");
+                return node;
             }
         }
 
@@ -618,8 +940,8 @@ namespace Microsoft.Boogie
                 isLeftMover = isLeftMover && actionInfo.IsLeftMover;
                 isRightMover = isRightMover && actionInfo.IsRightMover;
                 if (actionInfo.createdAtLayerNum > maxCalleeLayerNum)
-                { 
-                    maxCalleeLayerNum = actionInfo.createdAtLayerNum; 
+                {
+                    maxCalleeLayerNum = actionInfo.createdAtLayerNum;
                 }
                 if (actionInfo is AtomicActionInfo)
                 {
@@ -645,66 +967,36 @@ namespace Microsoft.Boogie
             return base.VisitParCallCmd(node);
         }
 
-        public override Cmd VisitAssignCmd(AssignCmd node)
-        {
-            Contract.Ensures(Contract.Result<Cmd>() == node);
-            for (int i = 0; i < node.Lhss.Count; ++i)
-            {
-                bool savedCanAccessSharedVars = canAccessSharedVars;
-                bool savedCanAccessAuxVars = canAccessGhostVars;
-                Variable v = node.Lhss[i].DeepAssignedVariable;
-                if (v is LocalVariable && ghostVars.Contains(v))
-                {
-                    canAccessSharedVars = true;
-                    canAccessGhostVars = true;
-                }
-                this.Visit(node.Lhss[i]);
-                this.Visit(node.Rhss[i]);
-                canAccessSharedVars = savedCanAccessSharedVars;
-                canAccessGhostVars = savedCanAccessAuxVars;
-            }
-            return node;
-        }
-
         public override Expr VisitIdentifierExpr(IdentifierExpr node)
         {
             if (node.Decl is GlobalVariable)
             {
-                if (!canAccessSharedVars)
+                if (sharedVarsAccessed == null)
                 {
                     Error(node, "Shared variable can be accessed only in atomic actions or specifications");
                 }
                 else if (this.globalVarToSharedVarInfo.ContainsKey(node.Decl))
                 {
-                    if (this.globalVarToSharedVarInfo[node.Decl].hideLayerNum < minLayerNum)
-                    {
-                        minLayerNum = this.globalVarToSharedVarInfo[node.Decl].hideLayerNum;
-                    }
-                    if (this.globalVarToSharedVarInfo[node.Decl].introLayerNum > maxLayerNum)
-                    {
-                        maxLayerNum = this.globalVarToSharedVarInfo[node.Decl].introLayerNum;
-                    }
+                    sharedVarsAccessed.Add(node.Decl);
                 }
                 else
                 {
                     Error(node, "Accessed shared variable must have layer annotation");
                 }
             }
-            else if (node.Decl is LocalVariable && ghostVars.Contains(node.Decl) && !canAccessGhostVars)
+            else if ((node.Decl is Formal || node.Decl is Variable) && localVarToLocalVariableInfo.ContainsKey(node.Decl))
             {
-                Error(node, "Ghost variable can be accessed only in assertions");
-            }
-
+                var localVariableInfo = localVarToLocalVariableInfo[node.Decl];
+                if (introducedLocalVarsUpperBound < localVariableInfo.layer)
+                {
+                    introducedLocalVarsUpperBound = localVariableInfo.layer;
+                }
+            } 
             return base.VisitIdentifierExpr(node);
         }
-        
+
         public override Ensures VisitEnsures(Ensures ensures)
         {
-            minLayerNum = int.MaxValue;
-            maxLayerNum = -1;
-            canAccessSharedVars = true;
-            Ensures ret = base.VisitEnsures(ensures);
-            canAccessSharedVars = false;
             ActionInfo actionInfo = procToActionInfo[enclosingProc];
             AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
             if (atomicActionInfo != null && atomicActionInfo.ensures == ensures)
@@ -713,35 +1005,53 @@ namespace Microsoft.Boogie
             }
             else
             {
+                sharedVarsAccessed = new HashSet<Variable>();
+                Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+                base.VisitEnsures(ensures); 
                 CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.createdAtLayerNum);
+                if (introducedLocalVarsUpperBound > Least(FindLayers(ensures.Attributes)))
+                {
+                    Error(ensures, "An introduced local variable is accessed but not available");
+                }
+                introducedLocalVarsUpperBound = int.MinValue;
+                sharedVarsAccessed = null;
             }
-            return ret;
+            return ensures;
         }
-        
+
         public override Requires VisitRequires(Requires requires)
         {
-            minLayerNum = int.MaxValue;
-            maxLayerNum = -1;
-            canAccessSharedVars = true;
-            Requires ret = base.VisitRequires(requires);
-            canAccessSharedVars = false;
+            sharedVarsAccessed = new HashSet<Variable>();
+            Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+            base.VisitRequires(requires);
             CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum);
-            return ret;
+            if (introducedLocalVarsUpperBound > Least(FindLayers(requires.Attributes)))
+            {
+                Error(requires, "An introduced local variable is accessed but not available");
+            }
+            introducedLocalVarsUpperBound = int.MinValue;
+            sharedVarsAccessed = null;
+            return requires;
         }
 
         public override Cmd VisitAssertCmd(AssertCmd node)
         {
             if (enclosingImpl == null)
+            {
+                // in this case, we are visiting an assert inside a CodeExpr
                 return base.VisitAssertCmd(node);
-            minLayerNum = int.MaxValue;
-            maxLayerNum = -1;
-            canAccessSharedVars = true;
-            canAccessGhostVars = true;
-            Cmd ret = base.VisitAssertCmd(node);
-            canAccessGhostVars = false;
-            canAccessSharedVars = false;
+            }
+            sharedVarsAccessed = new HashSet<Variable>();
+            Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+            base.VisitAssertCmd(node);
             CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum);
-            return ret;
+            if (introducedLocalVarsUpperBound > Least(FindLayers(node.Attributes)))
+            {
+                Error(node, "An introduced local variable is accessed but not available");
+            }
+            introducedLocalVarsUpperBound = int.MinValue;
+            sharedVarsAccessed = null;
+            return node;
         }
 
         private List<int> RemoveDuplicatesAndSort(List<int> attrs)
@@ -760,18 +1070,15 @@ namespace Microsoft.Boogie
                 Error(node, "layer not present");
                 return;
             }
+            LayerRange upperBound = FindLayerRange();
             absyToLayerNums[node] = new HashSet<int>();
             foreach (int layerNum in attrs)
             {
-                if (layerNum == leastUnimplementedLayerNum || !AllCreatedLayerNums.Contains(layerNum))
-                {
-                    Error(node, "Illegal layer number");
-                }
-                else if (layerNum > enclosingProcLayerNum)
+                if (layerNum > enclosingProcLayerNum)
                 {
                     Error(node, "The layer cannot be greater than the layer of enclosing procedure");
                 }
-                else if (maxLayerNum < layerNum && layerNum <= minLayerNum)
+                else if (upperBound.Contains(layerNum))
                 {
                     absyToLayerNums[node].Add(layerNum);
                 }
@@ -787,5 +1094,67 @@ namespace Microsoft.Boogie
             checkingContext.Error(node, message);
             errorCount++;
         }
+
+        private class PurityChecker : StandardVisitor
+        {
+            private CivlTypeChecker civlTypeChecker;
+
+            public PurityChecker(CivlTypeChecker civlTypeChecker)
+            {
+                this.civlTypeChecker = civlTypeChecker;
+            }
+            
+            public override Cmd VisitCallCmd(CallCmd node)
+            {
+                Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc;
+                if (!civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(node.Proc))
+                {
+                    civlTypeChecker.Error(node, "Atomic procedure can only call an atomic procedure");
+                    return base.VisitCallCmd(node);
+                }
+                var callerInfo = civlTypeChecker.procToAtomicProcedureInfo[enclosingProc];
+                var calleeInfo = civlTypeChecker.procToAtomicProcedureInfo[node.Proc];
+                if (calleeInfo.isPure)
+                {
+                    // do nothing
+                }
+                else if (callerInfo.isPure)
+                {
+                    civlTypeChecker.Error(node, "Pure procedure can only call pure procedures");
+                }
+                else if (!callerInfo.layerRange.Subset(calleeInfo.layerRange))
+                {
+                    civlTypeChecker.Error(node, "Caller layers must be subset of callee layers");
+                }
+                return base.VisitCallCmd(node);
+            }
+
+            public override Cmd VisitParCallCmd(ParCallCmd node)
+            {
+                civlTypeChecker.Error(node, "Atomic procedures cannot make parallel calls");
+                return node;
+            }
+
+            public override Expr VisitIdentifierExpr(IdentifierExpr node)
+            {
+                Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc;
+                if (node.Decl is GlobalVariable)
+                {
+                    if (civlTypeChecker.procToAtomicProcedureInfo[enclosingProc].isPure)
+                    {
+                        civlTypeChecker.Error(node, "Pure procedure cannot access global variables");
+                    } 
+                    else if (!civlTypeChecker.globalVarToSharedVarInfo.ContainsKey(node.Decl))
+                    {
+                        civlTypeChecker.Error(node, "Atomic procedure cannot access a global variable without layer numbers");
+                    } 
+                    else 
+                    {
+                        civlTypeChecker.sharedVarsAccessed.Add(node.Decl);
+                    }
+                }
+                return node;
+            }
+        }
     }
-}
\ No newline at end of file
+}
diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj
index f15ebca3..113019fd 100644
--- a/Source/Concurrency/Concurrency.csproj
+++ b/Source/Concurrency/Concurrency.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
   <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
   <PropertyGroup>
@@ -73,11 +73,11 @@
   <ItemGroup>
     <Compile Include="LinearSets.cs" />
     <Compile Include="MoverCheck.cs" />
-    <Compile Include="OwickiGries.cs" />
+    <Compile Include="CivlRefinement.cs" />
     <Compile Include="Program.cs" />
     <Compile Include="Properties\AssemblyInfo.cs" />
     <Compile Include="SimulationRelation.cs" />
-    <Compile Include="TypeCheck.cs" />
+    <Compile Include="CivlTypeChecker.cs" />
     <Compile Include="YieldTypeChecker.cs" />
   </ItemGroup>
   <ItemGroup>
@@ -112,4 +112,4 @@
   <Target Name="AfterBuild">
   </Target>
   -->
-</Project>
\ No newline at end of file
+</Project>
diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index 0fa04b1b..f654b688 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -626,10 +626,9 @@ namespace Microsoft.Boogie
                 var domainName = FindDomainName(v);
                 domainNameToScope[domainName].Add(v);
             }
-            foreach (Variable v in program.GlobalVariables)
+            foreach (Variable v in globalVarToDomainName.Keys)
             {
                 var domainName = FindDomainName(v);
-                if (domainName == null) continue;
                 domainNameToScope[domainName].Add(v);
             }
             foreach (string domainName in linearDomains.Keys)
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 7c6d4ac4..732bcaa4 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -10,29 +10,29 @@ namespace Microsoft.Boogie
     public class MoverCheck
     {
         LinearTypeChecker linearTypeChecker;
-        MoverTypeChecker moverTypeChecker;
+        CivlTypeChecker civlTypeChecker;
         List<Declaration> decls;
         HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> commutativityCheckerCache;
         HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> gatePreservationCheckerCache;
         HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> failurePreservationCheckerCache;
-        private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
+        private MoverCheck(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls)
         {
             this.linearTypeChecker = linearTypeChecker;
-            this.moverTypeChecker = moverTypeChecker;
+            this.civlTypeChecker = civlTypeChecker;
             this.decls = decls;
             this.commutativityCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
             this.gatePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
             this.failurePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
         }
 
-        public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
+        public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls)
         {
-            if (moverTypeChecker.procToActionInfo.Count == 0)
+            if (civlTypeChecker.procToActionInfo.Count == 0)
                 return;
 
-            List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
+            List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(civlTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
             sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; });
-            List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
+            List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(civlTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
             sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; });
 
             Dictionary<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>();
@@ -60,8 +60,8 @@ namespace Microsoft.Boogie
                 currPool = pools[currLayerNum];
             }
 
-            Program program = moverTypeChecker.program;
-            MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls);
+            Program program = civlTypeChecker.program;
+            MoverCheck moverChecking = new MoverCheck(linearTypeChecker, civlTypeChecker, decls);
             foreach (int layerNum in pools.Keys)
             {
                 foreach (AtomicActionInfo first in pools[layerNum])
@@ -537,7 +537,7 @@ namespace Microsoft.Boogie
             ensures.Add(ensureCheck);
             string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);
             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
-            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
+            civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks);
             impl.Proc = proc;
@@ -580,7 +580,7 @@ namespace Microsoft.Boogie
                 requires.Add(new Requires(false, assertCmd.Expr));
             string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
-            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
+            civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);
             impl.Proc = proc;
@@ -628,7 +628,7 @@ namespace Microsoft.Boogie
                 requires.Add(new Requires(false, assertCmd.Expr));
             string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
-            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
+            civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);
             impl.Proc = proc;
@@ -662,7 +662,7 @@ namespace Microsoft.Boogie
             blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));
             string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name);
             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
-            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
+            civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures);
             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);
             impl.Proc = proc;
diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs
index b56e1cf3..1be7cc07 100644
--- a/Source/Concurrency/Program.cs
+++ b/Source/Concurrency/Program.cs
@@ -7,20 +7,20 @@ namespace Microsoft.Boogie
 {
     public class Concurrency
     {
-        public static void Transform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)
+        public static void Transform(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker)
         {
             List<Declaration> originalDecls = new List<Declaration>();
             Program program = linearTypeChecker.program;
             foreach (var decl in program.TopLevelDeclarations)
             {
                 Procedure proc = decl as Procedure;
-                if (proc != null && moverTypeChecker.procToActionInfo.ContainsKey(proc))
+                if (proc != null && civlTypeChecker.procToActionInfo.ContainsKey(proc))
                 {
                     originalDecls.Add(proc);
                     continue;
                 }
                 Implementation impl = decl as Implementation;
-                if (impl != null && moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc))
+                if (impl != null && civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc))
                 {
                     originalDecls.Add(impl);
                 }
@@ -29,12 +29,12 @@ namespace Microsoft.Boogie
             List<Declaration> decls = new List<Declaration>();
             if (!CommandLineOptions.Clo.TrustAtomicityTypes)
             {
-                MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
+                MoverCheck.AddCheckers(linearTypeChecker, civlTypeChecker, decls);
             } 
-            OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
+            CivlRefinement.AddCheckers(linearTypeChecker, civlTypeChecker, decls);
             foreach (Declaration decl in decls)
             {
-                decl.Attributes = OwickiGries.RemoveYieldsAttribute(decl.Attributes);
+                decl.Attributes = CivlRefinement.RemoveYieldsAttribute(decl.Attributes);
             }
             program.RemoveTopLevelDeclarations(x => originalDecls.Contains(x));
             program.AddTopLevelDeclarations(decls);
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index a698c8fd..ed59d3ad 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 layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum));
+                civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {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 layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum));
+                civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {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 layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum));
+                civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {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.absyToLayerNums[assertCmd].Contains(currLayerNum))
+                if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && civlTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum))
                 {
                     return true;
                 }
@@ -132,25 +132,25 @@ namespace Microsoft.Boogie
             return false;
         }
         
-        public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker)
+        public static void PerformYieldSafeCheck(CivlTypeChecker civlTypeChecker)
         {
-            foreach (var impl in moverTypeChecker.program.Implementations)
+            foreach (var impl in civlTypeChecker.program.Implementations)
             {
-                if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue;
+                if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue;
                 impl.PruneUnreachableBlocks();
                 Graph<Block> implGraph = Program.GraphFromImpl(impl);
                 implGraph.ComputeLoops();
-                int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;
-                foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))
+                int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;
+                foreach (int layerNum in civlTypeChecker.AllLayerNums)
                 {
                     if (layerNum > specLayerNum) continue;
-                    YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers);
+                    YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers);
                 }
             }
         }
 
         int stateCounter;
-        MoverTypeChecker moverTypeChecker;
+        CivlTypeChecker civlTypeChecker;
         Implementation impl;
         int currLayerNum;
         Dictionary<Absy, int> absyToNode;
@@ -160,9 +160,9 @@ namespace Microsoft.Boogie
         Dictionary<Tuple<int, int>, int> edgeLabels;
         IEnumerable<Block> loopHeaders;
 
-        private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders)
+        private YieldTypeChecker(CivlTypeChecker civlTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders)
         {
-            this.moverTypeChecker = moverTypeChecker;
+            this.civlTypeChecker = civlTypeChecker;
             this.impl = impl;
             this.currLayerNum = currLayerNum;
             this.loopHeaders = loopHeaders;
@@ -226,20 +226,20 @@ namespace Microsoft.Boogie
                         CallCmd callCmd = cmd as CallCmd;
                         if (callCmd.IsAsync)
                         {
-                            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+                            ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc];
                             if (currLayerNum <= actionInfo.createdAtLayerNum)
                                 edgeLabels[edge] = 'L';
                             else
                                 edgeLabels[edge] = 'B';
                         }
-                        else if (!moverTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc))
+                        else if (!civlTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc))
                         {
                             edgeLabels[edge] = 'P';
                         }
                         else
                         {
                             MoverType moverType;
-                            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+                            ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc];
                             if (actionInfo.createdAtLayerNum >= 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].createdAtLayerNum >= currLayerNum)
+                            if (civlTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum)
                             {
                                 isYield = true;
                             }
@@ -294,7 +294,7 @@ namespace Microsoft.Boogie
                             int numAtomicActions = 0;
                             foreach (CallCmd callCmd in parCallCmd.CallCmds)
                             {
-                                ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+                                ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc];
                                 isRightMover = isRightMover && actionInfo.IsRightMover;
                                 isLeftMover = isLeftMover && actionInfo.IsLeftMover;
                                 if (actionInfo is AtomicActionInfo)
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 36c99b7b..8a8558bf 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -696,6 +696,8 @@ namespace Microsoft.Boogie {
       }
     }
 
+    public readonly ISet<string> NecessaryAssumes = new HashSet<string>();
+
     public IEnumerable<Block> Blocks()
     {
       return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item);
@@ -733,6 +735,45 @@ namespace Microsoft.Boogie {
       }
     }
 
+
+    /// <summary>
+    /// Finds blocks that break out of a loop in NaturalLoops(header, backEdgeNode)
+    /// </summary>
+    /// <param name="header"></param>
+    /// <param name="backEdgeNode"></param>
+    /// <returns></returns>
+    private HashSet<Block> GetBreakBlocksOfLoop(Block header, Block backEdgeNode, Graph<Block/*!*/>/*!*/ g)
+    {
+        Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option");
+        var immSuccBlks = new HashSet<Block>();
+        var loopBlocks = g.NaturalLoops(header, backEdgeNode);
+        foreach (Block/*!*/ block in loopBlocks)
+        {
+            Contract.Assert(block != null);
+            var auxCmd = block.TransferCmd as GotoCmd;
+            if (auxCmd == null) continue;
+            foreach (var bl in auxCmd.labelTargets)
+            {
+                if (loopBlocks.Contains(bl)) continue;
+                immSuccBlks.Add(bl);
+            }
+        }
+        return immSuccBlks;
+    }
+
+    private HashSet<Block> GetBlocksInAllNaturalLoops(Block header, Graph<Block/*!*/>/*!*/ g)
+    {
+        Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option");
+        var allBlocksInNaturalLoops = new HashSet<Block>();
+        foreach (Block/*!*/ source in g.BackEdgeNodes(header))
+        {
+            Contract.Assert(source != null);
+            g.NaturalLoops(header, source).Iter(b => allBlocksInNaturalLoops.Add(b));
+        }
+        return allBlocksInNaturalLoops;
+    }
+
+
     void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g,
                                   List<Implementation/*!*/>/*!*/ loopImpls,
                                   Dictionary<string, Dictionary<string, Block>> fullMap) {
@@ -788,7 +829,13 @@ namespace Microsoft.Boogie {
         foreach (Block/*!*/ b in g.BackEdgeNodes(header))
         {
             Contract.Assert(b != null);
-            foreach (Block/*!*/ block in g.NaturalLoops(header, b))
+            HashSet<Block> immSuccBlks = new HashSet<Block>();
+            if (detLoopExtract)
+            {
+                //Need to get the blocks that exit the loop, as we need to add them to targets and footprint
+                immSuccBlks = GetBreakBlocksOfLoop(header, b, g);
+            }
+            foreach (Block/*!*/ block in g.NaturalLoops(header, b).Union(immSuccBlks))
             {
                 Contract.Assert(block != null);
                 foreach (Cmd/*!*/ cmd in block.Cmds)
@@ -943,18 +990,16 @@ namespace Microsoft.Boogie {
                 GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd;
                 Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null && 
                     auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1);
+                //BUGFIX on 10/26/15: this contains nodes present in NaturalLoops for a different backedgenode
+                var loopNodes = GetBlocksInAllNaturalLoops(header, g); //var loopNodes = g.NaturalLoops(header, source); 
                 foreach(var bl in auxGotoCmd.labelTargets) {
-                    bool found = false;
-                    foreach(var n in g.NaturalLoops(header, source)) { //very expensive, can we do a contains?
-                        if (bl == n) { //clarify: is this the right comparison?
-                            found = true;
-                            break;
-                        }
-                    }
-                    if (!found) {
+                    if (g.Nodes.Contains(bl) && //newly created blocks are not present in NaturalLoop(header, xx, g)
+                        !loopNodes.Contains(bl)) {
                         Block auxNewBlock = new Block();
                         auxNewBlock.Label = ((Block)bl).Label;
-                        auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds);
+                        //these blocks may have read/write locals that are not present in naturalLoops
+                        //we need to capture these variables 
+                        auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds); 
                         //add restoration code for such blocks
                         if (loopHeaderToAssignCmd.ContainsKey(header))
                         {
@@ -2196,6 +2241,7 @@ namespace Microsoft.Boogie {
   }
   public class Incarnation : LocalVariable {
     public int incarnationNumber;
+    public readonly Variable OriginalVariable;
     public Incarnation(Variable/*!*/ var, int i) :
       base(
       var.tok,
@@ -2203,6 +2249,7 @@ namespace Microsoft.Boogie {
       ) {
       Contract.Requires(var != null);
       incarnationNumber = i;
+      OriginalVariable = var;
     }
 
   }
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 404945a9..2e33e1dd 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2463,6 +2463,12 @@ namespace Microsoft.Boogie {
       } finally {
         rc.TypeBinderState = previousTypeBinderState;
       }
+
+      var id = QKeyValue.FindStringAttribute(Attributes, "id");
+      if (id != null)
+      {
+        rc.AddStatementId(tok, id);
+      }
     }
 
     public override void AddAssignedVariables(List<Variable> vars) {
@@ -2890,6 +2896,12 @@ namespace Microsoft.Boogie {
     public override void Resolve(ResolutionContext rc) {
       //Contract.Requires(rc != null);
       Expr.Resolve(rc);
+
+      var id = QKeyValue.FindStringAttribute(Attributes, "id");
+      if (id != null)
+      {
+        rc.AddStatementId(tok, id);
+      }
     }
     public override void AddAssignedVariables(List<Variable> vars) {
       //Contract.Requires(vars != null);
@@ -3206,8 +3218,14 @@ namespace Microsoft.Boogie {
       this.Expr.Emit(stream);
       stream.WriteLine(";");
     }
+    public override void Resolve(ResolutionContext rc) {
+      //Contract.Requires(rc != null);
+      ResolveAttributes(Attributes, rc);
+      base.Resolve(rc);
+    }
     public override void Typecheck(TypecheckingContext tc) {
       //Contract.Requires(tc != null);
+      TypecheckAttributes(Attributes, tc);
       Expr.Typecheck(tc);
       Contract.Assert(Expr.Type != null);  // follows from Expr.Typecheck postcondition
       if (!Expr.Type.Unify(Type.Bool)) {
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 9f94490b..3a27eddf 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -338,6 +338,17 @@ namespace Microsoft.Boogie {
 
     public override void Resolve(ResolutionContext rc) {
       //Contract.Requires(rc != null);
+
+      if ((Key == "minimize" || Key == "maximize") && Params.Count != 1)
+      {
+        rc.Error(this, "attributes :minimize and :maximize accept only one argument");
+      }
+
+      if (Key == "verified_under" && Params.Count != 1)
+      {
+        rc.Error(this, "attribute :verified_under accepts only one argument");
+      }
+
       foreach (object p in Params) {
         if (p is Expr) {
           ((Expr)p).Resolve(rc);
@@ -348,8 +359,20 @@ namespace Microsoft.Boogie {
     public override void Typecheck(TypecheckingContext tc) {
       //Contract.Requires(tc != null);
       foreach (object p in Params) {
-        if (p is Expr) {
-          ((Expr)p).Typecheck(tc);
+        var expr = p as Expr;
+        if (expr != null) {
+          expr.Typecheck(tc);
+        }
+        if ((Key == "minimize" || Key == "maximize")
+            && (expr == null || !(expr.Type.IsInt || expr.Type.IsReal || expr.Type.IsBv)))
+        {
+          tc.Error(this, "attributes :minimize and :maximize accept only one argument of type int, real or bv");
+          break;
+        }
+        if (Key == "verified_under" && (expr == null || !expr.Type.IsBool))
+        {
+          tc.Error(this, "attribute :verified_under accepts only one argument of type bool");
+          break;
         }
       }
     }
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 2be1cdf7..e9aa3ceb 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -11,6 +11,7 @@ using System.IO;
 using System.Linq;
 using System.Diagnostics;
 using System.Diagnostics.Contracts;
+using System.Text.RegularExpressions;
 
 namespace Microsoft.Boogie {
   public class CommandLineOptionEngine
@@ -478,6 +479,8 @@ namespace Microsoft.Boogie {
     public string AbstractHoudini = null;
     public bool UseUnsatCoreForContractInfer = false;
     public bool PrintAssignment = false;
+    // TODO(wuestholz): Add documentation for this flag.
+    public bool PrintNecessaryAssumes = false;
     public int InlineDepth = -1;
     public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values
     public bool UseUncheckedContracts = false;
@@ -588,7 +591,7 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public string OwickiGriesDesugaredOutputFile = null;
+    public string CivlDesugaredFile = null;
     public bool TrustAtomicityTypes = false;
     public bool TrustNonInterference = false;
     public int TrustLayersUpto = -1;
@@ -915,9 +918,9 @@ namespace Microsoft.Boogie {
           } 
           return true;
 
-        case "OwickiGries":
+        case "CivlDesugaredFile":
           if (ps.ConfirmArgumentCount(1)) {
-              OwickiGriesDesugaredOutputFile = args[ps.i];
+              CivlDesugaredFile = args[ps.i];
           }
           return true;
 
@@ -1502,7 +1505,7 @@ namespace Microsoft.Boogie {
           return true;
 
         case "verifySnapshots":
-          ps.GetNumericArgument(ref VerifySnapshots, 3);
+          ps.GetNumericArgument(ref VerifySnapshots, 4);
           return true;
 
         case "traceCaching":
@@ -1618,6 +1621,7 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) ||
               ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||
               ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
+              ps.CheckBooleanFlag("printNecessaryAssumes", ref PrintNecessaryAssumes) ||
               ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) ||
               ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
               ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
@@ -1700,7 +1704,7 @@ namespace Microsoft.Boogie {
         // no preference
         return true;
       }
-      return ProcsToCheck.Contains(methodFullname);
+      return ProcsToCheck.Any(s => Regex.IsMatch(methodFullname, "^" + Regex.Escape(s).Replace(@"\*", ".*") + "$"));
     }
 
     public virtual StringCollection ParseNamedArgumentList(string argList) {
@@ -1857,7 +1861,15 @@ namespace Microsoft.Boogie {
   Multiple .bpl files supplied on the command line are concatenated into one
   Boogie program.
 
-  /proc:<p>      : limits which procedures to check
+  /proc:<p>      : Only check procedures matched by pattern <p>. This option
+                   may be specified multiple times to match multiple patterns.
+                   The pattern <p> matches the whole procedure name (i.e.
+                   pattern ""foo"" will only match a procedure called foo and
+                   not fooBar). The pattern <p> may contain * wildcards which
+                   match any character zero or more times. For example the
+                   pattern ""ab*d"" would match abd, abcd and abccd but not
+                   Aabd nor abdD. The pattern ""*ab*d*"" would match abd,
+                   abcd, abccd, Abd and abdD.
   /noResolve     : parse only
   /noTypecheck   : parse and resolve only
 
@@ -1961,6 +1973,10 @@ namespace Microsoft.Boogie {
                 0 - do not use any verification result caching (default)
                 1 - use the basic verification result caching
                 2 - use the more advanced verification result caching
+                3 - use the more advanced caching and report errors according
+                    to the new source locations for errors and their
+                    related locations (but not /errorTrace and CaptureState
+                    locations) 
   /verifySeparately
                 verify each input program separately
   /removeEmptyBlocks:<c>
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 474a91dd..279e00bf 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -339,6 +339,18 @@ namespace Microsoft.Boogie {
       varContext = varContext.ParentContext;
     }
 
+    public readonly ISet<string> StatementIds = new HashSet<string>();
+
+    public void AddStatementId(IToken tok, string name)
+    {
+      if (StatementIds.Contains(name))
+      {
+        Error(tok, "more than one statement with same id: " + name);
+        return;
+      }
+      StatementIds.Add(name);
+    }
+
     public void AddVariable(Variable var, bool global) {
       Contract.Requires(var != null);
       var previous = FindVariable(cce.NonNull(var.Name), !global);
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index f2d58045..9bc855be 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -135,7 +135,7 @@ namespace Microsoft.Boogie
 
       foreach (var e in errorInfo.Aux)
       {
-        if (!(skipExecutionTrace && e.Category.Contains("Execution trace")))
+        if (!(skipExecutionTrace && e.Category != null && e.Category.Contains("Execution trace")))
         {
           ReportBplError(e.Tok, e.FullMsg, false, tw);
         }
@@ -151,25 +151,18 @@ namespace Microsoft.Boogie
     {
       Contract.Requires(message != null);
 
-      if (category != null)
-      {
+      if (category != null) {
         message = string.Format("{0}: {1}", category, message);
       }
       string s;
-      if (tok != null)
-      {
+      if (tok != null) {
         s = string.Format("{0}({1},{2}): {3}", ExecutionEngine.GetFileNameForConsole(tok.filename), tok.line, tok.col, message);
-      }
-      else
-      {
+      } else {
         s = message;
       }
-      if (error)
-      {
+      if (error) {
         ErrorWriteLine(tw, s);
-      }
-      else
-      {
+      } else {
         tw.WriteLine(s);
       }
     }
@@ -489,8 +482,8 @@ namespace Microsoft.Boogie
         }
 
         LinearTypeChecker linearTypeChecker;
-        MoverTypeChecker moverTypeChecker;
-        PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out moverTypeChecker);
+        CivlTypeChecker civlTypeChecker;
+        PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out civlTypeChecker);
         if (oc != PipelineOutcome.ResolvedAndTypeChecked)
           return;
 
@@ -507,13 +500,13 @@ namespace Microsoft.Boogie
 
         if (CommandLineOptions.Clo.StratifiedInlining == 0)
         {
-          Concurrency.Transform(linearTypeChecker, moverTypeChecker);
+          Concurrency.Transform(linearTypeChecker, civlTypeChecker);
           (new LinearEraser()).VisitProgram(program);
-          if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)
+          if (CommandLineOptions.Clo.CivlDesugaredFile != null)
           {
               int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
               CommandLineOptions.Clo.PrintUnstructured = 1;
-              PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false, CommandLineOptions.Clo.PrettyPrint);
+              PrintBplFile(CommandLineOptions.Clo.CivlDesugaredFile, program, false, false, CommandLineOptions.Clo.PrettyPrint);
               CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
           }
         }
@@ -699,13 +692,13 @@ namespace Microsoft.Boogie
     ///  - TypeCheckingError if a type checking error occurred
     ///  - ResolvedAndTypeChecked if both resolution and type checking succeeded
     /// </summary>
-    public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker, out MoverTypeChecker moverTypeChecker)
+    public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker, out CivlTypeChecker civlTypeChecker)
     {
       Contract.Requires(program != null);
       Contract.Requires(bplFileName != null);
 
       linearTypeChecker = null;
-      moverTypeChecker = null;
+      civlTypeChecker = null;
 
       // ---------- Resolve ------------------------------------------------------------
 
@@ -742,11 +735,11 @@ namespace Microsoft.Boogie
 
       CollectModSets(program);
 
-      moverTypeChecker = new MoverTypeChecker(program);
-      moverTypeChecker.TypeCheck();
-      if (moverTypeChecker.errorCount != 0)
+      civlTypeChecker = new CivlTypeChecker(program);
+      civlTypeChecker.TypeCheck();
+      if (civlTypeChecker.errorCount != 0)
       {
-          Console.WriteLine("{0} type checking errors detected in {1}", moverTypeChecker.errorCount, GetFileNameForConsole(bplFileName));
+          Console.WriteLine("{0} type checking errors detected in {1}", civlTypeChecker.errorCount, GetFileNameForConsole(bplFileName));
           return PipelineOutcome.TypeCheckingError;
       }
 
@@ -1015,6 +1008,11 @@ namespace Microsoft.Boogie
         CleanupCheckers(requestId);
       }
 
+      if (CommandLineOptions.Clo.PrintNecessaryAssumes && program.NecessaryAssumes.Any())
+      {
+        Console.WriteLine("Necessary assume command(s): {0}", string.Join(", ", program.NecessaryAssumes));
+      }
+
       cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
 
       outputCollector.WriteMoreOutput();
@@ -1114,23 +1112,23 @@ namespace Microsoft.Boogie
       printer.Inform(string.Format("Verifying {0} ...", impl.Name), output);
 
       int priority = 0;
-      if (0 < CommandLineOptions.Clo.VerifySnapshots)
-      {
-        verificationResult = Cache.Lookup(impl, out priority);
-      }
-
       var wasCached = false;
-      if (verificationResult != null && priority == Priority.SKIP)
-      {
-        if (CommandLineOptions.Clo.XmlSink != null)
-        {
-          CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
-        }
+      if (0 < CommandLineOptions.Clo.VerifySnapshots) {
+        var cachedResults = Cache.Lookup(impl, out priority);
+        if (cachedResults != null && priority == Priority.SKIP) {
+          if (CommandLineOptions.Clo.XmlSink != null) {
+            CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, cachedResults.Start);
+          }
 
-        printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);
-        wasCached = true;
+          printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);
+          if (CommandLineOptions.Clo.VerifySnapshots < 3 || cachedResults.Outcome == ConditionGeneration.Outcome.Correct) {
+            verificationResult = cachedResults;
+            wasCached = true;
+          }
+        }
       }
-      else
+
+      if (!wasCached)
       {
         #region Verify the implementation
 
@@ -1365,8 +1363,8 @@ namespace Microsoft.Boogie
       Program p = ParseBoogieProgram(new List<string> { filename }, false);
       System.Diagnostics.Debug.Assert(p != null);
       LinearTypeChecker linearTypeChecker;
-      MoverTypeChecker moverTypeChecker;
-      PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker, out moverTypeChecker);
+      CivlTypeChecker civlTypeChecker;
+      PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker, out civlTypeChecker);
       System.Diagnostics.Debug.Assert(oc == PipelineOutcome.ResolvedAndTypeChecked);
       return p;
     }
@@ -1466,11 +1464,11 @@ namespace Microsoft.Boogie
 
       printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);
 
-      ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit);
+      ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit, errors);
     }
 
 
-    private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit)
+    private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit, List<Counterexample> errors)
     {
       ErrorInformation errorInfo = null;
 
@@ -1479,10 +1477,69 @@ namespace Microsoft.Boogie
         case VCGen.Outcome.ReachedBound:
           tw.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));
           break;
+        case VCGen.Outcome.Errors:
         case VCGen.Outcome.TimedOut:
           if (implName != null && implTok != null)
           {
-            errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId);
+            if (outcome == ConditionGeneration.Outcome.TimedOut || (errors != null && errors.Any(e => e.IsAuxiliaryCexForDiagnosingTimeouts)))
+            {
+              errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification of '{1}' timed out after {0} seconds", timeLimit, implName), requestId);
+            }
+
+            //  Report timed out assertions as auxiliary info.
+            if (errors != null)
+            {
+              var cmpr = new CounterexampleComparer();
+              var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(cmpr).ToList();
+              timedOutAssertions.Sort(cmpr);
+              if (0 < timedOutAssertions.Count)
+              {
+                errorInfo.Msg += string.Format(" with {0} check(s) that timed out individually", timedOutAssertions.Count);
+              }
+              foreach (Counterexample error in timedOutAssertions)
+              {
+                var callError = error as CallCounterexample;
+                var returnError = error as ReturnCounterexample;
+                var assertError = error as AssertCounterexample;
+                IToken tok = null;
+                string msg = null;
+                if (callError != null)
+                {
+                  tok = callError.FailingCall.tok;
+                  msg = callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.";
+                }
+                else if (returnError != null)
+                {
+                  tok = returnError.FailingReturn.tok;
+                  msg = "A postcondition might not hold on this return path.";
+                }
+                else
+                {
+                  tok = assertError.FailingAssert.tok;
+                  if (assertError.FailingAssert is LoopInitAssertCmd)
+                  {
+                    msg = "This loop invariant might not hold on entry.";
+                  }
+                  else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd)
+                  {
+                    msg = "This loop invariant might not be maintained by the loop.";
+                  }
+                  else
+                  {
+                    msg = assertError.FailingAssert.ErrorData as string;
+                    if (!CommandLineOptions.Clo.ForceBplErrors && assertError.FailingAssert.ErrorMessage != null)
+                    {
+                      msg = assertError.FailingAssert.ErrorMessage;
+                    }
+                    if (msg == null)
+                    {
+                      msg = "This assertion might not hold.";
+                    }
+                  }
+                }
+                errorInfo.AddAuxInfo(tok, msg, "Unverified check due to timeout");
+              }
+            }
           }
           break;
         case VCGen.Outcome.OutOfMemory:
@@ -1509,6 +1566,10 @@ namespace Microsoft.Boogie
             er(errorInfo);
           }
         }
+        else
+        {
+          printer.WriteErrorInformation(errorInfo, tw);
+        }
       }
     }
 
@@ -1582,8 +1643,9 @@ namespace Microsoft.Boogie
           }
           else
           {
-            Interlocked.Add(ref stats.ErrorCount, errors.Count);
-            if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, errors.Count); }
+            int cnt = errors.Where(e => !e.IsAuxiliaryCexForDiagnosingTimeouts).Count();
+            Interlocked.Add(ref stats.ErrorCount, cnt);
+            if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, cnt); }
           }
           break;
       }
@@ -1599,6 +1661,10 @@ namespace Microsoft.Boogie
         errors.Sort(new CounterexampleComparer());
         foreach (Counterexample error in errors)
         {
+          if (error.IsAuxiliaryCexForDiagnosingTimeouts)
+          {
+            continue;
+          }
           var errorInfo = CreateErrorInformation(error, outcome);
           errorInfo.ImplementationName = implName;
 
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index dfe32103..3159238c 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -172,48 +172,28 @@ namespace Microsoft.Boogie
         var vr = ExecutionEngine.Cache.Lookup(impl, out priority);
         if (vr != null && vr.ProgramId == programId)
         {
-          if (priority == Priority.LOW)
-          {
+          if (priority == Priority.LOW) {
             run.LowPriorityImplementationCount++;
-            if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)
-            {
-              SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);
-              if (vr.ProgramId != null)
-              {
-                var p = ExecutionEngine.CachedProgram(vr.ProgramId);
-                if (p != null)
-                {
-                  eai.Inject(impl, p);
-                  run.TransformedImplementationCount++;
-                }
-              }
-            }
-          }
-          else if (priority == Priority.MEDIUM)
-          {
+          } else if (priority == Priority.MEDIUM) {
             run.MediumPriorityImplementationCount++;
-            if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)
-            {
+          } else if (priority == Priority.HIGH) {
+            run.HighPriorityImplementationCount++;
+          } else if (priority == Priority.SKIP) {
+            run.SkippedImplementationCount++;
+          }
+
+          if (priority == Priority.LOW || priority == Priority.MEDIUM || 3 <= CommandLineOptions.Clo.VerifySnapshots) {
+            if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds) {
               SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);
-              if (vr.ProgramId != null)
-              {
+              if (vr.ProgramId != null) {
                 var p = ExecutionEngine.CachedProgram(vr.ProgramId);
-                if (p != null)
-                {
+                if (p != null) {
                   eai.Inject(impl, p);
                   run.TransformedImplementationCount++;
                 }
               }
             }
           }
-          else if (priority == Priority.HIGH)
-          {
-            run.HighPriorityImplementationCount++;
-          }
-          else if (priority == Priority.SKIP)
-          {
-            run.SkippedImplementationCount++;
-          }
         }
       }
       run.End = DateTime.UtcNow;
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index e93ecee9..300fbc10 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -86,6 +86,21 @@ namespace Microsoft.Boogie.SMTLib
       }
     }
 
+    public override void AssertNamed(VCExpr vc, bool polarity, string name)
+    {
+      string vcString;
+      if (polarity)
+      {
+        vcString = VCExpr2String(vc, 1);
+      }
+      else
+      {
+        vcString = "(not " + VCExpr2String(vc, 1) + ")";
+      }
+      AssertAxioms();
+      SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name));
+    }
+
     private void SetupAxiomBuilder(VCExpressionGenerator gen)
     {
       switch (CommandLineOptions.Clo.TypeEncodingMethod)
@@ -246,9 +261,9 @@ namespace Microsoft.Boogie.SMTLib
 
         // Set produce-unsat-cores last. It seems there's a bug in Z3 where if we set it earlier its value
         // gets reset by other set-option commands ( https://z3.codeplex.com/workitem/188 )
-        if (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini))
+        if (CommandLineOptions.Clo.PrintNecessaryAssumes || (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini)))
         {
-          SendThisVC("(set-option :produce-unsat-cores true)");
+          SendCommon("(set-option :produce-unsat-cores true)");
           this.usingUnsatCore = true;
         }
 
@@ -401,6 +416,8 @@ namespace Microsoft.Boogie.SMTLib
 
       PrepareCommon();
 
+      OptimizationRequests.Clear();
+
       string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
       FlushAxioms();
 
@@ -408,7 +425,11 @@ namespace Microsoft.Boogie.SMTLib
 
       SendThisVC("(push 1)");
       SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
+
       SendThisVC(vcString);
+
+      SendOptimizationRequests();
+
       FlushLogFile();
 
       if (Process != null) {
@@ -418,10 +439,21 @@ namespace Microsoft.Boogie.SMTLib
           Process.Inspector.NewProblem(descriptiveName, vc, handler);
       }
 
-      SendThisVC("(check-sat)");
+      SendCheckSat();
       FlushLogFile();
     }
 
+    private void SendOptimizationRequests()
+    {
+      if (options.Solver == SolverKind.Z3 && 0 < OptimizationRequests.Count)
+      {
+        foreach (var r in OptimizationRequests)
+        {
+          SendThisVC(r);
+        }
+      }
+    }
+
     public override void Reset(VCExpressionGenerator gen)
     {
       if (options.Solver == SolverKind.Z3)
@@ -446,6 +478,7 @@ namespace Microsoft.Boogie.SMTLib
       if (options.Solver == SolverKind.Z3)
       {
         this.gen = gen;
+        SendThisVC("(reset)");
         Namer.Reset();
         common.Clear();
         SetupAxiomBuilder(gen);
@@ -456,6 +489,8 @@ namespace Microsoft.Boogie.SMTLib
         ctx.KnownDatatypeConstructors.Clear();
         ctx.parent = this;
         DeclCollector.Reset();
+        NamedAssumes.Clear();
+        UsedNamedAssumes = null;
         SendThisVC("; did a full reset");
       }
     }
@@ -1264,6 +1299,38 @@ namespace Microsoft.Boogie.SMTLib
             
             result = GetResponse();
 
+            var reporter = handler as VC.VCGen.ErrorReporter;
+            // TODO(wuestholz): Is the reporter ever null?
+            if (usingUnsatCore && result == Outcome.Valid && reporter != null && 0 < NamedAssumes.Count)
+            {
+              if (usingUnsatCore)
+              {
+                UsedNamedAssumes = new HashSet<string>();
+                SendThisVC("(get-unsat-core)");
+                var resp = Process.GetProverResponse();
+                if (resp.Name != "")
+                {
+                  UsedNamedAssumes.Add(resp.Name);
+                  if (CommandLineOptions.Clo.PrintNecessaryAssumes)
+                  {
+                    reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length));
+                  }
+                }
+                foreach (var arg in resp.Arguments)
+                {
+                  UsedNamedAssumes.Add(arg.Name);
+                  if (CommandLineOptions.Clo.PrintNecessaryAssumes)
+                  {
+                    reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length));
+                  }
+                }
+              }
+              else
+              {
+                UsedNamedAssumes = null;
+              }
+            }
+
             if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut)
             {
               #region Run timeout diagnostics
@@ -1423,13 +1490,13 @@ namespace Microsoft.Boogie.SMTLib
               expr = "false";
             }
             SendThisVC("(assert " + expr + ")");
-            SendThisVC("(check-sat)");
+            SendCheckSat();
           }
           else {
             string source = labels[labels.Length - 2];
             string target = labels[labels.Length - 1];
             SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") (- " + target + "))))");
-            SendThisVC("(check-sat)");
+            SendCheckSat();
           }
         }
 
@@ -1474,7 +1541,7 @@ namespace Microsoft.Boogie.SMTLib
         SendThisVC("(apply (then (using-params propagate-values :max_rounds 1) simplify) :print false)");
       }
       FlushLogFile();
-      SendThisVC("(check-sat)");
+      SendCheckSat();
       queries++;
       return GetResponse();
     }
@@ -1812,6 +1879,7 @@ namespace Microsoft.Boogie.SMTLib
     private Model GetErrorModel() {
       if (!options.ExpectingModel())
         return null;
+
       SendThisVC("(get-model)");
       Process.Ping();
       Model theModel = null;
@@ -1906,6 +1974,9 @@ namespace Microsoft.Boogie.SMTLib
             result = Outcome.Invalid;
             wasUnknown = true;
             break;
+          case "objectives":
+            // We ignore this.
+            break;
           default:
             HandleProverError("Unexpected prover response: " + resp.ToString());
             break;
@@ -1944,6 +2015,8 @@ namespace Microsoft.Boogie.SMTLib
       return result;
     }
 
+    readonly IList<string> OptimizationRequests = new List<string>();
+
     protected string VCExpr2String(VCExpr expr, int polarity)
     {
       Contract.Requires(expr != null);
@@ -1983,10 +2056,8 @@ namespace Microsoft.Boogie.SMTLib
         DeclCollector.Collect(sortedExpr);
         FeedTypeDeclsToProver();
 
-
-
-        AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options));
-        string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options);
+        AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options, namedAssumes: NamedAssumes));
+        string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, NamedAssumes, OptimizationRequests);
         Contract.Assert(res != null);
 
         if (CommandLineOptions.Clo.Trace)
@@ -2094,19 +2165,20 @@ namespace Microsoft.Boogie.SMTLib
         throw new NotImplementedException();
     }
 
-    public override void Assert(VCExpr vc, bool polarity)
+    public override void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1)
     {
-        string a = "";
-        if (polarity)
-        {
-            a = "(assert " + VCExpr2String(vc, 1) + ")";
+        OptimizationRequests.Clear();
+        string assert = "assert";
+        if (options.Solver == SolverKind.Z3 && isSoft) {
+            assert += "-soft";
         }
-        else
-        {
-            a = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
+        var expr = polarity ? VCExpr2String(vc, 1) : "(not\n" + VCExpr2String(vc, 1) + "\n)";
+        if (options.Solver == SolverKind.Z3 && isSoft) {
+            expr += " :weight " + weight;
         }
         AssertAxioms();
-        SendThisVC(a);
+        SendThisVC("(" + assert + " " + expr + ")");
+        SendOptimizationRequests();
     }
 
     public override void DefineMacro(Macro f, VCExpr vc) {
@@ -2126,9 +2198,15 @@ namespace Microsoft.Boogie.SMTLib
     public override void Check()
     {
         PrepareCommon();
-        SendThisVC("(check-sat)");
+        SendCheckSat();
         FlushLogFile();
     }
+
+    public void SendCheckSat()
+    {
+      UsedNamedAssumes = null;
+      SendThisVC("(check-sat)");
+    }
 	
     public override void SetTimeOut(int ms)
     {
@@ -2325,21 +2403,6 @@ namespace Microsoft.Boogie.SMTLib
           return opts;
       }
 
-      public override void AssertNamed(VCExpr vc, bool polarity, string name)
-      {
-          string vcString;
-          if (polarity)
-          {
-              vcString = VCExpr2String(vc, 1);
-          }
-          else
-          {
-              vcString = "(not " + VCExpr2String(vc, 1) + ")";
-          }
-          AssertAxioms();
-          SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name));
-      }
-
       public override VCExpr ComputeInterpolant(VCExpr A, VCExpr B)
       {
           string A_str = VCExpr2String(A, 1);
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index dcf95bd2..06aa5bbe 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -34,14 +34,14 @@ namespace Microsoft.Boogie.SMTLib
   public class SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/>
   {
 
-    public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts)
+    public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, ISet<VCExprVar> namedAssumes = null, IList<string> optReqs = null, ISet<VCExprVar> tryAssumes = null)
     {
       Contract.Requires(e != null);
       Contract.Requires(namer != null);
       Contract.Ensures(Contract.Result<string>() != null);
 
       StringWriter sw = new StringWriter();
-      SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts);
+      SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, namedAssumes, optReqs);
       Contract.Assert(lin != null);
       lin.Linearise(e, LineariserOptions.Default);
       return cce.NonNull(sw.ToString());
@@ -74,12 +74,17 @@ namespace Microsoft.Boogie.SMTLib
     internal int UnderQuantifier = 0;
     internal readonly SMTLibProverOptions ProverOptions;
 
-    public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts)
+    readonly IList<string> OptimizationRequests;
+    readonly ISet<VCExprVar> NamedAssumes;
+
+    public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, ISet<VCExprVar> namedAssumes = null, IList<string> optReqs = null)
     {
       Contract.Requires(wr != null); Contract.Requires(namer != null);
       this.wr = wr;
       this.Namer = namer;
       this.ProverOptions = opts;
+      this.OptimizationRequests = optReqs;
+      this.NamedAssumes = namedAssumes;
     }
 
     public void Linearise(VCExpr expr, LineariserOptions options)
@@ -263,6 +268,26 @@ namespace Microsoft.Boogie.SMTLib
             }
             return true;
         }
+        if (OptimizationRequests != null
+            && (node.Op.Equals(VCExpressionGenerator.MinimizeOp) || node.Op.Equals(VCExpressionGenerator.MaximizeOp)))
+        {
+          string optOp = node.Op.Equals(VCExpressionGenerator.MinimizeOp) ? "minimize" : "maximize";
+          OptimizationRequests.Add(string.Format("({0} {1})", optOp, ToString(node[0], Namer, ProverOptions, NamedAssumes)));
+          Linearise(node[1], options);
+          return true;
+        }
+        if (node.Op is VCExprSoftOp)
+        {
+          Linearise(node[1], options);
+          return true;
+        }
+        if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp))
+        {
+          var exprVar = node[0] as VCExprVar;
+          NamedAssumes.Add(exprVar);
+          Linearise(node[1], options);
+          return true;
+        }
         return node.Accept<bool, LineariserOptions/*!*/>(OpLineariser, options);
     }
 
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 900bdbcc..f1179159 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Boogie.SMTLib
       "flet", "implies", "!=", "if_then_else",
       // Z3 extensions
       "lblneg", "lblpos", "lbl-lit",
-      "if", "&&", "||", "equals", "equiv", "bool",
+      "if", "&&", "||", "equals", "equiv", "bool", "minimize", "maximize",
       // Boogie-defined
       "real_pow", "UOrdering2", "UOrdering3", 
       // Floating point (final draft SMTLIB-v2.5)
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 32e28560..eaed83e9 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -210,7 +210,18 @@ void ObjectInvariant()
 
       if (node.Op is VCExprStoreOp) RegisterStore(node);
       else if (node.Op is VCExprSelectOp) RegisterSelect(node);
-      else {
+      else if (node.Op is VCExprSoftOp) {
+        var exprVar = node[0] as VCExprVar;
+        AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
+        AddDeclaration(string.Format("(assert-soft {0} :weight {1})", exprVar.Name, ((VCExprSoftOp)node.Op).Weight));
+      } else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) {
+        var exprVar = node[0] as VCExprVar;
+        AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
+        if (CommandLineOptions.Clo.PrintNecessaryAssumes)
+        {
+          AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name));
+        }
+      } else {
         VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
         if (op != null && 
           !(op.Func is DatatypeConstructor) && !(op.Func is DatatypeMembership) && !(op.Func is DatatypeSelector) && 
@@ -255,7 +266,10 @@ void ObjectInvariant()
         RegisterType(node.Type);
         string decl =
           "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
-        AddDeclaration(decl);
+        if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") || printedName.StartsWith("try$$")))
+        {
+          AddDeclaration(decl);
+        }
         KnownVariables.Add(node);
 		if(declHandler != null)
 			declHandler.VarDecl(node);
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index 6077f327..dc9ad10f 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -1115,7 +1115,7 @@ namespace Microsoft.Boogie.TypeErasure
       if (typeVarBindings.Count < node.TypeParameters.Count) {
         foreach (TypeVariable/*!*/ var in node.TypeParameters) {
           Contract.Assert(var != null);
-          if (typeVarBindings.All(b => !b.V.Equals(var)))
+          if (typeVarBindings.All(b => !b.V.Equals(bindings.TypeVariableBindings[var])))
             newBoundVars.Add((VCExprVar)bindings.TypeVariableBindings[var]);
         }
       }
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 0a9ba6b3..2c77a252 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -341,6 +341,10 @@ namespace Microsoft.Boogie {
 
     public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool);
 
+    public static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool);
+    public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool);
+    public static readonly VCExprOp NamedAssumeOp = new VCExprCustomOp("named_assume##dummy", 2, Type.Bool);
+
     public VCExprOp BoogieFunctionOp(Function func) {
       Contract.Requires(func != null);
       Contract.Ensures(Contract.Result<VCExprOp>() != null);
@@ -1565,6 +1569,16 @@ namespace Microsoft.Boogie.VCExprAST {
     }
   }
 
+  public class VCExprSoftOp : VCExprCustomOp
+  {
+    public readonly int Weight;
+
+    public VCExprSoftOp(int weight) : base("soft##dummy", 2, Microsoft.Boogie.Type.Bool)
+    {
+      Weight = weight;
+    }
+  }
+
   public class VCExprCustomOp : VCExprOp {
     public readonly string/*!*/ Name;
     int arity;
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 3c3b5cae..7bda0022 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -356,7 +356,7 @@ namespace Microsoft.Boogie {
       hasOutput = false;
       outputExn = null;
       this.handler = handler;
-
+      
       thmProver.Reset(gen);
       SetTimeout();
       proverStart = DateTime.UtcNow;
@@ -386,6 +386,7 @@ namespace Microsoft.Boogie {
   // -----------------------------------------------------------------------------------------------
 
   public abstract class ProverInterface {
+
     public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {
       Contract.Requires(prog != null);
 
@@ -452,6 +453,10 @@ namespace Microsoft.Boogie {
       Undetermined,
       Bounded
     }
+
+    public readonly ISet<VCExprVar> NamedAssumes = new HashSet<VCExprVar>();
+    public ISet<string> UsedNamedAssumes { get; protected set; }
+
     public class ErrorHandler {
       // Used in CheckOutcomeCore
       public virtual int StartingProcId()
@@ -542,7 +547,7 @@ namespace Microsoft.Boogie {
     }
 
     // (assert vc)
-    public virtual void Assert(VCExpr vc, bool polarity)
+    public virtual void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1)
     {
         throw new NotImplementedException();
     }
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 1f010757..19438924 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -85,6 +85,7 @@ namespace Microsoft.Boogie {
     public string RequestId;
     public abstract byte[] Checksum { get; }
     public byte[] SugaredCmdChecksum;
+    public bool IsAuxiliaryCexForDiagnosingTimeouts;
 
     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;
 
@@ -313,7 +314,7 @@ namespace Microsoft.Boogie {
     public abstract int GetLocation();
   }
 
-  public class CounterexampleComparer : IComparer<Counterexample> {
+  public class CounterexampleComparer : IComparer<Counterexample>, IEqualityComparer<Counterexample> {
 
     private int Compare(List<Block> bs1, List<Block> bs2)
     {
@@ -375,6 +376,16 @@ namespace Microsoft.Boogie {
       }
       return -1;
     }
+
+    public bool Equals(Counterexample x, Counterexample y)
+    {
+      return Compare(x, y) == 0;
+    }
+
+    public int GetHashCode(Counterexample obj)
+    {
+      return 0;
+    }
   }
 
   public class AssertCounterexample : Counterexample {
@@ -1122,7 +1133,8 @@ namespace VC {
         }
         if (returnBlocks > 1) {
           string unifiedExitLabel = "GeneratedUnifiedExit";
-          Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(Token.NoToken));
+          Block unifiedExit;
+          unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken));         
           Contract.Assert(unifiedExit != null);
           foreach (Block b in impl.Blocks) {
             if (b.TransferCmd is ReturnCmd) {
@@ -1528,6 +1540,26 @@ namespace VC {
         PredicateCmd pc = (PredicateCmd)c.Clone();
         Contract.Assert(pc != null);
 
+        QKeyValue current = pc.Attributes;
+        while (current != null)
+        {
+          if (current.Key == "minimize" || current.Key == "maximize") {
+            Contract.Assume(current.Params.Count == 1);
+            var param = current.Params[0] as Expr;
+            Contract.Assume(param != null && (param.Type.IsInt || param.Type.IsReal || param.Type.IsBv));
+            current.ClearParams();
+            current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
+          }
+          if (current.Key == "verified_under") {
+            Contract.Assume(current.Params.Count == 1);
+            var param = current.Params[0] as Expr;
+            Contract.Assume(param != null && param.Type.IsBool);
+            current.ClearParams();
+            current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
+          }
+          current = current.Next;
+        }
+
         Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
         if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) {
           string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 0e598267..789f86f5 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -584,9 +584,6 @@ namespace VC {
       vcgen.ConvertCFG2DAG(impl);
       vcgen.PassifyImpl(impl, out mvInfo);
 
-      if (PassiveImplInstrumentation != null)
-          PassiveImplInstrumentation(impl);
-                
       VCExpressionGenerator gen = proverInterface.VCExprGen;
       var exprGen = proverInterface.Context.ExprGen;
       var translator = proverInterface.Context.BoogieExprTranslator;
@@ -599,6 +596,9 @@ namespace VC {
 
       vcgen.InstrumentCallSites(impl);
 
+      if (PassiveImplInstrumentation != null)
+          PassiveImplInstrumentation(impl);
+
       label2absy = new Dictionary<int, Absy>();
       VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, proverInterface.Context);
       translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition); 
@@ -639,6 +639,7 @@ namespace VC {
 
   public abstract class StratifiedVCGenBase : VCGen {
     public readonly static string recordProcName = "boogie_si_record";
+    public readonly static string callSiteVarAttr = "callSiteVar";
     public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
     public ProverInterface prover;
 
@@ -699,7 +700,9 @@ namespace VC {
           if (!implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) continue;
           Variable callSiteVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "SICS" + callSiteId, Microsoft.Boogie.Type.Bool));
           implementation.LocVars.Add(callSiteVar);
-          newCmds.Add(new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar)));
+          var toInsert = new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar),
+              new QKeyValue(Token.NoToken, callSiteVarAttr, new List<object>(), null));
+          newCmds.Add(toInsert);
           callSiteId++;
         }
         block.Cmds = newCmds;
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index bf25e042..6e43e917 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1519,7 +1519,7 @@ namespace VC {
         }
     }
 
-    public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext)
+    public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null)
     {
       Contract.Requires(impl != null);
       Contract.Requires(proverContext != null);
@@ -1527,10 +1527,10 @@ namespace VC {
       Contract.Ensures(Contract.Result<VCExpr>() != null);
 
       label2absy = new Dictionary<int, Absy>();
-      return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);
+      return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext, namedAssumeVars: namedAssumeVars);
     }
 
-    public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) {
+    public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null) {
       Contract.Requires(impl != null);
       Contract.Requires(proverContext != null);
       Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -1632,7 +1632,7 @@ namespace VC {
           //use Duplicator and Substituter rather than new
           //nested IToken?
           //document expand attribute (search for {:ignore}, for example)
-          //fix up new CallCmd, new Requires, new Ensures in OwickiGries.cs
+          //fix up new CallCmd, new Requires, new Ensures in CivlRefinement.cs
           Func<Expr,Expr,Expr> withType = (Expr from, Expr to) =>
           {
             NAryExpr nFrom = from as NAryExpr;
@@ -1763,9 +1763,18 @@ namespace VC {
         {
           var checksum = a.Checksum;
           var oldCex = impl.ErrorChecksumToCachedError[checksum] as Counterexample;
-          if (oldCex != null)
-          {
-            callback.OnCounterexample(oldCex, null);
+          if (oldCex != null) {
+            if (CommandLineOptions.Clo.VerifySnapshots < 3) {
+              callback.OnCounterexample(oldCex, null);
+            } else {
+              // If possible, we use the old counterexample, but with the location information of "a"
+              var cex = AssertCmdToCloneCounterexample(a, oldCex);
+              callback.OnCounterexample(cex, null);
+              // OnCounterexample may have had side effects on the RequestId and OriginalRequestId fields.  We make
+              // any such updates available in oldCex. (Is this really a good design? --KRML)
+              oldCex.RequestId = cex.RequestId;
+              oldCex.OriginalRequestId = cex.OriginalRequestId;
+            }
           }
         }
       }
@@ -2012,6 +2021,16 @@ namespace VC {
       protected ProverContext/*!*/ context;
       Program/*!*/ program;
 
+      public IEnumerable<string> NecessaryAssumes
+      {
+        get { return program.NecessaryAssumes; }
+      }
+
+      public void AddNecessaryAssume(string id)
+      {
+        program.NecessaryAssumes.Add(id);
+      }
+
       public ErrorReporter(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,
           Dictionary<int, Absy>/*!*/ label2absy,
           List<Block/*!*/>/*!*/ blocks,
@@ -2104,6 +2123,7 @@ namespace VC {
           foreach (var cmd in assertCmds)
           {
             Counterexample cex = AssertCmdToCounterexample(cmd.Item1, cmd.Item2 , new List<Block>(), null, null, context);
+            cex.IsAuxiliaryCexForDiagnosingTimeouts = true;
             callback.OnCounterexample(cex, msg);
           }
         }
@@ -2219,10 +2239,11 @@ namespace VC {
       impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List<Cmd>(), new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] })));
       ResetPredecessors(impl.Blocks);
 
-      if(CommandLineOptions.Clo.KInductionDepth < 0) {
+      var k = Math.Max(CommandLineOptions.Clo.KInductionDepth, QKeyValue.FindIntAttribute(impl.Attributes, "kInductionDepth", -1));
+      if(k < 0) {
         ConvertCFG2DAGStandard(impl, edgesCut, taskID);
       } else {
-        ConvertCFG2DAGKInduction(impl, edgesCut, taskID);
+        ConvertCFG2DAGKInduction(impl, edgesCut, taskID, k);
       }
       
       #region Debug Tracing
@@ -2487,14 +2508,12 @@ namespace VC {
       return referencedVars;
     }
 
-    private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID) {
+    private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID, int inductionK) {
 
       // K-induction has not been adapted to be aware of these parameters which standard CFG to DAG transformation uses
       Contract.Requires(edgesCut == null);
       Contract.Requires(taskID == -1);
-
-      int inductionK = CommandLineOptions.Clo.KInductionDepth;
-      Contract.Assume(inductionK >= 0);
+      Contract.Requires(0 <= inductionK);
 
       bool contRuleApplication = true;
       while (contRuleApplication) {
@@ -2809,6 +2828,11 @@ namespace VC {
       mvInfo = new ModelViewInfo(program, impl);
       Convert2PassiveCmd(impl, mvInfo);
 
+      if (QKeyValue.FindBoolAttribute(impl.Attributes, "may_unverified_instrumentation"))
+      {
+        InstrumentWithMayUnverifiedConditions(impl, exitBlock);
+      }
+
       #region Peep-hole optimizations
       if (CommandLineOptions.Clo.RemoveEmptyBlocks){
         #region Get rid of empty blocks
@@ -2844,6 +2868,190 @@ namespace VC {
       return gotoCmdOrigins;
     }
 
+    #region Simplified May-Unverified Analysis and Instrumentation
+
+    static void InstrumentWithMayUnverifiedConditions(Implementation impl, Block unifiedExitBlock)
+    {
+      var q = new Queue<Block>();
+      q.Enqueue(unifiedExitBlock);
+      var conditionOnBlockEntry = new Dictionary<Block, HashSet<Variable>>();
+      while (q.Any())
+      {
+        var block = q.Dequeue();
+
+        if (conditionOnBlockEntry.ContainsKey(block))
+        {
+          continue;
+        }
+
+        var gotoCmd = block.TransferCmd as GotoCmd;
+        if (gotoCmd != null && gotoCmd.labelTargets.Any(b => !conditionOnBlockEntry.ContainsKey(b)))
+        {
+          q.Enqueue(block);
+          continue;
+        }
+
+        HashSet<Variable> cond = new HashSet<Variable>();
+        if (gotoCmd != null)
+        {
+          var mayInstrs = new List<Block>();
+          bool noInstr = true;
+          foreach (var succ in gotoCmd.labelTargets)
+          {
+            var c = conditionOnBlockEntry[succ];
+            if (c != null)
+            {
+              mayInstrs.Add(succ);
+            }
+            else
+            {
+              noInstr = false;
+            }
+            cond = JoinVariableSets(cond, c);
+          }
+          if (!noInstr)
+          {
+            foreach (var instr in mayInstrs)
+            {
+              InstrumentWithCondition(instr, 0, conditionOnBlockEntry[instr]);
+            }
+          }
+        }
+        
+        for (int i = block.Cmds.Count - 1; 0 <= i; i--)
+        {
+          var cmd = block.Cmds[i];
+          if (cond == null) { break; }
+
+          var assertCmd = cmd as AssertCmd;
+          if (assertCmd != null)
+          {
+            var litExpr = assertCmd.Expr as LiteralExpr;
+            if (litExpr != null && litExpr.IsTrue)
+            {
+              continue;
+            }
+
+            HashSet<Variable> vu = null;
+            if (assertCmd.VerifiedUnder == null)
+            {
+              vu = null;
+            }
+            else
+            {
+              HashSet<Variable> vars;
+              if (IsConjunctionOfAssumptionVariables(assertCmd.VerifiedUnder, out vars))
+              {
+                vu = vars;
+                // TODO(wuestholz): Maybe drop the :verified_under attribute.
+              }
+              else
+              {
+                vu = null;
+              }
+            }
+
+            if (vu == null)
+            {
+              InstrumentWithCondition(block, i + 1, cond);
+            }
+
+            cond = JoinVariableSets(cond, vu);
+          }
+        }
+
+        if (cond != null && block.Predecessors.Count == 0)
+        {
+          // TODO(wuestholz): Should we rather instrument each block?
+          InstrumentWithCondition(block, 0, cond);
+        }
+
+        foreach (var pred in block.Predecessors)
+        {
+          q.Enqueue(pred);
+        }
+
+        conditionOnBlockEntry[block] = cond;
+      }
+    }
+
+    private static void InstrumentWithCondition(Block block, int idx, HashSet<Variable> condition)
+    {
+      var conj = Expr.BinaryTreeAnd(condition.Select(v => (Expr)new IdentifierExpr(Token.NoToken, v)).ToList());
+      block.Cmds.Insert(idx, new AssumeCmd(Token.NoToken, Expr.Not(conj)));
+    }
+
+    static HashSet<Variable> JoinVariableSets(HashSet<Variable> c0, HashSet<Variable> c1)
+    {
+      // We use the following lattice:
+      // - Top: null (i.e., true)
+      // - Bottom: new HashSet<Variable>() (i.e., false)
+      // - Other Elements: new HashSet<Variable>(...) (i.e., conjunctions of assumption variables)
+
+      if (c0 == null || c1 == null)
+      {
+        return null;
+      }
+      var result = new HashSet<Variable>(c0);
+      result.UnionWith(c1);
+      return result;
+    }
+
+    static bool IsAssumptionVariableOrIncarnation(Variable v)
+    {
+      if (QKeyValue.FindBoolAttribute(v.Attributes, "assumption")) { return true; }
+      var incar = v as Incarnation;
+      return incar == null || QKeyValue.FindBoolAttribute(incar.OriginalVariable.Attributes, "assumption");
+    }
+
+    static bool IsConjunctionOfAssumptionVariables(Expr expr, out HashSet<Variable> variables)
+    {
+      Contract.Requires(expr != null);
+
+      variables = null;
+      var litExpr = expr as LiteralExpr;
+      if (litExpr != null && (litExpr.IsFalse || litExpr.IsTrue))
+      {
+        if (litExpr.IsTrue)
+        {
+          variables = new HashSet<Variable>();
+        }
+        return true;
+      }
+
+      var idExpr = expr as IdentifierExpr;
+      if (idExpr != null && IsAssumptionVariableOrIncarnation(idExpr.Decl))
+      {
+        variables = new HashSet<Variable>();
+        variables.Add(idExpr.Decl);
+        return true;
+      }
+
+      var andExpr = expr as NAryExpr;
+      if (andExpr != null)
+      {
+        var fun = andExpr.Fun as BinaryOperator;
+        if (fun != null && fun.Op == BinaryOperator.Opcode.And && andExpr.Args != null)
+        {
+          bool res = true;
+          variables = new HashSet<Variable>();
+          foreach (var op in andExpr.Args)
+          {
+            HashSet<Variable> vars;
+            var r = IsConjunctionOfAssumptionVariables(op, out vars);
+            res &= r;
+            variables = JoinVariableSets(variables, vars);
+            if (!res) { break; }
+          }
+          return res;
+        }
+      }
+
+      return false;
+    }
+
+    #endregion
+
     private static void HandleSelectiveChecking(Implementation impl)
     {
       if (QKeyValue.FindBoolAttribute(impl.Attributes, "selective_checking") ||
@@ -3137,6 +3345,31 @@ namespace VC {
       }
     }
 
+    /// <summary>
+    /// Returns a clone of "cex", but with the location stored in "cex" replaced by those from "assrt".
+    /// </summary>
+    public static Counterexample AssertCmdToCloneCounterexample(AssertCmd assrt, Counterexample cex) {
+      Contract.Requires(assrt != null);
+      Contract.Requires(cex != null);
+      Contract.Ensures(Contract.Result<Counterexample>() != null);
+
+      List<string> relatedInformation = new List<string>();
+
+      Counterexample cc;
+      if (assrt is AssertRequiresCmd) {
+        var aa = (AssertRequiresCmd)assrt;
+        cc = new CallCounterexample(cex.Trace, aa.Call, aa.Requires, cex.Model, cex.MvInfo, cex.Context, aa.Checksum);
+      } else if (assrt is AssertEnsuresCmd && cex is ReturnCounterexample) {
+        var aa = (AssertEnsuresCmd)assrt;
+        var oldCex = (ReturnCounterexample)cex;
+        cc = new ReturnCounterexample(cex.Trace, oldCex.FailingReturn, aa.Ensures, cex.Model, cex.MvInfo, cex.Context, aa.Checksum);
+      } else {
+        cc = new AssertCounterexample(cex.Trace, assrt, cex.Model, cex.MvInfo, cex.Context);
+      }
+      cc.relatedInformation = relatedInformation;
+      return cc;
+    }
+
     static VCExpr LetVC(Block startBlock,
                         VCExpr controlFlowVariableExpr,
                         Dictionary<int, Absy> label2absy,
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index b4ee4c09..cad5914b 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -87,7 +87,7 @@ namespace VC {
     /// <summary>
     /// Computes the wlp for an assert or assume command "cmd".
     /// </summary>
-    public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) {
+    internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) {
       Contract.Requires(cmd != null);
       Contract.Requires(N != null);
       Contract.Requires(ctxt != null);
@@ -186,17 +186,48 @@ namespace VC {
             if (naryExpr.Fun is FunctionCall) {
               int id = ac.UniqueId;
               ctxt.Label2absy[id] = ac;
-              return gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);
+              return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N));
             }
           }
         }
-        return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
+        var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
+        
+        var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id");
+        if (aid != null)
+        {
+          var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try");
+          var v = gen.Variable((isTry ? "try$$" : "assume$$") + aid, Microsoft.Boogie.Type.Bool);
+          expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr));
+        }
+        var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft");
+        var softWeight = QKeyValue.FindIntAttribute(ac.Attributes, "soft", 0);
+        if ((soft || 0 < softWeight) && aid != null)
+        {
+          var v = gen.Variable("soft$$" + aid, Microsoft.Boogie.Type.Bool);
+          expr = gen.Function(new VCExprSoftOp(Math.Max(softWeight, 1)), v, gen.ImpliesSimp(v, expr));
+        }
+        return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(expr, N));
       } else {
         Console.WriteLine(cmd.ToString());
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected command
       }
     }
-    
+
+    private static VCExpr MaybeWrapWithOptimization(VCContext ctxt, VCExpressionGenerator gen, QKeyValue attrs, VCExpr expr)
+    {
+      var min = QKeyValue.FindExprAttribute(attrs, "minimize");
+      if (min != null)
+      {
+        expr = gen.Function(VCExpressionGenerator.MinimizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(min), expr);
+      }
+      var max = QKeyValue.FindExprAttribute(attrs, "maximize");
+      if (max != null)
+      {
+        expr = gen.Function(VCExpressionGenerator.MaximizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(max), expr);
+      }
+      return expr;
+    }
+
     public static CommandLineOptions.SubsumptionOption Subsumption(AssertCmd ac) {
       Contract.Requires(ac != null);
       int n = QKeyValue.FindIntAttribute(ac.Attributes, "subsumption", -1);
diff --git a/Source/version.ssc b/Source/version.ssc
deleted file mode 100644
index 5bdcf170..00000000
--- a/Source/version.ssc
+++ /dev/null
@@ -1,12 +0,0 @@
-// ==++==
-// 
-//   
-// 
-// ==--==
-// Warning: Automatically generated file. DO NOT EDIT
-// Generated at Dienstag, 5. Juli 2011 11:26:45
-
-using System.Reflection;
-[assembly: AssemblyVersion("2.2.30705.1126")]
-[assembly: AssemblyFileVersion("2.2.30705.1126")]
-
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
index fddce05a..8d40b81d 100644
--- a/Test/aitest0/Intervals.bpl
+++ b/Test/aitest0/Intervals.bpl
@@ -332,3 +332,18 @@ procedure W0(N: real)
     assert N - i <= bf0 - 1.0;
   }
 }
+
+// mod
+
+procedure Mod0(n: int)
+  requires 10 < n;
+{
+    var i: int;
+
+    i := 0;
+    while (i < 10)
+    {
+        i := (i mod n) + 1;
+    }
+    assert i == 10;
+}
diff --git a/Test/aitest0/Intervals.bpl.expect b/Test/aitest0/Intervals.bpl.expect
index a0769ec5..980593a9 100644
--- a/Test/aitest0/Intervals.bpl.expect
+++ b/Test/aitest0/Intervals.bpl.expect
@@ -54,4 +54,4 @@ Execution trace:
     Intervals.bpl(303,3): anon3_LoopHead
     Intervals.bpl(303,3): anon3_LoopDone
 
-Boogie program verifier finished with 16 verified, 11 errors
+Boogie program verifier finished with 17 verified, 11 errors
diff --git a/Test/aitest0/Issue25.bpl b/Test/aitest0/Issue25.bpl
new file mode 100644
index 00000000..6ffcd113
--- /dev/null
+++ b/Test/aitest0/Issue25.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie -infer:j "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+const N: int;
+axiom 0 <= N;
+
+procedure vacuous_post()
+ensures (forall k, l: int :: 0 <= k && k <= l && l < N ==> N < N); // Used to verify at some point (see https://github.com/boogie-org/boogie/issues/25).
+{
+var x: int;
+x := -N;
+while (x != x) {
+}
+}
diff --git a/Test/aitest0/Issue25.bpl.expect b/Test/aitest0/Issue25.bpl.expect
new file mode 100644
index 00000000..f56502e2
--- /dev/null
+++ b/Test/aitest0/Issue25.bpl.expect
@@ -0,0 +1,8 @@
+Issue25.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
+Issue25.bpl(8,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+    Issue25.bpl(11,3): anon0
+    Issue25.bpl(12,1): anon2_LoopHead
+    Issue25.bpl(12,1): anon2_LoopDone
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/civl/DeviceCache.bpl.expect b/Test/civl/DeviceCache.bpl.expect
index c4cf5ccf..129e60e2 100644
--- a/Test/civl/DeviceCache.bpl.expect
+++ b/Test/civl/DeviceCache.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 30 verified, 0 errors
+Boogie program verifier finished with 39 verified, 0 errors
diff --git a/Test/civl/FlanaganQadeer.bpl.expect b/Test/civl/FlanaganQadeer.bpl.expect
index 00ddb38b..76a9a2bf 100644
--- a/Test/civl/FlanaganQadeer.bpl.expect
+++ b/Test/civl/FlanaganQadeer.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/Program1.bpl.expect b/Test/civl/Program1.bpl.expect
index 41374b00..00ddb38b 100644
--- a/Test/civl/Program1.bpl.expect
+++ b/Test/civl/Program1.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/Program2.bpl.expect b/Test/civl/Program2.bpl.expect
index a9949f2e..9823d44a 100644
--- a/Test/civl/Program2.bpl.expect
+++ b/Test/civl/Program2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/civl/Program3.bpl.expect b/Test/civl/Program3.bpl.expect
index a9949f2e..9823d44a 100644
--- a/Test/civl/Program3.bpl.expect
+++ b/Test/civl/Program3.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl
index 68c2a5f3..11ba8afa 100644
--- a/Test/civl/Program4.bpl
+++ b/Test/civl/Program4.bpl
@@ -1,67 +1,138 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-type Tid; 
-var {:layer 0,1} a:[Tid]int;
+var {:layer 0,2} a:[int]int;
+var {:layer 0,1} count: int;
+var {:layer 1,1} {:linear "tid"} allocated:[int]bool;
 
-procedure {:yields} {:layer 1} main() { 
-    var {:linear "tid"} tid:Tid;
+procedure {:yields} {:layer 2} main()
+requires {:layer 1} allocated == MapConstBool(false);
+{
+    var {:layer 1} {:linear "tid"} tid:int;
+    var i: int;
 
     yield;
-    while (true) { 
-        call tid := Allocate(); 
-	async call P(tid); 
+    assert {:layer 1} AllocInv(count, allocated);
+    while (true)
+    invariant {:layer 1} AllocInv(count, allocated);
+    { 
+        call tid, i := Allocate(); 
+	async call P(tid, i); 
 	yield;
+        assert {:layer 1} AllocInv(count, allocated);	
     }
     yield;
 }
 
-procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid) 
-ensures {:layer 1} a[tid] == old(a)[tid] + 1; 
+procedure {:yields} {:layer 2} P({:layer 1} {:linear "tid"} tid: int, i: int)
+requires {:layer 1} tid == i;
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
+ensures {:layer 2} a[tid] == old(a)[tid] + 1; 
 { 
     var t:int;
 
     yield;
-    assert {:layer 1} a[tid] == old(a)[tid];
-    call t := Read(tid); 
+    assert {:layer 1} AllocInv(count, allocated);
+    assert {:layer 2} a[tid] == old(a)[tid];
+    call t := Read(tid, i); 
     yield;
-    assert {:layer 1} a[tid] == t; 
-    call Write(tid, t + 1); 
+    assert {:layer 1} AllocInv(count, allocated);
+    assert {:layer 2} a[tid] == t; 
+    call Write(tid, i, t + 1); 
     yield;
-    assert {:layer 1} a[tid] == t + 1; 
+    assert {:layer 1} AllocInv(count, allocated);
+    assert {:layer 2} a[tid] == t + 1; 
 }
 
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid)
+procedure {:yields} {:layer 1,2} Allocate() returns ({:layer 1} {:linear "tid"} tid: int, i: int)
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} tid == i;
+ensures {:atomic}
+|{A:
+  return true;
+}|;
 {
     yield;
-    call tid := AllocateLow();
+    assert {:layer 1} AllocInv(count, allocated);
+    call i := AllocateLow();
+    call tid := MakeLinear(i);
     yield;
+    assert {:layer 1} AllocInv(count, allocated);    
 }
 
-procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);
+procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "tid"} tid: int, i: int) returns (val: int)
+requires {:layer 1} tid == i;
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
 ensures {:atomic}
 |{A:
   val := a[tid]; return true;
 }|;
+{
+    yield;
+    assert {:layer 1} AllocInv(count, allocated);
+    call val := ReadLow(i);
+    yield;
+    assert {:layer 1} AllocInv(count, allocated);
+}
 
-procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int);
+procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear "tid"} tid: int, i: int, val: int)
+requires {:layer 1} tid == i;
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
 ensures {:atomic}
 |{A:
   a[tid] := val; return true;
 }|;
+{
+    yield;
+    assert {:layer 1} AllocInv(count, allocated);
+    call WriteLow(i, val);
+    yield;
+    assert {:layer 1} AllocInv(count, allocated);
+}
 
-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid);
-ensures {:atomic} |{ A: return true; }|;
+function {:inline} AllocInv(count: int, allocated:[int]bool): (bool)
+{
+    (forall x: int :: allocated[x] ==> x < count)
+}
+
+procedure {:yields} {:layer 0,1} ReadLow(i: int) returns (val: int);
+ensures {:atomic}
+|{A:
+  val := a[i]; return true;
+}|;
+
+procedure {:yields} {:layer 0,1} WriteLow(i: int, val: int);
+ensures {:atomic}
+|{A:
+  a[i] := val; return true;
+}|;
 
+procedure {:yields} {:layer 0,1} AllocateLow() returns (i: int);
+ensures {:atomic}
+|{A:
+  i := count;
+  count := i + 1;
+  return true;
+}|;
 
+// We can prove that this primitive procedure preserves the permission invariant locally.
+// We only need to using its specification and the definitions of TidCollector and TidSetCollector.
+procedure {:layer 1} MakeLinear(i: int) returns ({:linear "tid"} tid: int);
+requires !allocated[i];
+modifies allocated;
+ensures tid == i && allocated == old(allocated)[i := true];
 
-function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;
-function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;
+function {:builtin "MapConst"} MapConstBool(bool): [int]bool;
+function {:builtin "MapOr"} MapOr([int]bool, [int]bool) : [int]bool;
 
-function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
 {
   MapConstBool(false)[x := true]
 }
-function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
+function {:inline} {:linear "tid"} TidSetCollector(x: [int]bool) : [int]bool
 {
   x
 }
diff --git a/Test/civl/Program4.bpl.expect b/Test/civl/Program4.bpl.expect
index a9949f2e..f08c6e00 100644
--- a/Test/civl/Program4.bpl.expect
+++ b/Test/civl/Program4.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Test/civl/Program5.bpl.expect b/Test/civl/Program5.bpl.expect
index fde7e712..4bcb1071 100644
--- a/Test/civl/Program5.bpl.expect
+++ b/Test/civl/Program5.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 18 verified, 0 errors
+Boogie program verifier finished with 21 verified, 0 errors
diff --git a/Test/civl/StoreBuffer.bpl.expect b/Test/civl/StoreBuffer.bpl.expect
index 8c74fe2e..1931ffd2 100644
--- a/Test/civl/StoreBuffer.bpl.expect
+++ b/Test/civl/StoreBuffer.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 17 verified, 0 errors
+Boogie program verifier finished with 27 verified, 0 errors
diff --git a/Test/civl/akash.bpl.expect b/Test/civl/akash.bpl.expect
index 00ddb38b..76a9a2bf 100644
--- a/Test/civl/akash.bpl.expect
+++ b/Test/civl/akash.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/alloc.bpl b/Test/civl/alloc.bpl
new file mode 100644
index 00000000..68b7e6c6
--- /dev/null
+++ b/Test/civl/alloc.bpl
@@ -0,0 +1,175 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
+
+type lmap;
+function {:linear "mem"} dom(lmap): [int]bool;
+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);
+
+function EmptyLmap(): (lmap);
+axiom (dom(EmptyLmap()) == MapConstBool(false));
+
+function Add(x: lmap, i: int): (lmap);
+axiom (forall x: lmap, i: int :: dom(Add(x, i)) == dom(x)[i:=true] && map(Add(x, i)) == map(x));
+
+function Remove(x: lmap, i: int): (lmap);
+axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));
+
+function {:inline} PoolInv(unallocated:[int]bool, pool: lmap) : (bool)
+{
+    (forall x: int :: unallocated[x] ==> dom(pool)[x])
+}
+
+procedure {:yields} {:layer 2} Main()
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
+{
+   var {:layer 1} {:linear "mem"} l: lmap;
+   var i: int;
+   par Yield() | Dummy();
+   while (*)
+   invariant {:layer 1} PoolInv(unallocated, pool);
+   {
+      call  l, i := Alloc();
+      async call Thread(l, i);
+      par Yield() | Dummy();
+   }
+   par Yield() | Dummy();
+}
+
+procedure {:yields} {:layer 2} Thread({:layer 1} {:linear_in "mem"} local_in: lmap, i: int)
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
+requires {:layer 1} dom(local_in)[i] && map(local_in)[i] == mem[i];
+requires {:layer 2} dom(local_in)[i];
+{
+    var y, o: int;
+    var {:layer 1} {:linear "mem"} local: lmap;
+    var {:layer 1} {:linear "mem"} l: lmap;
+
+    par YieldMem(local_in, i) | Dummy();
+    call local := Copy(local_in);
+    call local := Write(local, i, 42);
+    call o := Read(local, i);
+    assert {:layer 2} o == 42;
+    while (*)
+    invariant {:layer 1} PoolInv(unallocated, pool);
+    {
+        call l, y := Alloc();
+        call l := Write(l, y, 42);
+	call o := Read(l, y);
+	assert {:layer 2} o == 42;
+        call Free(l, y);
+	par Yield() | Dummy();
+    }
+    par Yield() | Dummy();
+}
+
+procedure {:pure} {:inline 1} Copy({:linear_in "mem"} l: lmap) returns ({:linear "mem"} l': lmap)
+{
+    l' := l;
+}
+
+procedure {:yields} {:layer 1,2} Alloc() returns ({:layer 1} {:linear "mem"} l: lmap, i: int)
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+ensures {:right} |{ A: assume dom(l)[i]; return true; }|;
+{
+    call Yield();
+    call i := PickAddr();
+    call l := AllocLinear(i);
+    call YieldMem(l, i);
+}
+
+procedure {:yields} {:layer 1,2} Free({:layer 1} {:linear_in "mem"} l: lmap, i: int)
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
+requires {:layer 1} dom(l)[i];
+ensures {:both} |{ A: return true; }|;
+{
+    call Yield();
+    call FreeLinear(l, i);
+    call ReturnAddr(i);
+    call Yield();
+}
+
+procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "mem"} l: lmap, i: int) returns (o: int)
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
+requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+ensures {:both} |{ A: assert dom(l)[i]; o := map(l)[i]; return true; }|;
+{
+    call YieldMem(l, i);
+    call o := ReadLow(i);
+    call YieldMem(l, i);
+}
+
+procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap)
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
+requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+ensures {:layer 1} dom(l')[i] && map(l')[i] == mem[i];
+ensures {:both} |{ A: assert dom(l)[i]; l' := cons(dom(l), map(l)[i := o]); return true; }|;
+{
+    call YieldMem(l, i);
+    call WriteLow(i, o);
+    call l' := WriteLinear(l, i, o);
+    call YieldMem(l', i);
+}
+
+procedure {:layer 1} AllocLinear(i: int) returns ({:linear "mem"} l: lmap);
+modifies pool;
+requires dom(pool)[i];
+ensures pool == Remove(old(pool), i) && dom(l)[i] && map(l)[i] == mem[i];
+
+procedure {:layer 1} FreeLinear({:linear_in "mem"} l: lmap, i: int);
+modifies pool;
+requires dom(l)[i];
+ensures pool == Add(old(pool), i);
+
+procedure {:layer 1} WriteLinear({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap);
+requires dom(l)[i];
+ensures l' == cons(dom(l), map(l)[i := o]);
+
+procedure {:yields} {:layer 1} Yield()
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
+{
+    yield;
+    assert {:layer 1} PoolInv(unallocated, pool);
+}
+
+procedure {:yields} {:layer 1} YieldMem({:layer 1} {:linear "mem"} l: lmap, i: int)
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
+requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+{
+    yield;
+    assert {:layer 1} PoolInv(unallocated, pool);
+    assert {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+}
+
+procedure {:yields} {:layer 2} Dummy()
+{
+    yield;
+}
+
+var {:layer 1, 1} {:linear "mem"} pool: lmap;
+var {:layer 0, 1} mem:[int]int;
+var {:layer 0, 1} unallocated:[int]bool;
+
+procedure {:yields} {:layer 0, 1} ReadLow(i: int) returns (o: int);
+ensures {:atomic} |{ A: o := mem[i]; return true; }|;
+
+procedure {:yields} {:layer 0, 1} WriteLow(i: int, o: int);
+ensures {:atomic} |{ A: mem[i] := o; return true; }|;
+
+procedure {:yields} {:layer 0, 1} PickAddr() returns (i: int);
+ensures {:atomic} |{ A: assume unallocated[i]; unallocated[i] := false; return true; }|;
+
+procedure {:yields} {:layer 0, 1} ReturnAddr(i: int);
+ensures {:atomic} |{ A: unallocated[i] := true; return true; }|;
\ No newline at end of file
diff --git a/Test/civl/alloc.bpl.expect b/Test/civl/alloc.bpl.expect
new file mode 100644
index 00000000..4bcb1071
--- /dev/null
+++ b/Test/civl/alloc.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 21 verified, 0 errors
diff --git a/Test/civl/bar.bpl.expect b/Test/civl/bar.bpl.expect
index 810c93bf..be6722fe 100644
--- a/Test/civl/bar.bpl.expect
+++ b/Test/civl/bar.bpl.expect
@@ -10,4 +10,4 @@ Execution trace:
     (0,0): anon00
     (0,0): inline$Impl_YieldChecker_PC_1$0$L0
 
-Boogie program verifier finished with 3 verified, 2 errors
+Boogie program verifier finished with 8 verified, 2 errors
diff --git a/Test/civl/chris2.bpl.expect b/Test/civl/chris2.bpl.expect
index ddb8537e..f3b66f4a 100644
--- a/Test/civl/chris2.bpl.expect
+++ b/Test/civl/chris2.bpl.expect
@@ -15,4 +15,4 @@ Execution trace:
 Execution trace:
     (0,0): this_A
 
-Boogie program verifier finished with 1 verified, 4 errors
+Boogie program verifier finished with 2 verified, 4 errors
diff --git a/Test/civl/chris5.bpl b/Test/civl/chris5.bpl
new file mode 100644
index 00000000..23ebe424
--- /dev/null
+++ b/Test/civl/chris5.bpl
@@ -0,0 +1,19 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var{:layer 1,1} g:int;
+
+procedure{:layer 1} P(x:int)
+  requires {:layer 1} x == 0;
+{
+}
+
+procedure{:yields}{:layer 1,2} Y(x:int)
+  ensures{:atomic} |{ A: return true; }|;
+{
+  yield;
+  
+  call P(x);
+  assert{:layer 1} x == 0;
+
+  yield;
+}
diff --git a/Test/civl/chris5.bpl.expect b/Test/civl/chris5.bpl.expect
new file mode 100644
index 00000000..32b474f5
--- /dev/null
+++ b/Test/civl/chris5.bpl.expect
@@ -0,0 +1,7 @@
+chris5.bpl(15,3): Error BP5002: A precondition for this call might not hold.
+chris5.bpl(6,3): Related location: This is the precondition that might not hold.
+Execution trace:
+    chris5.bpl(13,3): anon0
+    (0,0): anon00
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/civl/chris6.bpl b/Test/civl/chris6.bpl
new file mode 100644
index 00000000..a0aecf1e
--- /dev/null
+++ b/Test/civl/chris6.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure{:extern}{:yields}{:layer 1,2} P1();
+  requires{:layer 1} false;
+  ensures{:atomic} |{ A: return true; }|;
+
+procedure{:yields}{:layer 2,3} P2()
+  ensures{:atomic} |{ A: return true; }|;
+{
+  assert{:layer 1} false;
+  yield;
+  call P1();
+  yield;
+}
diff --git a/Test/civl/chris6.bpl.expect b/Test/civl/chris6.bpl.expect
new file mode 100644
index 00000000..229e4e10
--- /dev/null
+++ b/Test/civl/chris6.bpl.expect
@@ -0,0 +1,5 @@
+chris6.bpl(10,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    chris6.bpl(10,3): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/civl/chris7.bpl b/Test/civl/chris7.bpl
new file mode 100644
index 00000000..a8fd25d3
--- /dev/null
+++ b/Test/civl/chris7.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure{:layer 1}{:extern} P() returns(i:int);
+
+procedure{:yields}{:layer 1,1}{:extern} Y({:layer 1}x:int);
+
+procedure{:yields}{:layer 1,2} A({:layer 1}y:int)
+  ensures {:atomic} |{ A: return true; }|;
+{
+  var{:layer 1} tmp:int;
+  call Y(y);
+  call tmp := P();
+  call Y(tmp);
+}
diff --git a/Test/civl/chris7.bpl.expect b/Test/civl/chris7.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/civl/chris7.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/civl/chris8.bpl b/Test/civl/chris8.bpl
new file mode 100644
index 00000000..070cfec4
--- /dev/null
+++ b/Test/civl/chris8.bpl
@@ -0,0 +1,15 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var{:layer 1,1} x:int;
+
+procedure{:layer 1}{:extern} P1(i:int);
+procedure{:pure}{:extern} P2(j:int);
+
+procedure{:yields}{:layer 1,2} A1({:layer 1}i:int)
+  ensures {:atomic} |{ A: return true; }|;
+{
+  yield;
+  call P1(i);
+  call P2(i);
+  yield;
+}
diff --git a/Test/civl/chris8.bpl.expect b/Test/civl/chris8.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/civl/chris8.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/civl/civl-paper.bpl.expect b/Test/civl/civl-paper.bpl.expect
index 11d204a8..bd1df2f9 100644
--- a/Test/civl/civl-paper.bpl.expect
+++ b/Test/civl/civl-paper.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 35 verified, 0 errors
+Boogie program verifier finished with 45 verified, 0 errors
diff --git a/Test/civl/foo.bpl.expect b/Test/civl/foo.bpl.expect
index 41e30691..44a93860 100644
--- a/Test/civl/foo.bpl.expect
+++ b/Test/civl/foo.bpl.expect
@@ -5,4 +5,4 @@ Execution trace:
     foo.bpl(14,3): inline$Incr_1$0$A
     (0,0): inline$Impl_YieldChecker_PC_1$0$L0
 
-Boogie program verifier finished with 4 verified, 1 error
+Boogie program verifier finished with 9 verified, 1 error
diff --git a/Test/civl/funky.bpl b/Test/civl/funky.bpl
new file mode 100644
index 00000000..ad5bf271
--- /dev/null
+++ b/Test/civl/funky.bpl
@@ -0,0 +1,133 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+const nil: X;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+  MapConstBool(false)[x := true]
+}
+
+var {:layer 0, 3} A: X;
+var {:layer 0, 3} B: X;
+var {:layer 0, 3} counter: int;
+
+procedure {:yields} {:layer 0, 3} LockA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil; assume A == nil; A := tid; return true; }|;
+
+procedure {:yields} {:layer 0, 1} IncrA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter + 1; return true; }|;
+
+procedure {:yields} {:layer 0, 1} DecrA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter - 1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} UnlockA({:linear "tid"} tid: X);
+ensures {:left} |{ A: assert tid != nil && A == tid; A := nil; return true; }|;
+
+procedure {:yields} {:layer 0, 3} LockB({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil; assume B == nil; B := tid; return true; }|;
+
+procedure {:yields} {:layer 0, 2} IncrB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter + 1; return true; }|;
+
+procedure {:yields} {:layer 0, 1} DecrB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter - 1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} UnlockB({:linear "tid"} tid: X);
+ensures {:left} |{ A: assert tid != nil && B == tid; B := nil; return true; }|;
+
+procedure {:yields} {:layer 0, 3} AssertA({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} AssertB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|;
+
+procedure {:pure} AllocTid() returns ({:linear "tid"} tid: X);
+ensures tid != nil;
+
+procedure {:yields} {:layer 1, 2} AbsDecrB({:linear "tid"} tid: X)
+ensures {:right} |{ A: assert tid != nil && B == tid && counter == 0; counter := counter - 1; return true; }|;
+{
+    yield;
+    call DecrB(tid);
+    yield;
+}
+
+procedure {:yields} {:layer 2, 3} AbsAssertA({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|;
+{
+    yield;
+    call AssertA(tid);
+    yield;
+}
+
+procedure {:yields} {:layer 2, 3} AbsAssertB({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|;
+{
+    yield;
+    call AssertB(tid);
+    yield;
+}
+
+procedure {:yields} {:layer 1} TA({:linear "tid"} tid: X)
+requires {:layer 1} tid != nil;
+{
+    yield;
+    call LockA(tid);
+    call IncrA(tid);
+    call DecrA(tid);
+    call UnlockA(tid);
+    yield;
+}
+
+procedure {:yields} {:layer 2, 3} TB({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && counter == 0; return true; }|;
+{
+    yield;
+    call LockB(tid);
+    call AbsDecrB(tid);
+    call IncrB(tid);
+    call UnlockB(tid);
+    yield;
+}
+
+procedure {:yields} {:layer 3} AbsTB({:linear "tid"} tid: X)
+requires {:layer 3} tid != nil && counter == 0;
+{
+    yield;
+    assert {:layer 3} counter == 0;
+    call TB(tid);
+    yield;
+}
+
+procedure {:yields} {:layer 3} main({:linear "tid"} tid: X)
+requires {:layer 3} tid != nil && counter == 0;
+{
+    var {:linear "tid"} cid: X;
+    
+    yield;
+    assert {:layer 3} counter == 0;
+    while (*)
+    invariant {:layer 3} counter == 0;
+    {
+        if (*) {
+	    call cid := AllocTid();
+	    async call TA(cid);
+	}
+	if (*) {
+	    call cid := AllocTid();
+	    async call AbsTB(cid);
+	}
+    	yield;
+    	assert {:layer 3} counter == 0;
+	call LockA(tid);
+	call AbsAssertA(tid);
+	call LockB(tid);
+	call AbsAssertB(tid);
+	call UnlockB(tid);
+	call UnlockA(tid);
+	yield;
+    	assert {:layer 3} counter == 0;	
+    }
+    yield;
+}
\ No newline at end of file
diff --git a/Test/civl/funky.bpl.expect b/Test/civl/funky.bpl.expect
new file mode 100644
index 00000000..0a114594
--- /dev/null
+++ b/Test/civl/funky.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 75 verified, 0 errors
diff --git a/Test/civl/ghost.bpl b/Test/civl/ghost.bpl
index 74d16acf..1468fa56 100644
--- a/Test/civl/ghost.bpl
+++ b/Test/civl/ghost.bpl
@@ -5,7 +5,7 @@ var {:layer 0} x: int;
 procedure {:yields} {:layer 0,1} Incr();
 ensures {:right} |{ A: x := x + 1; return true; }|;
 
-procedure ghost(y: int) returns (z: int)
+procedure {:pure} ghost(y: int) returns (z: int)
 requires y == 1;
 ensures z == 2;
 {
@@ -15,8 +15,7 @@ ensures z == 2;
 procedure {:yields} {:layer 1,2} Incr2() 
 ensures {:right} |{ A: x := x + 2; return true; }|;
 {
-  var {:ghost} a: int;
-  var {:ghost} b: int;
+  var {:layer 1} a: int;
 
   yield;
   call a := ghost(1);
@@ -25,7 +24,7 @@ ensures {:right} |{ A: x := x + 2; return true; }|;
   yield;
 }
 
-procedure ghost_0() returns (z: int)
+procedure {:layer 1} ghost_0() returns (z: int)
 ensures z == x;
 {
   z := x;
@@ -34,8 +33,8 @@ ensures z == x;
 procedure {:yields} {:layer 1,2} Incr2_0() 
 ensures {:right} |{ A: x := x + 2; return true; }|;
 {
-  var {:ghost} a: int;
-  var {:ghost} b: int;
+  var {:layer 1} a: int;
+  var {:layer 1} b: int;
 
   yield;
   call a := ghost_0();
diff --git a/Test/civl/ghost.bpl.expect b/Test/civl/ghost.bpl.expect
index 9823d44a..76a9a2bf 100644
--- a/Test/civl/ghost.bpl.expect
+++ b/Test/civl/ghost.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 6 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/linear-set.bpl.expect b/Test/civl/linear-set.bpl.expect
index 00ddb38b..76a9a2bf 100644
--- a/Test/civl/linear-set.bpl.expect
+++ b/Test/civl/linear-set.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/linear-set2.bpl.expect b/Test/civl/linear-set2.bpl.expect
index 00ddb38b..76a9a2bf 100644
--- a/Test/civl/linear-set2.bpl.expect
+++ b/Test/civl/linear-set2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/lock-introduced.bpl b/Test/civl/lock-introduced.bpl
index fa0a3977..5403e5d4 100644
--- a/Test/civl/lock-introduced.bpl
+++ b/Test/civl/lock-introduced.bpl
@@ -67,6 +67,9 @@ ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|;
     yield;
     L: 
         call status := CAS(false, true);
+        if (status) {
+	    call SetLock(tid);
+	}
 	yield;
         goto A, B;
 
@@ -85,9 +88,16 @@ ensures {:atomic} |{ A: b := false; lock := nil; return true; }|;
 {
     yield;
     call SET(false);
+    call SetLock(nil);
     yield;
 }
 
+procedure {:layer 1} {:inline 1} SetLock(v: X)
+modifies lock;
+{
+    lock := v;
+}
+
 procedure {:yields} {:layer 0,1} CAS(prev: bool, next: bool) returns (status: bool);
 ensures {:atomic} |{ 
 A: goto B, C; 
diff --git a/Test/civl/lock-introduced.bpl.expect b/Test/civl/lock-introduced.bpl.expect
index f08c6e00..8c74fe2e 100644
--- a/Test/civl/lock-introduced.bpl.expect
+++ b/Test/civl/lock-introduced.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 12 verified, 0 errors
+Boogie program verifier finished with 17 verified, 0 errors
diff --git a/Test/civl/lock.bpl.expect b/Test/civl/lock.bpl.expect
index 3e6d423a..76a9a2bf 100644
--- a/Test/civl/lock.bpl.expect
+++ b/Test/civl/lock.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 5 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/lock2.bpl.expect b/Test/civl/lock2.bpl.expect
index 3e6d423a..76a9a2bf 100644
--- a/Test/civl/lock2.bpl.expect
+++ b/Test/civl/lock2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 5 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/multiset.bpl.expect b/Test/civl/multiset.bpl.expect
index 0a77c517..63682bb4 100644
--- a/Test/civl/multiset.bpl.expect
+++ b/Test/civl/multiset.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 78 verified, 0 errors
+Boogie program verifier finished with 85 verified, 0 errors
diff --git a/Test/civl/new1.bpl.expect b/Test/civl/new1.bpl.expect
index 41374b00..00ddb38b 100644
--- a/Test/civl/new1.bpl.expect
+++ b/Test/civl/new1.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/nocollector.bpl b/Test/civl/nocollector.bpl
new file mode 100644
index 00000000..5a6f1e5d
--- /dev/null
+++ b/Test/civl/nocollector.bpl
@@ -0,0 +1,8 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:linear "L"} x:int;
+
+procedure{:yields}{:layer 1} P()
+{
+  yield;
+}
diff --git a/Test/civl/nocollector.bpl.expect b/Test/civl/nocollector.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/civl/nocollector.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/civl/one.bpl.expect b/Test/civl/one.bpl.expect
index 37fad75c..41374b00 100644
--- a/Test/civl/one.bpl.expect
+++ b/Test/civl/one.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/civl/par-incr.bpl.expect b/Test/civl/par-incr.bpl.expect
index 00ddb38b..3e3dc54b 100644
--- a/Test/civl/par-incr.bpl.expect
+++ b/Test/civl/par-incr.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 7 verified, 0 errors
diff --git a/Test/civl/parallel1.bpl.expect b/Test/civl/parallel1.bpl.expect
index 889ee4f2..fa974099 100644
--- a/Test/civl/parallel1.bpl.expect
+++ b/Test/civl/parallel1.bpl.expect
@@ -5,4 +5,4 @@ Execution trace:
     parallel1.bpl(14,3): inline$Incr_1$0$A
     (0,0): inline$Impl_YieldChecker_PC_1$0$L0
 
-Boogie program verifier finished with 3 verified, 1 error
+Boogie program verifier finished with 7 verified, 1 error
diff --git a/Test/civl/parallel2.bpl.expect b/Test/civl/parallel2.bpl.expect
index 3e6d423a..12041afe 100644
--- a/Test/civl/parallel2.bpl.expect
+++ b/Test/civl/parallel2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 5 verified, 0 errors
+Boogie program verifier finished with 10 verified, 0 errors
diff --git a/Test/civl/parallel4.bpl.expect b/Test/civl/parallel4.bpl.expect
index 2d4c8148..baf228c8 100644
--- a/Test/civl/parallel4.bpl.expect
+++ b/Test/civl/parallel4.bpl.expect
@@ -3,4 +3,4 @@ Execution trace:
     parallel4.bpl(29,5): anon0
     (0,0): anon01
 
-Boogie program verifier finished with 3 verified, 1 error
+Boogie program verifier finished with 7 verified, 1 error
diff --git a/Test/civl/parallel5.bpl.expect b/Test/civl/parallel5.bpl.expect
index 3e6d423a..12041afe 100644
--- a/Test/civl/parallel5.bpl.expect
+++ b/Test/civl/parallel5.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 5 verified, 0 errors
+Boogie program verifier finished with 10 verified, 0 errors
diff --git a/Test/civl/perm.bpl.expect b/Test/civl/perm.bpl.expect
index 41374b00..00ddb38b 100644
--- a/Test/civl/perm.bpl.expect
+++ b/Test/civl/perm.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/t1.bpl.expect b/Test/civl/t1.bpl.expect
index fcef7e58..27a208d4 100644
--- a/Test/civl/t1.bpl.expect
+++ b/Test/civl/t1.bpl.expect
@@ -6,4 +6,4 @@ Execution trace:
     t1.bpl(25,21): inline$SetG_1$0$A
     (0,0): inline$Impl_YieldChecker_A_1$0$L1
 
-Boogie program verifier finished with 4 verified, 1 error
+Boogie program verifier finished with 9 verified, 1 error
diff --git a/Test/civl/termination2.bpl.expect b/Test/civl/termination2.bpl.expect
index 37fad75c..41374b00 100644
--- a/Test/civl/termination2.bpl.expect
+++ b/Test/civl/termination2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl
index 9fc55646..df19aae4 100644
--- a/Test/civl/ticket.bpl
+++ b/Test/civl/ticket.bpl
@@ -6,7 +6,6 @@ axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);
 axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
 
 type X;
-function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
 const nil: X;
 var {:layer 0,2} t: int;
 var {:layer 0,2} s: int;
@@ -42,7 +41,7 @@ ensures {:layer 1} {:layer 2} xl != nil;
 }
 
 procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)
-requires {:layer 2} xls' == mapconstbool(true);
+requires {:layer 2} xls' == MapConstBool(true);
 {
     var {:linear "tid"} tid: X;
     var {:linear "tid"} xls: [X]bool;
@@ -132,7 +131,7 @@ ensures {:layer 1} Inv1(T,t);
 }
 
 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; }|;
+ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
 
 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; }|;
diff --git a/Test/civl/ticket.bpl.expect b/Test/civl/ticket.bpl.expect
index b072912b..dc45a0ee 100644
--- a/Test/civl/ticket.bpl.expect
+++ b/Test/civl/ticket.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 16 verified, 0 errors
+Boogie program verifier finished with 24 verified, 0 errors
diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl
index 751ce861..a184886d 100644
--- a/Test/civl/treiber-stack.bpl
+++ b/Test/civl/treiber-stack.bpl
@@ -1,62 +1,71 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-type Node = int;
-const unique null: Node;
+
+const null: int;
 type lmap;
-function {:linear "Node"} dom(lmap): [Node]bool;
-function map(lmap): [Node]Node;
-function {:builtin "MapConst"} MapConstBool(bool) : [Node]bool;
+function {:linear "Node"} dom(lmap): [int]bool;
+function map(lmap): [int]int;
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
 
 function EmptyLmap(): (lmap);
 axiom (dom(EmptyLmap()) == MapConstBool(false));
 
-function Add(x: lmap, i: Node, v: Node): (lmap);
-axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);
+function Add(x: lmap, i: int, v: int): (lmap);
+axiom (forall x: lmap, i: int, v: int :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);
 
-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));
+function Remove(x: lmap, i: int): (lmap);
+axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));
 
-procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:Node);
-ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|;
+procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:int);
+ensures {:right} |{ A: assume v == null || dom(Stack)[v] || Used[v]; return true; }|;
 
-procedure {:yields} {:layer 0,1} Load(i:Node) returns (v:Node);
-ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C;
+procedure {:yields} {:layer 0,1} Load(i:int) returns (v:int);
+ensures {:right} |{ A: assert dom(Stack)[i] || 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} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);
+procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:int, v:int) 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} {:layer 0,1} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);
+procedure {:yields} {:layer 0,1} TransferToStack(oldVal: int, newVal: int, {: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} {:layer 0,1} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);
+procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: int, newVal: int) 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;
+                        B: assume oldVal == TopOfStack; TopOfStack := newVal; Used[oldVal] := true; Stack := Remove(Stack, oldVal); r := true; return true;
 		        C: assume oldVal != TopOfStack; r := false; return true; }|;
 
-var {:layer 0} TopOfStack: Node;
+var {:layer 0} TopOfStack: int;
 var {:linear "Node"} {:layer 0} Stack: lmap;
 
 
-function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool)
+function {:inline} Inv(TopOfStack: int, Stack: lmap) : (bool)
 {
   BetweenSet(map(Stack), TopOfStack, null)[TopOfStack] &&
   Subset(BetweenSet(map(Stack), TopOfStack, null), Union(Singleton(null), dom(Stack)))
 }
 
-var {:linear "Node"} {:layer 0} Used: lmap;
+var {:linear "Node"} {:layer 0} Used: [int]bool;
+
+function {:inline} {:linear "Node"} NodeCollector(x: int) : [int]bool
+{
+  MapConstBool(false)[x := true]
+}
+function {:inline} {:linear "Node"} NodeSetCollector(x: [int]bool) : [int]bool
+{
+  x
+}
 
-procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)
+procedure {:yields} {:layer 1} push(x: int, {: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;
+  var t: int;
   var g: bool;
   var {:linear "Node"} t_lmap: lmap;
 
@@ -71,7 +80,6 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret
     call t_lmap := Store(t_lmap, x, t);
     call g, t_lmap := TransferToStack(t, x, t_lmap); 
     if (g) {
-      assert {:layer 1} map(Stack)[x] == t;
       break;
     }
     yield; 
@@ -82,13 +90,13 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret
   assert {:expand} {:layer 1} Inv(TopOfStack, Stack);
 }
 
-procedure {:yields} {:layer 1} pop() returns (t: Node)
+procedure {:yields} {:layer 1} pop() returns (t: int)
 requires {:layer 1} Inv(TopOfStack, Stack);
 ensures {:layer 1} Inv(TopOfStack, Stack);
-ensures {:atomic} |{ A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;
+ensures {:atomic} |{ A: assume TopOfStack != null; t := TopOfStack; Used[t] := true; TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;
 {
   var g: bool;
-  var x: Node;
+  var x: int;
 
   yield;
   assert {:layer 1} Inv(TopOfStack, Stack);
@@ -115,7 +123,6 @@ function Subset([int]bool, [int]bool) returns (bool);
 
 function Empty() returns ([int]bool);
 function Singleton(int) returns ([int]bool);
-function Reachable([int,int]bool, int) returns ([int]bool);
 function Union([int]bool, [int]bool) returns ([int]bool);
 
 axiom(forall x:int :: !Empty()[x]);
diff --git a/Test/civl/treiber-stack.bpl.expect b/Test/civl/treiber-stack.bpl.expect
index 9823d44a..76a9a2bf 100644
--- a/Test/civl/treiber-stack.bpl.expect
+++ b/Test/civl/treiber-stack.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 6 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl
index 17f53401..0a2227b6 100644
--- a/Test/civl/wsq.bpl
+++ b/Test/civl/wsq.bpl
@@ -89,13 +89,11 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
 ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|;
 {
    var t: int;
-   var {:ghost} oldH:int;
-   var {:ghost} oldT:int;
-   var {:ghost} oldStatusT:bool;
+   var {:layer 3} oldH:int;
+   var {:layer 3} oldT:int;
+   var {:layer 3} oldStatusT:bool;
    
-
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
    assert {:layer 3} {:expand} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -104,8 +102,7 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I
 
    call t := readT_put(tid);
 
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && put_in_cs;
    assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -115,9 +112,8 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I
    
    call writeItems_put(tid,t, task);
 
-   oldH := H;
-   oldT := T;
-   oldStatusT := status[T];
+   call oldH, oldT := GhostRead();
+   call oldStatusT := GhostReadStatus();
    yield;
    assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && t == T && tid == ptTid && !take_in_cs && put_in_cs;
    assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -128,8 +124,7 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I
    
    call writeT_put(tid, t+1);
 
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
    assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -147,11 +142,10 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 {
    var h, t: int;
    var chk: bool;
-   var {:ghost} oldH:int;
-   var {:ghost} oldT:int;
+   var {:layer 3} oldH:int;
+   var {:layer 3} oldT:int;
 
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
    assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -164,8 +158,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
    invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
    {
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
     assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -173,8 +166,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
     
        call t := readT_take_init(tid);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
        assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
@@ -185,8 +177,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        t := t-1;
        call writeT_take(tid, t);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !take_in_cs && !put_in_cs && t_ss[tid] == t;
        assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
@@ -196,8 +187,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
     
        call h := readH_take(tid);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs  && !put_in_cs && h_ss[tid] == h && t_ss[tid] == t;  
        assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
@@ -214,8 +204,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
            call writeT_take_abort(tid, h);
            task := EMPTY;
  
-           oldH := H;
-           oldT := T;
+           call oldH, oldT := GhostRead();
            yield;
         assert {:layer 3} h <= H;
            assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; 
@@ -227,8 +216,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 
        call task, taskstatus := readItems(tid, t);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} H >= h;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && h_ss[tid] == h && t_ss[tid] == t;  
@@ -240,8 +228,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        if(t>h) {
         call takeExitCS(tid);
 
-           oldH := H;
-           oldT := T;    
+           call oldH, oldT := GhostRead();    
            yield;
            assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && h_ss[tid] == h && t_ss[tid] == t;  
         assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -250,8 +237,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
            return;
        }
 	   call writeT_take_eq(tid, h+1);
-	   oldH := H;
-       oldT := T;
+	   call oldH, oldT := GhostRead();
 	   
 	   yield;
 	   assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;
@@ -265,8 +251,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        call chk := CAS_H_take(tid, h,h+1);
 
 
-       oldH := H;
-       oldT := T;    
+       call oldH, oldT := GhostRead();    
        yield;
 	assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == oldH -1 && task != EMPTY);
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  
@@ -279,8 +264,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 
        if(!chk) {
     
-          oldH := H;
-          oldT := T;    
+          call oldH, oldT := GhostRead();    
           yield;
           assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  
          assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -290,8 +274,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
           goto LOOP_ENTRY_1;
        }
 
-       oldH := H;
-       oldT := T;    
+       call oldH, oldT := GhostRead();    
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  
     assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -301,8 +284,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        return;
    }
    
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !put_in_cs;
    assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -322,11 +304,10 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 {
    var h, t: int;
    var chk: bool;
-   var {:ghost} oldH:int;
-   var {:ghost} oldT:int;
+   var {:layer 3} oldH:int;
+   var {:layer 3} oldT:int;
 
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} stealerTid(tid);
    assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
@@ -341,8 +322,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
    invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
    invariant {:layer 3} !steal_in_cs[tid];
    {
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} stealerTid(tid);
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
@@ -352,8 +332,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
     
        call h := readH_steal(tid);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} H >= h;
     assert {:layer 3} !steal_in_cs[tid];
@@ -365,8 +344,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        call t := readT_steal(tid);
 
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} steal_in_cs[tid];
     assert {:layer 3} stealerTid(tid) && H >= h && steal_in_cs[tid] && h_ss[tid] == h;
@@ -381,8 +359,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
            task := EMPTY;
         call stealExitCS(tid);
 
-           oldH := H;
-           oldT := T;
+        call oldH, oldT := GhostRead();
            yield;
         assert {:layer 3} !steal_in_cs[tid];
         assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid] && h_ss[tid] == h;
@@ -395,8 +372,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        call task, taskstatus := readItems(tid, h);
 
 
-       oldH := H;
-       oldT := T;
+    call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} stealerTid(tid) && steal_in_cs[tid] && h_ss[tid] == h;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
@@ -408,8 +384,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 
        call chk := CAS_H_steal(tid, h,h+1);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} h_ss[tid] == h;
     assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == h && task != EMPTY && taskstatus == IN_Q);
@@ -423,8 +398,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
           goto LOOP_ENTRY_2;
        }
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
@@ -433,14 +407,24 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        return;
    }
    
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} chk && task != EMPTY;
    assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];
    assert {:layer 3} oldH <= H;
 }
 
+procedure {:layer 3} {:inline 1} GhostRead() returns (oldH: int, oldT: int)
+{
+   oldH := H;
+   oldT := T;
+}
+
+procedure {:layer 3} {:inline 1} GhostReadStatus() returns (oldStatus: bool)
+{
+   oldStatus := status[T];
+}
+
 procedure {:yields}{:layer 0,3} readH_take({:linear "tid"} tid:Tid) returns (y: int);
 ensures {:atomic} |{A:  assert tid == ptTid;
                        y := H;
diff --git a/Test/civl/wsq.bpl.expect b/Test/civl/wsq.bpl.expect
index a9949f2e..9823d44a 100644
--- a/Test/civl/wsq.bpl.expect
+++ b/Test/civl/wsq.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/commandline/multiple_procs_unusual_identifiers.bpl b/Test/commandline/multiple_procs_unusual_identifiers.bpl
new file mode 100644
index 00000000..a3a4a4c1
--- /dev/null
+++ b/Test/commandline/multiple_procs_unusual_identifiers.bpl
@@ -0,0 +1,75 @@
+// RUN: %boogie "-proc:*Bar*" "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 10 verified, 0 errors
+
+procedure foo()
+{
+    assert false;
+}
+
+procedure bar()
+{
+    assert false;
+}
+
+/* Start should be matched */
+
+procedure _Bar()
+{
+    assert true;
+}
+
+procedure .Bar()
+{
+    assert true;
+}
+
+procedure ..Bar..()
+{
+    assert true;
+}
+
+procedure $Bar()
+{
+    assert true;
+}
+
+procedure #Bar()
+{
+    assert true;
+}
+
+procedure 'Bar''()
+{
+    assert true;
+}
+
+procedure ``Bar``()
+{
+    assert true;
+}
+
+procedure ~Bar()
+{
+    assert true;
+}
+
+procedure Bar^^()
+{
+    assert true;
+}
+
+/* This is Boogie2 claims backslash is a valid identifier
+   but the parser rejects this.
+procedure Bar\\()
+{
+    assert true;
+}
+*/
+
+procedure ??Bar()
+{
+    assert true;
+}
+
+/* End should be matched */
diff --git a/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl b/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl
new file mode 100644
index 00000000..e0f8eef3
--- /dev/null
+++ b/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl
@@ -0,0 +1,28 @@
+// RUN: %boogie "-proc:*Bar" "-proc:*Foo" "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 4 verified, 0 errors
+
+procedure foo()
+{
+    assert false;
+}
+
+procedure helpfulFoo()
+{
+    assert true;
+}
+
+procedure Foo()
+{
+    assert true;
+}
+
+procedure translucentBar()
+{
+    assert true;
+}
+
+procedure opaqueBar()
+{
+    assert true;
+}
diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl
new file mode 100644
index 00000000..0f6571ba
--- /dev/null
+++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl
@@ -0,0 +1,17 @@
+// RUN: %boogie "-proc:*Bar" "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors
+procedure foo()
+{
+    assert false;
+}
+
+procedure translucentBar()
+{
+    assert true;
+}
+
+procedure opaqueBar()
+{
+    assert true;
+}
diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl
new file mode 100644
index 00000000..5cb102e2
--- /dev/null
+++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl
@@ -0,0 +1,17 @@
+// RUN: %boogie "-proc:bar*" "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors
+procedure foo()
+{
+    assert false;
+}
+
+procedure bar()
+{
+    assert true;
+}
+
+procedure barzzz()
+{
+    assert true;
+}
diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl
new file mode 100644
index 00000000..7e19fe79
--- /dev/null
+++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl
@@ -0,0 +1,23 @@
+// RUN: %boogie "-proc:trivial*ZZZ" "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors
+procedure foo()
+{
+    assert false;
+}
+
+// should not be matched
+procedure trivialFooZZX()
+{
+    assert false;
+}
+
+procedure trivialFooZZZ()
+{
+    assert true;
+}
+
+procedure trivialBarZZZ()
+{
+    assert true;
+}
diff --git a/Test/extractloops/detLoopExtract2.bpl b/Test/extractloops/detLoopExtract2.bpl
new file mode 100644
index 00000000..f2befc53
--- /dev/null
+++ b/Test/extractloops/detLoopExtract2.bpl
@@ -0,0 +1,27 @@
+// RUN: %boogie -nologo -nologo -stratifiedInline:1 -extractLoops -deterministicExtractLoops -recursionBound:6  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+//This example checks the bug fix in the loop extract for http://symdiff.codeplex.com/workitem/4
+procedure {:entrypoint} Main() returns(r:int)
+{ 
+  var i, j : int;
+  var Flag : bool;
+  var b : bool;
+  i := 0;
+  j := 0;
+  Flag := false;
+  while(i<3)
+  {
+    havoc b;
+    if (b || Flag) {
+      i := i + 1;
+      j := j + 1; 
+    }
+    else {
+     Flag := true;
+     j := j + 1;
+    }
+  }
+  assume !(i == j || i == j - 1);
+  return;
+}
diff --git a/Test/extractloops/detLoopExtract2.bpl.expect b/Test/extractloops/detLoopExtract2.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/extractloops/detLoopExtract2.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/extractloops/detLoopExtractNested.bpl b/Test/extractloops/detLoopExtractNested.bpl
new file mode 100644
index 00000000..65de20c1
--- /dev/null
+++ b/Test/extractloops/detLoopExtractNested.bpl
@@ -0,0 +1,23 @@
+// RUN: %boogie  -nologo -stratifiedInline:1 -extractLoops -deterministicExtractLoops -recursionBound:100  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+//This example checks the bug fix in the loop extract for http://symdiff.codeplex.com/workitem/1
+
+var t: int;
+procedure {:entrypoint} NestedLoops()
+modifies t;
+//ensures t == 6;
+{
+   var i:int, j:int;
+   i, j, t := 0, 0, 0;
+   while(i < 2) {
+     j := 0;
+     while (j < 3) {
+       t := t + 1;
+       j := j + 1;
+     }
+     i := i + 1;
+   }
+   assume true; //would be provable (!true) wihtout the fix
+}
+
diff --git a/Test/extractloops/detLoopExtractNested.bpl.expect b/Test/extractloops/detLoopExtractNested.bpl.expect
new file mode 100644
index 00000000..f4932ede
--- /dev/null
+++ b/Test/extractloops/detLoopExtractNested.bpl.expect
@@ -0,0 +1,19 @@
+(0,0): Error BP5001: This assertion might not hold.
+Execution trace:
+    detLoopExtractNested.bpl(12,12): anon0
+    detLoopExtractNested.bpl(14,8): anon5_LoopBody
+    detLoopExtractNested.bpl(16,10): anon6_LoopBody
+    detLoopExtractNested.bpl(16,10): anon6_LoopBody
+    detLoopExtractNested.bpl(16,10): anon6_LoopBody
+    detLoopExtractNested.bpl(15,6): anon6_LoopDone
+    detLoopExtractNested.bpl(15,6): anon6_LoopDone
+    detLoopExtractNested.bpl(14,8): anon5_LoopBody
+    detLoopExtractNested.bpl(16,10): anon6_LoopBody
+    detLoopExtractNested.bpl(16,10): anon6_LoopBody
+    detLoopExtractNested.bpl(16,10): anon6_LoopBody
+    detLoopExtractNested.bpl(15,6): anon6_LoopDone
+    detLoopExtractNested.bpl(15,6): anon6_LoopDone
+    detLoopExtractNested.bpl(13,4): anon5_LoopDone
+    detLoopExtractNested.bpl(13,4): anon5_LoopDone
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index b4f784d3..c3c294c9 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -89,11 +89,14 @@ modifies g;
 
 procedure {:yields} {:layer 0} I({:linear_in ""} x:int) returns({:linear ""} x':int)
 {
+  yield;
   x' := x;
+  yield;
 }
 
 procedure {:yields} {:layer 0} J()
 {
+  yield;
 }
 
 procedure {:yields} {:layer 1} P1({:linear_in ""} x:int) returns({:linear ""} x':int)
diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect
index 9f960f26..3c0d0b20 100644
--- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect
+++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect
@@ -127,7 +127,8 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(3832,3): inline$storm_IoCancelIrp$0$anon10#2
     daytona_bug2_ioctl_example_2.bpl(3892,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#2
     daytona_bug2_ioctl_example_2.bpl(3902,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Else#2
-    daytona_bug2_ioctl_example_2.bpl(3928,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Then#2
+    daytona_bug2_ioctl_example_2.bpl(3915,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Else#2
+    daytona_bug2_ioctl_example_2.bpl(3923,3): inline$storm_IoAcquireCancelSpinLock$0$anon10_Then#2
     daytona_bug2_ioctl_example_2.bpl(3933,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2
     daytona_bug2_ioctl_example_2.bpl(3944,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2
     daytona_bug2_ioctl_example_2.bpl(3949,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2
diff --git a/Test/optimization/Optimization0.bpl b/Test/optimization/Optimization0.bpl
new file mode 100644
index 00000000..24424e53
--- /dev/null
+++ b/Test/optimization/Optimization0.bpl
@@ -0,0 +1,84 @@
+// RUN: %boogie /printModel:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function may_fail(f: int) : bool;
+
+procedure test0()
+{
+    var x: int;
+
+    havoc x;
+    assume 42 < x;
+    assume {:minimize x} true;
+    assert may_fail(x);
+}
+
+procedure test1()
+{
+    var x: int;
+
+    x := 24;
+    if (*) {
+        x := 42;
+    }
+    assume {:minimize x} true;
+    assert may_fail(x);
+}
+
+procedure test2()
+{
+    var x: int;
+
+    x := 1;
+    while (*) {
+        x := x + 1;
+    }
+    assume {:minimize x} true;
+    assert x < 10;
+}
+
+procedure test3()
+{
+    var x: int;
+
+    havoc x;
+    assume x < 42;
+    assume {:maximize x} true;
+    assert may_fail(x);
+}
+
+procedure test4()
+{
+    var x: int;
+
+    x := 24;
+    if (*) {
+        x := 42;
+    }
+    assume {:maximize x} true;
+    assert may_fail(x);
+}
+
+procedure test5()
+{
+    var x: int;
+
+    x := 1;
+    while (*) {
+        x := x - 1;
+    }
+    assume {:maximize x} true;
+    assert x < 1;
+}
+
+procedure test6()
+{
+    var x: int;
+
+    x := 1;
+    if (*) {
+        x := 2;
+    }
+    assume {:maximize x} true;
+    assert may_fail(x);
+}
diff --git a/Test/optimization/Optimization0.bpl.expect b/Test/optimization/Optimization0.bpl.expect
new file mode 100644
index 00000000..f5a51848
--- /dev/null
+++ b/Test/optimization/Optimization0.bpl.expect
@@ -0,0 +1,135 @@
+*** MODEL
+%lbl%@280 -> false
+%lbl%+260 -> true
+%lbl%+39 -> true
+x@0 -> 43
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  43 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(13,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(10,5): anon0
+*** MODEL
+%lbl%@321 -> false
+%lbl%+299 -> true
+%lbl%+66 -> true
+%lbl%+68 -> true
+x@0@@0 -> 24
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  24 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(25,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(20,7): anon0
+    Optimization0.bpl(21,5): anon3_Else
+    Optimization0.bpl(24,5): anon2
+*** MODEL
+%lbl%@353 -> false
+%lbl%+335 -> true
+%lbl%+95 -> true
+%lbl%+99 -> true
+x@0@@1 -> 10
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+*** END_MODEL
+Optimization0.bpl(37,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(32,7): anon0
+    Optimization0.bpl(33,5): anon3_LoopHead
+    Optimization0.bpl(33,5): anon3_LoopDone
+*** MODEL
+%lbl%@386 -> false
+%lbl%+122 -> true
+%lbl%+375 -> true
+x@0@@2 -> 41
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  41 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(47,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(44,5): anon0
+*** MODEL
+%lbl%@414 -> false
+%lbl%+147 -> true
+%lbl%+151 -> true
+%lbl%+392 -> true
+x@0@@3 -> 42
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  42 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(59,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(54,7): anon0
+    Optimization0.bpl(56,11): anon3_Then
+    Optimization0.bpl(58,5): anon2
+*** MODEL
+%lbl%@446 -> false
+%lbl%+178 -> true
+%lbl%+182 -> true
+%lbl%+428 -> true
+x@0@@4 -> 1
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+*** END_MODEL
+Optimization0.bpl(71,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(66,7): anon0
+    Optimization0.bpl(67,5): anon3_LoopHead
+    Optimization0.bpl(67,5): anon3_LoopDone
+*** MODEL
+%lbl%@490 -> false
+%lbl%+209 -> true
+%lbl%+213 -> true
+%lbl%+468 -> true
+x@0@@5 -> 2
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  2 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(83,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(78,7): anon0
+    Optimization0.bpl(80,11): anon3_Then
+    Optimization0.bpl(82,5): anon2
+
+Boogie program verifier finished with 0 verified, 7 errors
diff --git a/Test/optimization/Optimization1.bpl b/Test/optimization/Optimization1.bpl
new file mode 100644
index 00000000..60df1edd
--- /dev/null
+++ b/Test/optimization/Optimization1.bpl
@@ -0,0 +1,32 @@
+// RUN: %boogie /noVerify /printModel:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0(n: int)
+{
+    assume {:minimize} true;
+}
+
+procedure test1(n: int)
+{
+    assume {:maximize} true;
+}
+
+procedure test2(n: int)
+{
+    assume {:minimize n, n} true;
+}
+
+procedure test3(n: int)
+{
+    assume {:maximize n, n} true;
+}
+
+procedure test4(n: int)
+{
+    assume {:minimize true} true;
+}
+
+procedure test5(n: int)
+{
+    assume {:maximize true} true;
+}
diff --git a/Test/optimization/Optimization1.bpl.expect b/Test/optimization/Optimization1.bpl.expect
new file mode 100644
index 00000000..d8508807
--- /dev/null
+++ b/Test/optimization/Optimization1.bpl.expect
@@ -0,0 +1,5 @@
+Optimization1.bpl(6,11): Error: attributes :minimize and :maximize accept only one argument
+Optimization1.bpl(11,11): Error: attributes :minimize and :maximize accept only one argument
+Optimization1.bpl(16,11): Error: attributes :minimize and :maximize accept only one argument
+Optimization1.bpl(21,11): Error: attributes :minimize and :maximize accept only one argument
+4 name resolution errors detected in Optimization1.bpl
diff --git a/Test/optimization/Optimization2.bpl b/Test/optimization/Optimization2.bpl
new file mode 100644
index 00000000..7d80d735
--- /dev/null
+++ b/Test/optimization/Optimization2.bpl
@@ -0,0 +1,12 @@
+// RUN: %boogie /noVerify /printModel:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0(n: int)
+{
+    assume {:minimize true} true;
+}
+
+procedure test1(n: int)
+{
+    assume {:maximize true} true;
+}
diff --git a/Test/optimization/Optimization2.bpl.expect b/Test/optimization/Optimization2.bpl.expect
new file mode 100644
index 00000000..cab2fd3d
--- /dev/null
+++ b/Test/optimization/Optimization2.bpl.expect
@@ -0,0 +1,3 @@
+Optimization2.bpl(6,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv
+Optimization2.bpl(11,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv
+2 type checking errors detected in Optimization2.bpl
diff --git a/Test/optimization/Optimization3.bpl b/Test/optimization/Optimization3.bpl
new file mode 100644
index 00000000..02499c31
--- /dev/null
+++ b/Test/optimization/Optimization3.bpl
@@ -0,0 +1,20 @@
+// RUN: %boogie /printModel:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0()
+{
+    var x: int;
+
+    assume x < 42;
+    assume {:maximize x} true;
+    assert (exists y: int :: y < x);
+}
+
+procedure test1()
+{
+    var x: int;
+
+    assume x < 42;
+    assume {:maximize x} true;
+    assert (forall y: int :: y < x);
+}
diff --git a/Test/optimization/Optimization3.bpl.expect b/Test/optimization/Optimization3.bpl.expect
new file mode 100644
index 00000000..6a0066fc
--- /dev/null
+++ b/Test/optimization/Optimization3.bpl.expect
@@ -0,0 +1,31 @@
+*** MODEL
+%lbl%@80 -> false
+%lbl%+33 -> true
+%lbl%+61 -> true
+x -> 41
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+*** END_MODEL
+Optimization3.bpl(10,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization3.bpl(8,5): anon0
+*** MODEL
+%lbl%@115 -> false
+%lbl%+105 -> true
+%lbl%+56 -> true
+x@@0 -> 41
+y@@0!1!1 -> 719
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+*** END_MODEL
+Optimization3.bpl(19,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization3.bpl(17,5): anon0
+
+Boogie program verifier finished with 0 verified, 2 errors
diff --git a/Test/optimization/lit.local.cfg b/Test/optimization/lit.local.cfg
new file mode 100644
index 00000000..35c7e558
--- /dev/null
+++ b/Test/optimization/lit.local.cfg
@@ -0,0 +1,3 @@
+# Do not run tests in this directory and below
+config.unsupported = True
+# TODO(wuestholz): Enable these tests once we can rely on a version of Z3 that includes changeset 5948013b1b04d8529bce366c0c7b87e1d88a1827.
diff --git a/Test/snapshots/Snapshots38.v0.bpl b/Test/snapshots/Snapshots38.v0.bpl
new file mode 100644
index 00000000..496a75a9
--- /dev/null
+++ b/Test/snapshots/Snapshots38.v0.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "-1"} Callee();
+
+implementation {:id "Callee"} {:checksum "0"} Callee()
+{
+    var r: int;
+
+    call r := Sum(42);
+    assert r != 0;
+}
+
+procedure {:checksum "1"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n != 0 ==> 1 <= r;
diff --git a/Test/snapshots/Snapshots38.v1.bpl b/Test/snapshots/Snapshots38.v1.bpl
new file mode 100644
index 00000000..062b22ea
--- /dev/null
+++ b/Test/snapshots/Snapshots38.v1.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "-1"} Callee();
+
+implementation {:id "Callee"} {:checksum "2"} Callee()
+{
+    var r: int;
+
+    call r := Sum(42);
+    assert r != 0;
+    assert 42 <= r;
+}
+
+procedure {:checksum "1"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n != 0 ==> 1 <= r;
diff --git a/Test/snapshots/Snapshots38.v2.bpl b/Test/snapshots/Snapshots38.v2.bpl
new file mode 100644
index 00000000..5c4b69d6
--- /dev/null
+++ b/Test/snapshots/Snapshots38.v2.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "-1"} Callee();
+
+implementation {:id "Callee"} {:checksum "2"} Callee()
+{
+    var r: int;
+
+    call r := Sum(42);
+    assert r != 0;
+    assert 42 <= r;
+}
+
+procedure {:checksum "3"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n != 0 ==> n <= r;
diff --git a/Test/snapshots/Snapshots39.v0.bpl b/Test/snapshots/Snapshots39.v0.bpl
new file mode 100644
index 00000000..083d497e
--- /dev/null
+++ b/Test/snapshots/Snapshots39.v0.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "-1"} Callee();
+
+implementation {:id "Callee"} {:checksum "0"} Callee()
+{
+    var r: int;
+
+    call r := Sum(42);
+    assert r != 0;
+}
+
+procedure {:checksum "1"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n <= r;
diff --git a/Test/snapshots/Snapshots39.v1.bpl b/Test/snapshots/Snapshots39.v1.bpl
new file mode 100644
index 00000000..09850bfc
--- /dev/null
+++ b/Test/snapshots/Snapshots39.v1.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "-1"} Callee();
+
+implementation {:id "Callee"} {:checksum "2"} Callee()
+{
+    var r: int;
+
+    call r := Sum(42);
+    assert r != 0;
+    assert r == (42 * 43) div 2;
+}
+
+procedure {:checksum "1"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n <= r;
diff --git a/Test/snapshots/Snapshots39.v2.bpl b/Test/snapshots/Snapshots39.v2.bpl
new file mode 100644
index 00000000..4bdc4b6e
--- /dev/null
+++ b/Test/snapshots/Snapshots39.v2.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "-1"} Callee();
+
+implementation {:id "Callee"} {:checksum "2"} Callee()
+{
+    var r: int;
+
+    call r := Sum(42);
+    assert r != 0;
+    assert r == (42 * 43) div 2;
+}
+
+procedure {:checksum "3"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures r == (n * (n + 1)) div 2;
diff --git a/Test/snapshots/Snapshots40.v0.bpl b/Test/snapshots/Snapshots40.v0.bpl
new file mode 100644
index 00000000..27839752
--- /dev/null
+++ b/Test/snapshots/Snapshots40.v0.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "-1"} Foo(b: bool);
+
+implementation {:id "Foo"} {:checksum "0"} Foo(b: bool)
+{
+    var r: int;
+
+    assert b;
+    call r := Sum(42);
+    assert r != 0;
+}
+
+procedure {:checksum "1"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n <= r;
diff --git a/Test/snapshots/Snapshots40.v1.bpl b/Test/snapshots/Snapshots40.v1.bpl
new file mode 100644
index 00000000..e1c505f8
--- /dev/null
+++ b/Test/snapshots/Snapshots40.v1.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "-1"} Foo(b: bool);
+
+implementation {:id "Foo"} {:checksum "2"} Foo(b: bool)
+{
+    var r: int;
+
+    assert b;
+    call r := Sum(42);
+    assert r != 0;
+    assert r == (42 * 43) div 2;
+}
+
+procedure {:checksum "1"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n <= r;
diff --git a/Test/snapshots/Snapshots40.v2.bpl b/Test/snapshots/Snapshots40.v2.bpl
new file mode 100644
index 00000000..842d33f5
--- /dev/null
+++ b/Test/snapshots/Snapshots40.v2.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "-1"} Foo(b: bool);
+
+implementation {:id "Foo"} {:checksum "2"} Foo(b: bool)
+{
+    var r: int;
+
+    assert b;
+    call r := Sum(42);
+    assert r != 0;
+    assert r == (42 * 43) div 2;
+}
+
+procedure {:checksum "3"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures r == (n * (n + 1)) div 2;
diff --git a/Test/snapshots/Snapshots41.v0.bpl b/Test/snapshots/Snapshots41.v0.bpl
new file mode 100644
index 00000000..dbfe3e2d
--- /dev/null
+++ b/Test/snapshots/Snapshots41.v0.bpl
@@ -0,0 +1,35 @@
+procedure {:checksum "0"} M(x: int);
+implementation {:id "M"} {:checksum "1"} M(x: int)
+{                     assert x < 20 || 10 <= x;  // always true
+  assert x < 10;  // error
+  call Other(x);  // error: precondition violation
+}
+
+procedure {:checksum "10"} Other(y: int);
+  requires 0 <= y;
+implementation {:id "Other"} {:checksum "11"} Other(y: int)
+{
+}
+
+procedure {:checksum "20"} Posty() returns (z: int);
+  ensures 2 <= z;  // error: postcondition violation
+implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
+{
+  var t: int;
+  t := 20;
+  if (t < z) {
+  } else {  // the postcondition violation occurs on this 'else' branch
+  }
+}
+
+procedure {:checksum "30"} NoChangeWhazzoeva(u: int);
+implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
+{
+  assert u != 53;  // error
+}
+
+procedure {:checksum "40"} NoChangeAndCorrect();
+implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect()
+{
+  assert true;
+}
diff --git a/Test/snapshots/Snapshots41.v1.bpl b/Test/snapshots/Snapshots41.v1.bpl
new file mode 100644
index 00000000..9864e0e4
--- /dev/null
+++ b/Test/snapshots/Snapshots41.v1.bpl
@@ -0,0 +1,39 @@
+procedure {:checksum "0"} M(x: int);
+implementation {:id "M"} {:checksum "1"} M(x: int)
+{
+assert x < 20 || 10 <= x;  // always true
+  
+       assert x < 10;  // error
+  call Other(x);  // error: precondition violation
+  assert x == 7;  // error: this is a new error in v1
+}
+
+
+       procedure {:checksum "10"} Other(y: int);
+         requires 0 <= y;
+       implementation {:id "Other"} {:checksum "11"} Other(y: int)
+       {
+       }
+
+
+
+procedure {:checksum "20"} Posty() returns (z: int);
+  ensures 2 <= z;  // error: postcondition violation
+implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
+{
+  var t: int;
+  t := 20;
+  if (t < z) {
+    assert true;  // this is a new assert
+  } else {  // the postcondition violation occurs on this 'else' branch
+  }
+}
+
+  procedure   {:checksum "30"} NoChangeWhazzoeva(u: int);
+  implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
+  {
+       assert u != 53;  // error
+  }
+
+procedure {:checksum "40"} NoChangeAndCorrect();
+implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() { assert true; }
diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index d4e18910..1d6e7c95 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,3 @@
-// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl Snapshots36.bpl Snapshots37.bpl > "%t"
+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl Snapshots36.bpl Snapshots37.bpl Snapshots38.bpl Snapshots39.bpl Snapshots40.bpl > "%t"
+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:3 -verifySeparately -noinfer Snapshots41.bpl >> "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 4ef6bd20..393c9330 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -666,3 +666,145 @@ Processing command (at Snapshots37.v1.bpl(8,5)) assert l[0];
 Snapshots37.v1.bpl(8,5): Error BP5001: This assertion might not hold.
 
 Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots38.v0.bpl(7,5)) assert 0 <= call0formal#AT#n;
+  >>> DoNothingToAssert
+Processing command (at Snapshots38.v0.bpl(8,5)) assert r != 0;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots38.v1.bpl(7,5)) assert 0 <= call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v1.bpl(8,5)) assert r != 0;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v1.bpl(9,5)) assert 42 <= r;
+  >>> DoNothingToAssert
+Snapshots38.v1.bpl(9,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure Sum in implementation Callee (at Snapshots38.v2.bpl(7,5)):
+  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n))
+  >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n != 0 ==> 1 <= call1formal#AT#r))
+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r);
+Processing command (at Snapshots38.v2.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v2.bpl(7,5)) assert 0 <= call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v2.bpl(8,5)) assert r != 0;
+  >>> MarkAsPartiallyVerified
+Processing command (at Snapshots38.v2.bpl(9,5)) assert 42 <= r;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots39.v0.bpl(7,5)) assert 0 <= call0formal#AT#n;
+  >>> DoNothingToAssert
+Processing command (at Snapshots39.v0.bpl(8,5)) assert r != 0;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots39.v1.bpl(7,5)) assert 0 <= call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v1.bpl(8,5)) assert r != 0;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v1.bpl(9,5)) assert r == 42 * 43 div 2;
+  >>> DoNothingToAssert
+Snapshots39.v1.bpl(9,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure Sum in implementation Callee (at Snapshots39.v2.bpl(7,5)):
+  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n))
+  >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n <= call1formal#AT#r))
+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r);
+Processing command (at Snapshots39.v2.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v2.bpl(7,5)) assert 0 <= call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v2.bpl(8,5)) assert r != 0;
+  >>> MarkAsPartiallyVerified
+Processing command (at Snapshots39.v2.bpl(9,5)) assert r == 42 * 43 div 2;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots40.v0.bpl(7,5)) assert b;
+  >>> DoNothingToAssert
+Processing command (at Snapshots40.v0.bpl(8,5)) assert 0 <= call0formal#AT#n;
+  >>> DoNothingToAssert
+Processing command (at Snapshots40.v0.bpl(9,5)) assert r != 0;
+  >>> DoNothingToAssert
+Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots40.v1.bpl(7,5)) assert b;
+  >>> RecycleError
+Processing command (at Snapshots40.v1.bpl(8,5)) assert 0 <= call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v1.bpl(9,5)) assert r != 0;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v1.bpl(10,5)) assert r == 42 * 43 div 2;
+  >>> DoNothingToAssert
+Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold.
+Snapshots40.v1.bpl(10,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing call to procedure Sum in implementation Foo (at Snapshots40.v2.bpl(8,5)):
+  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n))
+  >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n <= call1formal#AT#r))
+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r);
+Processing command (at Snapshots40.v2.bpl(7,5)) assert b;
+  >>> RecycleError
+Processing command (at Snapshots40.v2.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v2.bpl(8,5)) assert 0 <= call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v2.bpl(9,5)) assert r != 0;
+  >>> MarkAsPartiallyVerified
+Processing command (at Snapshots40.v2.bpl(10,5)) assert r == 42 * 43 div 2;
+  >>> DoNothingToAssert
+Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots41.v0.bpl(3,23)) assert x < 20 || 10 <= x;
+  >>> DoNothingToAssert
+Processing command (at Snapshots41.v0.bpl(4,3)) assert x < 10;
+  >>> DoNothingToAssert
+Processing command (at Snapshots41.v0.bpl(5,3)) assert 0 <= call0formal#AT#y;
+  >>> DoNothingToAssert
+Snapshots41.v0.bpl(4,3): Error BP5001: This assertion might not hold.
+Snapshots41.v0.bpl(5,3): Error BP5002: A precondition for this call might not hold.
+Snapshots41.v0.bpl(9,3): Related location: This is the precondition that might not hold.
+Processing command (at Snapshots41.v0.bpl(15,3)) assert 2 <= z;
+  >>> DoNothingToAssert
+Snapshots41.v0.bpl(22,3): Error BP5003: A postcondition might not hold on this return path.
+Snapshots41.v0.bpl(15,3): Related location: This is the postcondition that might not hold.
+Processing command (at Snapshots41.v0.bpl(28,3)) assert u != 53;
+  >>> DoNothingToAssert
+Snapshots41.v0.bpl(28,3): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots41.v0.bpl(34,3)) assert true;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 2 verified, 4 errors
+Processing command (at Snapshots41.v1.bpl(4,1)) assert x < 20 || 10 <= x;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots41.v1.bpl(6,8)) assert x < 10;
+  >>> RecycleError
+Processing command (at Snapshots41.v1.bpl(7,3)) assert 0 <= call0formal#AT#y;
+  >>> RecycleError
+Processing command (at Snapshots41.v1.bpl(8,3)) assert x == 7;
+  >>> DoNothingToAssert
+Snapshots41.v1.bpl(6,8): Error BP5001: This assertion might not hold.
+Snapshots41.v1.bpl(7,3): Error BP5002: A precondition for this call might not hold.
+Snapshots41.v1.bpl(13,10): Related location: This is the precondition that might not hold.
+Snapshots41.v1.bpl(8,3): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots41.v1.bpl(27,5)) assert true;
+  >>> DoNothingToAssert
+Processing command (at Snapshots41.v1.bpl(21,3)) assert 2 <= z;
+  >>> DoNothingToAssert
+Snapshots41.v1.bpl(29,3): Error BP5003: A postcondition might not hold on this return path.
+Snapshots41.v1.bpl(21,3): Related location: This is the postcondition that might not hold.
+Processing command (at Snapshots41.v1.bpl(35,8)) assert u != 53;
+  >>> RecycleError
+Snapshots41.v1.bpl(35,8): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 2 verified, 5 errors
diff --git a/Test/test0/AssertVerifiedUnder0.bpl b/Test/test0/AssertVerifiedUnder0.bpl
new file mode 100644
index 00000000..1b054f68
--- /dev/null
+++ b/Test/test0/AssertVerifiedUnder0.bpl
@@ -0,0 +1,8 @@
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0()
+{
+    assert {:verified_under} true;
+    assert {:verified_under true, false} true;
+}
diff --git a/Test/test0/AssertVerifiedUnder0.bpl.expect b/Test/test0/AssertVerifiedUnder0.bpl.expect
new file mode 100644
index 00000000..b3d8177d
--- /dev/null
+++ b/Test/test0/AssertVerifiedUnder0.bpl.expect
@@ -0,0 +1,3 @@
+AssertVerifiedUnder0.bpl(6,11): Error: attribute :verified_under accepts only one argument
+AssertVerifiedUnder0.bpl(7,11): Error: attribute :verified_under accepts only one argument
+2 name resolution errors detected in AssertVerifiedUnder0.bpl
diff --git a/Test/test1/AssertVerifiedUnder0.bpl b/Test/test1/AssertVerifiedUnder0.bpl
new file mode 100644
index 00000000..e419a5ef
--- /dev/null
+++ b/Test/test1/AssertVerifiedUnder0.bpl
@@ -0,0 +1,8 @@
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0()
+{
+    assert {:verified_under 4} true;
+    assert {:verified_under 3.0} true;
+}
diff --git a/Test/test1/AssertVerifiedUnder0.bpl.expect b/Test/test1/AssertVerifiedUnder0.bpl.expect
new file mode 100644
index 00000000..6d3c04cd
--- /dev/null
+++ b/Test/test1/AssertVerifiedUnder0.bpl.expect
@@ -0,0 +1,3 @@
+AssertVerifiedUnder0.bpl(6,11): Error: attribute :verified_under accepts only one argument of type bool
+AssertVerifiedUnder0.bpl(7,11): Error: attribute :verified_under accepts only one argument of type bool
+2 type checking errors detected in AssertVerifiedUnder0.bpl
diff --git a/Test/test1/StatementIds0.bpl b/Test/test1/StatementIds0.bpl
new file mode 100644
index 00000000..abf26159
--- /dev/null
+++ b/Test/test1/StatementIds0.bpl
@@ -0,0 +1,24 @@
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0(n: int)
+{
+    assume {:id "s0"} true;
+    assert {:id "s0"} true;
+}
+
+procedure test1()
+{
+    call {:id "s0"} P();
+}
+
+procedure test2(n: int)
+{
+    while (*)
+      invariant {:id "s0"} true;
+      invariant {:id "s0"} true;
+    {
+    }
+}
+
+procedure P();
diff --git a/Test/test1/StatementIds0.bpl.expect b/Test/test1/StatementIds0.bpl.expect
new file mode 100644
index 00000000..4783d912
--- /dev/null
+++ b/Test/test1/StatementIds0.bpl.expect
@@ -0,0 +1,5 @@
+StatementIds0.bpl(7,4): Error: more than one statement with same id: s0
+StatementIds0.bpl(12,4): Error: more than one statement with same id: s0
+StatementIds0.bpl(18,6): Error: more than one statement with same id: s0
+StatementIds0.bpl(19,6): Error: more than one statement with same id: s0
+4 name resolution errors detected in StatementIds0.bpl
diff --git a/Test/test15/CaptureState.bpl.expect b/Test/test15/CaptureState.bpl.expect
index 5d9d41c5..6939fee4 100644
--- a/Test/test15/CaptureState.bpl.expect
+++ b/Test/test15/CaptureState.bpl.expect
@@ -14,17 +14,17 @@ $mv_state_const -> 3
 F -> T@FieldName!val!0
 Heap -> |T@[Ref,FieldName]Int!val!0|
 m -> **m
-m@0 -> (- 276)
-m@1 -> (- 275)
-m@3 -> (- 275)
+m@0 -> (- 2)
+m@1 -> (- 1)
+m@3 -> (- 1)
 r -> **r
-r@0 -> (- 550)
+r@0 -> (- 2)
 this -> T@Ref!val!0
 x -> 719
 y -> **y
 Select_[Ref,FieldName]$int -> {
-  |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 276)
-  else -> (- 276)
+  |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 2)
+  else -> (- 2)
 }
 $mv_state -> {
   3 0 -> true
@@ -49,13 +49,13 @@ tickleBool -> {
 *** STATE top
 *** END_STATE
 *** STATE then
-  m -> (- 276)
+  m -> (- 2)
 *** END_STATE
 *** STATE postUpdate0
-  m -> (- 275)
+  m -> (- 1)
 *** END_STATE
 *** STATE end
-  r -> (- 550)
+  r -> (- 2)
   m -> 7
 *** END_STATE
 *** END_MODEL
diff --git a/Test/test2/BadLineNumber.bpl b/Test/test2/BadLineNumber.bpl
new file mode 100644
index 00000000..b8776a4e
--- /dev/null
+++ b/Test/test2/BadLineNumber.bpl
@@ -0,0 +1,15 @@
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure p();
+  ensures false;
+
+implementation p()
+{
+    if (*)
+    {
+    }
+    else
+    {
+    }
+}
\ No newline at end of file
diff --git a/Test/test2/BadLineNumber.bpl.expect b/Test/test2/BadLineNumber.bpl.expect
new file mode 100644
index 00000000..bc5d1984
--- /dev/null
+++ b/Test/test2/BadLineNumber.bpl.expect
@@ -0,0 +1,7 @@
+BadLineNumber.bpl(15,1): Error BP5003: A postcondition might not hold on this return path.
+BadLineNumber.bpl(5,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    BadLineNumber.bpl(9,5): anon0
+    BadLineNumber.bpl(14,5): anon3_Else
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test2/BoundedTypeParameterQuantifier.bpl b/Test/test2/BoundedTypeParameterQuantifier.bpl
new file mode 100644
index 00000000..146ba445
--- /dev/null
+++ b/Test/test2/BoundedTypeParameterQuantifier.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie /proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function Map#Domain<QUN, YAN>(Map QUN YAN): [QUN] bool;
+function Map#Empty<QUN, YAN>(): Map QUN YAN;
+type Map QUN YAN;
+
+axiom (forall<QUN, YAN> u: QUN ::
+        { Map#Domain(Map#Empty(): Map QUN YAN)[u] }
+        !Map#Domain(Map#Empty(): Map QUN YAN)[u]);
+
+procedure P()
+{
+}
diff --git a/Test/test2/BoundedTypeParameterQuantifier.bpl.expect b/Test/test2/BoundedTypeParameterQuantifier.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/test2/BoundedTypeParameterQuantifier.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/unnecessaryassumes/unnecessaryassumes0.bpl b/Test/unnecessaryassumes/unnecessaryassumes0.bpl
new file mode 100644
index 00000000..a955495a
--- /dev/null
+++ b/Test/unnecessaryassumes/unnecessaryassumes0.bpl
@@ -0,0 +1,13 @@
+// RUN: %boogie /printNecessaryAssumes "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0(n: int)
+{
+    assume {:id "s0"} 0 < n;
+    assume {:id "s0"} 0 < n;
+}
+
+procedure test1(n: int)
+{
+    assume {:id "s0"} 0 < n;
+}
diff --git a/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect
new file mode 100644
index 00000000..9e420fa7
--- /dev/null
+++ b/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect
@@ -0,0 +1,3 @@
+unnecessaryassumes0.bpl(7,4): Error: more than one statement with same id: s0
+unnecessaryassumes0.bpl(12,4): Error: more than one statement with same id: s0
+2 name resolution errors detected in unnecessaryassumes0.bpl
diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl b/Test/unnecessaryassumes/unnecessaryassumes1.bpl
new file mode 100644
index 00000000..04226dfd
--- /dev/null
+++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl
@@ -0,0 +1,23 @@
+// RUN: %boogie /printNecessaryAssumes "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0(n: int)
+{
+    assume {:id "s0"} 0 < n;
+    assert 0 <= n;  // verified under s0
+}
+
+procedure test1(n: int)
+{
+    assume 0 < n;
+    assume {:id "s1"} n == 3;
+    assert 0 <= n;  // verified under true
+}
+
+procedure test2(n: int)
+{
+    assume 0 < n;
+    assume {:id "s2"} n <= 42;
+    assume {:id "s3"} 42 <= n;
+    assert n == 42;  // verified under s2 and s3
+}
diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect
new file mode 100644
index 00000000..0d3aeca2
--- /dev/null
+++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect
@@ -0,0 +1,3 @@
+Necessary assume command(s): s0, s2, s3
+
+Boogie program verifier finished with 3 verified, 0 errors