Merge branch 'master' of https://github.com/boogie-org/boogie

71 files changed, 1636 insertions, 299 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/CivlRefinement.cs b/Source/Concurrency/CivlRefinement.cs
index dfe50ef9..75ff2358 100644
--- a/Source/Concurrency/CivlRefinement.cs
+++ b/Source/Concurrency/CivlRefinement.cs
@@ -315,19 +315,9 @@ namespace Microsoft.Boogie
             foreach (var v in civlTypeChecker.localVarToLocalVariableInfo.Keys)
             {
                 LocalVariableInfo info = civlTypeChecker.localVarToLocalVariableInfo[v];
-                if (info.isGhost)
+                if (layerNum < info.layer)
                 {
-                    if (info.layer != layerNum)
-                    {
-                        availableVars.Remove(v);
-                    }
-                }
-                else
-                {
-                    if (layerNum < info.layer)
-                    {
-                        availableVars.Remove(v);
-                    }
+                    availableVars.Remove(v);
                 }
             }
             return availableVars;
diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
index 71feb927..b426d9ed 100644
--- a/Source/Concurrency/CivlTypeChecker.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -333,26 +333,24 @@ namespace Microsoft.Boogie
     public class AtomicProcedureInfo
     {
         public bool isPure;
-        public HashSet<int> layers;
+        public LayerRange layerRange;
         public AtomicProcedureInfo()
         {
             this.isPure = true;
-            this.layers = null;
+            this.layerRange = null;
         }
-        public AtomicProcedureInfo(HashSet<int> layers)
+        public AtomicProcedureInfo(LayerRange layerRange)
         {
             this.isPure = false;
-            this.layers = layers;
+            this.layerRange = layerRange;
         }
     }
 
     public class LocalVariableInfo
     {
-        public bool isGhost;
         public int layer;
-        public LocalVariableInfo(bool isGhost, int layer)
+        public LocalVariableInfo(int layer)
         {
-            this.isGhost = isGhost;
             this.layer = layer;
         }
     }
@@ -364,7 +362,6 @@ namespace Microsoft.Boogie
         Implementation enclosingImpl;
         HashSet<Variable> sharedVarsAccessed;
         int introducedLocalVarsUpperBound;
-        int ghostVarIntroLayerAllowed;
 
         public Program program;
         public int errorCount;
@@ -373,28 +370,15 @@ namespace Microsoft.Boogie
         public Dictionary<Procedure, AtomicProcedureInfo> procToAtomicProcedureInfo;
         public Dictionary<Absy, HashSet<int>> absyToLayerNums;
         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 (callCmd.Proc.Modifies.Count > 0)
