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

35 files changed, 969 insertions, 160 deletions

diff --git a/README.md b/README.md
index e86eb187..a976b249 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,17 @@
 # Boogie
 
-[![Build Status](https://travis-ci.org/boogie-org/boogie.svg)](https://travis-ci.org/boogie-org/boogie)
+## Build Status
+
+| Linux                         | Windows                         |
+|-------------------------------|---------------------------------|
+| [![linux build status][1]][2] | [![windows_build_status][3]][4] |
+
+[1]: https://travis-ci.org/boogie-org/boogie.svg
+[2]: https://travis-ci.org/boogie-org/boogie
+[3]: https://pmbuilds.inf.ethz.ch/buildStatus/icon?job=boogie
+[4]: #FIXME
+
+## About
 
 Boogie is an intermediate verification language (IVL), intended as a layer on which
 to build program verifiers for other languages. Several program verifiers have
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index a1a54024..56bfc90f 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2427,6 +2427,28 @@ namespace Microsoft.Boogie {
       functionDependencies.Add(function);

     }

 

+    public bool SignatureEquals(DeclWithFormals other)

+    {

+      Contract.Requires(other != null);

+

+      string sig = null;

+      string otherSig = null;

+      using (var strWr = new System.IO.StringWriter())

+      using (var tokTxtWr = new TokenTextWriter("<no file>", strWr, false, false))

+      {

+        EmitSignature(tokTxtWr, this is Function);

+        sig = strWr.ToString();

+      }

+

+      using (var otherStrWr = new System.IO.StringWriter())

+      using (var otherTokTxtWr = new TokenTextWriter("<no file>", otherStrWr, false, false))

+      {

+        EmitSignature(otherTokTxtWr, other is Function);

+        otherSig = otherStrWr.ToString();

+      }

+      return sig == otherSig;

+    }

+

     protected void EmitSignature(TokenTextWriter stream, bool shortRet) {

       Contract.Requires(stream != null);

       Type.EmitOptionalTypeParams(stream, TypeParameters);

@@ -3295,6 +3317,8 @@ namespace Microsoft.Boogie {
       RecycledFailingAssertions.Add(assertion);

     }

 

+    public Cmd ExplicitAssumptionAboutCachedPrecondition { get; set; }

+

     // Strongly connected components

     private StronglyConnectedComponents<Block/*!*/> scc;

     [ContractInvariantMethod]

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index b5581ea6..f659f9ea 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1144,6 +1144,12 @@ namespace Microsoft.Boogie {
         return;

       }

 

+      if (cmd.IrrelevantForChecksumComputation)

+      {

+        cmd.Checksum = currentChecksum;

+        return;

+      }

+

       var assumeCmd = cmd as AssumeCmd;

       if (assumeCmd != null

           && QKeyValue.FindBoolAttribute(assumeCmd.Attributes, "assumption_variable_initialization"))

@@ -1161,7 +1167,7 @@ namespace Microsoft.Boogie {
         if (havocCmd != null)

         {

           tokTxtWr.Write("havoc ");

-          var relevantVars = havocCmd.Vars.Where(e => usedVariables.Contains(e.Decl) && !e.Decl.Name.StartsWith("a##post##")).OrderBy(e => e.Name).ToList();

+          var relevantVars = havocCmd.Vars.Where(e => usedVariables.Contains(e.Decl) && !e.Decl.Name.StartsWith("a##cached##")).OrderBy(e => e.Name).ToList();

           relevantVars.Emit(tokTxtWr, true);

           tokTxtWr.WriteLine(";");

         }

@@ -1244,6 +1250,7 @@ namespace Microsoft.Boogie {
   public abstract class Cmd : Absy {

     public byte[] Checksum { get; internal set; }

     public byte[] SugaredCmdChecksum { get; internal set; }

+    public bool IrrelevantForChecksumComputation { get; set; }

 

     public Cmd(IToken/*!*/ tok)

       : base(tok) {

@@ -1522,18 +1529,6 @@ namespace Microsoft.Boogie {
     }

 

     public override void Emit(TokenTextWriter stream, int level) {

-      if (stream.UseForComputingChecksums)

-      {

-        var lhs = Lhss.FirstOrDefault() as SimpleAssignLhs;

-        if (lhs != null

-            && lhs.AssignedVariable.Decl != null

-            && (QKeyValue.FindBoolAttribute(lhs.AssignedVariable.Decl.Attributes, "assumption")

-                || lhs.AssignedVariable.Decl.Name.Contains("##old##")))

-        {

-          return;

-        }

-      }

-      

       stream.Write(this, level, "");

 

       string/*!*/ sep = "";

@@ -2656,6 +2651,13 @@ namespace Microsoft.Boogie {
             reqCopy.Condition = Substituter.Apply(s, req.Condition);

             AssertCmd/*!*/ a = new AssertRequiresCmd(this, reqCopy);

             Contract.Assert(a != null);

+            if (Attributes != null)

+            {

+              // Inherit attributes of call.

+              var attrCopy = (QKeyValue)cce.NonNull(Attributes.Clone());

+              attrCopy = Substituter.Apply(s, attrCopy);

+              a.Attributes = attrCopy;

+            }

             a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;

             newBlockBody.Add(a);

           }

@@ -2676,6 +2678,13 @@ namespace Microsoft.Boogie {
         Contract.Assert(expr != null);

         AssertCmd/*!*/ a = new AssertCmd(tok, expr);

         Contract.Assert(a != null);

+        if (Attributes != null)

+        {

+          // Inherit attributes of call.

+          var attrCopy = (QKeyValue)cce.NonNull(Attributes.Clone());

+          attrCopy = Substituter.Apply(s, attrCopy);

+          a.Attributes = attrCopy;

+        }

         a.ErrorDataEnhanced = AssertCmd.GenerateBoundVarMiningStrategy(expr);

         newBlockBody.Add(a);

       }

@@ -2835,7 +2844,7 @@ namespace Microsoft.Boogie {
       var clauses = procedure.Ensures.Select(e => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, substOldCombined, e.Condition, program)).Concat(modifies);

       // TODO(wuestholz): Try extracting a function for each clause:

       // return Conjunction(clauses.Select(c => extract(c)));

-      var conj = Conjunction(clauses);

+      var conj = Expr.And(clauses, true);

       return conj != null ? extract(conj) : conj;

     }

 

@@ -2846,30 +2855,10 @@ namespace Microsoft.Boogie {
       var clauses = procedure.Requires.Where(r => !r.Free).Select(r => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, r.Condition, program));

       // TODO(wuestholz): Try extracting a function for each clause:

       // return Conjunction(clauses.Select(c => extract(c)));

-      var conj = Conjunction(clauses);

+      var conj = Expr.And(clauses, true);

       return conj != null ? extract(conj) : conj;

     }

 

-    private static Expr Conjunction(IEnumerable<Expr> conjuncts)

-    {

-      // TODO(wuestholz): Maybe we should use 'LiteralExpr.BinaryTreeAnd' instead.

-      Expr result = null;

-      foreach (var c in conjuncts)

-      {

-        if (result != null)

-        {

-          result = LiteralExpr.And(result, c);

-          result.Type = Type.Bool;

-        }

-        else

-        {

-          result = c;

-          result.Type = Type.Bool;

-        }

-      }

-      return result;

-    }

-

     public override Absy StdDispatch(StandardVisitor visitor) {

       //Contract.Requires(visitor != null);

       Contract.Ensures(Contract.Result<Absy>() != null);

@@ -3212,9 +3201,6 @@ namespace Microsoft.Boogie {
     }

     public override void Emit(TokenTextWriter stream, int level) {

       //Contract.Requires(stream != null);

-

-      if (stream.UseForComputingChecksums && QKeyValue.FindBoolAttribute(Attributes, "precondition_previous_snapshot")) { return; }

-

       stream.Write(this, level, "assume ");

       EmitAttributes(stream, Attributes);

       this.Expr.Emit(stream);

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index f3a943b8..c19140d7 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -467,6 +467,29 @@ namespace Microsoft.Boogie {
         var mid = (start + end) / 2;

         return Expr.And(BinaryTreeAnd(terms, start, mid), BinaryTreeAnd(terms, mid + 1, end));

     }

+

+    public static Expr And(IEnumerable<Expr> conjuncts, bool returnNullIfEmpty = false)

+    {

+      Expr result = null;

+      foreach (var c in conjuncts)

+      {

+        if (result != null)

+        {

+          result = LiteralExpr.And(result, c);

+          result.Type = Type.Bool;

+        }

+        else

+        {

+          result = c;

+          result.Type = Type.Bool;

+        }

+      }

+      if (result == null && !returnNullIfEmpty)

+      {

+        result = Expr.True;

+      }

+      return result;

+    }

   }

   [ContractClassFor(typeof(Expr))]

   public abstract class ExprContracts : Expr {

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index dbbb6fd0..03545cbf 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -557,6 +557,7 @@ namespace Microsoft.Boogie {
     public bool UseSmtOutputFormat = false;

     public bool WeakArrayTheory = false;

     public bool UseLabels = true;

+    public bool RunDiagnosticsOnTimeout = false;

     public bool SIBoolControlVC = false;

     public bool MonomorphicArrays {

       get {

@@ -1585,6 +1586,7 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("weakArrayTheory", ref WeakArrayTheory) || 

               ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||

               ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||

+              ps.CheckBooleanFlag("runDiagnosticsOnTimeout", ref RunDiagnosticsOnTimeout) ||

               ps.CheckBooleanFlag("boolControlVC", ref SIBoolControlVC, true) ||

               ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||

               ps.CheckBooleanFlag("explainHoudini", ref ExplainHoudini) ||

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 77086f0f..0feb5e35 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -539,7 +539,7 @@ namespace Microsoft.Boogie {
         HavocCmd/*!*/ havocCmd = (HavocCmd)cmd;

         foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) {

           Contract.Assert(expr != null);

-          if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##post##"))) {

+          if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##cached##"))) {

             liveSet.Remove(expr.Decl);

           }

         }

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 181b80a1..7f021c43 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -583,6 +583,15 @@ namespace Microsoft.Boogie {
       return (Expr)new FunctionCallReresolvingReplacingOldSubstituter(program, always, forOld).Visit(expr);

     }

 

+    public static Expr FunctionCallReresolvingApply(Substitution always, Substitution forOld, Expr expr, Program program)

+    {

+      Contract.Requires(always != null);

+      Contract.Requires(forOld != null);

+      Contract.Requires(expr != null);

+      Contract.Ensures(Contract.Result<Expr>() != null);

+      return (Expr)new FunctionCallReresolvingNormalSubstituter(program, always, forOld).Visit(expr);

+    }

+

     // ----------------------------- Substitutions for Cmd -------------------------------

 

     /// <summary>

@@ -660,7 +669,7 @@ namespace Microsoft.Boogie {
 

     // ------------------------------------------------------------

 

-    private sealed class NormalSubstituter : Duplicator

+    private class NormalSubstituter : Duplicator

     {

       private readonly Substitution/*!*/ always;

       private readonly Substitution/*!*/ forold;

@@ -744,6 +753,32 @@ namespace Microsoft.Boogie {
       }

     }

 

+    private sealed class FunctionCallReresolvingNormalSubstituter : NormalSubstituter

+    {

+      readonly Program Program;

+

+      public FunctionCallReresolvingNormalSubstituter(Program program, Substitution always, Substitution forold)

+        : base(always, forold)

+      {

+        Program = program;

+      }

+

+      public override Expr VisitNAryExpr(NAryExpr node)

+      {

+        var result = base.VisitNAryExpr(node);

+        var nAryExpr = result as NAryExpr;

+        if (nAryExpr != null)

+        {

+          var funCall = nAryExpr.Fun as FunctionCall;

+          if (funCall != null)

+          {

+            funCall.Func = Program.FindFunction(funCall.FunctionName);

+          }

+        }

+        return result;

+      }

+    }

+

     private class ReplacingOldSubstituter : Duplicator {

       private readonly Substitution/*!*/ always;

       private readonly Substitution/*!*/ forold;

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 5d20e6e8..a18cee05 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -96,7 +96,65 @@ namespace Microsoft.Boogie
       assumptionVariableCount = 0;

       temporaryVariableCount = 0;

       currentImplementation = implementation;

-      var result = VisitImplementation(implementation);

+

+      #region Introduce explict assumption about the precondition.

+

+      var oldProc = programInCachedSnapshot.FindProcedure(currentImplementation.Proc.Name);

+      if (oldProc != null

+          && oldProc.DependencyChecksum != currentImplementation.Proc.DependencyChecksum

+          && currentImplementation.ExplicitAssumptionAboutCachedPrecondition == null)

+      {

+        var axioms = new List<Axiom>();

+        var after = new List<Cmd>();

+        Expr assumedExpr = new LiteralExpr(Token.NoToken, false);

+        var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program, true);

+        if (canUseSpecs && oldProc.SignatureEquals(currentImplementation.Proc))

+        {

+          var always = Substituter.SubstitutionFromHashtable(currentImplementation.GetImplFormalMap(), true, currentImplementation.Proc);

+          var forOld = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());

+          var clauses = oldProc.Requires.Select(r => Substituter.FunctionCallReresolvingApply(always, forOld, r.Condition, Program));

+          var conj = Expr.And(clauses, true);

+          assumedExpr = conj != null ? FunctionExtractor.Extract(conj, Program, axioms) : new LiteralExpr(Token.NoToken, true);

+        }

+

+        if (assumedExpr != null)

+        {

+          var lv = new LocalVariable(Token.NoToken,

+            new TypedIdent(Token.NoToken, string.Format("a##cached##{0}", FreshAssumptionVariableName), Type.Bool),

+            new QKeyValue(Token.NoToken, "assumption", new List<object>(), null));

+          currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs);

+          var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));

+          var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr);

+          var assumed = new AssignCmd(currentImplementation.tok, new List<AssignLhs> { lhs }, new List<Expr> { rhs });

+          assumed.IrrelevantForChecksumComputation = true;

+          currentImplementation.ExplicitAssumptionAboutCachedPrecondition = assumed;

+          after.Add(assumed);

+        }

+

+        if (CommandLineOptions.Clo.TraceCachingForTesting || CommandLineOptions.Clo.TraceCachingForBenchmarking)

+        {

+          using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))

+          {

+            var loc = currentImplementation.tok != null && currentImplementation.tok != Token.NoToken ? string.Format("{0}({1},{2})", currentImplementation.tok.filename, currentImplementation.tok.line, currentImplementation.tok.col) : "<unknown location>";

+            Console.Out.WriteLine("Processing implementation {0} (at {1}):", currentImplementation.Name, loc);

+            foreach (var a in axioms)

+            {

+              Console.Out.Write("  >>> added axiom: ");

+              a.Expr.Emit(tokTxtWr);

+              Console.Out.WriteLine();

+            }

+            foreach (var b in after)

+            {

+              Console.Out.Write("  >>> added after assuming the current precondition: ");

+              b.Emit(tokTxtWr, 0);

+            }

+          }

+        }

+      }

+

+      #endregion

+

+      var result = VisitImplementation(currentImplementation);

       currentImplementation = null;

       this.programInCachedSnapshot = null;

       return result;

@@ -192,7 +250,7 @@ namespace Microsoft.Boogie
         Expr assumedExpr = new LiteralExpr(Token.NoToken, false);

         // TODO(wuestholz): Try out two alternatives: only do this for low priority implementations or not at all.

         var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program);

-        if (canUseSpecs)

+        if (canUseSpecs && oldProc.SignatureEquals(node.Proc))

         {

           var desugaring = node.Desugaring;

           Contract.Assert(desugaring != null);

@@ -200,6 +258,7 @@ namespace Microsoft.Boogie
           if (precond != null)

           {

             var assume = new AssumeCmd(node.tok, precond, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));

+            assume.IrrelevantForChecksumComputation = true;

             beforePrecondtionCheck.Add(assume);

           }

 

@@ -211,7 +270,9 @@ namespace Microsoft.Boogie
               new TypedIdent(Token.NoToken, string.Format("{0}##old##{1}", unmod.Name, FreshTemporaryVariableName), unmod.Type));

             var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldUnmod));

             var rhs = new IdentifierExpr(Token.NoToken, unmod.Decl);

