Merge branch 'upstream' into dfsg_free

27 files changed, 1383 insertions, 413 deletions

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 0d2676f2..2fd37463 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -698,9 +698,13 @@ namespace Microsoft.Boogie.AbstractInterpretation
             lo = Lo; hi = Hi;
             if (hi != null) {
               Lo = node.Type.IsReal ? -hi : 1 - hi;
+            } else {
+              Lo = null;
             }
             if (lo != null) {
               Hi = node.Type.IsReal ? -lo : 1 - lo;
+            } else {
+              Hi = null;
             }
           }
           else if (op.Op == UnaryOperator.Opcode.Not) {
@@ -880,6 +884,10 @@ namespace Microsoft.Boogie.AbstractInterpretation
               if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
                 Lo = BigInteger.Zero;
                 Hi = hi1;
+                if (lo0 < lo1 && hi0 != null && hi0 < lo1) {
+                  Lo = lo0;
+                  Hi = hi0;
+                }
               }
               break;
             case BinaryOperator.Opcode.RealDiv:
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/CivlRefinement.cs
index 2ad08024..75ff2358 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/CivlRefinement.cs
@@ -13,7 +13,7 @@ namespace Microsoft.Boogie
 {
     public class MyDuplicator : Duplicator
     {
-        MoverTypeChecker moverTypeChecker;
+        CivlTypeChecker civlTypeChecker;
         public int layerNum;
         Procedure enclosingProc;
         Implementation enclosingImpl;
@@ -23,9 +23,9 @@ namespace Microsoft.Boogie
         public HashSet<Procedure> yieldingProcs;
         public List<Implementation> impls;
 
-        public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum)
+        public MyDuplicator(CivlTypeChecker civlTypeChecker, int layerNum)
         {
-            this.moverTypeChecker = moverTypeChecker;
+            this.civlTypeChecker = civlTypeChecker;
             this.layerNum = layerNum;
             this.enclosingProc = null;
             this.enclosingImpl = null;
@@ -38,11 +38,19 @@ namespace Microsoft.Boogie
 
         private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds)
         {
-            int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;
+            int enclosingProcLayerNum = civlTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;
             Procedure originalProc = originalCallCmd.Proc;
-            if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))
+            
+            if (civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(originalProc))
+            {
+                if (civlTypeChecker.CallExists(originalCallCmd, enclosingProcLayerNum, layerNum))
+                {
+                    newCmds.Add(callCmd);
+                }
+            }
+            else if (civlTypeChecker.procToActionInfo.ContainsKey(originalProc))
             {
-                AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo;
+                AtomicActionInfo atomicActionInfo = civlTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo;
                 if (atomicActionInfo != null && atomicActionInfo.gate.Count > 0 && layerNum == enclosingProcLayerNum)
                 {
                     newCmds.Add(new HavocCmd(Token.NoToken, new List<IdentifierExpr>(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) })));
@@ -57,8 +65,12 @@ namespace Microsoft.Boogie
                         newCmds.Add(Substituter.Apply(subst, assertCmd));
                     }
                 }
+                newCmds.Add(callCmd);
+            }
+            else
+            {
+                Debug.Assert(false);
             }
-            newCmds.Add(callCmd);
         }
 
         private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List<Cmd> newCmds)
@@ -66,7 +78,7 @@ namespace Microsoft.Boogie
             int maxCalleeLayerNum = 0;
             foreach (CallCmd iter in originalParCallCmd.CallCmds)
             {
-                int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum;
+                int calleeLayerNum = civlTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum;
                 if (calleeLayerNum > maxCalleeLayerNum)
                     maxCalleeLayerNum = calleeLayerNum;
             }
@@ -144,7 +156,7 @@ namespace Microsoft.Boogie
 
         public override Procedure VisitProcedure(Procedure node)
         {
-            if (!moverTypeChecker.procToActionInfo.ContainsKey(node))
+            if (!civlTypeChecker.procToActionInfo.ContainsKey(node))
                 return node;
             if (!procMap.ContainsKey(node))
             {
@@ -155,7 +167,7 @@ namespace Microsoft.Boogie
                 proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies);
                 proc.OutParams = this.VisitVariableSeq(node.OutParams);
 
-                ActionInfo actionInfo = moverTypeChecker.procToActionInfo[node];
+                ActionInfo actionInfo = civlTypeChecker.procToActionInfo[node];
                 if (actionInfo.createdAtLayerNum < layerNum)
                 {
                     proc.Requires = new List<Requires>();
@@ -198,7 +210,7 @@ namespace Microsoft.Boogie
                 }
                 procMap[node] = proc;
                 proc.Modifies = new List<IdentifierExpr>();
-                moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));
+                civlTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));
             }
             return procMap[node];
         }
@@ -220,7 +232,7 @@ namespace Microsoft.Boogie
             Requires requires = base.VisitRequires(node);
             if (node.Free)
                 return requires;
-            if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
+            if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum))
                 requires.Condition = Expr.True;
             return requires;
         }
@@ -230,12 +242,12 @@ namespace Microsoft.Boogie
             Ensures ensures = base.VisitEnsures(node);
             if (node.Free)
                 return ensures;
-            AtomicActionInfo atomicActionInfo =  moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo;
+            AtomicActionInfo atomicActionInfo =  civlTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo;
             bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node;
-            if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
+            if (isAtomicSpecification || !civlTypeChecker.absyToLayerNums[node].Contains(layerNum))
             {
                 ensures.Condition = Expr.True;
-                ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes);
+                ensures.Attributes = CivlRefinement.RemoveMoverAttribute(ensures.Attributes);
             }
             return ensures;
         }
@@ -243,16 +255,16 @@ namespace Microsoft.Boogie
         public override Cmd VisitAssertCmd(AssertCmd node)
         {
             AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node);
-            if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
+            if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum))
                 assertCmd.Expr = Expr.True;
             return assertCmd;
         }
     }
 
-    public class OwickiGries
+    public class CivlRefinement
     {
         LinearTypeChecker linearTypeChecker;
-        MoverTypeChecker moverTypeChecker;
+        CivlTypeChecker civlTypeChecker;
         Dictionary<Absy, Absy> absyMap;
         Dictionary<Implementation, Implementation> implMap;
         HashSet<Procedure> yieldingProcs;
@@ -269,17 +281,17 @@ namespace Microsoft.Boogie
         Expr beta;
         HashSet<Variable> frame;
 
-        public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator)
+        public CivlRefinement(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, MyDuplicator duplicator)
         {
             this.linearTypeChecker = linearTypeChecker;
-            this.moverTypeChecker = moverTypeChecker;
+            this.civlTypeChecker = civlTypeChecker;
             this.absyMap = duplicator.absyMap;
             this.layerNum = duplicator.layerNum;
             this.implMap = duplicator.implMap;
             this.yieldingProcs = duplicator.yieldingProcs;
             Program program = linearTypeChecker.program;
             globalMods = new List<IdentifierExpr>();
-            foreach (Variable g in moverTypeChecker.SharedVariables)
+            foreach (Variable g in civlTypeChecker.SharedVariables)
             {
                 globalMods.Add(Expr.Ident(g));
             }
@@ -291,7 +303,24 @@ namespace Microsoft.Boogie
 
         private IEnumerable<Variable> AvailableLinearVars(Absy absy)
         {
-            return linearTypeChecker.AvailableLinearVars(absyMap[absy]);
+            HashSet<Variable> availableVars = new HashSet<Variable>(linearTypeChecker.AvailableLinearVars(absyMap[absy]));
+            foreach (var g in civlTypeChecker.globalVarToSharedVarInfo.Keys)
+            {
+                SharedVariableInfo info = civlTypeChecker.globalVarToSharedVarInfo[g];
+                if (!(info.introLayerNum <= layerNum && layerNum <= info.hideLayerNum))
+                {
+                    availableVars.Remove(g);
+                }
+            }
+            foreach (var v in civlTypeChecker.localVarToLocalVariableInfo.Keys)
+            {
+                LocalVariableInfo info = civlTypeChecker.localVarToLocalVariableInfo[v];
+                if (layerNum < info.layer)
+                {
+                    availableVars.Remove(v);
+                }
+            }
+            return availableVars;
         }
 
         private CallCmd CallToYieldProc(IToken tok, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
@@ -715,7 +744,7 @@ namespace Microsoft.Boogie
             }
 
             Procedure originalProc = implMap[impl].Proc;
-            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];
+            ActionInfo actionInfo = civlTypeChecker.procToActionInfo[originalProc];
             if (actionInfo.createdAtLayerNum == this.layerNum)
             {
                 pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool));
@@ -738,19 +767,14 @@ namespace Microsoft.Boogie
                     foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);
                 }
                 Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);
-                frame = new HashSet<Variable>(moverTypeChecker.SharedVariables);
-                HashSet<Variable> introducedVars = new HashSet<Variable>();
-                foreach (Variable v in moverTypeChecker.SharedVariables)
+                frame = new HashSet<Variable>(civlTypeChecker.SharedVariables);
+                foreach (Variable v in civlTypeChecker.SharedVariables)
                 {
-                    if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || 
-                        moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)
+                    if (civlTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || 
+                        civlTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)
                     {
                         frame.Remove(v);
                     }
-                    if (moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum == actionInfo.createdAtLayerNum)
-                    {
-                        introducedVars.Add(v);
-                    }
                 }
                 AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
                 if (atomicActionInfo == null)
@@ -764,7 +788,7 @@ namespace Microsoft.Boogie
                 }
                 else
                 {
-                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, introducedVars)).TransitionRelationCompute(true);
+                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(civlTypeChecker.program, atomicActionInfo, frame, new HashSet<Variable>())).TransitionRelationCompute(true);
                     beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);
                     Expr alphaExpr = Expr.True;
                     foreach (AssertCmd assertCmd in atomicActionInfo.gate)
@@ -1175,31 +1199,31 @@ namespace Microsoft.Boogie
             return decls;
         }
 
-        public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
+        public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls)
         {
             Program program = linearTypeChecker.program;
-            foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))
+            foreach (int layerNum in civlTypeChecker.AllLayerNums)
             {
                 if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;
 
-                MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, layerNum);
+                MyDuplicator duplicator = new MyDuplicator(civlTypeChecker, layerNum);
                 foreach (var proc in program.Procedures)
                 {
-                    if (!moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue;
+                    if (!civlTypeChecker.procToActionInfo.ContainsKey(proc)) continue;
                     Procedure duplicateProc = duplicator.VisitProcedure(proc);
                     decls.Add(duplicateProc);
                 }
                 decls.AddRange(duplicator.impls);
-                OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator);
+                CivlRefinement civlTransform = new CivlRefinement(linearTypeChecker, civlTypeChecker, duplicator);
                 foreach (var impl in program.Implementations)
                 {
-                    if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum)
+                    if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum)
                         continue;
                     Implementation duplicateImpl = duplicator.VisitImplementation(impl);
-                    ogTransform.TransformImpl(duplicateImpl);
+                    civlTransform.TransformImpl(duplicateImpl);
                     decls.Add(duplicateImpl);
                 }
-                decls.AddRange(ogTransform.Collect());
+                decls.AddRange(civlTransform.Collect());
             }
         }
     }
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/CivlTypeChecker.cs
index c821117a..b426d9ed 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -280,22 +280,111 @@ namespace Microsoft.Boogie
         }
     }
 