-            {
-                return enclosingProcLayerNum == layerNum;
-            }
-            if (callCmd.Outs.Count == 0)
-            {
-                return true;
-            }
-            var outputVar = callCmd.Outs[0].Decl;
-            var localVariableInfo = localVarToLocalVariableInfo[outputVar];
-            if (localVariableInfo.isGhost)
-            {
-                return localVariableInfo.layer == layerNum;
-            }
             if (atomicProcedureInfo.isPure)
             {
-                return localVariableInfo.layer <= layerNum;
+                return pureCallLayer[callCmd] <= layerNum;
             }
             else
             {
@@ -456,13 +440,13 @@ namespace Microsoft.Boogie
             this.enclosingImpl = null;
             this.sharedVarsAccessed = null;
             this.introducedLocalVarsUpperBound = int.MinValue;
-            this.ghostVarIntroLayerAllowed = 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.procToAtomicProcedureInfo = new Dictionary<Procedure, AtomicProcedureInfo>();
+            this.pureCallLayer = new Dictionary<CallCmd, int>();
             
             foreach (var g in program.GlobalVariables)
             {
@@ -553,27 +537,39 @@ namespace Microsoft.Boogie
             foreach (var proc in program.Procedures)
             {
                 if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
-                var procLayerNums = RemoveDuplicatesAndSort(FindLayers(proc.Attributes));
+                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;
                     }
-                    else if (globalVarToSharedVarInfo[ie.Decl].introLayerNum != procLayerNums[0])
-                    {
-                        Error(proc, "The introduction layer of a modified global variable must be identical to the layer of the atomic procedure");
-                    }
                 }
-                if (proc.Modifies.Count == 0 || procLayerNums.Count == 1)
+                int lower, upper;
+                if (procLayerNums.Count == 1)
+                {
+                    lower = procLayerNums[0];
+                    upper = procLayerNums[0];
+                }
+                else if (procLayerNums.Count == 2)
                 {
-                    procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(new HashSet<int>(procLayerNums));
+                    lower = procLayerNums[0];
+                    upper = procLayerNums[1];
+                    if (lower >= upper)
+                    {
+                        Error(proc, "Lower layer must be less than upper layer");
+                        continue;
+                    }
                 }
                 else
                 {
-                    Error(proc, "An atomic procedure with more than one layer must not modify a global variable");
+                    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;
 
@@ -592,7 +588,7 @@ namespace Microsoft.Boogie
                     this.sharedVarsAccessed = new HashSet<Variable>();
                     (new PurityChecker(this)).VisitImplementation(impl);
                     LayerRange upperBound = FindLayerRange();
-                    LayerRange lowerBound = new LayerRange(atomicProcedureInfo.layers);
+                    LayerRange lowerBound = atomicProcedureInfo.layerRange;
                     if (!lowerBound.Subset(upperBound))
                     {
                         Error(impl, "Atomic procedure cannot access global variable");
@@ -695,14 +691,14 @@ namespace Microsoft.Boogie
                     Variable v = proc.InParams[i];
                     var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum);
                     if (layer == int.MinValue) continue;
-                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer);
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
                 }
                 for (int i = 0; i < proc.OutParams.Count; i++)
                 {
                     Variable v = proc.OutParams[i];
                     var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum);
                     if (layer == int.MinValue) continue;
-                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer);
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
                 }
             }
             foreach (Implementation node in program.Implementations)
@@ -712,21 +708,21 @@ namespace Microsoft.Boogie
                 {
                     var layer = FindLocalVariableLayer(node, v, procToActionInfo[node.Proc].createdAtLayerNum);
                     if (layer == int.MinValue) continue;
-                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(QKeyValue.FindBoolAttribute(node.Attributes, "ghost"), layer);
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
                 }
                 for (int i = 0; i < node.Proc.InParams.Count; i++)
                 {
                     Variable v = node.Proc.InParams[i];
                     if (!localVarToLocalVariableInfo.ContainsKey(v)) continue;
                     var layer = localVarToLocalVariableInfo[v].layer;
-                    localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(false, layer);
+                    localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(layer);
                 }
                 for (int i = 0; i < node.Proc.OutParams.Count; i++)
                 {
                     Variable v = node.Proc.OutParams[i];
                     if (!localVarToLocalVariableInfo.ContainsKey(v)) continue;
                     var layer = localVarToLocalVariableInfo[v].layer;
-                    localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(false, layer);
+                    localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(layer);
                 }
             }
             if (errorCount > 0) return; 