-            before.Add(new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs }));

+            var cmd = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });

+            cmd.IrrelevantForChecksumComputation = true;

+            before.Add(cmd);

             var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, oldUnmod), new IdentifierExpr(Token.NoToken, unmod.Decl));

             eq.Type = Type.Bool;

             eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY;

@@ -227,22 +288,29 @@ namespace Microsoft.Boogie
             oldSubst[mod.Decl] = new IdentifierExpr(Token.NoToken, oldMod);

             var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldMod));

             var rhs = new IdentifierExpr(Token.NoToken, mod.Decl);

-            before.Add(new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs }));

+            var cmd = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });

+            cmd.IrrelevantForChecksumComputation = true;

+            before.Add(cmd);

           }

           

           assumedExpr = node.Postcondition(oldProc, eqs, oldSubst, Program, e => FunctionExtractor.Extract(e, Program, axioms));

+          if (assumedExpr == null)

+          {

+            assumedExpr = new LiteralExpr(Token.NoToken, true);

+          }

         }

 

         if (assumedExpr != null)

         {

           var lv = new LocalVariable(Token.NoToken,

-            new TypedIdent(Token.NoToken, string.Format("a##post##{0}", FreshAssumptionVariableName), Type.Bool),

+            new TypedIdent(Token.NoToken, string.Format("a##cached##{0}", FreshAssumptionVariableName), Type.Bool),

             new QKeyValue(Token.NoToken, "assumption", new List<object>(), null));

           node.AssignedAssumptionVariable = lv;

           currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs);

           var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));

           var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr);

           var assumed = new AssignCmd(node.tok, new List<AssignLhs> { lhs }, new List<Expr> { rhs });

+          assumed.IrrelevantForChecksumComputation = true;

           after.Add(assumed);

         }

 

@@ -431,7 +499,7 @@ namespace Microsoft.Boogie
       }

     }

 

-    public static bool CanExpressOldSpecs(Procedure oldProc, Program newProg)

+    public static bool CanExpressOldSpecs(Procedure oldProc, Program newProg, bool ignoreModifiesClauses = false)

     {

       Contract.Requires(oldProc != null && newProg != null);

 

@@ -439,7 +507,7 @@ namespace Microsoft.Boogie
       var globals = newProg.GlobalVariables;

       return oldProc.DependenciesCollected

              && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum)))

-             && oldProc.Modifies.All(m => globals.Any(g => g.Name == m.Name));

+             && (ignoreModifiesClauses || oldProc.Modifies.All(m => globals.Any(g => g.Name == m.Name)));

     }

 

     public override Procedure VisitProcedure(Procedure node)

@@ -599,6 +667,10 @@ namespace Microsoft.Boogie
       {

         priority = Priority.LOW;

       }

+      else if (result.Outcome == ConditionGeneration.Outcome.TimedOut && CommandLineOptions.Clo.RunDiagnosticsOnTimeout)