-    public class MoverTypeChecker : ReadOnlyVisitor
+    public class LayerRange
+    {
+        public int lowerLayerNum;
+        public int upperLayerNum;
+        public LayerRange(int layer)
+        {
+            this.lowerLayerNum = layer;
+            this.upperLayerNum = layer;
+        }
+        public LayerRange(int lower, int upper)
+        {
+            this.lowerLayerNum = lower;
+            this.upperLayerNum = upper;
+        }
+        public LayerRange(IEnumerable<int> layerNums)
+        {
+            int min = int.MaxValue;
+            int max = int.MinValue;
+            foreach (var layerNum in layerNums)
+            {
+                if (layerNum < min)
+                {
+                    min = layerNum;
+                }
+                if (max < layerNum)
+                {
+                    max = layerNum;
+                }
+            }
+            this.lowerLayerNum = min;
+            this.upperLayerNum = max;
+        }
+        public bool Contains(int layerNum)
+        {
+            return lowerLayerNum <= layerNum && layerNum <= upperLayerNum;
+        }
+        public bool Subset(int lower, int upper)
+        {
+            return lower <= lowerLayerNum && upperLayerNum <= upper;
+        }
+        public bool Equal(int lower, int upper)
+        {
+            return lower == lowerLayerNum && upperLayerNum == upper;
+        }
+        public bool Subset(LayerRange info)
+        {
+            return info.lowerLayerNum <= lowerLayerNum && upperLayerNum <= info.upperLayerNum;
+        }
+    }
+
+    public class AtomicProcedureInfo
+    {
+        public bool isPure;
+        public LayerRange layerRange;
+        public AtomicProcedureInfo()
+        {
+            this.isPure = true;
+            this.layerRange = null;
+        }
+        public AtomicProcedureInfo(LayerRange layerRange)
+        {
+            this.isPure = false;
+            this.layerRange = layerRange;
+        }
+    }
+
+    public class LocalVariableInfo
+    {
+        public int layer;
+        public LocalVariableInfo(int layer)
+        {
+            this.layer = layer;
+        }
+    }
+
+    public class CivlTypeChecker : ReadOnlyVisitor
     {
         CheckingContext checkingContext;
-        public int errorCount;
-        public Dictionary<Variable, SharedVariableInfo> globalVarToSharedVarInfo;
         Procedure enclosingProc;
         Implementation enclosingImpl;
-        public Dictionary<Procedure, ActionInfo> procToActionInfo;
+        HashSet<Variable> sharedVarsAccessed;
+        int introducedLocalVarsUpperBound;
+
         public Program program;
-        bool canAccessSharedVars;
-        bool canAccessGhostVars;
-        int minLayerNum;
-        int maxLayerNum;
+        public int errorCount;
+        public Dictionary<Variable, SharedVariableInfo> globalVarToSharedVarInfo;
+        public Dictionary<Procedure, ActionInfo> procToActionInfo;
+        public Dictionary<Procedure, AtomicProcedureInfo> procToAtomicProcedureInfo;
         public Dictionary<Absy, HashSet<int>> absyToLayerNums;
-        HashSet<Variable> ghostVars;
-        public int leastUnimplementedLayerNum;
+        public Dictionary<Variable, LocalVariableInfo> localVarToLocalVariableInfo;
+        Dictionary<CallCmd, int> pureCallLayer;
+
+        public bool CallExists(CallCmd callCmd, int enclosingProcLayerNum, int layerNum)
+        {
+            Debug.Assert(procToAtomicProcedureInfo.ContainsKey(callCmd.Proc));
+            var atomicProcedureInfo = procToAtomicProcedureInfo[callCmd.Proc];
+            if (atomicProcedureInfo.isPure)
+            {
+                return pureCallLayer[callCmd] <= layerNum;
+            }
+            else
+            {
+                return enclosingProcLayerNum == layerNum;
+            }
+        }
 
         private static List<int> FindLayers(QKeyValue kv)
         {
@@ -316,6 +405,19 @@ namespace Microsoft.Boogie
             return layers;
         }
 
+        private static int Least(IEnumerable<int> layerNums)
+        {
+            int least = int.MaxValue;
+            foreach (var layer in layerNums)
+            {
+                if (layer < least)
+                {
+                    least = layer;
+                }
+            }
+            return least;
+        }
+
         private static MoverType GetMoverType(Ensures e)
         {
             if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
@@ -329,28 +431,29 @@ namespace Microsoft.Boogie
             return MoverType.Top;
         }
 
-        public MoverTypeChecker(Program program)
+        public CivlTypeChecker(Program program)
         {
-            this.ghostVars = new HashSet<Variable>();
-            this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();
-            this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();
-            this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
             this.errorCount = 0;
             this.checkingContext = new CheckingContext(null);
             this.program = program;
             this.enclosingProc = null;
             this.enclosingImpl = null;
-            this.canAccessSharedVars = false;
-            this.canAccessGhostVars = false;
-            this.minLayerNum = int.MaxValue;
-            this.maxLayerNum = -1;
-            this.leastUnimplementedLayerNum = int.MaxValue;
+            this.sharedVarsAccessed = null;
+            this.introducedLocalVarsUpperBound = int.MinValue;
+
+            this.localVarToLocalVariableInfo = new Dictionary<Variable, LocalVariableInfo>();
+            this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();
+            this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();
+            this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
+            this.procToAtomicProcedureInfo = new Dictionary<Procedure, AtomicProcedureInfo>();
+            this.pureCallLayer = new Dictionary<CallCmd, int>();
+            
             foreach (var g in program.GlobalVariables)
             {
                 List<int> layerNums = FindLayers(g.Attributes);
                 if (layerNums.Count == 0)
                 {
-                    // Cannot access atomic actions
+                    // Inaccessible from  yielding and atomic procedures
                 }
                 else if (layerNums.Count == 1)
                 {
@@ -366,28 +469,137 @@ namespace Microsoft.Boogie
                 }
             }
         }
-        
-        private HashSet<int> allCreatedLayerNums;
-        public IEnumerable<int> AllCreatedLayerNums
+
+        private HashSet<int> allLayerNums;
+        public IEnumerable<int> AllLayerNums
         {
             get
             {
-                if (allCreatedLayerNums == null)
+                if (allLayerNums == null)
                 {
-                    allCreatedLayerNums = new HashSet<int>();
+                    allLayerNums = new HashSet<int>();
                     foreach (ActionInfo actionInfo in procToActionInfo.Values)
                     {
-                        allCreatedLayerNums.Add(actionInfo.createdAtLayerNum);
+                        allLayerNums.Add(actionInfo.createdAtLayerNum);
+                    }
+                    foreach (var layerNums in absyToLayerNums.Values)
+                    {
+                        foreach (var layer in layerNums)
+                        {
+                            allLayerNums.Add(layer);
+                        }
                     }
                 }
-                return allCreatedLayerNums;
+                return allLayerNums;
+            }
+        }
+
+        private LayerRange FindLayerRange()
+        {
+            int maxIntroLayerNum = int.MinValue;
+            int minHideLayerNum = int.MaxValue;
+            foreach (var g in sharedVarsAccessed)
+            {
+                if (globalVarToSharedVarInfo[g].introLayerNum > maxIntroLayerNum)
+                {
+                    maxIntroLayerNum = globalVarToSharedVarInfo[g].introLayerNum;
+                }
+                if (globalVarToSharedVarInfo[g].hideLayerNum < minHideLayerNum)
+                {
+                    minHideLayerNum = globalVarToSharedVarInfo[g].hideLayerNum;
+                }
             }
+            return new LayerRange(maxIntroLayerNum, minHideLayerNum);
         }
 
         public void TypeCheck()
         {
             foreach (var proc in program.Procedures)
             {
+                if (!QKeyValue.FindBoolAttribute(proc.Attributes, "pure")) continue;
+                if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
+                {
+                    Error(proc, "Pure procedure must not yield");
+                    continue;
+                }
+                if (QKeyValue.FindBoolAttribute(proc.Attributes, "layer"))
+                {
+                    Error(proc, "Pure procedure must not have layers");
+                    continue;
+                }
+                if (proc.Modifies.Count > 0)
+                {
+                    Error(proc, "Pure procedure must not modify a global variable");
+                    continue;
+                }
+                procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo();
+            }
+            foreach (var proc in program.Procedures)
+            {
+                if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
+                var procLayerNums = FindLayers(proc.Attributes);
+                if (procLayerNums.Count == 0) continue;
+                foreach (IdentifierExpr ie in proc.Modifies)
+                {
+                    if (!globalVarToSharedVarInfo.ContainsKey(ie.Decl))
+                    {
+                        Error(proc, "Atomic procedure cannot modify a global variable without layer numbers");
+                        continue;
+                    }
+                }
+                int lower, upper;
+                if (procLayerNums.Count == 1)
+                {
+                    lower = procLayerNums[0];
+                    upper = procLayerNums[0];
+                }
+                else if (procLayerNums.Count == 2)
+                {
+                    lower = procLayerNums[0];
+                    upper = procLayerNums[1];
+                    if (lower >= upper)
+                    {
+                        Error(proc, "Lower layer must be less than upper layer");
+                        continue;
+                    }
+                }
+                else
+                {
+                    Error(proc, "Atomic procedure must specify a layer range");
+                    continue;
+                }
+                LayerRange layerRange = new LayerRange(lower, upper);
+                procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(layerRange);
+            }
+            if (errorCount > 0) return;
+
+            foreach (Implementation impl in program.Implementations)
+            {
+                if (!procToAtomicProcedureInfo.ContainsKey(impl.Proc)) continue;
+                var atomicProcedureInfo = procToAtomicProcedureInfo[impl.Proc];
+                if (atomicProcedureInfo.isPure)
+                {
+                    this.enclosingImpl = impl;
+                    (new PurityChecker(this)).VisitImplementation(impl);
+                }
+                else 
+                {
+                    this.enclosingImpl = impl;
+                    this.sharedVarsAccessed = new HashSet<Variable>();
+                    (new PurityChecker(this)).VisitImplementation(impl);
+                    LayerRange upperBound = FindLayerRange();
+                    LayerRange lowerBound = atomicProcedureInfo.layerRange;
+                    if (!lowerBound.Subset(upperBound))
+                    {
+                        Error(impl, "Atomic procedure cannot access global variable");
+                    }
+                    this.sharedVarsAccessed = null;
+                }
+            }
+            if (errorCount > 0) return; 
+            
+            foreach (var proc in program.Procedures)
+            {
                 if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
 
                 int createdAtLayerNum;  // must be initialized by the following code, otherwise it is an error
@@ -428,25 +640,21 @@ namespace Microsoft.Boogie
                         continue;
                     }
 
-                    minLayerNum = int.MaxValue;
-                    maxLayerNum = -1;
-                    canAccessSharedVars = true;
+                    sharedVarsAccessed = new HashSet<Variable>();
                     enclosingProc = proc;
                     enclosingImpl = null;
                     base.VisitEnsures(e);
-                    canAccessSharedVars = false;
-                    if (maxLayerNum > createdAtLayerNum)
-                    {
-                        Error(e, "A variable being accessed is introduced after this action is created");
-                    }
-                    else if (availableUptoLayerNum > minLayerNum)
+                    LayerRange upperBound = FindLayerRange();
+                    LayerRange lowerBound = new LayerRange(createdAtLayerNum, availableUptoLayerNum);
+                    if (lowerBound.Subset(upperBound))
                     {
-                        Error(e, "A variable being accessed is hidden before this action becomes unavailable");
+                        procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum);
                     }
                     else
                     {
-                        procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum);
+                        Error(e, "A variable being accessed in this action is unavailable");
                     }
+                    sharedVarsAccessed = null;
                 }
                 if (errorCount > 0) continue;
                 if (!procToActionInfo.ContainsKey(proc))
@@ -463,52 +671,63 @@ namespace Microsoft.Boogie
                 }
             }
             if (errorCount > 0) return;
+            
             foreach (var impl in program.Implementations)
             {
                 if (!procToActionInfo.ContainsKey(impl.Proc)) continue;
+                ActionInfo actionInfo = procToActionInfo[impl.Proc];
                 procToActionInfo[impl.Proc].hasImplementation = true;
-            }
-            foreach (var proc in procToActionInfo.Keys)
-            {
-                ActionInfo actionInfo = procToActionInfo[proc];
-                if (actionInfo.isExtern && actionInfo.hasImplementation)
+                if (actionInfo.isExtern)
                 {
-                    Error(proc, "Extern procedure cannot have an implementation");
-                    continue;
+                    Error(impl.Proc, "Extern procedure cannot have an implementation");
                 }
-                if (actionInfo.isExtern || actionInfo.hasImplementation) continue;
-                if (leastUnimplementedLayerNum == int.MaxValue)
+            }
+            if (errorCount > 0) return;
+
+            foreach (Procedure proc in procToActionInfo.Keys)
+            {
+                for (int i = 0; i < proc.InParams.Count; i++)
                 {
-                    leastUnimplementedLayerNum = actionInfo.createdAtLayerNum;
+                    Variable v = proc.InParams[i];
+                    var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum);
+                    if (layer == int.MinValue) continue;
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
                 }
-                else if (leastUnimplementedLayerNum != actionInfo.createdAtLayerNum)
+                for (int i = 0; i < proc.OutParams.Count; i++)
                 {
-                    Error(proc, "All unimplemented atomic actions must be created at the same layer");
+                    Variable v = proc.OutParams[i];
+                    var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum);
+                    if (layer == int.MinValue) continue;
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
                 }
             }
-            foreach (var g in this.globalVarToSharedVarInfo.Keys)
+            foreach (Implementation node in program.Implementations)
             {
-                var info = globalVarToSharedVarInfo[g];
-                if (!this.AllCreatedLayerNums.Contains(info.introLayerNum))
+                if (!procToActionInfo.ContainsKey(node.Proc)) continue;
+                foreach (Variable v in node.LocVars)
                 {
-                    Error(g, "Variable must be introduced with creation of some atomic action");
+                    var layer = FindLocalVariableLayer(node, v, procToActionInfo[node.Proc].createdAtLayerNum);
+                    if (layer == int.MinValue) continue;
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
                 }
-                if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum))
+                for (int i = 0; i < node.Proc.InParams.Count; i++)
                 {
-                    Error(g, "Variable must be hidden with creation of some atomic action");
+                    Variable v = node.Proc.InParams[i];
+                    if (!localVarToLocalVariableInfo.ContainsKey(v)) continue;
+                    var layer = localVarToLocalVariableInfo[v].layer;
+                    localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(layer);
                 }
-            }
-            if (errorCount > 0) return;
-            this.VisitProgram(program);
-            foreach (Procedure proc in program.Procedures)
-            {
-                if (procToActionInfo.ContainsKey(proc)) continue;
-                foreach (var ie in proc.Modifies)
+                for (int i = 0; i < node.Proc.OutParams.Count; i++)
                 {
-                    if (!SharedVariables.Contains(ie.Decl)) continue;
-                    Error(proc, "A ghost procedure must not modify a global variable with layer annotation");
+                    Variable v = node.Proc.OutParams[i];
+                    if (!localVarToLocalVariableInfo.ContainsKey(v)) continue;
+                    var layer = localVarToLocalVariableInfo[v].layer;
+                    localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(layer);
                 }
             }
+            if (errorCount > 0) return; 
+            
+            this.VisitProgram(program);
             if (errorCount > 0) return;
             YieldTypeChecker.PerformYieldSafeCheck(this);
             new LayerEraser().VisitProgram(program);
@@ -516,9 +735,26 @@ namespace Microsoft.Boogie
 
         public IEnumerable<Variable> SharedVariables
         {
-            get { return this.globalVarToSharedVarInfo.Keys;  }
+            get { return this.globalVarToSharedVarInfo.Keys; }
         }