@@ -818,13 +814,17 @@ namespace Microsoft.Boogie
                 }
                 for (int i = 0; i < node.Ins.Count; i++)
                 {
-                    var formal = node.Proc.InParams[i];
-                    if (localVarToLocalVariableInfo.ContainsKey(formal))
+                    Visit(node.Ins[i]);
+                    if (introducedLocalVarsUpperBound != int.MinValue)
                     {
-                        introducedLocalVarsUpperBound = localVarToLocalVariableInfo[formal].layer;
+                        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;
                     }
-                    Visit(node.Ins[i]);
-                    introducedLocalVarsUpperBound = int.MinValue;
                 }
                 for (int i = 0; i < node.Outs.Count; i++)
                 {
@@ -840,69 +840,83 @@ namespace Microsoft.Boogie
             }
             else if (procToAtomicProcedureInfo.ContainsKey(node.Proc))
             {
-                // 1. Outputs are either all ghost or all introduced.
-                // 2. All outputs have the same layer; call it output layer.
-                // 3. If callee is impure and has outputs, output layer is a member of layer set of callee.
-                // 4. If callee is impure and has introduced outputs, then creation number of caller belongs to layer set of callee.
-                // 5. If callee is impure and modifies globals, then creation number of caller belongs to layer set of callee.
-                
-                Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
-                bool isGhost = false; // This assignment stops the compiler from complaining.
-                                      // In the absence of errors, isGhost is initialized by loop below.
-                foreach (var ie in node.Outs)
+                var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc];                
+                if (atomicProcedureInfo.isPure)
                 {
-                    if (localVarToLocalVariableInfo.ContainsKey(ie.Decl))
+                    if (node.Outs.Count > 0)
                     {
-                        var localVariableInfo = localVarToLocalVariableInfo[ie.Decl];
-                        if (introducedLocalVarsUpperBound == int.MinValue)
+                        int inferredLayer = int.MinValue;
+                        foreach (var ie in node.Outs)
                         {
-                            introducedLocalVarsUpperBound = localVariableInfo.layer;
-                            isGhost = localVariableInfo.isGhost;
-                            var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc];
-                            if (!atomicProcedureInfo.isPure)
+                            if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl)) continue;
+                            if (inferredLayer < localVarToLocalVariableInfo[ie.Decl].layer)
                             {
-                                if (!atomicProcedureInfo.layers.Contains(introducedLocalVarsUpperBound))
+                                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, "Layer of output variable must be a layer of the callee");
+                                    Error(node, "Output variable must be introduced");
                                 }
-                                if (!isGhost && !atomicProcedureInfo.layers.Contains(enclosingProcLayerNum))
+                                else if (inferredLayer != localVarToLocalVariableInfo[ie.Decl].layer)
                                 {
-                                    Error(node, "The creation layer of caller must be a layer of the callee");
+                                    Error(node, "All output variables must be introduced at the same layer");
                                 }
                             }
                         }
-                        else
+                        Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+                        foreach (var e in node.Ins)
                         {
-                            if (localVariableInfo.layer != introducedLocalVarsUpperBound)
+                            Visit(e);
+                            if (inferredLayer < introducedLocalVarsUpperBound)
                             {
-                                Error(node, "All outputs must have the same layer");
-                            }
-                            if (localVariableInfo.isGhost != isGhost)
-                            {
-                                Error(node, "Outputs are either all ghost or all introduced");
+                                Error(node, "An introduced local variable is not accessible");
                             }
+                            introducedLocalVarsUpperBound = int.MinValue;
                         }
                     }
                     else
                     {
-                        Error(node, "Output variable must be a ghost or introduced local variable");
+                        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;
                     }
                 }
-
-                if (node.Proc.Modifies.Count > 0)
+                else
                 {
-                    var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc];
-                    if (!atomicProcedureInfo.layers.Contains(enclosingProcLayerNum))
+                    if (enclosingProcLayerNum != atomicProcedureInfo.layerRange.upperLayerNum)
                     {
-                        Error(node, "The layer of called atomic procedure must be identical to the creation layer of callee");
+                        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");
                     }
-                    introducedLocalVarsUpperBound = enclosingProcLayerNum;
-                }
-                foreach (var e in node.Ins)
-                {
-                    Visit(e);
                 }
-                introducedLocalVarsUpperBound = int.MinValue;
                 return node;
             }
             else  
@@ -973,19 +987,9 @@ namespace Microsoft.Boogie
             else if ((node.Decl is Formal || node.Decl is Variable) && localVarToLocalVariableInfo.ContainsKey(node.Decl))
             {
                 var localVariableInfo = localVarToLocalVariableInfo[node.Decl];
-                if (localVariableInfo.isGhost)
+                if (introducedLocalVarsUpperBound < localVariableInfo.layer)
                 {
-                    if (ghostVarIntroLayerAllowed != localVariableInfo.layer)
-                    {
-                        Error(node, "Ghost variable inaccessible");
-                    }
-                }
-                else
-                {
-                    if (introducedLocalVarsUpperBound < localVariableInfo.layer)
-                    {
-                        Error(node, "Introduced variable inaccessible");
-                    }
+                    introducedLocalVarsUpperBound = localVariableInfo.layer;
                 }
             } 
             return base.VisitIdentifierExpr(node);
@@ -1003,9 +1007,12 @@ namespace Microsoft.Boogie
             {
                 sharedVarsAccessed = new HashSet<Variable>();
                 Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
-                introducedLocalVarsUpperBound = Least(FindLayers(ensures.Attributes));
                 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;
             }