+      {

+        priority = Priority.MEDIUM;

+      }

       else

       {

         priority = Priority.SKIP;

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 210d9f6c..522e8174 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -601,19 +601,24 @@ namespace Microsoft.Boogie.Houdini {
             // Inline functions

             (new InlineFunctionCalls()).VisitBlockList(impl.Blocks);

 

-            ExtractQuantifiedExprs(impl);

+            

             StripOutermostForall(impl);

+            //ExtractQuantifiedExprs(impl);

+            ExtractBoolExprs(impl);

 

             //CommandLineOptions.Clo.PrintInstrumented = true;

-            //var tt = new TokenTextWriter(Console.Out);

-            //impl.Emit(tt, 0);

-            //tt.Close();

+            //using (var tt = new TokenTextWriter(Console.Out))

+            //    impl.Emit(tt, 0);

 

             // Intercept the FunctionCalls of the existential functions, and replace them with Boolean constants

             var existentialFunctionNames = new HashSet<string>(existentialFunctions.Keys);

             var fv = new ReplaceFunctionCalls(existentialFunctionNames);

             fv.VisitBlockList(impl.Blocks);

 

+            //using (var tt = new TokenTextWriter(Console.Out))

+            //    impl.Emit(tt, 0);

+

+

             impl2functionsAsserted.Add(impl.Name, fv.functionsAsserted);

             impl2functionsAssumed.Add(impl.Name, fv.functionsAssumed);

 

@@ -684,6 +689,24 @@ namespace Microsoft.Boogie.Houdini {
             }

         }

 

+        // convert "foo(... e ...) to:

+        //    (p iff e) ==> foo(... p ...) 

+        // where p is a fresh boolean variable, foo is an existential constant

+        // and e is a Boolean-typed argument of foo

+        private void ExtractBoolExprs(Implementation impl)

+        {

+            var funcs = new HashSet<string>(existentialFunctions.Keys);

+            foreach (var blk in impl.Blocks)

+            {

+                foreach (var acmd in blk.Cmds.OfType<AssertCmd>())

+                {

+                    var ret = ExtractBoolArgs.Extract(acmd.Expr, funcs);

+                    acmd.Expr = ret.Item1;

+                    impl.LocVars.AddRange(ret.Item2);

+                }

+            }

+        }

+

         // convert "assert e1 && forall x: e2" to

         //    assert e1 && e2[x <- x@bound]

         private void StripOutermostForall(Implementation impl)

@@ -967,6 +990,61 @@ namespace Microsoft.Boogie.Houdini {
 

     }

 

+    // convert "foo(... e ...) to:

+    //    (p iff e) ==> foo(... p ...) 

+    // where p is a fresh boolean variable, foo is an existential constant

+    // and e is a Boolean-typed argument of foo

+    class ExtractBoolArgs : StandardVisitor

+    {

+        static int freshConstCounter = 0;

+        HashSet<string> existentialFunctions;

+        HashSet<Constant> newConstants;

+

+        private ExtractBoolArgs(HashSet<string> existentialFunctions)

+        {

+            this.existentialFunctions = existentialFunctions;

+            this.newConstants = new HashSet<Constant>();

+        }

+

+        public static Tuple<Expr, IEnumerable<Constant>> Extract(Expr expr, HashSet<string> existentialFunctions)

+        {

+            var eq = new ExtractBoolArgs(existentialFunctions);

+            expr = eq.VisitExpr(expr);

+            return Tuple.Create(expr, eq.newConstants.AsEnumerable());

+        }

+

+        public override Expr VisitNAryExpr(NAryExpr node)

+        {

+            if (node.Fun is FunctionCall && existentialFunctions.Contains((node.Fun as FunctionCall).FunctionName))

+            {

+                var constants = new Dictionary<Constant, Expr>();

+                for (int i = 0; i < node.Args.Count; i++)

+                {

+                    if (node.Args[i].Type == Type.Bool)

+                    {

+                        var constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken,

+                            "boolArg@const" + freshConstCounter, Microsoft.Boogie.Type.Bool), false);

+                        freshConstCounter++;

+                        constants.Add(constant, node.Args[i]);

+                        node.Args[i] = Expr.Ident(constant);

+                    }

+                }

+

+                newConstants.UnionWith(constants.Keys);

+

+                Expr ret = Expr.True;

+                foreach (var tup in constants)

+                {

+                    ret = Expr.And(ret, Expr.Eq(Expr.Ident(tup.Key), tup.Value));

+                }

+                return Expr.Imp(ret, node);

+            } 

+

+            return base.VisitNAryExpr(node);

+        }

+    }

+

+

     // convert "foo(... forall e ...) to:

     //    (p iff forall e) ==> foo(... p ...) 

     // where p is a fresh boolean variable and foo is an existential constant

@@ -1277,6 +1355,13 @@ namespace Microsoft.Boogie.Houdini {
         }

     }

 

+    public class PredicateAbsFullElem : PredicateAbsElem

+    {

+        public PredicateAbsFullElem()

+            : base(1000)

+        { }

+    }