-        
+
+        private int FindLocalVariableLayer(Declaration decl, Variable v, int enclosingProcLayerNum)
+        {
+            var layers = FindLayers(v.Attributes);
+            if (layers.Count == 0) return int.MinValue;
+            if (layers.Count > 1)
+            {
+                Error(decl, "Incorrect number of layers");
+                return int.MinValue;
+            }
+            if (layers[0] > enclosingProcLayerNum)
+            {
+                Error(decl, "Layer of local variable cannot be greater than the creation layer of enclosing procedure");
+                return int.MinValue;
+            }
+            return layers[0];
+        }
+
         public override Implementation VisitImplementation(Implementation node)
         {
             if (!procToActionInfo.ContainsKey(node.Proc))
@@ -527,17 +763,9 @@ namespace Microsoft.Boogie
             }
             this.enclosingImpl = node;
             this.enclosingProc = null;
-            ghostVars = new HashSet<Variable>();
-            foreach (Variable v in node.LocVars)
-            {
-                if (QKeyValue.FindBoolAttribute(v.Attributes, "ghost"))
-                {
-                    ghostVars.Add(v);
-                }
-            }
             return base.VisitImplementation(node);
         }
-        
+
         public override Procedure VisitProcedure(Procedure node)
         {
             if (!procToActionInfo.ContainsKey(node))
@@ -584,23 +812,117 @@ namespace Microsoft.Boogie
                 {
                     Error(node, "The callee is not available in the caller procedure");
                 }
-                return base.VisitCallCmd(node);
+                for (int i = 0; i < node.Ins.Count; i++)
+                {
+                    Visit(node.Ins[i]);
+                    if (introducedLocalVarsUpperBound != int.MinValue)
+                    {
+                        var formal = node.Proc.InParams[i];
+                        if (!localVarToLocalVariableInfo.ContainsKey(formal) ||
+                            introducedLocalVarsUpperBound > localVarToLocalVariableInfo[formal].layer)
+                        {
+                            Error(node, "An introduced local variable is accessed but not available");
+                        }
+                        introducedLocalVarsUpperBound = int.MinValue;
+                    }
+                }
+                for (int i = 0; i < node.Outs.Count; i++)
+                {
+                    var formal = node.Proc.OutParams[i];
+                    if (!localVarToLocalVariableInfo.ContainsKey(formal)) continue;
+                    var actual = node.Outs[i].Decl;
+                    if (localVarToLocalVariableInfo.ContainsKey(actual) && 
+                        localVarToLocalVariableInfo[formal].layer <= localVarToLocalVariableInfo[actual].layer)
+                        continue;
+                    Error(node, "Formal parameter of call must be introduced no later than the actual parameter");
+                }
+                return node;
             }
-            else
+            else if (procToAtomicProcedureInfo.ContainsKey(node.Proc))
             {
-                foreach (var ie in node.Outs)
+                var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc];                
+                if (atomicProcedureInfo.isPure)
                 {
-                    if (ghostVars.Contains(ie.Decl)) continue;
-                    Error(node, "The output of a ghost procedure must be assigned to a ghost variable");
+                    if (node.Outs.Count > 0)
+                    {
+                        int inferredLayer = int.MinValue;
+                        foreach (var ie in node.Outs)
+                        {
+                            if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl)) continue;
+                            if (inferredLayer < localVarToLocalVariableInfo[ie.Decl].layer)
+                            {
+                                inferredLayer = localVarToLocalVariableInfo[ie.Decl].layer;
+                            }
+                        }
+                        pureCallLayer[node] = inferredLayer;
+                        if (inferredLayer != int.MinValue)
+                        {
+                            foreach (var ie in node.Outs)
+                            {
+                                if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl))
+                                {
+                                    Error(node, "Output variable must be introduced");
+                                }
+                                else if (inferredLayer != localVarToLocalVariableInfo[ie.Decl].layer)
+                                {
+                                    Error(node, "All output variables must be introduced at the same layer");
+                                }
+                            }
+                        }
+                        Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+                        foreach (var e in node.Ins)
+                        {
+                            Visit(e);
+                            if (inferredLayer < introducedLocalVarsUpperBound)
+                            {
+                                Error(node, "An introduced local variable is not accessible");
+                            }
+                            introducedLocalVarsUpperBound = int.MinValue;
+                        }
+                    }
+                    else
+                    {
+                        Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+                        int inferredLayer = int.MinValue;
+                        foreach (var e in node.Ins)
+                        {
+                            Visit(e);
+                            if (inferredLayer < introducedLocalVarsUpperBound)
+                            {
+                                inferredLayer = introducedLocalVarsUpperBound;
+                            }
+                            introducedLocalVarsUpperBound = int.MinValue;
+                        }
+                        pureCallLayer[node] = inferredLayer;
+                    }
                 }
-                bool savedCanAccessSharedVars = canAccessSharedVars;
-                bool savedCanAccessAuxVars = canAccessGhostVars;
-                canAccessSharedVars = true;
-                canAccessGhostVars = true;
-                var retVal = base.VisitCallCmd(node);
-                canAccessSharedVars = savedCanAccessSharedVars;
-                canAccessGhostVars = savedCanAccessAuxVars;
-                return retVal;
+                else
+                {
+                    if (enclosingProcLayerNum != atomicProcedureInfo.layerRange.upperLayerNum)
+                    {
+                        Error(node, "Creation layer of caller must be the upper bound of the layer range of callee");
+                    }
+                    foreach (var ie in node.Proc.Modifies)
+                    {
+                        if (enclosingProcLayerNum != globalVarToSharedVarInfo[ie.Decl].introLayerNum)
+                        {
+                            Error(node, "Creation layer of caller must be identical to the introduction layer of modified variable");
+                        }
+                    }
+                    foreach (var ie in node.Outs)
+                    {
+                        if (localVarToLocalVariableInfo.ContainsKey(ie.Decl) &&
+                            enclosingProcLayerNum == localVarToLocalVariableInfo[ie.Decl].layer)
+                            continue;
+                        Error(node, "Output variable must be introduced at the creation layer of caller");
+                    }
+                }
+                return node;
+            }
+            else  
+            {
+                Error(node, "A yielding procedure can call only atomic or yielding procedures");
+                return node;
             }
         }
 
@@ -618,8 +940,8 @@ namespace Microsoft.Boogie
                 isLeftMover = isLeftMover && actionInfo.IsLeftMover;
                 isRightMover = isRightMover && actionInfo.IsRightMover;
                 if (actionInfo.createdAtLayerNum > maxCalleeLayerNum)
-                { 
-                    maxCalleeLayerNum = actionInfo.createdAtLayerNum; 
+                {
+                    maxCalleeLayerNum = actionInfo.createdAtLayerNum;
                 }
                 if (actionInfo is AtomicActionInfo)
                 {
@@ -645,66 +967,36 @@ namespace Microsoft.Boogie
             return base.VisitParCallCmd(node);
         }
 
-        public override Cmd VisitAssignCmd(AssignCmd node)
-        {
-            Contract.Ensures(Contract.Result<Cmd>() == node);
-            for (int i = 0; i < node.Lhss.Count; ++i)
-            {
-                bool savedCanAccessSharedVars = canAccessSharedVars;
-                bool savedCanAccessAuxVars = canAccessGhostVars;
-                Variable v = node.Lhss[i].DeepAssignedVariable;
-                if (v is LocalVariable && ghostVars.Contains(v))
-                {
-                    canAccessSharedVars = true;
-                    canAccessGhostVars = true;
-                }
-                this.Visit(node.Lhss[i]);
-                this.Visit(node.Rhss[i]);
-                canAccessSharedVars = savedCanAccessSharedVars;
-                canAccessGhostVars = savedCanAccessAuxVars;
-            }
-            return node;
-        }
-
         public override Expr VisitIdentifierExpr(IdentifierExpr node)
         {
             if (node.Decl is GlobalVariable)
             {
-                if (!canAccessSharedVars)
+                if (sharedVarsAccessed == null)
                 {
                     Error(node, "Shared variable can be accessed only in atomic actions or specifications");
                 }
                 else if (this.globalVarToSharedVarInfo.ContainsKey(node.Decl))
                 {
-                    if (this.globalVarToSharedVarInfo[node.Decl].hideLayerNum < minLayerNum)
-                    {
-                        minLayerNum = this.globalVarToSharedVarInfo[node.Decl].hideLayerNum;
-                    }
-                    if (this.globalVarToSharedVarInfo[node.Decl].introLayerNum > maxLayerNum)
-                    {
-                        maxLayerNum = this.globalVarToSharedVarInfo[node.Decl].introLayerNum;
-                    }
+                    sharedVarsAccessed.Add(node.Decl);
                 }
                 else
                 {
                     Error(node, "Accessed shared variable must have layer annotation");
                 }
             }
-            else if (node.Decl is LocalVariable && ghostVars.Contains(node.Decl) && !canAccessGhostVars)
+            else if ((node.Decl is Formal || node.Decl is Variable) && localVarToLocalVariableInfo.ContainsKey(node.Decl))
             {
-                Error(node, "Ghost variable can be accessed only in assertions");
-            }
-
+                var localVariableInfo = localVarToLocalVariableInfo[node.Decl];
+                if (introducedLocalVarsUpperBound < localVariableInfo.layer)
+                {
+                    introducedLocalVarsUpperBound = localVariableInfo.layer;
+                }
+            } 
             return base.VisitIdentifierExpr(node);
         }
-        
+
         public override Ensures VisitEnsures(Ensures ensures)
         {
-            minLayerNum = int.MaxValue;
-            maxLayerNum = -1;
-            canAccessSharedVars = true;
-            Ensures ret = base.VisitEnsures(ensures);
-            canAccessSharedVars = false;
             ActionInfo actionInfo = procToActionInfo[enclosingProc];
             AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
             if (atomicActionInfo != null && atomicActionInfo.ensures == ensures)
@@ -713,35 +1005,53 @@ namespace Microsoft.Boogie
             }
             else
             {
+                sharedVarsAccessed = new HashSet<Variable>();
+                Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+                base.VisitEnsures(ensures); 
                 CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.createdAtLayerNum);
+                if (introducedLocalVarsUpperBound > Least(FindLayers(ensures.Attributes)))
+                {
+                    Error(ensures, "An introduced local variable is accessed but not available");
+                }
+                introducedLocalVarsUpperBound = int.MinValue;
+                sharedVarsAccessed = null;
             }
-            return ret;
+            return ensures;
         }
-        
+
         public override Requires VisitRequires(Requires requires)
         {
-            minLayerNum = int.MaxValue;
-            maxLayerNum = -1;
-            canAccessSharedVars = true;
-            Requires ret = base.VisitRequires(requires);
-            canAccessSharedVars = false;
+            sharedVarsAccessed = new HashSet<Variable>();
+            Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+            base.VisitRequires(requires);
             CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum);
-            return ret;
+            if (introducedLocalVarsUpperBound > Least(FindLayers(requires.Attributes)))
+            {
+                Error(requires, "An introduced local variable is accessed but not available");
+            }
+            introducedLocalVarsUpperBound = int.MinValue;
+            sharedVarsAccessed = null;
+            return requires;
         }
 
         public override Cmd VisitAssertCmd(AssertCmd node)
         {
             if (enclosingImpl == null)
+            {
+                // in this case, we are visiting an assert inside a CodeExpr
                 return base.VisitAssertCmd(node);
-            minLayerNum = int.MaxValue;
-            maxLayerNum = -1;
-            canAccessSharedVars = true;
-            canAccessGhostVars = true;
-            Cmd ret = base.VisitAssertCmd(node);
-            canAccessGhostVars = false;
-            canAccessSharedVars = false;
+            }
+            sharedVarsAccessed = new HashSet<Variable>();
+            Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+            base.VisitAssertCmd(node);
             CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum);
-            return ret;
+            if (introducedLocalVarsUpperBound > Least(FindLayers(node.Attributes)))
+            {
+                Error(node, "An introduced local variable is accessed but not available");
+            }
+            introducedLocalVarsUpperBound = int.MinValue;
+            sharedVarsAccessed = null;
+            return node;
         }
 
         private List<int> RemoveDuplicatesAndSort(List<int> attrs)
@@ -760,18 +1070,15 @@ namespace Microsoft.Boogie
                 Error(node, "layer not present");
                 return;
             }
+            LayerRange upperBound = FindLayerRange();
             absyToLayerNums[node] = new HashSet<int>();
             foreach (int layerNum in attrs)
             {
-                if (layerNum == leastUnimplementedLayerNum || !AllCreatedLayerNums.Contains(layerNum))
-                {
-                    Error(node, "Illegal layer number");
-                }
-                else if (layerNum > enclosingProcLayerNum)
+                if (layerNum > enclosingProcLayerNum)
                 {
                     Error(node, "The layer cannot be greater than the layer of enclosing procedure");
                 }
-                else if (maxLayerNum < layerNum && layerNum <= minLayerNum)
+                else if (upperBound.Contains(layerNum))
                 {
                     absyToLayerNums[node].Add(layerNum);
                 }
@@ -787,5 +1094,67 @@ namespace Microsoft.Boogie
             checkingContext.Error(node, message);
             errorCount++;
         }