@@ -1016,9 +1023,12 @@ namespace Microsoft.Boogie
         {
             sharedVarsAccessed = new HashSet<Variable>();
             Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
-            introducedLocalVarsUpperBound = Least(FindLayers(requires.Attributes));
             base.VisitRequires(requires);
             CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum);
+            if (introducedLocalVarsUpperBound > Least(FindLayers(requires.Attributes)))
+            {
+                Error(requires, "An introduced local variable is accessed but not available");
+            }
             introducedLocalVarsUpperBound = int.MinValue;
             sharedVarsAccessed = null;
             return requires;
@@ -1033,16 +1043,13 @@ namespace Microsoft.Boogie
             }
             sharedVarsAccessed = new HashSet<Variable>();
             Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
-            var layerNums = FindLayers(node.Attributes);
-            introducedLocalVarsUpperBound = Least(layerNums);
-            if (layerNums.Count == 1)
-            {
-                ghostVarIntroLayerAllowed = layerNums[0];
-            }
             base.VisitAssertCmd(node);
             CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum);
+            if (introducedLocalVarsUpperBound > Least(FindLayers(node.Attributes)))
+            {
+                Error(node, "An introduced local variable is accessed but not available");
+            }
             introducedLocalVarsUpperBound = int.MinValue;
-            ghostVarIntroLayerAllowed = int.MinValue;
             sharedVarsAccessed = null;
             return node;
         }
@@ -1115,7 +1122,7 @@ namespace Microsoft.Boogie
                 {
                     civlTypeChecker.Error(node, "Pure procedure can only call pure procedures");
                 }
-                else if (!callerInfo.layers.IsSubsetOf(calleeInfo.layers))
+                else if (!callerInfo.layerRange.Subset(calleeInfo.layerRange))
                 {
                     civlTypeChecker.Error(node, "Caller layers must be subset of callee layers");
                 }
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index c2e68002..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);
@@ -750,15 +752,28 @@ namespace Microsoft.Boogie {
             Contract.Assert(block != null);
             var auxCmd = block.TransferCmd as GotoCmd;
             if (auxCmd == null) continue;
-            foreach(var bl in auxCmd.labelTargets)
+            foreach (var bl in auxCmd.labelTargets)
             {
                 if (loopBlocks.Contains(bl)) continue;
-                immSuccBlks.Add(bl); 
+                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) {
@@ -975,10 +990,11 @@ namespace Microsoft.Boogie {
                 GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd;
                 Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null && 
                     auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1);
-                var blksThatBreakOut = GetBreakBlocksOfLoop(header, source, g);
-                var loopNodes = g.NaturalLoops(header, source);
+                //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) {
-                    if (!loopNodes.Contains(bl)) {
+                    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;
                         //these blocks may have read/write locals that are not present in naturalLoops
@@ -2225,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,
@@ -2232,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 f4cba1dc..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;
@@ -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
 
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 9623139a..9bc855be 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1008,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();
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index e93ecee9..7e98e8f8 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -246,9 +246,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 +401,8 @@ namespace Microsoft.Boogie.SMTLib
 
       PrepareCommon();
 
+      OptimizationRequests.Clear();
+
       string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
       FlushAxioms();
 
@@ -408,7 +410,20 @@ namespace Microsoft.Boogie.SMTLib
 
       SendThisVC("(push 1)");
       SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
+
+      if (CommandLineOptions.Clo.PrintNecessaryAssumes && NamedAssumeVars != null)
+      {
+        foreach (var v in NamedAssumeVars)
+        {
+          SendThisVC(string.Format("(declare-fun {0} () Bool)", v));
+          SendThisVC(string.Format("(assert (! {0} :named {1}))", v, "aux$$" + v.Name));
+        }
+      }
+
       SendThisVC(vcString);
+
+      SendOptimizationRequests();
+
       FlushLogFile();
 
       if (Process != null) {
@@ -422,6 +437,17 @@ namespace Microsoft.Boogie.SMTLib
       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 +472,7 @@ namespace Microsoft.Boogie.SMTLib
       if (options.Solver == SolverKind.Z3)
       {
         this.gen = gen;
+        SendThisVC("(reset)");
         Namer.Reset();
         common.Clear();
         SetupAxiomBuilder(gen);
@@ -1264,6 +1291,22 @@ namespace Microsoft.Boogie.SMTLib
             
             result = GetResponse();
 
+            var reporter = handler as VC.VCGen.ErrorReporter;
+            // TODO(wuestholz): Is the reporter ever null?
+            if (CommandLineOptions.Clo.PrintNecessaryAssumes && NamedAssumeVars != null && NamedAssumeVars.Any() && result == Outcome.Valid && reporter != null)
+            {
+              SendThisVC("(get-unsat-core)");
+              var resp = Process.GetProverResponse();
+              if (resp.Name != "")
+              {
+                 reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length));
+              }
+              foreach (var arg in resp.Arguments)
+              {
+                reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length));
+              }
+            }
+
             if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut)
             {
               #region Run timeout diagnostics
@@ -1812,6 +1855,7 @@ namespace Microsoft.Boogie.SMTLib
     private Model GetErrorModel() {
       if (!options.ExpectingModel())
         return null;
+
       SendThisVC("(get-model)");
       Process.Ping();
       Model theModel = null;
@@ -1906,6 +1950,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 +1991,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 +2032,8 @@ namespace Microsoft.Boogie.SMTLib
         DeclCollector.Collect(sortedExpr);
         FeedTypeDeclsToProver();
 
-
-
         AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options));