+

     public class PredicateAbsElem : IAbstractDomain

     {

         public static class ExprExt

@@ -1300,7 +1385,6 @@ namespace Microsoft.Boogie.Houdini {
 

         class Disjunct

         {

-            public static int DisjunctBound = 3;

             HashSet<int> pos;

             HashSet<int> neg;

             bool isTrue;

@@ -1312,7 +1396,7 @@ namespace Microsoft.Boogie.Houdini {
                 neg = new HashSet<int>();

             }

 

-            public Disjunct(IEnumerable<int> pos, IEnumerable<int> neg)

+            public Disjunct(IEnumerable<int> pos, IEnumerable<int> neg, int bound)

             {

                 this.isTrue = false;

                 this.pos = new HashSet<int>(pos);

@@ -1323,7 +1407,7 @@ namespace Microsoft.Boogie.Houdini {
                     this.pos = new HashSet<int>();

                     this.neg = new HashSet<int>();

                 }

-                if (this.pos.Count + this.neg.Count > DisjunctBound)

+                if (this.pos.Count + this.neg.Count > bound)

                 {

                     // Set to true

                     this.isTrue = true;

@@ -1333,14 +1417,14 @@ namespace Microsoft.Boogie.Houdini {
 

             }

 

-            public Disjunct OR(Disjunct that)

+            public Disjunct OR(Disjunct that, int bound)

             {

                 if (isTrue)

                     return this;

                 if (that.isTrue)

                     return that;

 

-                return new Disjunct(this.pos.Concat(that.pos), this.neg.Concat(that.neg));

+                return new Disjunct(this.pos.Concat(that.pos), this.neg.Concat(that.neg), bound);

             }

 

             public bool Implies(Disjunct that)

@@ -1363,17 +1447,26 @@ namespace Microsoft.Boogie.Houdini {
 

         // Conjunction of Disjuncts

         List<Disjunct> conjuncts;

+        int DisjunctBound;

         bool isFalse;

 

         public PredicateAbsElem()

         {

             this.conjuncts = new List<Disjunct>();

             this.isFalse = true;

+            this.DisjunctBound = 3;

+        }

+

+        public PredicateAbsElem(int bound)

+        {

+            this.conjuncts = new List<Disjunct>();

+            this.isFalse = true;

+            this.DisjunctBound = bound;

         }

 

         public IAbstractDomain Bottom()

         {

-            return new PredicateAbsElem();

+            return new PredicateAbsElem(DisjunctBound);

         }

 

         public IAbstractDomain MakeTop(out bool changed)

@@ -1384,7 +1477,7 @@ namespace Microsoft.Boogie.Houdini {
                 return this;

             }

             changed = true;

-            var ret = new PredicateAbsElem();

+            var ret = new PredicateAbsElem(DisjunctBound);

             ret.isFalse = false;

             return ret;

         }

@@ -1398,21 +1491,21 @@ namespace Microsoft.Boogie.Houdini {
             if (!this.isFalse && conjuncts.Count == 0)

                 return this;

 

-            var ret = new PredicateAbsElem();

+            var ret = new PredicateAbsElem(DisjunctBound);

             ret.isFalse = false;

 

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

             {

                 var b = (state[i] as Model.Boolean).Value;

                 Disjunct d = null;

-                if (b) d = new Disjunct(new int[] { i }, new int[] { });

-                else d = new Disjunct(new int[] { }, new int[] { i });

+                if (b) d = new Disjunct(new int[] { i }, new int[] { }, DisjunctBound);

+                else d = new Disjunct(new int[] { }, new int[] { i }, DisjunctBound);

 

                 if (isFalse)

                     ret.AddDisjunct(d);

                 else

                 {

-                    conjuncts.Iter(c => ret.AddDisjunct(c.OR(d)));

+                    conjuncts.Iter(c => ret.AddDisjunct(c.OR(d, DisjunctBound)));

                 }

             }

 

@@ -2136,6 +2229,7 @@ namespace Microsoft.Boogie.Houdini {
                   System.Tuple.Create("Intervals", new Intervals() as IAbstractDomain),

                   System.Tuple.Create("ConstantProp", ConstantProp.GetBottom() as IAbstractDomain),

                   System.Tuple.Create("PredicateAbs", new PredicateAbsElem() as IAbstractDomain),

+                  System.Tuple.Create("PredicateAbsFull", new PredicateAbsFullElem() as IAbstractDomain),

                   System.Tuple.Create("ImplicationDomain", ImplicationDomain.GetBottom() as IAbstractDomain),

                   System.Tuple.Create("PowDomain", PowDomain.GetBottom() as IAbstractDomain),

                   System.Tuple.Create("EqualitiesDomain", EqualitiesDomain.GetBottom() as IAbstractDomain),

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 30056d99..d9da29cc 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -238,6 +238,7 @@ namespace Microsoft.Boogie.Houdini {
       stats.proverTime += queryTime;

       stats.numProverQueries++;

       if (CommandLineOptions.Clo.Trace) {

+        Console.WriteLine("Outcome = " + proverOutcome);

         Console.WriteLine("Time taken = " + queryTime);

       }

 

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 868b9ee3..594f2509 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -261,6 +261,11 @@ namespace Microsoft.Boogie.SMTLib
           SendCommon("(assert (and (tickleBool true) (tickleBool false)))");

         }

 

+        if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout)

+        {

+          SendCommon("(declare-fun timeoutDiagnostics (Int) Bool)");

+        }

+

         if (ctx.KnownDatatypeConstructors.Count > 0)

         {

           GraphUtil.Graph<CtorType> dependencyGraph = new GraphUtil.Graph<CtorType>();

@@ -393,6 +398,7 @@ namespace Microsoft.Boogie.SMTLib
       }

 

       PrepareCommon();

+

       string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";

       FlushAxioms();

 

@@ -1232,54 +1238,154 @@ namespace Microsoft.Boogie.SMTLib
         currentErrorHandler = handler;

         FlushProverWarnings();

 

-        int errorsLeft;

+        int errorLimit;

         if (CommandLineOptions.Clo.ConcurrentHoudini) {

           Contract.Assert(taskID >= 0);

-          errorsLeft = CommandLineOptions.Clo.Cho[taskID].ProverCCLimit;

+          errorLimit = CommandLineOptions.Clo.Cho[taskID].ProverCCLimit;

         } else {

-          errorsLeft = CommandLineOptions.Clo.ProverCCLimit;

+          errorLimit = CommandLineOptions.Clo.ProverCCLimit;

         }

 

-        if (errorsLeft < 1)

-          errorsLeft = 1;

+        if (errorLimit < 1)

+          errorLimit = 1;

+

+        int errorsLeft = errorLimit;

 

         var globalResult = Outcome.Undetermined;

 

         while (true) {

-          errorsLeft--;

           string[] labels = null;

+          bool popLater = false;

 

-          result = GetResponse();

-          if (globalResult == Outcome.Undetermined)

-            globalResult = result;

+          try {

+            errorsLeft--;

+            

+            result = GetResponse();

 

-          if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) {

-            IList<string> xlabels;

-            if (CommandLineOptions.Clo.UseLabels) {

-              labels = GetLabelsInfo();

-              if (labels == null)

-              {

-                xlabels = new string[] { };

-              }

-              else

+            if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut)

+            {

+              #region Run timeout diagnostics

+

+              SendThisVC("; begin timeout diagnostics");

+

+              var unverified = new SortedSet<int>(ctx.TimeoutDiagnosticIDToAssertion.Keys);

+              var lastCnt = unverified.Count + 1;

+              var mod = 2;

+              var timeLimit = options.TimeLimit;

+              var timeLimitFactor = 1;

+              while (true)

               {

-                xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();

+                // TODO(wuestholz): Try out different ways for splitting up the work.

+                var split0 = new SortedSet<int>(unverified.Where((val, idx) => idx % mod == 0));

+                var split1 = new SortedSet<int>(unverified.Except(split0));

+

+                int cnt = unverified.Count;

+

+                if (cnt == 0)

+                {

+                  result = Outcome.Valid;

+                  break;

+                }

+                else if (lastCnt == cnt)

+                {

+                  if (mod < cnt)

+                  {

+                    mod++;

+                  }

+                  else if (timeLimitFactor <= 3 && 0 < timeLimit)

+                  {

+                    // TODO(wuestholz): Add a commandline option to control this.

+                    timeLimitFactor++;

+                  }

+                  else

+                  {

+                    // Give up and report which assertions were not verified.

+                    var cmds = unverified.Select(id => ctx.TimeoutDiagnosticIDToAssertion[id]);

+

+                    if (cmds.Any())

+                    {

+                      handler.OnResourceExceeded("timeout after running diagnostics", cmds);

+                    }

+

+                    break;

+                  }

+                }

+                else

+                {

+                  mod = 2;

+                }

+                lastCnt = cnt;

+

+                if (0 < split0.Count)

+                {

+                  var result0 = CheckSplit(split0, ref popLater, timeLimitFactor * timeLimit);

+                  if (result0 == Outcome.Valid)

+                  {

+                    unverified.ExceptWith(split0);

+                  }

+                  else if (result0 == Outcome.Invalid)

+                  {

+                    result = result0;

+                    break;

+                  }

+                }

+

+                if (0 < split1.Count)

+                {

+                  var result1 = CheckSplit(split1, ref popLater, timeLimitFactor * timeLimit);

+                  if (result1 == Outcome.Valid)

+                  {

+                    unverified.ExceptWith(split1);

+                  }

+                  else if (result1 == Outcome.Invalid)

+                  {

+                    result = result1;

+                    break;

+                  }

+                }

               }

+

+              SendThisVC("; end timeout diagnostics");

+

+              #endregion

             }

-            else if(CommandLineOptions.Clo.SIBoolControlVC) {

-                labels = new string[0];

+

+            if (globalResult == Outcome.Undetermined)

+              globalResult = result;

+            

+            if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) {

+              IList<string> xlabels;

+              if (CommandLineOptions.Clo.UseLabels) {

+                labels = GetLabelsInfo();

+                if (labels == null)

+                {

+                  xlabels = new string[] { };

+                }

+                else

+                {

+                  xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();

+                }

+              }

+              else if(CommandLineOptions.Clo.SIBoolControlVC) {

+                  labels = new string[0];

+                  xlabels = labels;

+              } else {

+                labels = CalculatePath(handler.StartingProcId());

                 xlabels = labels;

-            } else {

-              labels = CalculatePath(handler.StartingProcId());

-              xlabels = labels;

+              }

+                Model model = (result == Outcome.TimeOut || result == Outcome.OutOfMemory) ? null :

+                    GetErrorModel();

+              handler.OnModel(xlabels, model, result);

+            }

+            

+            if (labels == null || !labels.Any() || errorsLeft == 0) break;

+          } finally {

+            if (popLater)

+            {

+              SendThisVC("(pop 1)");

             }

-              Model model = (result == Outcome.TimeOut || result == Outcome.OutOfMemory) ? null :

-                  GetErrorModel();

-            handler.OnModel(xlabels, model, result);

           }

 

-          if (labels == null || !labels.Any() || errorsLeft == 0) break;

-

           if (CommandLineOptions.Clo.UseLabels) {

             var negLabels = labels.Where(l => l.StartsWith("@")).ToArray();

             var posLabels = labels.Where(l => !l.StartsWith("@"));

@@ -1315,6 +1421,37 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

+    private Outcome CheckSplit(SortedSet<int> split, ref bool popLater, int timeLimit)

+    {

+      if (popLater)

+      {

+        SendThisVC("(pop 1)");

+      }

+

+      SendThisVC("(push 1)");

+      SendThisVC(string.Format("(set-option :{0} {1})", Z3.SetTimeoutOption(), timeLimit));

+      popLater = true;

+

+      SendThisVC(string.Format("; checking split VC with {0} unverified assertions", split.Count));

+      var expr = VCExpressionGenerator.True;

+      foreach (var i in ctx.TimeoutDiagnosticIDToAssertion.Keys)

+      {

+        var lit = VCExprGen.Function(VCExpressionGenerator.TimeoutDiagnosticsOp, VCExprGen.Integer(Microsoft.Basetypes.BigNum.FromInt(i)));

+        if (split.Contains(i)) {

+          lit = VCExprGen.Not(lit);

+        }

+        expr = VCExprGen.AndSimp(expr, lit);

+      }

+      SendThisVC("(assert " + VCExpr2String(expr, 1) + ")");

+      if (options.Solver == SolverKind.Z3)

+      {

+        SendThisVC("(apply (then (using-params propagate-values :max_rounds 1) simplify) :print false)");

+      }

+      FlushLogFile();

+      SendThisVC("(check-sat)");

+      return GetResponse();

+    }

+

     public override string[] CalculatePath(int controlFlowConstant) {

       SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " 0)))");

       var path = new List<string>();

diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 3ef2039b..40007ab9 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -98,9 +98,14 @@ namespace Microsoft.Boogie.SMTLib
       return "|" + s + "|";

     }

 

-    static string NonKeyword(string s)

+    static string FilterReserved(string s)

     {

-      if (reservedSmtWords.Contains(s) || char.IsDigit(s[0]))

+      // Note symbols starting with ``.`` and ``@`` are reserved for internal

+      // solver use in SMT-LIBv2 however if we check for the first character

+      // being ``@`` then Boogie's tests fail spectacularly because they are

+      // used for labels so we don't check for it here. It hopefully won't matter

+      // in practice because ``@`` cannot be legally used in Boogie identifiers.

+      if (reservedSmtWords.Contains(s) || char.IsDigit(s[0]) || s[0] == '.')

         s = "q@" + s;

 

       // | and \ are illegal even in quoted identifiers

@@ -120,17 +125,17 @@ namespace Microsoft.Boogie.SMTLib
 

     public static string QuoteId(string s)

     {

-      return AddQuotes(NonKeyword(s));

+      return AddQuotes(FilterReserved(s));

     }

 

     public override string GetQuotedLocalName(object thingie, string inherentName)

     {

-      return AddQuotes(base.GetLocalName(thingie, NonKeyword(inherentName)));

+      return AddQuotes(base.GetLocalName(thingie, FilterReserved(inherentName)));

     }

 

     public override string GetQuotedName(object thingie, string inherentName)

     {

-      return AddQuotes(base.GetName(thingie, NonKeyword(inherentName)));

+      return AddQuotes(base.GetName(thingie, FilterReserved(inherentName)));

     }

 

     public SMTLibNamer()

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 30363102..9205d54c 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -231,6 +231,7 @@ void ObjectInvariant()
             else

                 decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")";

             AddDeclaration(decl);

+            if (declHandler != null) declHandler.FuncDecl(f);

           }

           KnownFunctions.Add(f);

         } else {

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 4f8dc08e..15573f5b 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -339,6 +339,8 @@ namespace Microsoft.Boogie {
 

     public static readonly VCExprOp TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool);

 

+    public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool);

+

     public VCExprOp BoogieFunctionOp(Function func) {

       Contract.Requires(func != null);

       Contract.Ensures(Contract.Result<VCExprOp>() != null);

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index da8624e9..7c690eff 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -461,7 +461,7 @@ namespace Microsoft.Boogie {
         Contract.Requires(cce.NonNullElements(labels));

       }

 

-      public virtual void OnResourceExceeded(string message) {

+      public virtual void OnResourceExceeded(string message, IEnumerable<Tuple<AssertCmd, TransferCmd>> assertCmds = null) {

         Contract.Requires(message != null);

       }

 

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 515ec16d..a19f983a 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -768,6 +768,7 @@ namespace VC {
         Contract.Assert(req != null);

         Expr e = Substituter.Apply(formalProcImplSubst, req.Condition);

         Cmd c = new AssumeCmd(req.tok, e);

+        c.IrrelevantForChecksumComputation = true;

         insertionPoint.Cmds.Add(c);

         if (debugWriter != null) {

           c.Emit(debugWriter, 1);

@@ -775,6 +776,11 @@ namespace VC {
       }

       origStartBlock.Predecessors.Add(insertionPoint);

 

+      if (impl.ExplicitAssumptionAboutCachedPrecondition != null)

+      {

+        insertionPoint.Cmds.Add(impl.ExplicitAssumptionAboutCachedPrecondition);

+      }

+

       if (debugWriter != null) {

         debugWriter.WriteLine();

       }

@@ -1275,7 +1281,7 @@ namespace VC {
           IdentifierExpr v_prime_exp = new IdentifierExpr(v_prime.tok, v_prime);

           #endregion

           #region Create the assume command itself

-          AssumeCmd ac = new AssumeCmd(v.tok, TypedExprEq(v_prime_exp, pred_incarnation_exp, v_prime.Name.Contains("a##post##")));

+          AssumeCmd ac = new AssumeCmd(v.tok, TypedExprEq(v_prime_exp, pred_incarnation_exp, v_prime.Name.Contains("a##cached##")));

           pred.Cmds.Add(ac);

           #endregion

           #endregion

@@ -1697,7 +1703,7 @@ namespace VC {
             }

           

             #region Create an assume command with the new variable

-            assumptions.Add(TypedExprEq(x_prime_exp, copies[i], x_prime_exp.Decl != null && x_prime_exp.Decl.Name.Contains("a##post##")));

+            assumptions.Add(TypedExprEq(x_prime_exp, copies[i], x_prime_exp.Decl != null && x_prime_exp.Decl.Name.Contains("a##cached##")));

             #endregion

           }

         }

@@ -1720,6 +1726,7 @@ namespace VC {
         if (currentImplementation != null

             && currentImplementation.HasCachedSnapshot

             && !currentImplementation.AnyErrorsInCachedSnapshot

+            && currentImplementation.DoomedInjectedAssumptionVariables.Count == 0

             && currentImplementation.InjectedAssumptionVariables.Count == 1

             && assign.Lhss.Count == 1)

         {

@@ -1742,9 +1749,9 @@ namespace VC {
         Contract.Assert(c != null);

         // If an assumption variable for postconditions is included here, it must have been assigned within a loop.

         // We do not need to havoc it if we have performed a modular proof of the loop (i.e., using only the loop

-        // invariant) in the previous snapshot and are therefore not going refer to the assumption variable after

-        // the loop. We can achieve this by simply not updating/adding it in the incarnation map.

-        List<IdentifierExpr> havocVars = hc.Vars.Where(v => !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##post##"))).ToList();

+        // invariant) in the previous snapshot and, consequently, the corresponding assumption did not affect the

+        // anything after the loop. We can achieve this by simply not updating/adding it in the incarnation map.

+        List<IdentifierExpr> havocVars = hc.Vars.Where(v => !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##cached##"))).ToList();

         // First, compute the new incarnations

         foreach (IdentifierExpr ie in havocVars) {

           Contract.Assert(ie != null);

@@ -1767,6 +1774,18 @@ namespace VC {
             }

           }

         }

+

+        // Add the following assume-statement for each assumption variable 'v', where 'v_post' is the new incarnation and 'v_pre' is the old one:

+        // assume v_post ==> v_pre;

+        foreach (IdentifierExpr ie in havocVars)

+        {

+          if (QKeyValue.FindBoolAttribute(ie.Decl.Attributes, "assumption"))

+          {

+            var preInc = (Expr)(preHavocIncarnationMap[ie.Decl].Clone());

+            var postInc = (Expr)(incarnationMap[ie.Decl].Clone());

+            passiveCmds.Add(new AssumeCmd(c.tok, Expr.Imp(postInc, preInc)));

+          }

+        }

       }

       #endregion

  else if (c is CommentCmd) {

diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index 83787dc5..ddc34976 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -22,6 +22,8 @@ namespace Microsoft.Boogie
   /// </summary>

   [ContractClass(typeof(ProverContextContracts))]

   public abstract class ProverContext : ICloneable {

+    public int TimoutDiagnosticsCount { get; set; }

+    public readonly Dictionary<int, Tuple<AssertCmd, TransferCmd>> TimeoutDiagnosticIDToAssertion = new Dictionary<int, Tuple<AssertCmd, TransferCmd>>();

     protected virtual void ProcessDeclaration(Declaration decl) {Contract.Requires(decl != null);}

     public virtual void DeclareType(TypeCtorDecl t, string attributes) {Contract.Requires(t != null); ProcessDeclaration(t); }

     public virtual void DeclareConstant(Constant c, bool uniq, string attributes) {Contract.Requires(c != null); ProcessDeclaration(c); }

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 7dbf6b05..5c698633 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -2189,7 +2189,13 @@ namespace Microsoft.Boogie
 					idx.Add(args[1]);

 					return Expr.Store(args[0],idx,args[2]);

 				}

-				

+

+                if (f.Op is VCExprBoogieFunctionOp)

+                {

+                    return new NAryExpr(Token.NoToken, 

+                        new FunctionCall((f.Op as VCExprBoogieFunctionOp).Func), args);

+                }

+

 				var op = VCOpToOp (f.Op);

 				return MakeBinary(op,args);

 			}

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 6f8d3668..69b7c8cc 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -2273,7 +2273,7 @@ namespace VC {
         return;

       }

 

-      public override void OnResourceExceeded(string message)

+      public override void OnResourceExceeded(string message, IEnumerable<Tuple<AssertCmd, TransferCmd>> assertCmds = null)

       {

           //Contract.Requires(message != null);

       }

@@ -2609,6 +2609,9 @@ namespace VC {
           if(impl.LocVars.Any(v => isVisible(v)))

               throw new InvalidProgramForSecureVc("SecureVc: Visible Local variables not allowed");

 

+          // Desugar procedure calls

+          DesugarCalls(impl);

+

           // Gather spec, remove existing ensures

           var secureAsserts = new List<AssertCmd>();

           var logicalAsserts = new List<AssertCmd>();

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 560f55b4..3a483a58 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2096,9 +2096,17 @@ namespace VC {
         return cce.NonNull((Absy)label2absy[id]);

       }

 

-      public override void OnResourceExceeded(string msg) {

+      public override void OnResourceExceeded(string msg, IEnumerable<Tuple<AssertCmd, TransferCmd>> assertCmds = null) {

         //Contract.Requires(msg != null);

         resourceExceededMessage = msg;

+        if (assertCmds != null)

+        {

+          foreach (var cmd in assertCmds)

+          {

+            Counterexample cex = AssertCmdToCounterexample(cmd.Item1, cmd.Item2 , new List<Block>(), null, null, context);

+            callback.OnCounterexample(cex, msg);

+          }

+        }

       }

 

       public override void OnProverWarning(string msg) {

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 45e511f0..82d3b607 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -118,6 +118,17 @@ namespace VC {
           if (ac.VerifiedUnder != null)

           {

             VU = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.VerifiedUnder);

+

+            if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout)

+            {

+              ctxt.Ctxt.TimeoutDiagnosticIDToAssertion[ctxt.Ctxt.TimoutDiagnosticsCount] = new Tuple<AssertCmd,TransferCmd>(ac, b.TransferCmd);

+              VU = gen.Or(VU, gen.Function(VCExpressionGenerator.TimeoutDiagnosticsOp, gen.Integer(BigNum.FromInt(ctxt.Ctxt.TimoutDiagnosticsCount++))));

+            }

+          }

+          else if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout)

+          {

+            ctxt.Ctxt.TimeoutDiagnosticIDToAssertion[ctxt.Ctxt.TimoutDiagnosticsCount] = new Tuple<AssertCmd,TransferCmd>(ac, b.TransferCmd);

+            VU = gen.Function(VCExpressionGenerator.TimeoutDiagnosticsOp, gen.Integer(BigNum.FromInt(ctxt.Ctxt.TimoutDiagnosticsCount++)));

           }

           ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;

         }

diff --git a/Test/prover/usedot.bpl b/Test/prover/usedot.bpl
new file mode 100644
index 00000000..5815236e
--- /dev/null
+++ b/Test/prover/usedot.bpl
@@ -0,0 +1,9 @@
+// RUN: %boogie -typeEncoding:m -proverLog:"%t.smt2" "%s"
+// RUN: %OutputCheck "%s" --file-to-check="%t.smt2"
+procedure foo() {
+  // . is an illegal starting character in SMT-LIBv2
+  // so test that we don't emit it as a symbol name.
+  // CHECK-L:(declare-fun q@.x () Int)
+  var .x:int;
+  assert .x == 0;
+}
diff --git a/Test/secure/tworound.bpl b/Test/secure/tworound.bpl
new file mode 100644
index 00000000..a78c4af4
--- /dev/null
+++ b/Test/secure/tworound.bpl
@@ -0,0 +1,116 @@
+type T = bv4;
+function {:bvbuiltin "bvult"} bvlt(p1: T, p2: T) : bool; // unsigned less than
+function {:bvbuiltin "bvxor"} xorT(p1: T, p2: T) : T;
+function {:bvbuiltin "bvadd"} bvadd(p1: T, p2: T) : T;
+
+
+procedure bar({:visible} v: T)
+  returns ({:hidden} h: T)
+  ensures true;
+{
+  h := v;
+}
+
+procedure foo0({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
+  returns ({:visible} r1: bool, {:visible} r2: bool, 
+      {:visible} s1: T, {:visible} s2: T, {:visible} s3: T, {:visible} s4: T)
+  ensures (r2 == bvlt(bvadd(x1,x2), bvadd(y1,y2))) && (r1 == bvlt(x1, y1));
+{
+   var {:hidden} t1, t2: T;
+
+   r1 := bvlt(x1, y1);
+
+   havoc s1;
+   havoc s2;
+
+   s3 := xorT(x1, s1);
+   s4 := xorT(y1, s2);
+
+   t1 := xorT(s1, s3);
+   t2 := xorT(s2, s4);
+
+   r2 := bvlt(bvadd(x2, t1), bvadd(y2, t2));
+}
+
+
+procedure foo1({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
+  returns ({:visible} r1: bool, {:visible} r2: bool, 
+      {:visible} s1: T, {:visible} s2: T, {:hidden} s3: T, {:hidden} s4: T)
+  ensures (r2 == bvlt(bvadd(x1,x2), bvadd(y1,y2))) && (r1 == bvlt(x1, y1));
+{
+   var {:hidden} t1, t2: T;
+
+   r1 := bvlt(x1, y1);
+
+   havoc s1;
+   havoc s2;
+
+   s3 := xorT(x1, s1);
+   s4 := xorT(y1, s2);
+
+   t1 := xorT(s1, s3);
+   t2 := xorT(s2, s4);
+
+   r2 := bvlt(bvadd(x2, t1), bvadd(y2, t2));
+}
+
+
+
+procedure foo2({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
+  returns ({:visible} r1: bool, {:visible} r2: bool, 
+      {:visible} s1: T, {:visible} s2: T)
+  ensures (r2 == bvlt(bvadd(x1,x2), bvadd(y1,y2))) && (r1 == bvlt(x1, y1)); 
+{
+   var {:hidden} t1, t2: T;
+   var {:hidden} s3, s4: T;
+
+   r1 := bvlt(x1, y1);
+
+   havoc s1;
+   havoc s2;
+
+   s3 := xorT(x1, s1);
+   s4 := xorT(y1, s2);
+
+   t1 := xorT(s1, s3);
+   t2 := xorT(s2, s4);
+
+   r2 := bvlt(bvadd(x2, t1), bvadd(y2, t2));
+}
+
+procedure foo3({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
+  returns ({:visible} r1: bool, {:visible} r2: bool, 
+      {:visible} s1: T, {:visible} s2: T, {:hidden} s3: T, {:hidden} s4: T)
+  ensures (r2 == bvlt(bvadd(x1,x2), bvadd(y1,y2))) && (r1 == bvlt(x1, y1)) && (s4 == xorT(y1,s2)) && (s3 == xorT(x1, s1));
+{
+   var {:hidden} t1, t2: T;
+
+   r1 := bvlt(x1, y1);
+
+   havoc s1;
+   havoc s2;
+
+   s3 := xorT(x1, s1);
+   s4 := xorT(y1, s2);
+
+   t1 := xorT(s1, s3);
+   t2 := xorT(s2, s4);
+
+   r2 := bvlt(bvadd(x2, t1), bvadd(y2, t2));
+}
+
+
+
+procedure bid({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
+  returns ({:visible} r: bool)
+  ensures r == bvlt(bvadd(x1,x2), bvadd(y1,y2));
+{
+  var {:hidden} r1, r2: bool;
+  var {:hidden} s1, s2, s3, s4: T;
+
+  call r1, r2, s1, s2, s3, s4 := foo1(x1, x2, y1, y2);
+
+  r := r2;
+}
+
+
diff --git a/Test/snapshots/Snapshots34.v0.bpl b/Test/snapshots/Snapshots34.v0.bpl
new file mode 100644
index 00000000..e3522645
--- /dev/null
+++ b/Test/snapshots/Snapshots34.v0.bpl
@@ -0,0 +1,7 @@
+procedure {:checksum "0"} P();

+  requires 0 != 0;

+

+implementation {:id "P"} {:checksum "1"} P()

+{

+    assert 1 != 1;

+}

diff --git a/Test/snapshots/Snapshots34.v1.bpl b/Test/snapshots/Snapshots34.v1.bpl
new file mode 100644
index 00000000..b374f7c0
--- /dev/null
+++ b/Test/snapshots/Snapshots34.v1.bpl
@@ -0,0 +1,6 @@
+procedure {:checksum "2"} P();

+

+implementation {:id "P"} {:checksum "1"} P()

+{

+    assert 1 != 1;

+}

diff --git a/Test/snapshots/Snapshots35.v0.bpl b/Test/snapshots/Snapshots35.v0.bpl
new file mode 100644
index 00000000..adfd6a69
--- /dev/null
+++ b/Test/snapshots/Snapshots35.v0.bpl
@@ -0,0 +1,7 @@
+procedure {:checksum "0"} P(b: bool);

+  requires b;

+

+implementation {:id "P"} {:checksum "1"} P(p: bool)

+{

+    assert p;

+}

diff --git a/Test/snapshots/Snapshots35.v1.bpl b/Test/snapshots/Snapshots35.v1.bpl
new file mode 100644
index 00000000..bec381af
--- /dev/null
+++ b/Test/snapshots/Snapshots35.v1.bpl
@@ -0,0 +1,6 @@
+procedure {:checksum "2"} P(b: bool);

+

+implementation {:id "P"} {:checksum "1"} P(p: bool)

+{

+    assert p;

+}

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index a203ffac..01a231fe 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl > "%t"

+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl > "%t"

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

diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 8f3c2015..637dd088 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -40,8 +40,13 @@ Snapshots1.v1.bpl(13,5): Error BP5001: This assertion might not hold.
 

 Boogie program verifier finished with 1 verified, 1 error

 Processing call to procedure P2 in implementation P1 (at Snapshots1.v2.bpl(5,5)):

+  >>> added after: a##cached##0 := a##cached##0 && true;

+Processing implementation P2 (at Snapshots1.v2.bpl(12,51)):

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && true;

 Processing command (at Snapshots1.v2.bpl(5,5)) assert false;

   >>> DoNothingToAssert

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && true;

+  >>> AssumeNegationOfAssumptionVariable

 Snapshots1.v2.bpl(5,5): Error BP5002: A precondition for this call might not hold.

 Snapshots1.v2.bpl(10,3): Related location: This is the precondition that might not hold.

 Processing command (at Snapshots1.v2.bpl(14,5)) assert 2 != 2;

@@ -52,34 +57,45 @@ Boogie program verifier finished with 1 verified, 1 error
 Boogie program verifier finished with 1 verified, 0 errors

 

 Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P0 (at Snapshots2.v2.bpl(4,51)):

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && true;

 Processing call to procedure P0 in implementation P0 (at Snapshots2.v2.bpl(6,5)):

+  >>> added after: a##cached##1 := a##cached##1 && true;

 Processing command (at Snapshots2.v2.bpl(6,5)) assert F0();

   >>> DoNothingToAssert

 

 Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P0 (at Snapshots2.v3.bpl(4,51)):

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;

 Processing call to procedure P0 in implementation P0 (at Snapshots2.v3.bpl(6,5)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##1 := a##cached##1 && false;

 Processing command (at Snapshots2.v3.bpl(6,5)) assert F0();

   >>> DoNothingToAssert

 

 Boogie program verifier finished with 1 verified, 0 errors

 

 Boogie program verifier finished with 1 verified, 0 errors

-Processing call to procedure P0 in implementation P0 (at Snapshots2.v5.bpl(7,5)):

+Processing implementation P0 (at Snapshots2.v5.bpl(5,51)):

   >>> added axiom: ##extracted_function##1() == F0()

-  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1();

-Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1();

-  >>> MarkAsFullyVerified

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();

+Processing call to procedure P0 in implementation P0 (at Snapshots2.v5.bpl(7,5)):

+  >>> added axiom: ##extracted_function##2() == F0()

+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##2();

+  >>> added after: a##cached##1 := a##cached##1 && true;

+Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##2();

+  >>> MarkAsPartiallyVerified

 Processing command (at Snapshots2.v5.bpl(7,5)) assert F0();

-  >>> MarkAsFullyVerified

+  >>> MarkAsPartiallyVerified

 Processing command (at Snapshots2.v5.bpl(3,1)) assert F0();

-  >>> MarkAsFullyVerified

+  >>> MarkAsPartiallyVerified

 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing command (at Snapshots3.v0.bpl(2,1)) assert G();

   >>> DoNothingToAssert

 

 Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P0 (at Snapshots3.v1.bpl(4,51)):

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;

 Processing command (at Snapshots3.v1.bpl(2,1)) assert G();

   >>> DoNothingToAssert

 Snapshots3.v1.bpl(6,1): Error BP5003: A postcondition might not hold on this return path.

@@ -89,7 +105,7 @@ Boogie program verifier finished with 0 verified, 1 error
 

 Boogie program verifier finished with 3 verified, 0 errors

 Processing call to procedure P2 in implementation P1 (at Snapshots4.v1.bpl(14,5)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##0 := a##cached##0 && false;

 Processing command (at Snapshots4.v1.bpl(23,5)) assert false;

   >>> DoNothingToAssert

 Snapshots4.v1.bpl(23,5): Error BP5001: This assertion might not hold.

@@ -103,6 +119,8 @@ Processing command (at Snapshots5.v0.bpl(5,5)) assert false;
   >>> DoNothingToAssert

 

 Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P0 (at Snapshots5.v1.bpl(3,51)):

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;

 Processing command (at Snapshots5.v1.bpl(5,5)) assert false;

   >>> DoNothingToAssert

 Snapshots5.v1.bpl(5,5): Error BP5001: This assertion might not hold.

@@ -115,8 +133,8 @@ Boogie program verifier finished with 1 verified, 0 errors
 Processing call to procedure N in implementation M (at Snapshots6.v1.bpl(11,5)):

   >>> added axiom: (forall y##old##0: int, y: int :: {:weight 30} { ##extracted_function##1(y##old##0, y) } ##extracted_function##1(y##old##0, y) == (y##old##0 == y))

   >>> added before: y##old##0 := y;

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(y##old##0, y);

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(y##old##0, y);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(y##old##0, y);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(y##old##0, y);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots6.v1.bpl(13,5)) assert y == 0;

   >>> MarkAsPartiallyVerified

@@ -130,8 +148,8 @@ Boogie program verifier finished with 1 verified, 0 errors
 Processing call to procedure N in implementation M (at Snapshots7.v1.bpl(12,5)):

   >>> added axiom: (forall y: int, z: int :: {:weight 30} { ##extracted_function##1(y, z) } ##extracted_function##1(y, z) == (y < z))

   >>> added before: y##old##0 := y;

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(y, z);

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(y, z);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(y, z);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(y, z);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots7.v1.bpl(14,5)) assert y < 0;

   >>> MarkAsPartiallyVerified

@@ -147,12 +165,12 @@ Processing call to procedure N in implementation M (at Snapshots8.v1.bpl(8,5)):
   >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))

   >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))

   >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

 Processing command (at Snapshots8.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

   >>> MarkAsFullyVerified

 Processing command (at Snapshots8.v1.bpl(8,5)) assert 0 < call0formal#AT#n;

   >>> MarkAsFullyVerified

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots8.v1.bpl(10,5)) assert 0 <= x;

   >>> MarkAsPartiallyVerified

@@ -170,12 +188,12 @@ Processing call to procedure N in implementation M (at Snapshots9.v1.bpl(8,5)):
   >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n && true))

   >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r && true))

   >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

 Processing command (at Snapshots9.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

   >>> MarkAsFullyVerified

 Processing command (at Snapshots9.v1.bpl(8,5)) assert 0 < call0formal#AT#n;

   >>> MarkAsFullyVerified

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots9.v1.bpl(10,5)) assert 0 <= x;

   >>> MarkAsPartiallyVerified

@@ -191,12 +209,12 @@ Processing call to procedure N in implementation M (at Snapshots10.v1.bpl(8,5)):
   >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))

   >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))

   >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

 Processing command (at Snapshots10.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

   >>> MarkAsFullyVerified

 Processing command (at Snapshots10.v1.bpl(8,5)) assert 0 < call0formal#AT#n;

   >>> MarkAsFullyVerified

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots10.v1.bpl(12,5)) assert 0 <= x;

   >>> MarkAsPartiallyVerified

@@ -214,7 +232,7 @@ Processing call to procedure N in implementation M (at Snapshots11.v1.bpl(7,5)):
   >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))

   >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))

   >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

 Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

   >>> DropAssume

 Processing command (at Snapshots11.v1.bpl(7,5)) assert 0 < call0formal#AT#n;

@@ -230,7 +248,7 @@ Processing command (at Snapshots12.v0.bpl(7,5)) assert false;
 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure N in implementation M (at Snapshots12.v1.bpl(5,5)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##0 := a##cached##0 && false;

 Processing command (at Snapshots12.v1.bpl(7,5)) assert false;

   >>> DoNothingToAssert

 Snapshots12.v1.bpl(7,5): Error BP5001: This assertion might not hold.

@@ -241,7 +259,7 @@ Processing command (at Snapshots13.v0.bpl(7,5)) assert false;
 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure N in implementation M (at Snapshots13.v1.bpl(5,5)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##0 := a##cached##0 && false;

 Processing command (at Snapshots13.v1.bpl(7,5)) assert false;

   >>> DoNothingToAssert

 Snapshots13.v1.bpl(7,5): Error BP5001: This assertion might not hold.

@@ -253,8 +271,8 @@ Processing command (at Snapshots14.v0.bpl(7,5)) assert false;
 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure N in implementation M (at Snapshots14.v1.bpl(5,5)):

   >>> added axiom: ##extracted_function##1() == (F() && G())

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1();

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1();

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1();

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots14.v1.bpl(7,5)) assert false;

   >>> MarkAsPartiallyVerified

@@ -270,9 +288,9 @@ Processing command (at Snapshots15.v0.bpl(13,5)) assert false;
 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(7,5)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##0 := a##cached##0 && false;

 Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(11,5)):

-  >>> added after: a##post##1 := a##post##1 && false;

+  >>> added after: a##cached##1 := a##cached##1 && false;

 Processing command (at Snapshots15.v1.bpl(5,5)) assert true;

   >>> MarkAsFullyVerified

 Processing command (at Snapshots15.v1.bpl(9,5)) assert true;

@@ -302,11 +320,11 @@ Processing command (at Snapshots17.v0.bpl(20,13)) assert x == 1;
 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(14,13)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##0 := a##cached##0 && false;

 Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(16,13)):

-  >>> added after: a##post##1 := a##post##1 && false;

+  >>> added after: a##cached##1 := a##cached##1 && false;

 Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(23,9)):

-  >>> added after: a##post##2 := a##post##2 && false;

+  >>> added after: a##cached##2 := a##cached##2 && false;

 Processing command (at Snapshots17.v1.bpl(28,5)) assert true;

   >>> MarkAsFullyVerified

 Processing command (at Snapshots17.v1.bpl(25,9)) assert false;

@@ -328,9 +346,9 @@ Processing command (at Snapshots18.v0.bpl(20,5)) assert 2 != 2;
 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(9,9)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##0 := a##cached##0 && false;

 Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(10,9)):

-  >>> added after: a##post##1 := a##post##1 && false;

+  >>> added after: a##cached##1 := a##cached##1 && false;

 Processing command (at Snapshots18.v1.bpl(7,9)) assert 0 == 0;

   >>> MarkAsFullyVerified

 Processing command (at Snapshots18.v1.bpl(17,9)) assert 1 != 1;

@@ -351,13 +369,14 @@ Boogie program verifier finished with 0 verified, 1 error
 Processing call to procedure N in implementation M (at Snapshots19.v1.bpl(5,5)):

   >>> added axiom: ##extracted_function##1() == (2 == 2)

   >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1();

+  >>> added after: a##cached##0 := a##cached##0 && true;

 Processing command (at Snapshots19.v1.bpl(5,5)) assume {:precondition_previous_snapshot} ##extracted_function##1();

   >>> MarkAsFullyVerified

 Processing command (at Snapshots19.v1.bpl(5,5)) assert 2 == 2;

   >>> MarkAsFullyVerified

 Processing command (at Snapshots19.v1.bpl(7,5)) assert 1 != 1;

-  >>> RecycleError

-Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold.

+  >>> DoNothingToAssert

+Snapshots19.v1.bpl(7,5): Error BP5001: This assertion might not hold.

 

 Boogie program verifier finished with 0 verified, 1 error

 Processing command (at Snapshots20.v0.bpl(9,9)) assert 1 != 1;

@@ -371,7 +390,7 @@ Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold.
 Boogie program verifier finished with 0 verified, 1 error

 Processing call to procedure N in implementation M (at Snapshots20.v1.bpl(7,9)):

   >>> added axiom: ##extracted_function##1() == (0 != 0)

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1();

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1();

 Processing command (at Snapshots20.v1.bpl(9,9)) assert 1 != 1;

   >>> MarkAsPartiallyVerified

 Processing command (at Snapshots20.v1.bpl(13,9)) assert 2 != 2;

@@ -567,8 +586,8 @@ Processing command (at Snapshots31.v0.bpl(10,5)) assert 0 < g;
 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure Q in implementation P (at Snapshots31.v1.bpl(9,5)):

   >>> added axiom: (forall call0old#AT#g: int, g: int :: {:weight 30} { ##extracted_function##1(call0old#AT#g, g) } ##extracted_function##1(call0old#AT#g, g) == (call0old#AT#g < g))

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g, g);

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g, g);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#g, g);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#g, g);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots31.v1.bpl(10,5)) assert 0 < g;

   >>> MarkAsPartiallyVerified

@@ -582,8 +601,8 @@ Boogie program verifier finished with 1 verified, 0 errors
 Processing call to procedure Q in implementation P (at Snapshots32.v1.bpl(8,5)):

   >>> added axiom: (forall g##old##0: int, g: int :: {:weight 30} { ##extracted_function##1(g##old##0, g) } ##extracted_function##1(g##old##0, g) == (g##old##0 < g))

   >>> added before: g##old##0 := g;

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(g##old##0, g);

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(g##old##0, g);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(g##old##0, g);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(g##old##0, g);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots32.v1.bpl(9,5)) assert 0 < g;

   >>> MarkAsPartiallyVerified

@@ -594,7 +613,38 @@ Processing command (at Snapshots33.v0.bpl(10,5)) assert 0 < g;
   >>> DoNothingToAssert

 

 Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P (at Snapshots33.v1.bpl(3,42)):

+  >>> added axiom: (forall g: int :: {:weight 30} { ##extracted_function##1(g) } ##extracted_function##1(g) == (g == 0))

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(g);

 Processing call to procedure Q in implementation P (at Snapshots33.v1.bpl(5,5)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##1 := a##cached##1 && false;

+

+Boogie program verifier finished with 1 verified, 0 errors

+Processing command (at Snapshots34.v0.bpl(6,5)) assert 1 != 1;

+  >>> DoNothingToAssert

+

+Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P (at Snapshots34.v1.bpl(3,42)):

+  >>> added axiom: ##extracted_function##1() == (0 != 0)

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();

+  >>> AssumeNegationOfAssumptionVariable

+Processing command (at Snapshots34.v1.bpl(5,5)) assert 1 != 1;

+  >>> MarkAsPartiallyVerified

+Snapshots34.v1.bpl(5,5): Error BP5001: This assertion might not hold.

+

+Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots35.v0.bpl(6,5)) assert p;

+  >>> DoNothingToAssert

 

 Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P (at Snapshots35.v1.bpl(3,42)):

+  >>> added axiom: (forall p: bool :: {:weight 30} { ##extracted_function##1(p) } ##extracted_function##1(p) == p)

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(p);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(p);

+  >>> AssumeNegationOfAssumptionVariable

+Processing command (at Snapshots35.v1.bpl(5,5)) assert p;

+  >>> MarkAsPartiallyVerified

+Snapshots35.v1.bpl(5,5): Error BP5001: This assertion might not hold.

+

+Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/test2/AssumptionVariables0.bpl b/Test/test2/AssumptionVariables0.bpl
index cc73707c..766c9d1e 100644
--- a/Test/test2/AssumptionVariables0.bpl
+++ b/Test/test2/AssumptionVariables0.bpl
@@ -28,13 +28,46 @@ procedure Test2()
 }

 

 

-var {:assumption} a0: bool;

+var {:assumption} ga0: bool;

 

 

 procedure Test3()

-  modifies a0;

+  modifies ga0;

 {

-    a0 := a0 && true;

+    ga0 := ga0 && true;

 

-    assert a0;  // error

+    assert ga0;  // error

+}

+

+

+procedure Test4()

+{

+    var {:assumption} a0: bool;

+    var tmp: bool;

+

+    tmp := a0;

+

+    havoc a0;

+

+    assert a0 ==> tmp;

+}

+

+

+procedure Test5(A: bool)

+{

+    var {:assumption} a0: bool;

+    var tmp0, tmp1: bool;

+

+    a0 := a0 && A;

+    tmp0 := a0;

+

+    havoc a0;

+

+    assert a0 ==> tmp0;

+

+    tmp1 := a0;

+

+    havoc a0;

+

+    assert a0 ==> tmp1;

 }

diff --git a/Test/test2/AssumptionVariables0.bpl.expect b/Test/test2/AssumptionVariables0.bpl.expect
index 54ddb2a9..44292082 100644
--- a/Test/test2/AssumptionVariables0.bpl.expect
+++ b/Test/test2/AssumptionVariables0.bpl.expect
@@ -1,11 +1,11 @@
-AssumptionVariables0.bpl(17,5): Error BP5001: This assertion might not hold.
-Execution trace:
-    AssumptionVariables0.bpl(15,8): anon0
-AssumptionVariables0.bpl(27,5): Error BP5001: This assertion might not hold.
-Execution trace:
-    AssumptionVariables0.bpl(25,5): anon0
-AssumptionVariables0.bpl(39,5): Error BP5001: This assertion might not hold.
-Execution trace:
-    AssumptionVariables0.bpl(37,8): anon0
-
-Boogie program verifier finished with 1 verified, 3 errors
+AssumptionVariables0.bpl(17,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    AssumptionVariables0.bpl(15,8): anon0

+AssumptionVariables0.bpl(27,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    AssumptionVariables0.bpl(25,5): anon0

+AssumptionVariables0.bpl(39,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    AssumptionVariables0.bpl(37,9): anon0

+

+Boogie program verifier finished with 3 verified, 3 errors

diff --git a/Test/test2/CallVerifiedUnder0.bpl b/Test/test2/CallVerifiedUnder0.bpl
new file mode 100644
index 00000000..9ac9dec7
--- /dev/null
+++ b/Test/test2/CallVerifiedUnder0.bpl
@@ -0,0 +1,42 @@
+// RUN: %boogie -noinfer "%s" > "%t"

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

+

+procedure A(P: bool);

+  requires P;

+

+procedure Test0()

+{

+    call {:verified_under false} A(false);  // error

+}

+

+

+procedure Test1()

+{

+    call {:verified_under true} A(false);

+}

+

+

+procedure Test2(P: bool, A: bool)

+{

+    call {:verified_under A} A(P);  // error

+}

+

+

+procedure Test3(P: bool, A: bool)

+  requires !A ==> P;

+{

+    call {:verified_under A} A(P);

+}

+

+

+procedure Test4(P: bool, A: bool)

+{

+    call {:verified_under A} {:verified_under true} A(P);  // error

+}

+

+

+procedure Test5(P: bool, A: bool)

+  requires !A ==> P;

+{

+    call {:verified_under A} {:verified_under true} A(P);

+}

diff --git a/Test/test2/CallVerifiedUnder0.bpl.expect b/Test/test2/CallVerifiedUnder0.bpl.expect
new file mode 100644
index 00000000..5d407874
--- /dev/null
+++ b/Test/test2/CallVerifiedUnder0.bpl.expect
@@ -0,0 +1,14 @@
+CallVerifiedUnder0.bpl(9,5): Error BP5002: A precondition for this call might not hold.

+CallVerifiedUnder0.bpl(5,3): Related location: This is the precondition that might not hold.

+Execution trace:

+    CallVerifiedUnder0.bpl(9,5): anon0

+CallVerifiedUnder0.bpl(21,5): Error BP5002: A precondition for this call might not hold.

+CallVerifiedUnder0.bpl(5,3): Related location: This is the precondition that might not hold.

+Execution trace:

+    CallVerifiedUnder0.bpl(21,5): anon0

+CallVerifiedUnder0.bpl(34,5): Error BP5002: A precondition for this call might not hold.

+CallVerifiedUnder0.bpl(5,3): Related location: This is the precondition that might not hold.

+Execution trace:

+    CallVerifiedUnder0.bpl(34,5): anon0

+

+Boogie program verifier finished with 3 verified, 3 errors

diff --git a/Test/test2/InvariantVerifiedUnder0.bpl b/Test/test2/InvariantVerifiedUnder0.bpl
new file mode 100644
index 00000000..6cade5a5
--- /dev/null
+++ b/Test/test2/InvariantVerifiedUnder0.bpl
@@ -0,0 +1,54 @@
+// RUN: %boogie -noinfer "%s" > "%t"

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

+

+procedure Test0()

+{

+    while (*)

+      invariant {:verified_under false} false;  // error

+    {}

+}

+

+

+procedure Test1()

+{

+    while (*)

+      invariant {:verified_under true} false;

+    {}

+}

+

+

+procedure Test2(P: bool, Q: bool, A: bool)

+{

+    while (*)

+      invariant {:verified_under A} P;  // error

+      invariant {:verified_under A} Q;  // error

+    {}

+}

+

+

+procedure Test3(P: bool, Q: bool, A: bool)

+  requires !A ==> P;

+{

+    while (*)

+      invariant {:verified_under A} P;

+      invariant {:verified_under A} Q;  // error

+    {}

+}

+

+procedure Test4(P: bool, Q: bool, A: bool)

+{

+    while (*)

+      invariant {:verified_under A} {:verified_under true} P;  // error

+      invariant {:verified_under A} {:verified_under true} Q;  // error

+    {}

+}

+

+

+procedure Test5(P: bool, Q: bool, A: bool)

+  requires !A ==> Q;

+{

+    while (*)

+      invariant {:verified_under A} {:verified_under true} P;  // error

+      invariant {:verified_under A} {:verified_under true} Q;

+    {}

+}

diff --git a/Test/test2/InvariantVerifiedUnder0.bpl.expect b/Test/test2/InvariantVerifiedUnder0.bpl.expect
new file mode 100644
index 00000000..171a6760
--- /dev/null
+++ b/Test/test2/InvariantVerifiedUnder0.bpl.expect
@@ -0,0 +1,23 @@
+InvariantVerifiedUnder0.bpl(7,7): Error BP5001: This assertion might not hold.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(6,5): anon0

+InvariantVerifiedUnder0.bpl(23,7): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(22,5): anon0

+InvariantVerifiedUnder0.bpl(24,7): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(22,5): anon0

+InvariantVerifiedUnder0.bpl(34,7): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(32,5): anon0

+InvariantVerifiedUnder0.bpl(41,7): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(40,5): anon0

+InvariantVerifiedUnder0.bpl(42,7): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(40,5): anon0

+InvariantVerifiedUnder0.bpl(51,7): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(50,5): anon0

+

+Boogie program verifier finished with 1 verified, 7 errors