+
+        private class PurityChecker : StandardVisitor
+        {
+            private CivlTypeChecker civlTypeChecker;
+
+            public PurityChecker(CivlTypeChecker civlTypeChecker)
+            {
+                this.civlTypeChecker = civlTypeChecker;
+            }
+            
+            public override Cmd VisitCallCmd(CallCmd node)
+            {
+                Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc;
+                if (!civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(node.Proc))
+                {
+                    civlTypeChecker.Error(node, "Atomic procedure can only call an atomic procedure");
+                    return base.VisitCallCmd(node);
+                }
+                var callerInfo = civlTypeChecker.procToAtomicProcedureInfo[enclosingProc];
+                var calleeInfo = civlTypeChecker.procToAtomicProcedureInfo[node.Proc];
+                if (calleeInfo.isPure)
+                {
+                    // do nothing
+                }
+                else if (callerInfo.isPure)
+                {
+                    civlTypeChecker.Error(node, "Pure procedure can only call pure procedures");
+                }
+                else if (!callerInfo.layerRange.Subset(calleeInfo.layerRange))
+                {
+                    civlTypeChecker.Error(node, "Caller layers must be subset of callee layers");
+                }
+                return base.VisitCallCmd(node);
+            }
+
+            public override Cmd VisitParCallCmd(ParCallCmd node)
+            {
+                civlTypeChecker.Error(node, "Atomic procedures cannot make parallel calls");
+                return node;
+            }
+
+            public override Expr VisitIdentifierExpr(IdentifierExpr node)
+            {
+                Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc;
+                if (node.Decl is GlobalVariable)
+                {
+                    if (civlTypeChecker.procToAtomicProcedureInfo[enclosingProc].isPure)
+                    {
+                        civlTypeChecker.Error(node, "Pure procedure cannot access global variables");
+                    } 
+                    else if (!civlTypeChecker.globalVarToSharedVarInfo.ContainsKey(node.Decl))
+                    {
+                        civlTypeChecker.Error(node, "Atomic procedure cannot access a global variable without layer numbers");
+                    } 
+                    else 
+                    {
+                        civlTypeChecker.sharedVarsAccessed.Add(node.Decl);
+                    }
+                }
+                return node;
+            }
+        }
     }
-}
\ No newline at end of file
+}
diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj
index f15ebca3..113019fd 100644
--- a/Source/Concurrency/Concurrency.csproj
+++ b/Source/Concurrency/Concurrency.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
   <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
   <PropertyGroup>
@@ -73,11 +73,11 @@
   <ItemGroup>
     <Compile Include="LinearSets.cs" />
     <Compile Include="MoverCheck.cs" />
-    <Compile Include="OwickiGries.cs" />
+    <Compile Include="CivlRefinement.cs" />
     <Compile Include="Program.cs" />
     <Compile Include="Properties\AssemblyInfo.cs" />
     <Compile Include="SimulationRelation.cs" />
-    <Compile Include="TypeCheck.cs" />
+    <Compile Include="CivlTypeChecker.cs" />
     <Compile Include="YieldTypeChecker.cs" />
   </ItemGroup>
   <ItemGroup>
@@ -112,4 +112,4 @@
   <Target Name="AfterBuild">
   </Target>
   -->
-</Project>
\ No newline at end of file
+</Project>
diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index 0fa04b1b..f654b688 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -626,10 +626,9 @@ namespace Microsoft.Boogie
                 var domainName = FindDomainName(v);
                 domainNameToScope[domainName].Add(v);
             }
-            foreach (Variable v in program.GlobalVariables)
+            foreach (Variable v in globalVarToDomainName.Keys)
             {
                 var domainName = FindDomainName(v);
-                if (domainName == null) continue;
                 domainNameToScope[domainName].Add(v);
             }
             foreach (string domainName in linearDomains.Keys)
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 7c6d4ac4..732bcaa4 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -10,29 +10,29 @@ namespace Microsoft.Boogie
     public class MoverCheck
     {
         LinearTypeChecker linearTypeChecker;
-        MoverTypeChecker moverTypeChecker;
+        CivlTypeChecker civlTypeChecker;
         List<Declaration> decls;
         HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> commutativityCheckerCache;
         HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> gatePreservationCheckerCache;
         HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> failurePreservationCheckerCache;
-        private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
+        private MoverCheck(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls)
         {
             this.linearTypeChecker = linearTypeChecker;
-            this.moverTypeChecker = moverTypeChecker;
+            this.civlTypeChecker = civlTypeChecker;
             this.decls = decls;
             this.commutativityCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
             this.gatePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
             this.failurePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
         }
 
-        public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
+        public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls)
         {
-            if (moverTypeChecker.procToActionInfo.Count == 0)
+            if (civlTypeChecker.procToActionInfo.Count == 0)
                 return;
 
-            List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
+            List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(civlTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
             sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; });
-            List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
+            List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(civlTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
             sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; });
 
             Dictionary<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>();
@@ -60,8 +60,8 @@ namespace Microsoft.Boogie
                 currPool = pools[currLayerNum];
             }
 
-            Program program = moverTypeChecker.program;
-            MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls);
+            Program program = civlTypeChecker.program;
+            MoverCheck moverChecking = new MoverCheck(linearTypeChecker, civlTypeChecker, decls);
             foreach (int layerNum in pools.Keys)
             {
                 foreach (AtomicActionInfo first in pools[layerNum])
@@ -537,7 +537,7 @@ namespace Microsoft.Boogie
             ensures.Add(ensureCheck);
             string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);
             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
-            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
+            civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks);
             impl.Proc = proc;
@@ -580,7 +580,7 @@ namespace Microsoft.Boogie
                 requires.Add(new Requires(false, assertCmd.Expr));
             string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
-            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
+            civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);
             impl.Proc = proc;
@@ -628,7 +628,7 @@ namespace Microsoft.Boogie
                 requires.Add(new Requires(false, assertCmd.Expr));
             string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
-            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
+            civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);
             impl.Proc = proc;
@@ -662,7 +662,7 @@ namespace Microsoft.Boogie
             blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));
             string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name);
             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
-            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
+            civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures);
             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);
             impl.Proc = proc;
diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs
index b56e1cf3..1be7cc07 100644
--- a/Source/Concurrency/Program.cs
+++ b/Source/Concurrency/Program.cs
@@ -7,20 +7,20 @@ namespace Microsoft.Boogie
 {
     public class Concurrency
     {
-        public static void Transform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)
+        public static void Transform(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker)
         {
             List<Declaration> originalDecls = new List<Declaration>();
             Program program = linearTypeChecker.program;
             foreach (var decl in program.TopLevelDeclarations)
             {
                 Procedure proc = decl as Procedure;
-                if (proc != null && moverTypeChecker.procToActionInfo.ContainsKey(proc))
+                if (proc != null && civlTypeChecker.procToActionInfo.ContainsKey(proc))
                 {
                     originalDecls.Add(proc);
                     continue;
                 }
                 Implementation impl = decl as Implementation;
-                if (impl != null && moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc))
+                if (impl != null && civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc))
                 {
                     originalDecls.Add(impl);
                 }
@@ -29,12 +29,12 @@ namespace Microsoft.Boogie
             List<Declaration> decls = new List<Declaration>();
             if (!CommandLineOptions.Clo.TrustAtomicityTypes)
             {
-                MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
+                MoverCheck.AddCheckers(linearTypeChecker, civlTypeChecker, decls);
             } 
-            OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
+            CivlRefinement.AddCheckers(linearTypeChecker, civlTypeChecker, decls);
             foreach (Declaration decl in decls)
             {
-                decl.Attributes = OwickiGries.RemoveYieldsAttribute(decl.Attributes);
+                decl.Attributes = CivlRefinement.RemoveYieldsAttribute(decl.Attributes);
             }
             program.RemoveTopLevelDeclarations(x => originalDecls.Contains(x));
             program.AddTopLevelDeclarations(decls);
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index a698c8fd..ed59d3ad 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -81,7 +81,7 @@ namespace Microsoft.Boogie
             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();
             if (simulationRelation[initialState].Count == 0)
             {
-                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum));
+                civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum));
             }
         }
 
@@ -97,7 +97,7 @@ namespace Microsoft.Boogie
             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();
             if (simulationRelation[initialState].Count == 0)
             {
-                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum));
+                civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum));
             }
         }
 
@@ -115,7 +115,7 @@ namespace Microsoft.Boogie
             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();
             if (simulationRelation[initialState].Count == 0)
             {
-                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum));
+                civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum));
             }
         }
 
@@ -124,7 +124,7 @@ namespace Microsoft.Boogie
             foreach (Cmd cmd in block.Cmds)
             {
                 AssertCmd assertCmd = cmd as AssertCmd;
-                if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && moverTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum))
+                if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && civlTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum))
                 {
                     return true;
                 }
@@ -132,25 +132,25 @@ namespace Microsoft.Boogie
             return false;
         }
         
-        public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker)
+        public static void PerformYieldSafeCheck(CivlTypeChecker civlTypeChecker)
         {
-            foreach (var impl in moverTypeChecker.program.Implementations)
+            foreach (var impl in civlTypeChecker.program.Implementations)
             {
-                if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue;
+                if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue;
                 impl.PruneUnreachableBlocks();
                 Graph<Block> implGraph = Program.GraphFromImpl(impl);
                 implGraph.ComputeLoops();
-                int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;
-                foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))
+                int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;
+                foreach (int layerNum in civlTypeChecker.AllLayerNums)
                 {
                     if (layerNum > specLayerNum) continue;
-                    YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers);
+                    YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers);
                 }
             }
         }
 
         int stateCounter;
-        MoverTypeChecker moverTypeChecker;
+        CivlTypeChecker civlTypeChecker;
         Implementation impl;
         int currLayerNum;
         Dictionary<Absy, int> absyToNode;
@@ -160,9 +160,9 @@ namespace Microsoft.Boogie
         Dictionary<Tuple<int, int>, int> edgeLabels;
         IEnumerable<Block> loopHeaders;
 
-        private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders)
+        private YieldTypeChecker(CivlTypeChecker civlTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders)
         {
-            this.moverTypeChecker = moverTypeChecker;
+            this.civlTypeChecker = civlTypeChecker;
             this.impl = impl;
             this.currLayerNum = currLayerNum;
             this.loopHeaders = loopHeaders;
@@ -226,20 +226,20 @@ namespace Microsoft.Boogie
                         CallCmd callCmd = cmd as CallCmd;
                         if (callCmd.IsAsync)
                         {
-                            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+                            ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc];
                             if (currLayerNum <= actionInfo.createdAtLayerNum)
                                 edgeLabels[edge] = 'L';
                             else
                                 edgeLabels[edge] = 'B';
                         }
-                        else if (!moverTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc))
+                        else if (!civlTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc))
                         {
                             edgeLabels[edge] = 'P';
                         }
                         else
                         {
                             MoverType moverType;
-                            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+                            ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc];
                             if (actionInfo.createdAtLayerNum >= currLayerNum)
                             {
                                 moverType = MoverType.Top;
@@ -280,7 +280,7 @@ namespace Microsoft.Boogie
                         bool isLeftMover = true;
                         foreach (CallCmd callCmd in parCallCmd.CallCmds)
                         {
-                            if (moverTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum)
+                            if (civlTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum)
                             {
                                 isYield = true;
                             }
@@ -294,7 +294,7 @@ namespace Microsoft.Boogie
                             int numAtomicActions = 0;
                             foreach (CallCmd callCmd in parCallCmd.CallCmds)
                             {
-                                ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+                                ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc];
                                 isRightMover = isRightMover && actionInfo.IsRightMover;
                                 isLeftMover = isLeftMover && actionInfo.IsLeftMover;
                                 if (actionInfo is AtomicActionInfo)
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 36c99b7b..8a8558bf 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -696,6 +696,8 @@ namespace Microsoft.Boogie {
       }
     }
 
+    public readonly ISet<string> NecessaryAssumes = new HashSet<string>();
+
     public IEnumerable<Block> Blocks()
     {
       return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item);
@@ -733,6 +735,45 @@ namespace Microsoft.Boogie {
       }
     }
 