-        string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options);
+        string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, OptimizationRequests);
         Contract.Assert(res != null);
 
         if (CommandLineOptions.Clo.Trace)
@@ -2096,6 +2143,7 @@ namespace Microsoft.Boogie.SMTLib
 
     public override void Assert(VCExpr vc, bool polarity)
     {
+        OptimizationRequests.Clear();
         string a = "";
         if (polarity)
         {
@@ -2107,6 +2155,7 @@ namespace Microsoft.Boogie.SMTLib
         }
         AssertAxioms();
         SendThisVC(a);
+        SendOptimizationRequests();
     }
 
     public override void DefineMacro(Macro f, VCExpr vc) {
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index dcf95bd2..de8798b8 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, IList<string> optReqs = 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, optReqs);
       Contract.Assert(lin != null);
       lin.Linearise(e, LineariserOptions.Default);
       return cce.NonNull(sw.ToString());
@@ -74,12 +74,15 @@ namespace Microsoft.Boogie.SMTLib
     internal int UnderQuantifier = 0;
     internal readonly SMTLibProverOptions ProverOptions;
 
-    public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts)
+    readonly IList<string> OptimizationRequests;
+
+    public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList<string> optReqs = null)
     {
       Contract.Requires(wr != null); Contract.Requires(namer != null);
       this.wr = wr;
       this.Namer = namer;
       this.ProverOptions = opts;
+      this.OptimizationRequests = optReqs;
     }
 
     public void Linearise(VCExpr expr, LineariserOptions options)
@@ -263,6 +266,14 @@ 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)));
+          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..1c23c22f 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -255,7 +255,10 @@ void ObjectInvariant()
         RegisterType(node.Type);
         string decl =
           "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