+
+    /// <summary>
+    /// Finds blocks that break out of a loop in NaturalLoops(header, backEdgeNode)
+    /// </summary>
+    /// <param name="header"></param>
+    /// <param name="backEdgeNode"></param>
+    /// <returns></returns>
+    private HashSet<Block> GetBreakBlocksOfLoop(Block header, Block backEdgeNode, Graph<Block/*!*/>/*!*/ g)
+    {
+        Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option");
+        var immSuccBlks = new HashSet<Block>();
+        var loopBlocks = g.NaturalLoops(header, backEdgeNode);
+        foreach (Block/*!*/ block in loopBlocks)
+        {
+            Contract.Assert(block != null);
+            var auxCmd = block.TransferCmd as GotoCmd;
+            if (auxCmd == null) continue;
+            foreach (var bl in auxCmd.labelTargets)
+            {
+                if (loopBlocks.Contains(bl)) continue;
+                immSuccBlks.Add(bl);
+            }
+        }
+        return immSuccBlks;
+    }
+
+    private HashSet<Block> GetBlocksInAllNaturalLoops(Block header, Graph<Block/*!*/>/*!*/ g)
+    {
+        Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option");
+        var allBlocksInNaturalLoops = new HashSet<Block>();
+        foreach (Block/*!*/ source in g.BackEdgeNodes(header))
+        {
+            Contract.Assert(source != null);
+            g.NaturalLoops(header, source).Iter(b => allBlocksInNaturalLoops.Add(b));
+        }
+        return allBlocksInNaturalLoops;
+    }
+
+
     void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g,
                                   List<Implementation/*!*/>/*!*/ loopImpls,
                                   Dictionary<string, Dictionary<string, Block>> fullMap) {
@@ -788,7 +829,13 @@ namespace Microsoft.Boogie {
         foreach (Block/*!*/ b in g.BackEdgeNodes(header))
         {
             Contract.Assert(b != null);
-            foreach (Block/*!*/ block in g.NaturalLoops(header, b))
+            HashSet<Block> immSuccBlks = new HashSet<Block>();
+            if (detLoopExtract)
+            {
+                //Need to get the blocks that exit the loop, as we need to add them to targets and footprint
+                immSuccBlks = GetBreakBlocksOfLoop(header, b, g);
+            }
+            foreach (Block/*!*/ block in g.NaturalLoops(header, b).Union(immSuccBlks))
             {
                 Contract.Assert(block != null);
                 foreach (Cmd/*!*/ cmd in block.Cmds)
@@ -943,18 +990,16 @@ namespace Microsoft.Boogie {
                 GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd;
                 Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null && 
                     auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1);
+                //BUGFIX on 10/26/15: this contains nodes present in NaturalLoops for a different backedgenode
+                var loopNodes = GetBlocksInAllNaturalLoops(header, g); //var loopNodes = g.NaturalLoops(header, source); 
                 foreach(var bl in auxGotoCmd.labelTargets) {
-                    bool found = false;
-                    foreach(var n in g.NaturalLoops(header, source)) { //very expensive, can we do a contains?
-                        if (bl == n) { //clarify: is this the right comparison?
-                            found = true;
-                            break;
-                        }
-                    }
-                    if (!found) {
+                    if (g.Nodes.Contains(bl) && //newly created blocks are not present in NaturalLoop(header, xx, g)
+                        !loopNodes.Contains(bl)) {
                         Block auxNewBlock = new Block();
                         auxNewBlock.Label = ((Block)bl).Label;
-                        auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds);
+                        //these blocks may have read/write locals that are not present in naturalLoops
+                        //we need to capture these variables 
+                        auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds); 
                         //add restoration code for such blocks
                         if (loopHeaderToAssignCmd.ContainsKey(header))
                         {
@@ -2196,6 +2241,7 @@ namespace Microsoft.Boogie {
   }
   public class Incarnation : LocalVariable {
     public int incarnationNumber;
+    public readonly Variable OriginalVariable;
     public Incarnation(Variable/*!*/ var, int i) :
       base(
       var.tok,
@@ -2203,6 +2249,7 @@ namespace Microsoft.Boogie {
       ) {
       Contract.Requires(var != null);
       incarnationNumber = i;
+      OriginalVariable = var;
     }
 
   }
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 404945a9..2e33e1dd 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2463,6 +2463,12 @@ namespace Microsoft.Boogie {
       } finally {
         rc.TypeBinderState = previousTypeBinderState;
       }
+
+      var id = QKeyValue.FindStringAttribute(Attributes, "id");
+      if (id != null)
+      {
+        rc.AddStatementId(tok, id);
+      }
     }
 
     public override void AddAssignedVariables(List<Variable> vars) {
@@ -2890,6 +2896,12 @@ namespace Microsoft.Boogie {
     public override void Resolve(ResolutionContext rc) {
       //Contract.Requires(rc != null);
       Expr.Resolve(rc);
+
+      var id = QKeyValue.FindStringAttribute(Attributes, "id");
+      if (id != null)
+      {
+        rc.AddStatementId(tok, id);
+      }
     }
     public override void AddAssignedVariables(List<Variable> vars) {
       //Contract.Requires(vars != null);
@@ -3206,8 +3218,14 @@ namespace Microsoft.Boogie {
       this.Expr.Emit(stream);
       stream.WriteLine(";");
     }
+    public override void Resolve(ResolutionContext rc) {
+      //Contract.Requires(rc != null);
+      ResolveAttributes(Attributes, rc);
+      base.Resolve(rc);
+    }
     public override void Typecheck(TypecheckingContext tc) {
       //Contract.Requires(tc != null);
+      TypecheckAttributes(Attributes, tc);
       Expr.Typecheck(tc);
       Contract.Assert(Expr.Type != null);  // follows from Expr.Typecheck postcondition
       if (!Expr.Type.Unify(Type.Bool)) {
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 9f94490b..3a27eddf 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -338,6 +338,17 @@ namespace Microsoft.Boogie {
 
     public override void Resolve(ResolutionContext rc) {
       //Contract.Requires(rc != null);
+
+      if ((Key == "minimize" || Key == "maximize") && Params.Count != 1)
+      {
+        rc.Error(this, "attributes :minimize and :maximize accept only one argument");
+      }
+
+      if (Key == "verified_under" && Params.Count != 1)
+      {
+        rc.Error(this, "attribute :verified_under accepts only one argument");
+      }
+
       foreach (object p in Params) {
         if (p is Expr) {
           ((Expr)p).Resolve(rc);
@@ -348,8 +359,20 @@ namespace Microsoft.Boogie {
     public override void Typecheck(TypecheckingContext tc) {
       //Contract.Requires(tc != null);
       foreach (object p in Params) {
-        if (p is Expr) {
-          ((Expr)p).Typecheck(tc);
+        var expr = p as Expr;
+        if (expr != null) {
+          expr.Typecheck(tc);
+        }
+        if ((Key == "minimize" || Key == "maximize")
+            && (expr == null || !(expr.Type.IsInt || expr.Type.IsReal || expr.Type.IsBv)))
+        {
+          tc.Error(this, "attributes :minimize and :maximize accept only one argument of type int, real or bv");
+          break;
+        }
+        if (Key == "verified_under" && (expr == null || !expr.Type.IsBool))
+        {
+          tc.Error(this, "attribute :verified_under accepts only one argument of type bool");
+          break;
         }
       }
     }
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 2be1cdf7..e9aa3ceb 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -11,6 +11,7 @@ using System.IO;
 using System.Linq;
 using System.Diagnostics;
 using System.Diagnostics.Contracts;
+using System.Text.RegularExpressions;
 
 namespace Microsoft.Boogie {
   public class CommandLineOptionEngine
@@ -478,6 +479,8 @@ namespace Microsoft.Boogie {
     public string AbstractHoudini = null;
     public bool UseUnsatCoreForContractInfer = false;
     public bool PrintAssignment = false;
+    // TODO(wuestholz): Add documentation for this flag.
+    public bool PrintNecessaryAssumes = false;
     public int InlineDepth = -1;
     public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values
     public bool UseUncheckedContracts = false;
@@ -588,7 +591,7 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public string OwickiGriesDesugaredOutputFile = null;
+    public string CivlDesugaredFile = null;
     public bool TrustAtomicityTypes = false;
     public bool TrustNonInterference = false;
     public int TrustLayersUpto = -1;
@@ -915,9 +918,9 @@ namespace Microsoft.Boogie {
           } 
           return true;
 
-        case "OwickiGries":
+        case "CivlDesugaredFile":
           if (ps.ConfirmArgumentCount(1)) {
-              OwickiGriesDesugaredOutputFile = args[ps.i];
+              CivlDesugaredFile = args[ps.i];
           }
           return true;
 
@@ -1502,7 +1505,7 @@ namespace Microsoft.Boogie {
           return true;
 
         case "verifySnapshots":
-          ps.GetNumericArgument(ref VerifySnapshots, 3);
+          ps.GetNumericArgument(ref VerifySnapshots, 4);
           return true;
 
         case "traceCaching":
@@ -1618,6 +1621,7 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) ||
               ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||
               ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
+              ps.CheckBooleanFlag("printNecessaryAssumes", ref PrintNecessaryAssumes) ||
               ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) ||
               ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
               ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
@@ -1700,7 +1704,7 @@ namespace Microsoft.Boogie {
         // no preference
         return true;
       }
-      return ProcsToCheck.Contains(methodFullname);
+      return ProcsToCheck.Any(s => Regex.IsMatch(methodFullname, "^" + Regex.Escape(s).Replace(@"\*", ".*") + "$"));
     }
 
     public virtual StringCollection ParseNamedArgumentList(string argList) {
@@ -1857,7 +1861,15 @@ namespace Microsoft.Boogie {
   Multiple .bpl files supplied on the command line are concatenated into one
   Boogie program.
 
-  /proc:<p>      : limits which procedures to check
+  /proc:<p>      : Only check procedures matched by pattern <p>. This option
+                   may be specified multiple times to match multiple patterns.
+                   The pattern <p> matches the whole procedure name (i.e.
+                   pattern ""foo"" will only match a procedure called foo and
+                   not fooBar). The pattern <p> may contain * wildcards which
+                   match any character zero or more times. For example the
+                   pattern ""ab*d"" would match abd, abcd and abccd but not
+                   Aabd nor abdD. The pattern ""*ab*d*"" would match abd,
+                   abcd, abccd, Abd and abdD.
   /noResolve     : parse only
   /noTypecheck   : parse and resolve only
 
@@ -1961,6 +1973,10 @@ namespace Microsoft.Boogie {
                 0 - do not use any verification result caching (default)
                 1 - use the basic verification result caching
                 2 - use the more advanced verification result caching
+                3 - use the more advanced caching and report errors according
+                    to the new source locations for errors and their
+                    related locations (but not /errorTrace and CaptureState
+                    locations) 
   /verifySeparately
                 verify each input program separately
   /removeEmptyBlocks:<c>
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 474a91dd..279e00bf 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -339,6 +339,18 @@ namespace Microsoft.Boogie {
       varContext = varContext.ParentContext;
     }
 
+    public readonly ISet<string> StatementIds = new HashSet<string>();
+
+    public void AddStatementId(IToken tok, string name)
+    {
+      if (StatementIds.Contains(name))
+      {
+        Error(tok, "more than one statement with same id: " + name);
+        return;
+      }
+      StatementIds.Add(name);
+    }
+
     public void AddVariable(Variable var, bool global) {
       Contract.Requires(var != null);
       var previous = FindVariable(cce.NonNull(var.Name), !global);
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index f2d58045..9bc855be 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -135,7 +135,7 @@ namespace Microsoft.Boogie
 
       foreach (var e in errorInfo.Aux)
       {
-        if (!(skipExecutionTrace && e.Category.Contains("Execution trace")))
+        if (!(skipExecutionTrace && e.Category != null && e.Category.Contains("Execution trace")))
         {
           ReportBplError(e.Tok, e.FullMsg, false, tw);
         }
@@ -151,25 +151,18 @@ namespace Microsoft.Boogie
     {
       Contract.Requires(message != null);
 
-      if (category != null)
-      {
+      if (category != null) {
         message = string.Format("{0}: {1}", category, message);
       }
       string s;
-      if (tok != null)
-      {
+      if (tok != null) {
         s = string.Format("{0}({1},{2}): {3}", ExecutionEngine.GetFileNameForConsole(tok.filename), tok.line, tok.col, message);
-      }
-      else
-      {
+      } else {
         s = message;
       }
-      if (error)
-      {
+      if (error) {
         ErrorWriteLine(tw, s);
-      }
-      else
-      {
+      } else {
         tw.WriteLine(s);
       }
     }
@@ -489,8 +482,8 @@ namespace Microsoft.Boogie
         }
 
         LinearTypeChecker linearTypeChecker;
-        MoverTypeChecker moverTypeChecker;
-        PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out moverTypeChecker);
+        CivlTypeChecker civlTypeChecker;
+        PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out civlTypeChecker);
         if (oc != PipelineOutcome.ResolvedAndTypeChecked)
           return;
 
@@ -507,13 +500,13 @@ namespace Microsoft.Boogie
 
         if (CommandLineOptions.Clo.StratifiedInlining == 0)
         {
-          Concurrency.Transform(linearTypeChecker, moverTypeChecker);
+          Concurrency.Transform(linearTypeChecker, civlTypeChecker);
           (new LinearEraser()).VisitProgram(program);
-          if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)
+          if (CommandLineOptions.Clo.CivlDesugaredFile != null)
           {
               int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
               CommandLineOptions.Clo.PrintUnstructured = 1;
-              PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false, CommandLineOptions.Clo.PrettyPrint);
+              PrintBplFile(CommandLineOptions.Clo.CivlDesugaredFile, program, false, false, CommandLineOptions.Clo.PrettyPrint);
               CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
           }
         }
@@ -699,13 +692,13 @@ namespace Microsoft.Boogie
     ///  - TypeCheckingError if a type checking error occurred
     ///  - ResolvedAndTypeChecked if both resolution and type checking succeeded
     /// </summary>
-    public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker, out MoverTypeChecker moverTypeChecker)
+    public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker, out CivlTypeChecker civlTypeChecker)
     {
       Contract.Requires(program != null);
       Contract.Requires(bplFileName != null);
 
       linearTypeChecker = null;
-      moverTypeChecker = null;
+      civlTypeChecker = null;
 
       // ---------- Resolve ------------------------------------------------------------
 
@@ -742,11 +735,11 @@ namespace Microsoft.Boogie
 
       CollectModSets(program);
 
-      moverTypeChecker = new MoverTypeChecker(program);
-      moverTypeChecker.TypeCheck();
-      if (moverTypeChecker.errorCount != 0)
+      civlTypeChecker = new CivlTypeChecker(program);
+      civlTypeChecker.TypeCheck();
+      if (civlTypeChecker.errorCount != 0)
       {
-          Console.WriteLine("{0} type checking errors detected in {1}", moverTypeChecker.errorCount, GetFileNameForConsole(bplFileName));
+          Console.WriteLine("{0} type checking errors detected in {1}", civlTypeChecker.errorCount, GetFileNameForConsole(bplFileName));
           return PipelineOutcome.TypeCheckingError;
       }
 
@@ -1015,6 +1008,11 @@ namespace Microsoft.Boogie
         CleanupCheckers(requestId);
       }
 
+      if (CommandLineOptions.Clo.PrintNecessaryAssumes && program.NecessaryAssumes.Any())
+      {
+        Console.WriteLine("Necessary assume command(s): {0}", string.Join(", ", program.NecessaryAssumes));
+      }
+
       cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
 
       outputCollector.WriteMoreOutput();
@@ -1114,23 +1112,23 @@ namespace Microsoft.Boogie
       printer.Inform(string.Format("Verifying {0} ...", impl.Name), output);
 
       int priority = 0;
-      if (0 < CommandLineOptions.Clo.VerifySnapshots)
-      {
-        verificationResult = Cache.Lookup(impl, out priority);
-      }
-
       var wasCached = false;
-      if (verificationResult != null && priority == Priority.SKIP)
-      {
-        if (CommandLineOptions.Clo.XmlSink != null)
-        {
-          CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
-        }
+      if (0 < CommandLineOptions.Clo.VerifySnapshots) {
+        var cachedResults = Cache.Lookup(impl, out priority);
+        if (cachedResults != null && priority == Priority.SKIP) {
+          if (CommandLineOptions.Clo.XmlSink != null) {
+            CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, cachedResults.Start);
+          }
 
-        printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);
-        wasCached = true;
+          printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);
+          if (CommandLineOptions.Clo.VerifySnapshots < 3 || cachedResults.Outcome == ConditionGeneration.Outcome.Correct) {
+            verificationResult = cachedResults;
+            wasCached = true;
+          }
+        }
       }
-      else
+
+      if (!wasCached)
       {
         #region Verify the implementation
 
@@ -1365,8 +1363,8 @@ namespace Microsoft.Boogie
       Program p = ParseBoogieProgram(new List<string> { filename }, false);
       System.Diagnostics.Debug.Assert(p != null);
       LinearTypeChecker linearTypeChecker;
-      MoverTypeChecker moverTypeChecker;
-      PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker, out moverTypeChecker);
+      CivlTypeChecker civlTypeChecker;
+      PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker, out civlTypeChecker);
       System.Diagnostics.Debug.Assert(oc == PipelineOutcome.ResolvedAndTypeChecked);
       return p;
     }
@@ -1466,11 +1464,11 @@ namespace Microsoft.Boogie
 
       printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);
 
-      ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit);
+      ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit, errors);
     }
 
 
-    private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit)
+    private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit, List<Counterexample> errors)
     {
       ErrorInformation errorInfo = null;
 
@@ -1479,10 +1477,69 @@ namespace Microsoft.Boogie
         case VCGen.Outcome.ReachedBound:
           tw.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));
           break;
+        case VCGen.Outcome.Errors:
         case VCGen.Outcome.TimedOut:
           if (implName != null && implTok != null)
           {
-            errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId);
+            if (outcome == ConditionGeneration.Outcome.TimedOut || (errors != null && errors.Any(e => e.IsAuxiliaryCexForDiagnosingTimeouts)))
+            {
+              errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification of '{1}' timed out after {0} seconds", timeLimit, implName), requestId);
+            }
+
+            //  Report timed out assertions as auxiliary info.
+            if (errors != null)
+            {
+              var cmpr = new CounterexampleComparer();
+              var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(cmpr).ToList();
+              timedOutAssertions.Sort(cmpr);
+              if (0 < timedOutAssertions.Count)
+              {
+                errorInfo.Msg += string.Format(" with {0} check(s) that timed out individually", timedOutAssertions.Count);
+              }
+              foreach (Counterexample error in timedOutAssertions)
+              {
+                var callError = error as CallCounterexample;
+                var returnError = error as ReturnCounterexample;
+                var assertError = error as AssertCounterexample;
+                IToken tok = null;
+                string msg = null;
+                if (callError != null)
+                {
+                  tok = callError.FailingCall.tok;
+                  msg = callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.";
+                }
+                else if (returnError != null)
+                {
+                  tok = returnError.FailingReturn.tok;
+                  msg = "A postcondition might not hold on this return path.";
+                }
+                else
+                {
+                  tok = assertError.FailingAssert.tok;
+                  if (assertError.FailingAssert is LoopInitAssertCmd)
+                  {
+                    msg = "This loop invariant might not hold on entry.";
+                  }
+                  else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd)
+                  {
+                    msg = "This loop invariant might not be maintained by the loop.";
+                  }
+                  else
+                  {
+                    msg = assertError.FailingAssert.ErrorData as string;
+                    if (!CommandLineOptions.Clo.ForceBplErrors && assertError.FailingAssert.ErrorMessage != null)
+                    {
+                      msg = assertError.FailingAssert.ErrorMessage;
+                    }
+                    if (msg == null)
+                    {
+                      msg = "This assertion might not hold.";
+                    }
+                  }
+                }
+                errorInfo.AddAuxInfo(tok, msg, "Unverified check due to timeout");
+              }
+            }
           }
           break;
         case VCGen.Outcome.OutOfMemory:
@@ -1509,6 +1566,10 @@ namespace Microsoft.Boogie
             er(errorInfo);
           }
         }
+        else
+        {
+          printer.WriteErrorInformation(errorInfo, tw);
+        }
       }
     }
 
@@ -1582,8 +1643,9 @@ namespace Microsoft.Boogie
           }
           else
           {
-            Interlocked.Add(ref stats.ErrorCount, errors.Count);
-            if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, errors.Count); }
+            int cnt = errors.Where(e => !e.IsAuxiliaryCexForDiagnosingTimeouts).Count();
+            Interlocked.Add(ref stats.ErrorCount, cnt);
+            if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, cnt); }
           }
           break;
       }
@@ -1599,6 +1661,10 @@ namespace Microsoft.Boogie
         errors.Sort(new CounterexampleComparer());
         foreach (Counterexample error in errors)
         {
+          if (error.IsAuxiliaryCexForDiagnosingTimeouts)
+          {
+            continue;
+          }
           var errorInfo = CreateErrorInformation(error, outcome);
           errorInfo.ImplementationName = implName;
 
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index dfe32103..3159238c 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -172,48 +172,28 @@ namespace Microsoft.Boogie
         var vr = ExecutionEngine.Cache.Lookup(impl, out priority);
         if (vr != null && vr.ProgramId == programId)
         {
-          if (priority == Priority.LOW)
-          {
+          if (priority == Priority.LOW) {
             run.LowPriorityImplementationCount++;
-            if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)
-            {
-              SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);
-              if (vr.ProgramId != null)
-              {
-                var p = ExecutionEngine.CachedProgram(vr.ProgramId);
-                if (p != null)
-                {
-                  eai.Inject(impl, p);
-                  run.TransformedImplementationCount++;
-                }
-              }
-            }
-          }
-          else if (priority == Priority.MEDIUM)
-          {
+          } else if (priority == Priority.MEDIUM) {
             run.MediumPriorityImplementationCount++;
-            if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)
-            {
+          } else if (priority == Priority.HIGH) {
+            run.HighPriorityImplementationCount++;
+          } else if (priority == Priority.SKIP) {
+            run.SkippedImplementationCount++;
+          }
+
+          if (priority == Priority.LOW || priority == Priority.MEDIUM || 3 <= CommandLineOptions.Clo.VerifySnapshots) {
+            if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds) {
               SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);
-              if (vr.ProgramId != null)
-              {
+              if (vr.ProgramId != null) {
                 var p = ExecutionEngine.CachedProgram(vr.ProgramId);
-                if (p != null)
-                {
+                if (p != null) {
                   eai.Inject(impl, p);
                   run.TransformedImplementationCount++;
                 }
               }
             }
           }
-          else if (priority == Priority.HIGH)
-          {
-            run.HighPriorityImplementationCount++;
-          }
-          else if (priority == Priority.SKIP)
-          {
-            run.SkippedImplementationCount++;
-          }
         }
       }
       run.End = DateTime.UtcNow;
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index e93ecee9..300fbc10 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -86,6 +86,21 @@ namespace Microsoft.Boogie.SMTLib
       }
     }
 
+    public override void AssertNamed(VCExpr vc, bool polarity, string name)
+    {
+      string vcString;
+      if (polarity)
+      {
+        vcString = VCExpr2String(vc, 1);
+      }
+      else
+      {
+        vcString = "(not " + VCExpr2String(vc, 1) + ")";
+      }
+      AssertAxioms();
+      SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name));
+    }
+
     private void SetupAxiomBuilder(VCExpressionGenerator gen)
     {
       switch (CommandLineOptions.Clo.TypeEncodingMethod)
@@ -246,9 +261,9 @@ namespace Microsoft.Boogie.SMTLib
 
         // Set produce-unsat-cores last. It seems there's a bug in Z3 where if we set it earlier its value
         // gets reset by other set-option commands ( https://z3.codeplex.com/workitem/188 )
-        if (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini))
+        if (CommandLineOptions.Clo.PrintNecessaryAssumes || (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini)))
         {
-          SendThisVC("(set-option :produce-unsat-cores true)");
+          SendCommon("(set-option :produce-unsat-cores true)");
           this.usingUnsatCore = true;
         }
 
@@ -401,6 +416,8 @@ namespace Microsoft.Boogie.SMTLib
 
       PrepareCommon();
 
+      OptimizationRequests.Clear();
+
       string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
       FlushAxioms();
 
@@ -408,7 +425,11 @@ namespace Microsoft.Boogie.SMTLib
 
       SendThisVC("(push 1)");
       SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
+
       SendThisVC(vcString);
+
+      SendOptimizationRequests();
+
       FlushLogFile();
 
       if (Process != null) {
@@ -418,10 +439,21 @@ namespace Microsoft.Boogie.SMTLib
           Process.Inspector.NewProblem(descriptiveName, vc, handler);
       }
 
-      SendThisVC("(check-sat)");
+      SendCheckSat();
       FlushLogFile();
     }
 
+    private void SendOptimizationRequests()
+    {
+      if (options.Solver == SolverKind.Z3 && 0 < OptimizationRequests.Count)
+      {
+        foreach (var r in OptimizationRequests)
+        {
+          SendThisVC(r);
+        }
+      }
+    }
+
     public override void Reset(VCExpressionGenerator gen)
     {
       if (options.Solver == SolverKind.Z3)
@@ -446,6 +478,7 @@ namespace Microsoft.Boogie.SMTLib
       if (options.Solver == SolverKind.Z3)
       {
         this.gen = gen;
+        SendThisVC("(reset)");
         Namer.Reset();
         common.Clear();
         SetupAxiomBuilder(gen);
@@ -456,6 +489,8 @@ namespace Microsoft.Boogie.SMTLib
         ctx.KnownDatatypeConstructors.Clear();
         ctx.parent = this;
         DeclCollector.Reset();
+        NamedAssumes.Clear();
+        UsedNamedAssumes = null;
         SendThisVC("; did a full reset");
       }
     }
@@ -1264,6 +1299,38 @@ namespace Microsoft.Boogie.SMTLib
             
             result = GetResponse();
 
+            var reporter = handler as VC.VCGen.ErrorReporter;
+            // TODO(wuestholz): Is the reporter ever null?
+            if (usingUnsatCore && result == Outcome.Valid && reporter != null && 0 < NamedAssumes.Count)
+            {
+              if (usingUnsatCore)
+              {
+                UsedNamedAssumes = new HashSet<string>();
+                SendThisVC("(get-unsat-core)");
+                var resp = Process.GetProverResponse();
+                if (resp.Name != "")
+                {
+                  UsedNamedAssumes.Add(resp.Name);
+                  if (CommandLineOptions.Clo.PrintNecessaryAssumes)
+                  {
+                    reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length));
+                  }
+                }
+                foreach (var arg in resp.Arguments)
+                {
+                  UsedNamedAssumes.Add(arg.Name);
+                  if (CommandLineOptions.Clo.PrintNecessaryAssumes)
+                  {
+                    reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length));
+                  }
+                }
+              }
+              else
+              {
+                UsedNamedAssumes = null;
+              }
+            }
+
             if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut)
             {
               #region Run timeout diagnostics
@@ -1423,13 +1490,13 @@ namespace Microsoft.Boogie.SMTLib
               expr = "false";
             }
             SendThisVC("(assert " + expr + ")");
-            SendThisVC("(check-sat)");
+            SendCheckSat();
           }
           else {
             string source = labels[labels.Length - 2];
             string target = labels[labels.Length - 1];
             SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") (- " + target + "))))");
-            SendThisVC("(check-sat)");
+            SendCheckSat();
           }
         }
 
@@ -1474,7 +1541,7 @@ namespace Microsoft.Boogie.SMTLib
         SendThisVC("(apply (then (using-params propagate-values :max_rounds 1) simplify) :print false)");
       }
       FlushLogFile();
-      SendThisVC("(check-sat)");
+      SendCheckSat();
       queries++;
       return GetResponse();
     }
@@ -1812,6 +1879,7 @@ namespace Microsoft.Boogie.SMTLib
     private Model GetErrorModel() {
       if (!options.ExpectingModel())
         return null;
+
       SendThisVC("(get-model)");
       Process.Ping();
       Model theModel = null;
@@ -1906,6 +1974,9 @@ namespace Microsoft.Boogie.SMTLib
             result = Outcome.Invalid;
             wasUnknown = true;
             break;
+          case "objectives":
+            // We ignore this.
+            break;
           default:
             HandleProverError("Unexpected prover response: " + resp.ToString());
             break;
@@ -1944,6 +2015,8 @@ namespace Microsoft.Boogie.SMTLib
       return result;
     }
 
+    readonly IList<string> OptimizationRequests = new List<string>();
+
     protected string VCExpr2String(VCExpr expr, int polarity)
     {
       Contract.Requires(expr != null);
@@ -1983,10 +2056,8 @@ namespace Microsoft.Boogie.SMTLib
         DeclCollector.Collect(sortedExpr);
         FeedTypeDeclsToProver();
 
-
-
-        AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options));
-        string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options);
+        AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options, namedAssumes: NamedAssumes));
+        string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, NamedAssumes, OptimizationRequests);
         Contract.Assert(res != null);
 
         if (CommandLineOptions.Clo.Trace)
@@ -2094,19 +2165,20 @@ namespace Microsoft.Boogie.SMTLib
         throw new NotImplementedException();
     }
 