-        AddDeclaration(decl);
+        if (!printedName.StartsWith("assume$$"))
+        {
+          AddDeclaration(decl);
+        }
         KnownVariables.Add(node);
 		if(declHandler != null)
 			declHandler.VarDecl(node);
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 0a9ba6b3..2fbb102c 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -341,6 +341,9 @@ 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 VCExprOp BoogieFunctionOp(Function func) {
       Contract.Requires(func != null);
       Contract.Ensures(Contract.Result<VCExprOp>() != null);
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 3c3b5cae..8c1ae407 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -346,7 +346,7 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
+    public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, IList<VCExprVar> namedAssumeVars = null) {
       Contract.Requires(descriptiveName != null);
       Contract.Requires(vc != null);
       Contract.Requires(handler != null);
@@ -356,10 +356,11 @@ namespace Microsoft.Boogie {
       hasOutput = false;
       outputExn = null;
       this.handler = handler;
-
+      
       thmProver.Reset(gen);
       SetTimeout();
       proverStart = DateTime.UtcNow;
+      thmProver.NamedAssumeVars = namedAssumeVars;
       thmProver.BeginCheck(descriptiveName, vc, handler);
       //  gen.ClearSharedFormulas();    PR: don't know yet what to do with this guy
 
@@ -386,6 +387,9 @@ namespace Microsoft.Boogie {
   // -----------------------------------------------------------------------------------------------
 
   public abstract class ProverInterface {
+
+    public IList<VCExprVar> NamedAssumeVars;
+
     public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {
       Contract.Requires(prog != null);
 
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index ae0a1147..19438924 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1133,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) {
@@ -1539,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/VC.cs b/Source/VCGeneration/VC.cs
index 33e2f928..ad067c04 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1386,7 +1386,8 @@ namespace VC {
         var exprGen = ctx.ExprGen;
         VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
 
-        VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context);
+        var namedAssumeVars = new List<VCExprVar>();
+        VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context, namedAssumeVars: namedAssumeVars);
         Contract.Assert(vc != null);
 
         if (!CommandLineOptions.Clo.UseLabels)
@@ -1414,7 +1415,7 @@ namespace VC {
         string desc = cce.NonNull(impl.Name);
         if (no >= 0)
           desc += "_split" + no;
-        checker.BeginCheck(desc, vc, reporter);
+        checker.BeginCheck(desc, vc, reporter, namedAssumeVars);
       }
 
       private void SoundnessCheck(HashSet<List<Block>/*!*/>/*!*/ cache, Block/*!*/ orig, List<Block/*!*/>/*!*/ copies) {
@@ -1519,7 +1520,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 +1528,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);
@@ -1567,7 +1568,8 @@ namespace VC {
           }
           break;
         case CommandLineOptions.VCVariety.DagIterative:
-          vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount);
+          // TODO(wuestholz): Support named assume statements not just for this encoding.
+          vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount, namedAssumeVars: namedAssumeVars);
           break;
         case CommandLineOptions.VCVariety.Doomed:
           vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount);
@@ -2021,6 +2023,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,
@@ -2229,10 +2241,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
@@ -2497,14 +2510,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) {
@@ -2819,6 +2830,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
@@ -2854,6 +2870,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") ||
@@ -3193,7 +3393,7 @@ namespace VC {
                                  Dictionary<int, Absy> label2absy,
                                  ProverContext proverCtxt,
                                  out int assertionCount,
-                                 bool isPositiveContext = true)
+                                 bool isPositiveContext = true, IList<VCExprVar> namedAssumeVars = null)
     {
       Contract.Requires(blocks != null);
       Contract.Requires(proverCtxt != null);
@@ -3253,7 +3453,7 @@ namespace VC {
         }
 
         VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext);
-        VCExpr vc = Wlp.Block(block, SuccCorrect, context);
+        VCExpr vc = Wlp.Block(block, SuccCorrect, context, namedAssumeVars);
         assertionCount += context.AssertionCount;
 
         VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool);
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index b4ee4c09..508a1400 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -48,7 +48,7 @@ namespace VC {
   
   public class Wlp
   {
-    public static VCExpr Block(Block b, VCExpr N, VCContext ctxt)
+    public static VCExpr Block(Block b, VCExpr N, VCContext ctxt, IList<VCExprVar> namedAssumeVars = null)
       //modifies ctxt.*;
     {
       Contract.Requires(b != null);
@@ -63,7 +63,7 @@ namespace VC {
 
       for (int i = b.Cmds.Count; --i >= 0; )
       {
-        res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt);
+        res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt, namedAssumeVars);
       }
       
       int id = b.UniqueId;
@@ -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, IList<VCExprVar> namedAssumeVars = null) {
       Contract.Requires(cmd != null);
       Contract.Requires(N != null);
       Contract.Requires(ctxt != null);
@@ -186,17 +186,41 @@ 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 (CommandLineOptions.Clo.PrintNecessaryAssumes && aid != null && namedAssumeVars != null)
+        {
+          var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool);
+          namedAssumeVars.Add(v);
+          expr = 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/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 9823d44a..f08c6e00 100644
--- a/Test/civl/Program4.bpl.expect
+++ b/Test/civl/Program4.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 6 verified, 0 errors
+Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Test/civl/alloc.bpl b/Test/civl/alloc.bpl
index 33535b00..68b7e6c6 100644
--- a/Test/civl/alloc.bpl
+++ b/Test/civl/alloc.bpl
@@ -11,21 +11,26 @@ axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && m
 function EmptyLmap(): (lmap);
 axiom (dom(EmptyLmap()) == MapConstBool(false));
 
-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 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} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+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} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+   invariant {:layer 1} PoolInv(unallocated, pool);
    {
       call  l, i := Alloc();
       async call Thread(l, i);
@@ -35,8 +40,8 @@ ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
 }
 
 procedure {:yields} {:layer 2} Thread({:layer 1} {:linear_in "mem"} local_in: lmap, i: int)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+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];
 {
@@ -50,13 +55,13 @@ requires {:layer 2} dom(local_in)[i];
     call o := Read(local, i);
     assert {:layer 2} o == 42;
     while (*)
-    invariant {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+    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);
+        call Free(l, y);
 	par Yield() | Dummy();
     }
     par Yield() | Dummy();