-    public override void Assert(VCExpr vc, bool polarity)
+    public override void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1)
     {
-        string a = "";
-        if (polarity)
-        {
-            a = "(assert " + VCExpr2String(vc, 1) + ")";
+        OptimizationRequests.Clear();
+        string assert = "assert";
+        if (options.Solver == SolverKind.Z3 && isSoft) {
+            assert += "-soft";
         }
-        else
-        {
-            a = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
+        var expr = polarity ? VCExpr2String(vc, 1) : "(not\n" + VCExpr2String(vc, 1) + "\n)";
+        if (options.Solver == SolverKind.Z3 && isSoft) {
+            expr += " :weight " + weight;
         }
         AssertAxioms();
-        SendThisVC(a);
+        SendThisVC("(" + assert + " " + expr + ")");
+        SendOptimizationRequests();
     }
 
     public override void DefineMacro(Macro f, VCExpr vc) {
@@ -2126,9 +2198,15 @@ namespace Microsoft.Boogie.SMTLib
     public override void Check()
     {
         PrepareCommon();
-        SendThisVC("(check-sat)");
+        SendCheckSat();
         FlushLogFile();
     }
+
+    public void SendCheckSat()
+    {
+      UsedNamedAssumes = null;
+      SendThisVC("(check-sat)");
+    }
 	
     public override void SetTimeOut(int ms)
     {
@@ -2325,21 +2403,6 @@ namespace Microsoft.Boogie.SMTLib
           return opts;
       }
 
-      public override void AssertNamed(VCExpr vc, bool polarity, string name)
-      {
-          string vcString;
-          if (polarity)
-          {
-              vcString = VCExpr2String(vc, 1);
-          }
-          else
-          {
-              vcString = "(not " + VCExpr2String(vc, 1) + ")";
-          }
-          AssertAxioms();
-          SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name));
-      }
-
       public override VCExpr ComputeInterpolant(VCExpr A, VCExpr B)
       {
           string A_str = VCExpr2String(A, 1);
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index dcf95bd2..06aa5bbe 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -34,14 +34,14 @@ namespace Microsoft.Boogie.SMTLib
   public class SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/>
   {
 
-    public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts)
+    public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, ISet<VCExprVar> namedAssumes = null, IList<string> optReqs = null, ISet<VCExprVar> tryAssumes = null)
     {
       Contract.Requires(e != null);
       Contract.Requires(namer != null);
       Contract.Ensures(Contract.Result<string>() != null);
 
       StringWriter sw = new StringWriter();
-      SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts);
+      SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, namedAssumes, optReqs);
       Contract.Assert(lin != null);
       lin.Linearise(e, LineariserOptions.Default);
       return cce.NonNull(sw.ToString());
@@ -74,12 +74,17 @@ namespace Microsoft.Boogie.SMTLib
     internal int UnderQuantifier = 0;
     internal readonly SMTLibProverOptions ProverOptions;
 
-    public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts)
+    readonly IList<string> OptimizationRequests;
+    readonly ISet<VCExprVar> NamedAssumes;
+
+    public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, ISet<VCExprVar> namedAssumes = null, IList<string> optReqs = null)
     {
       Contract.Requires(wr != null); Contract.Requires(namer != null);
       this.wr = wr;
       this.Namer = namer;
       this.ProverOptions = opts;
+      this.OptimizationRequests = optReqs;
+      this.NamedAssumes = namedAssumes;
     }
 
     public void Linearise(VCExpr expr, LineariserOptions options)
@@ -263,6 +268,26 @@ namespace Microsoft.Boogie.SMTLib
             }
             return true;
         }
+        if (OptimizationRequests != null
+            && (node.Op.Equals(VCExpressionGenerator.MinimizeOp) || node.Op.Equals(VCExpressionGenerator.MaximizeOp)))
+        {
+          string optOp = node.Op.Equals(VCExpressionGenerator.MinimizeOp) ? "minimize" : "maximize";
+          OptimizationRequests.Add(string.Format("({0} {1})", optOp, ToString(node[0], Namer, ProverOptions, NamedAssumes)));
+          Linearise(node[1], options);
+          return true;
+        }
+        if (node.Op is VCExprSoftOp)
+        {
+          Linearise(node[1], options);
+          return true;
+        }
+        if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp))
+        {
+          var exprVar = node[0] as VCExprVar;
+          NamedAssumes.Add(exprVar);
+          Linearise(node[1], options);
+          return true;
+        }
         return node.Accept<bool, LineariserOptions/*!*/>(OpLineariser, options);
     }
 
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 900bdbcc..f1179159 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Boogie.SMTLib
       "flet", "implies", "!=", "if_then_else",
       // Z3 extensions
       "lblneg", "lblpos", "lbl-lit",
-      "if", "&&", "||", "equals", "equiv", "bool",
+      "if", "&&", "||", "equals", "equiv", "bool", "minimize", "maximize",
       // Boogie-defined
       "real_pow", "UOrdering2", "UOrdering3", 
       // Floating point (final draft SMTLIB-v2.5)
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 32e28560..eaed83e9 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -210,7 +210,18 @@ void ObjectInvariant()
 
       if (node.Op is VCExprStoreOp) RegisterStore(node);
       else if (node.Op is VCExprSelectOp) RegisterSelect(node);
-      else {
+      else if (node.Op is VCExprSoftOp) {
+        var exprVar = node[0] as VCExprVar;
+        AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
+        AddDeclaration(string.Format("(assert-soft {0} :weight {1})", exprVar.Name, ((VCExprSoftOp)node.Op).Weight));
+      } else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) {
+        var exprVar = node[0] as VCExprVar;
+        AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
+        if (CommandLineOptions.Clo.PrintNecessaryAssumes)
+        {
+          AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name));
+        }
+      } else {
         VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
         if (op != null && 
           !(op.Func is DatatypeConstructor) && !(op.Func is DatatypeMembership) && !(op.Func is DatatypeSelector) && 
@@ -255,7 +266,10 @@ void ObjectInvariant()
         RegisterType(node.Type);
         string decl =
           "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
-        AddDeclaration(decl);
+        if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") || printedName.StartsWith("try$$")))
+        {
+          AddDeclaration(decl);
+        }
         KnownVariables.Add(node);
 		if(declHandler != null)
 			declHandler.VarDecl(node);
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index 6077f327..dc9ad10f 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -1115,7 +1115,7 @@ namespace Microsoft.Boogie.TypeErasure
       if (typeVarBindings.Count < node.TypeParameters.Count) {
         foreach (TypeVariable/*!*/ var in node.TypeParameters) {
           Contract.Assert(var != null);
-          if (typeVarBindings.All(b => !b.V.Equals(var)))
+          if (typeVarBindings.All(b => !b.V.Equals(bindings.TypeVariableBindings[var])))
             newBoundVars.Add((VCExprVar)bindings.TypeVariableBindings[var]);
         }
       }
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 0a9ba6b3..2c77a252 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -341,6 +341,10 @@ namespace Microsoft.Boogie {
 
     public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool);
 
+    public static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool);
+    public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool);
+    public static readonly VCExprOp NamedAssumeOp = new VCExprCustomOp("named_assume##dummy", 2, Type.Bool);
+
     public VCExprOp BoogieFunctionOp(Function func) {
       Contract.Requires(func != null);
       Contract.Ensures(Contract.Result<VCExprOp>() != null);
@@ -1565,6 +1569,16 @@ namespace Microsoft.Boogie.VCExprAST {
     }
   }
 
+  public class VCExprSoftOp : VCExprCustomOp
+  {
+    public readonly int Weight;
+
+    public VCExprSoftOp(int weight) : base("soft##dummy", 2, Microsoft.Boogie.Type.Bool)
+    {
+      Weight = weight;
+    }
+  }
+
   public class VCExprCustomOp : VCExprOp {
     public readonly string/*!*/ Name;
     int arity;
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 3c3b5cae..7bda0022 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -356,7 +356,7 @@ namespace Microsoft.Boogie {
       hasOutput = false;
       outputExn = null;
       this.handler = handler;
-
+      
       thmProver.Reset(gen);
       SetTimeout();
       proverStart = DateTime.UtcNow;
@@ -386,6 +386,7 @@ namespace Microsoft.Boogie {
   // -----------------------------------------------------------------------------------------------
 
   public abstract class ProverInterface {
+
     public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {
       Contract.Requires(prog != null);
 
@@ -452,6 +453,10 @@ namespace Microsoft.Boogie {
       Undetermined,
       Bounded
     }
+
+    public readonly ISet<VCExprVar> NamedAssumes = new HashSet<VCExprVar>();
+    public ISet<string> UsedNamedAssumes { get; protected set; }
+
     public class ErrorHandler {
       // Used in CheckOutcomeCore
       public virtual int StartingProcId()
@@ -542,7 +547,7 @@ namespace Microsoft.Boogie {
     }
 
     // (assert vc)
-    public virtual void Assert(VCExpr vc, bool polarity)
+    public virtual void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1)
     {
         throw new NotImplementedException();
     }
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 1f010757..19438924 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -85,6 +85,7 @@ namespace Microsoft.Boogie {
     public string RequestId;
     public abstract byte[] Checksum { get; }
     public byte[] SugaredCmdChecksum;
+    public bool IsAuxiliaryCexForDiagnosingTimeouts;
 
     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;
 
@@ -313,7 +314,7 @@ namespace Microsoft.Boogie {
     public abstract int GetLocation();
   }
 
-  public class CounterexampleComparer : IComparer<Counterexample> {
+  public class CounterexampleComparer : IComparer<Counterexample>, IEqualityComparer<Counterexample> {
 
     private int Compare(List<Block> bs1, List<Block> bs2)
     {
@@ -375,6 +376,16 @@ namespace Microsoft.Boogie {
       }
       return -1;
     }
+
+    public bool Equals(Counterexample x, Counterexample y)
+    {
+      return Compare(x, y) == 0;
+    }
+
+    public int GetHashCode(Counterexample obj)
+    {
+      return 0;
+    }
   }
 
   public class AssertCounterexample : Counterexample {
@@ -1122,7 +1133,8 @@ namespace VC {
         }
         if (returnBlocks > 1) {
           string unifiedExitLabel = "GeneratedUnifiedExit";
-          Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(Token.NoToken));
+          Block unifiedExit;
+          unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken));         
           Contract.Assert(unifiedExit != null);
           foreach (Block b in impl.Blocks) {
             if (b.TransferCmd is ReturnCmd) {
@@ -1528,6 +1540,26 @@ namespace VC {
         PredicateCmd pc = (PredicateCmd)c.Clone();
         Contract.Assert(pc != null);
 
+        QKeyValue current = pc.Attributes;
+        while (current != null)
+        {
+          if (current.Key == "minimize" || current.Key == "maximize") {
+            Contract.Assume(current.Params.Count == 1);
+            var param = current.Params[0] as Expr;
+            Contract.Assume(param != null && (param.Type.IsInt || param.Type.IsReal || param.Type.IsBv));
+            current.ClearParams();
+            current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
+          }
+          if (current.Key == "verified_under") {
+            Contract.Assume(current.Params.Count == 1);
+            var param = current.Params[0] as Expr;
+            Contract.Assume(param != null && param.Type.IsBool);
+            current.ClearParams();
+            current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
+          }
+          current = current.Next;
+        }
+
         Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
         if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) {
           string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 0e598267..789f86f5 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -584,9 +584,6 @@ namespace VC {
       vcgen.ConvertCFG2DAG(impl);
       vcgen.PassifyImpl(impl, out mvInfo);
 
-      if (PassiveImplInstrumentation != null)
-          PassiveImplInstrumentation(impl);
-                
       VCExpressionGenerator gen = proverInterface.VCExprGen;
       var exprGen = proverInterface.Context.ExprGen;
       var translator = proverInterface.Context.BoogieExprTranslator;
@@ -599,6 +596,9 @@ namespace VC {
 
       vcgen.InstrumentCallSites(impl);
 
+      if (PassiveImplInstrumentation != null)
+          PassiveImplInstrumentation(impl);
+
       label2absy = new Dictionary<int, Absy>();
       VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, proverInterface.Context);
       translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition); 
@@ -639,6 +639,7 @@ namespace VC {
 
   public abstract class StratifiedVCGenBase : VCGen {
     public readonly static string recordProcName = "boogie_si_record";
+    public readonly static string callSiteVarAttr = "callSiteVar";
     public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
     public ProverInterface prover;
 
@@ -699,7 +700,9 @@ namespace VC {
           if (!implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) continue;
           Variable callSiteVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "SICS" + callSiteId, Microsoft.Boogie.Type.Bool));
           implementation.LocVars.Add(callSiteVar);
-          newCmds.Add(new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar)));
+          var toInsert = new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar),
+              new QKeyValue(Token.NoToken, callSiteVarAttr, new List<object>(), null));
+          newCmds.Add(toInsert);
           callSiteId++;
         }
         block.Cmds = newCmds;
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index bf25e042..6e43e917 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1519,7 +1519,7 @@ namespace VC {
         }
     }
 
-    public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext)
+    public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null)
     {
       Contract.Requires(impl != null);
       Contract.Requires(proverContext != null);
@@ -1527,10 +1527,10 @@ namespace VC {
       Contract.Ensures(Contract.Result<VCExpr>() != null);
 
       label2absy = new Dictionary<int, Absy>();
-      return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);
+      return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext, namedAssumeVars: namedAssumeVars);
     }
 
-    public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) {
+    public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null) {
       Contract.Requires(impl != null);
       Contract.Requires(proverContext != null);
       Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -1632,7 +1632,7 @@ namespace VC {
           //use Duplicator and Substituter rather than new
           //nested IToken?
           //document expand attribute (search for {:ignore}, for example)
-          //fix up new CallCmd, new Requires, new Ensures in OwickiGries.cs
+          //fix up new CallCmd, new Requires, new Ensures in CivlRefinement.cs
           Func<Expr,Expr,Expr> withType = (Expr from, Expr to) =>
           {
             NAryExpr nFrom = from as NAryExpr;
@@ -1763,9 +1763,18 @@ namespace VC {
         {
           var checksum = a.Checksum;
           var oldCex = impl.ErrorChecksumToCachedError[checksum] as Counterexample;
-          if (oldCex != null)
-          {
-            callback.OnCounterexample(oldCex, null);
+          if (oldCex != null) {
+            if (CommandLineOptions.Clo.VerifySnapshots < 3) {
+              callback.OnCounterexample(oldCex, null);
+            } else {
+              // If possible, we use the old counterexample, but with the location information of "a"
+              var cex = AssertCmdToCloneCounterexample(a, oldCex);
+              callback.OnCounterexample(cex, null);
+              // OnCounterexample may have had side effects on the RequestId and OriginalRequestId fields.  We make
+              // any such updates available in oldCex. (Is this really a good design? --KRML)
+              oldCex.RequestId = cex.RequestId;
+              oldCex.OriginalRequestId = cex.OriginalRequestId;
+            }
           }
         }
       }
@@ -2012,6 +2021,16 @@ namespace VC {
       protected ProverContext/*!*/ context;
       Program/*!*/ program;
 
+      public IEnumerable<string> NecessaryAssumes
+      {
+        get { return program.NecessaryAssumes; }
+      }
+
+      public void AddNecessaryAssume(string id)
+      {
+        program.NecessaryAssumes.Add(id);
+      }
+
       public ErrorReporter(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,
           Dictionary<int, Absy>/*!*/ label2absy,
           List<Block/*!*/>/*!*/ blocks,
@@ -2104,6 +2123,7 @@ namespace VC {
           foreach (var cmd in assertCmds)
           {
             Counterexample cex = AssertCmdToCounterexample(cmd.Item1, cmd.Item2 , new List<Block>(), null, null, context);
+            cex.IsAuxiliaryCexForDiagnosingTimeouts = true;
             callback.OnCounterexample(cex, msg);
           }
         }
@@ -2219,10 +2239,11 @@ namespace VC {
       impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List<Cmd>(), new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] })));
       ResetPredecessors(impl.Blocks);
 
-      if(CommandLineOptions.Clo.KInductionDepth < 0) {
+      var k = Math.Max(CommandLineOptions.Clo.KInductionDepth, QKeyValue.FindIntAttribute(impl.Attributes, "kInductionDepth", -1));
+      if(k < 0) {
         ConvertCFG2DAGStandard(impl, edgesCut, taskID);
       } else {
-        ConvertCFG2DAGKInduction(impl, edgesCut, taskID);
+        ConvertCFG2DAGKInduction(impl, edgesCut, taskID, k);
       }
       
       #region Debug Tracing
@@ -2487,14 +2508,12 @@ namespace VC {
       return referencedVars;
     }
 
-    private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID) {
+    private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID, int inductionK) {
 
       // K-induction has not been adapted to be aware of these parameters which standard CFG to DAG transformation uses
       Contract.Requires(edgesCut == null);
       Contract.Requires(taskID == -1);
-
-      int inductionK = CommandLineOptions.Clo.KInductionDepth;
-      Contract.Assume(inductionK >= 0);
+      Contract.Requires(0 <= inductionK);
 
       bool contRuleApplication = true;
       while (contRuleApplication) {
@@ -2809,6 +2828,11 @@ namespace VC {
       mvInfo = new ModelViewInfo(program, impl);
       Convert2PassiveCmd(impl, mvInfo);
 
+      if (QKeyValue.FindBoolAttribute(impl.Attributes, "may_unverified_instrumentation"))
+      {
+        InstrumentWithMayUnverifiedConditions(impl, exitBlock);
+      }
+
       #region Peep-hole optimizations
       if (CommandLineOptions.Clo.RemoveEmptyBlocks){
         #region Get rid of empty blocks
@@ -2844,6 +2868,190 @@ namespace VC {
       return gotoCmdOrigins;
     }
 
+    #region Simplified May-Unverified Analysis and Instrumentation
+
+    static void InstrumentWithMayUnverifiedConditions(Implementation impl, Block unifiedExitBlock)
+    {
+      var q = new Queue<Block>();
+      q.Enqueue(unifiedExitBlock);
+      var conditionOnBlockEntry = new Dictionary<Block, HashSet<Variable>>();
+      while (q.Any())
+      {
+        var block = q.Dequeue();
+
+        if (conditionOnBlockEntry.ContainsKey(block))
+        {
+          continue;
+        }
+
+        var gotoCmd = block.TransferCmd as GotoCmd;
+        if (gotoCmd != null && gotoCmd.labelTargets.Any(b => !conditionOnBlockEntry.ContainsKey(b)))
+        {
+          q.Enqueue(block);
+          continue;
+        }
+
+        HashSet<Variable> cond = new HashSet<Variable>();
+        if (gotoCmd != null)
+        {
+          var mayInstrs = new List<Block>();
+          bool noInstr = true;
+          foreach (var succ in gotoCmd.labelTargets)
+          {
+            var c = conditionOnBlockEntry[succ];
+            if (c != null)
+            {
+              mayInstrs.Add(succ);
+            }
+            else
+            {
+              noInstr = false;
+            }
+            cond = JoinVariableSets(cond, c);
+          }
+          if (!noInstr)
+          {
+            foreach (var instr in mayInstrs)
+            {
+              InstrumentWithCondition(instr, 0, conditionOnBlockEntry[instr]);
+            }
+          }
+        }
+        
+        for (int i = block.Cmds.Count - 1; 0 <= i; i--)
+        {
+          var cmd = block.Cmds[i];
+          if (cond == null) { break; }
+
+          var assertCmd = cmd as AssertCmd;
+          if (assertCmd != null)
+          {
+            var litExpr = assertCmd.Expr as LiteralExpr;
+            if (litExpr != null && litExpr.IsTrue)
+            {
+              continue;
+            }
+
+            HashSet<Variable> vu = null;
+            if (assertCmd.VerifiedUnder == null)
+            {
+              vu = null;
+            }
+            else
+            {
+              HashSet<Variable> vars;
+              if (IsConjunctionOfAssumptionVariables(assertCmd.VerifiedUnder, out vars))
+              {
+                vu = vars;
+                // TODO(wuestholz): Maybe drop the :verified_under attribute.
+              }
+              else
+              {
+                vu = null;
+              }
+            }
+
+            if (vu == null)
+            {
+              InstrumentWithCondition(block, i + 1, cond);
+            }
+
+            cond = JoinVariableSets(cond, vu);
+          }
+        }
+
+        if (cond != null && block.Predecessors.Count == 0)
+        {
+          // TODO(wuestholz): Should we rather instrument each block?
+          InstrumentWithCondition(block, 0, cond);
+        }
+
+        foreach (var pred in block.Predecessors)
+        {
+          q.Enqueue(pred);
+        }
+
+        conditionOnBlockEntry[block] = cond;
+      }
+    }
+
+    private static void InstrumentWithCondition(Block block, int idx, HashSet<Variable> condition)
+    {
+      var conj = Expr.BinaryTreeAnd(condition.Select(v => (Expr)new IdentifierExpr(Token.NoToken, v)).ToList());
+      block.Cmds.Insert(idx, new AssumeCmd(Token.NoToken, Expr.Not(conj)));
+    }
+
+    static HashSet<Variable> JoinVariableSets(HashSet<Variable> c0, HashSet<Variable> c1)
+    {
+      // We use the following lattice:
+      // - Top: null (i.e., true)
+      // - Bottom: new HashSet<Variable>() (i.e., false)
+      // - Other Elements: new HashSet<Variable>(...) (i.e., conjunctions of assumption variables)
+
+      if (c0 == null || c1 == null)
+      {
+        return null;
+      }
+      var result = new HashSet<Variable>(c0);
+      result.UnionWith(c1);
+      return result;
+    }
+
+    static bool IsAssumptionVariableOrIncarnation(Variable v)
+    {
+      if (QKeyValue.FindBoolAttribute(v.Attributes, "assumption")) { return true; }
+      var incar = v as Incarnation;
+      return incar == null || QKeyValue.FindBoolAttribute(incar.OriginalVariable.Attributes, "assumption");
+    }
+
+    static bool IsConjunctionOfAssumptionVariables(Expr expr, out HashSet<Variable> variables)
+    {
+      Contract.Requires(expr != null);
+
+      variables = null;
+      var litExpr = expr as LiteralExpr;
+      if (litExpr != null && (litExpr.IsFalse || litExpr.IsTrue))
+      {
+        if (litExpr.IsTrue)
+        {
+          variables = new HashSet<Variable>();
+        }
+        return true;
+      }
+
+      var idExpr = expr as IdentifierExpr;
+      if (idExpr != null && IsAssumptionVariableOrIncarnation(idExpr.Decl))
+      {
+        variables = new HashSet<Variable>();
+        variables.Add(idExpr.Decl);
+        return true;
+      }
+
+      var andExpr = expr as NAryExpr;
+      if (andExpr != null)
+      {
+        var fun = andExpr.Fun as BinaryOperator;
+        if (fun != null && fun.Op == BinaryOperator.Opcode.And && andExpr.Args != null)
+        {
+          bool res = true;
+          variables = new HashSet<Variable>();
+          foreach (var op in andExpr.Args)
+          {
+            HashSet<Variable> vars;
+            var r = IsConjunctionOfAssumptionVariables(op, out vars);
+            res &= r;
+            variables = JoinVariableSets(variables, vars);
+            if (!res) { break; }
+          }
+          return res;
+        }
+      }
+
+      return false;
+    }
+
+    #endregion
+
     private static void HandleSelectiveChecking(Implementation impl)
     {
       if (QKeyValue.FindBoolAttribute(impl.Attributes, "selective_checking") ||
@@ -3137,6 +3345,31 @@ namespace VC {
       }
     }
 
+    /// <summary>
+    /// Returns a clone of "cex", but with the location stored in "cex" replaced by those from "assrt".
+    /// </summary>
+    public static Counterexample AssertCmdToCloneCounterexample(AssertCmd assrt, Counterexample cex) {
+      Contract.Requires(assrt != null);
+      Contract.Requires(cex != null);
+      Contract.Ensures(Contract.Result<Counterexample>() != null);
+
+      List<string> relatedInformation = new List<string>();
+
+      Counterexample cc;
+      if (assrt is AssertRequiresCmd) {
+        var aa = (AssertRequiresCmd)assrt;
+        cc = new CallCounterexample(cex.Trace, aa.Call, aa.Requires, cex.Model, cex.MvInfo, cex.Context, aa.Checksum);
+      } else if (assrt is AssertEnsuresCmd && cex is ReturnCounterexample) {
+        var aa = (AssertEnsuresCmd)assrt;
+        var oldCex = (ReturnCounterexample)cex;
+        cc = new ReturnCounterexample(cex.Trace, oldCex.FailingReturn, aa.Ensures, cex.Model, cex.MvInfo, cex.Context, aa.Checksum);
+      } else {
+        cc = new AssertCounterexample(cex.Trace, assrt, cex.Model, cex.MvInfo, cex.Context);
+      }
+      cc.relatedInformation = relatedInformation;
+      return cc;
+    }
+
     static VCExpr LetVC(Block startBlock,
                         VCExpr controlFlowVariableExpr,
                         Dictionary<int, Absy> label2absy,
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index b4ee4c09..cad5914b 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -87,7 +87,7 @@ namespace VC {
     /// <summary>
     /// Computes the wlp for an assert or assume command "cmd".
     /// </summary>
-    public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) {
+    internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) {
       Contract.Requires(cmd != null);
       Contract.Requires(N != null);
       Contract.Requires(ctxt != null);
@@ -186,17 +186,48 @@ namespace VC {
             if (naryExpr.Fun is FunctionCall) {
               int id = ac.UniqueId;
               ctxt.Label2absy[id] = ac;
-              return gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);
+              return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N));
             }
           }
         }
-        return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
+        var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
+        
+        var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id");
+        if (aid != null)
+        {
+          var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try");
+          var v = gen.Variable((isTry ? "try$$" : "assume$$") + aid, Microsoft.Boogie.Type.Bool);
+          expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr));
+        }
+        var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft");
+        var softWeight = QKeyValue.FindIntAttribute(ac.Attributes, "soft", 0);
+        if ((soft || 0 < softWeight) && aid != null)
+        {
+          var v = gen.Variable("soft$$" + aid, Microsoft.Boogie.Type.Bool);
+          expr = gen.Function(new VCExprSoftOp(Math.Max(softWeight, 1)), v, gen.ImpliesSimp(v, expr));
+        }
+        return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(expr, N));
       } else {
         Console.WriteLine(cmd.ToString());
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected command
       }
     }
-    
+
+    private static VCExpr MaybeWrapWithOptimization(VCContext ctxt, VCExpressionGenerator gen, QKeyValue attrs, VCExpr expr)
+    {
+      var min = QKeyValue.FindExprAttribute(attrs, "minimize");
+      if (min != null)
+      {
+        expr = gen.Function(VCExpressionGenerator.MinimizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(min), expr);
+      }
+      var max = QKeyValue.FindExprAttribute(attrs, "maximize");
+      if (max != null)
+      {
+        expr = gen.Function(VCExpressionGenerator.MaximizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(max), expr);
+      }
+      return expr;
+    }
+
     public static CommandLineOptions.SubsumptionOption Subsumption(AssertCmd ac) {
       Contract.Requires(ac != null);
       int n = QKeyValue.FindIntAttribute(ac.Attributes, "subsumption", -1);
diff --git a/Source/version.ssc b/Source/version.ssc
deleted file mode 100644
index 5bdcf170..00000000
--- a/Source/version.ssc
+++ /dev/null
@@ -1,12 +0,0 @@
-// ==++==
-// 
-//   
-// 
-// ==--==
-// Warning: Automatically generated file. DO NOT EDIT
-// Generated at Dienstag, 5. Juli 2011 11:26:45
-
-using System.Reflection;
-[assembly: AssemblyVersion("2.2.30705.1126")]
-[assembly: AssemblyFileVersion("2.2.30705.1126")]
-