@@ -68,8 +73,8 @@ procedure {:pure} {:inline 1} Copy({:linear_in "mem"} l: lmap) returns ({:linear
 }
 
 procedure {:yields} {:layer 1,2} Alloc() returns ({:layer 1} {:linear "mem"} l: lmap, i: int)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+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; }|;
 {
@@ -79,17 +84,21 @@ ensures {:right} |{ A: assume dom(l)[i]; return true; }|;
     call YieldMem(l, i);
 }
 
-procedure {:yields} {:layer 1,2} Free({:layer 1} {:linear_in "mem"} l: lmap)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+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} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+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; }|;
 {
@@ -99,8 +108,8 @@ ensures {:both} |{ A: assert dom(l)[i]; o := map(l)[i]; return true; }|;
 }
 
 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} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+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; }|;
@@ -116,26 +125,31 @@ 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} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
 {
     yield;
-    assert {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+    assert {:layer 1} PoolInv(unallocated, pool);
 }
 
 procedure {:yields} {:layer 1} YieldMem({:layer 1} {:linear "mem"} l: lmap, i: int)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+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} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+    assert {:layer 1} PoolInv(unallocated, pool);
     assert {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
 }
 
@@ -144,7 +158,7 @@ procedure {:yields} {:layer 2} Dummy()
     yield;
 }
 
-var {:layer 1, 1} pool: lmap;
+var {:layer 1, 1} {:linear "mem"} pool: lmap;
 var {:layer 0, 1} mem:[int]int;
 var {:layer 0, 1} unallocated:[int]bool;
 
@@ -155,4 +169,7 @@ 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; }|;
\ No newline at end of file
+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/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/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/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/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/wsq.bpl b/Test/civl/wsq.bpl
index 39dad919..0a2227b6 100644
--- a/Test/civl/wsq.bpl
+++ b/Test/civl/wsq.bpl
@@ -89,9 +89,9 @@ 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} {:layer 3} oldH:int;
-   var {:ghost} {:layer 3} oldT:int;
-   var {:ghost} {:layer 3} oldStatusT:bool;
+   var {:layer 3} oldH:int;
+   var {:layer 3} oldT:int;
+   var {:layer 3} oldStatusT:bool;
    
    call oldH, oldT := GhostRead();
    yield;
@@ -142,8 +142,8 @@ 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} {:layer 3} oldH:int;
-   var {:ghost} {:layer 3} oldT:int;
+   var {:layer 3} oldH:int;
+   var {:layer 3} oldT:int;
 
    call oldH, oldT := GhostRead();
    yield;
@@ -304,8 +304,8 @@ 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} {:layer 3} oldH:int;
-   var {:ghost} {:layer 3} oldT:int;
+   var {:layer 3} oldH:int;
+   var {:layer 3} oldT:int;
 
    call oldH, oldT := GhostRead();
    yield;
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/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/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..dd04bb46
--- /dev/null
+++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect
@@ -0,0 +1,3 @@
+Necessary assume command(s): s0, s3, s2
+
+Boogie program verifier finished with 3 verified, 0 errors