Merge

20 files changed, 213 insertions, 198 deletions

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 6cce0aac..1ac80970 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -659,7 +659,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
         Lo = Hi = null;

         return base.VisitExpr(node);

       }

-      public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {

+      public override Expr VisitLiteralExpr(LiteralExpr node) {

         if (node.Val is BigNum) {

           var n = ((BigNum)node.Val).ToBigInteger;

           Lo = n;

@@ -944,11 +944,11 @@ namespace Microsoft.Boogie.AbstractInterpretation
         // don't recurse on subexpression

         return node;

       }

-      public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {

+      public override Expr VisitBvConcatExpr(BvConcatExpr node) {

         // don't recurse on subexpression

         return node;

       }

-      public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) {

+      public override Expr VisitBvExtractExpr(BvExtractExpr node) {

         // don't recurse on subexpression

         return node;

       }

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 817897b7..9f7e57cf 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -128,10 +128,10 @@ namespace Microsoft.Boogie {
     public Absy(IToken tok) {

       Contract.Requires(tok != null);

       this._tok = tok;

-      this.uniqueId = AbsyNodeCount++;

+      this.uniqueId = System.Threading.Interlocked.Increment(ref CurrentAbsyNodeId);

     }

 

-    private static int AbsyNodeCount = 0;

+    private static int CurrentAbsyNodeId = -1;

 

     // We uniquely number every AST node to make them

     // suitable for our implementation of functional maps.

@@ -162,7 +162,7 @@ namespace Microsoft.Boogie {
     public virtual Absy Clone() {

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

       Absy/*!*/ result = cce.NonNull((Absy/*!*/)this.MemberwiseClone());

-      result.uniqueId = AbsyNodeCount++; // BUGBUG??

+      result.uniqueId = System.Threading.Interlocked.Increment(ref CurrentAbsyNodeId); // BUGBUG??

 

       if (InternalNumberedMetadata != null) {

         // This should probably use the lock

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index d14250c1..b5581ea6 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -3216,10 +3216,7 @@ namespace Microsoft.Boogie {
       if (stream.UseForComputingChecksums && QKeyValue.FindBoolAttribute(Attributes, "precondition_previous_snapshot")) { return; }

 

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

-      if (!stream.UseForComputingChecksums)

-      {

-        EmitAttributes(stream, Attributes);

-      }

+      EmitAttributes(stream, Attributes);

       this.Expr.Emit(stream);

       stream.WriteLine(";");

     }

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index e2113ab5..4a7db752 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -754,7 +754,7 @@ namespace Microsoft.Boogie {
     }

     public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

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

-      if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

+      if (CommandLineOptions.Clo.PrintWithUniqueASTIds && !stream.UseForComputingChecksums) {

         stream.Write("{0}^^", this.Decl == null ? "NoDecl" : "h" + this.Decl.GetHashCode());

       }

       stream.Write(this, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name));

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index c5b7b317..86338d30 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -622,10 +622,9 @@ namespace Microsoft.Boogie {
   public abstract class QuantifierExpr : BinderExpr {

     public Trigger Triggers;

 

-    static int SkolemIds = 0;

+    static int SkolemIds = -1;

     public static int GetNextSkolemId() {

-      SkolemIds++;

-      return SkolemIds;

+      return System.Threading.Interlocked.Increment(ref SkolemIds);

     }

 

     public readonly int SkolemId;

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 072e0323..3559e0c9 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -431,7 +431,28 @@ namespace Microsoft.Boogie {
     public bool Trace = false;

     public bool TraceTimes = false;

     public bool TraceProofObligations = false;

-    public int TraceCaching = 0;

+    public bool TraceCachingForTesting

+    {

+      get

+      {

+        return TraceCaching == 1 || TraceCaching == 3;

+      }

+    }

+    public bool TraceCachingForBenchmarking

+    {

+      get

+      {

+        return TraceCaching == 2 || TraceCaching == 3;

+      }

+    }

+    public bool TraceCachingForDebugging

+    {

+      get

+      {

+        return TraceCaching == 3;

+      }

+    }

+    internal int TraceCaching = 0;

     public bool NoResolve = false;

     public bool NoTypecheck = false;

     public bool OverlookBoogieTypeErrors = false;

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 32eb2480..4350571a 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -77,11 +77,11 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Block>() != null);

       return base.VisitBlock((Block) node.Clone());

     }

-    public override BvConcatExpr VisitBvConcatExpr (BvConcatExpr node) {

+    public override Expr VisitBvConcatExpr (BvConcatExpr node) {

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

       return base.VisitBvConcatExpr((BvConcatExpr) node.Clone());

     }

-    public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) {

+    public override Expr VisitBvExtractExpr(BvExtractExpr node) {

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

       return base.VisitBvExtractExpr((BvExtractExpr) node.Clone());

     }

@@ -204,7 +204,7 @@ namespace Microsoft.Boogie {
         Contract.Ensures(Contract.Result<List<Ensures>>() != null);

         return base.VisitEnsuresSeq(new List<Ensures>(ensuresSeq));

     }

-    public override ExistsExpr VisitExistsExpr(ExistsExpr node) {

+    public override Expr VisitExistsExpr(ExistsExpr node) {

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

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

       return base.VisitExistsExpr((ExistsExpr)node.Clone());

@@ -219,7 +219,7 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<List<Expr>>() != null);

       return base.VisitExprSeq(new List<Expr>(list));

     }

-    public override ForallExpr VisitForallExpr(ForallExpr node) {

+    public override Expr VisitForallExpr(ForallExpr node) {

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

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

       return base.VisitForallExpr((ForallExpr)node.Clone());

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

       return impl;

     }

-    public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {

+    public override Expr VisitLiteralExpr(LiteralExpr node) {

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

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

       return base.VisitLiteralExpr((LiteralExpr)node.Clone());

diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs
index b477e7de..d75a4b7d 100644
--- a/Source/Core/InterProceduralReachabilityGraph.cs
+++ b/Source/Core/InterProceduralReachabilityGraph.cs
@@ -12,8 +12,8 @@ namespace Microsoft.Boogie
   public interface IInterproceduralReachabilityGraph {

 

     bool MayReach(Block src, Block dst);

-    void dump();

 

+    void dump();

 

     Block GetNewEntryBlock(string p);

 

@@ -58,7 +58,15 @@ namespace Microsoft.Boogie
           }

         }

       }

-      

+

+      foreach(var n in nodes) {

+        // If there are disconnected nodes, put them into the

+        // graph as self-loops so that every node is represented in

+        // the graph

+        if(!reachabilityGraph.Nodes.Contains(n)) {

+          reachabilityGraph.AddEdge(n, n);

+        }

+      }

     }

 

     private IEnumerable<Block> OriginalProgramBlocks()

@@ -142,10 +150,9 @@ namespace Microsoft.Boogie
         newProcedureExitNodes[impl.Name] = newExit;

         foreach (Block b in impl.Blocks)

         {

-          List<List<Cmd>> partition = PartitionCmdsAccordingToPredicate(b.Cmds, Item => Item is CallCmd);

           Block prev = null;

           int i = 0;

-          foreach (List<Cmd> cmds in partition)

+          foreach (List<Cmd> cmds in SeparateCallCmds(b.Cmds))

           {

             Block newBlock;

             if (prev == null)

@@ -190,16 +197,24 @@ namespace Microsoft.Boogie
       #endregion

     }

 

-    public static List<List<Cmd>> PartitionCmdsAccordingToPredicate(List<Cmd> Cmds, Func<Cmd, bool> Predicate) {

+    private static List<List<Cmd>> SeparateCallCmds(List<Cmd> Cmds) {

       List<List<Cmd>> result = new List<List<Cmd>>();

-      List<Cmd> current = new List<Cmd>();

-      result.Add(current);

-      foreach(Cmd cmd in Cmds) {

-        if(Predicate(cmd) && current.Count > 0) {

-           current = new List<Cmd>();

-           result.Add(current);

+      int currentIndex = 0;

+      while(currentIndex < Cmds.Count) {

+        if(Cmds[currentIndex] is CallCmd) {

+          result.Add(new List<Cmd> { Cmds[currentIndex] });

+          currentIndex++;

+        } else {

+          List<Cmd> nonCallCmds = new List<Cmd>();

+          while(currentIndex < Cmds.Count && !(Cmds[currentIndex] is CallCmd)) {

+            nonCallCmds.Add(Cmds[currentIndex]);

+            currentIndex++;

+          }

+          result.Add(nonCallCmds);

         }

-        current.Add(cmd);

+      }

+      if(result.Count == 0) {

+        result.Add(new List<Cmd>());

       }

       return result;

     }

diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs
index 603f7e72..d07eaac6 100644
--- a/Source/Core/LambdaHelper.cs
+++ b/Source/Core/LambdaHelper.cs
@@ -65,6 +65,12 @@ namespace Microsoft.Boogie {
 

       int lambdaid = 0;

 

+      string FreshLambdaFunctionName()

+      {

+        // TODO(wuestholz): Should we use a counter per top-level declaration?

+        return string.Format("lambda#{0}", lambdaid++);

+      }

+

       public override Expr VisitLambdaExpr(LambdaExpr lambda) {

         var baseResult = base.VisitLambdaExpr(lambda);

         lambda = baseResult as LambdaExpr;

@@ -168,7 +174,7 @@ namespace Microsoft.Boogie {
           if (CommandLineOptions.Clo.TraceVerify) {

             Console.WriteLine("New lambda: {0}", lam_str);

           }

-          Function fn = new Function(tok, "lambda#" + lambdaid++, freshTypeVars, formals, res, "auto-generated lambda function",

+          Function fn = new Function(tok, FreshLambdaFunctionName(), freshTypeVars, formals, res, "auto-generated lambda function",

             Substituter.Apply(Substituter.SubstitutionFromHashtable(substFnAttrs), lambdaAttrs));

 

           fcall = new FunctionCall(new IdentifierExpr(tok, fn.Name));

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index f7538b53..82cd5025 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -103,7 +103,7 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Type>() != null);

       return this.VisitType(node);

     }

-    public virtual BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {

+    public virtual Expr VisitBvConcatExpr(BvConcatExpr node) {

       Contract.Requires(node != null);

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

       node.E0 = this.VisitExpr(node.E0);

@@ -239,13 +239,13 @@ namespace Microsoft.Boogie {
       node.OutParams = this.VisitVariableSeq(node.OutParams);

       return node;

     }

-    public virtual ExistsExpr VisitExistsExpr(ExistsExpr node) {

+    public virtual Expr VisitExistsExpr(ExistsExpr node) {

       Contract.Requires(node != null);

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

       node = (ExistsExpr)this.VisitQuantifierExpr(node);

       return node;

     }

-    public virtual BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) {

+    public virtual Expr VisitBvExtractExpr(BvExtractExpr node) {

       Contract.Requires(node != null);

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

       node.Bitvector = this.VisitExpr(node.Bitvector);

@@ -290,7 +290,7 @@ namespace Microsoft.Boogie {
         ensuresSeq[i] = this.VisitEnsures(ensuresSeq[i]);

       return ensuresSeq;

     }

-    public virtual ForallExpr VisitForallExpr(ForallExpr node) {

+    public virtual Expr VisitForallExpr(ForallExpr node) {

       Contract.Requires(node != null);

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

       node = (ForallExpr)this.VisitQuantifierExpr(node);

@@ -359,7 +359,7 @@ namespace Microsoft.Boogie {
       node = (Implementation)this.VisitDeclWithFormals(node); // do this first or last?

       return node;

     }

-    public virtual LiteralExpr VisitLiteralExpr(LiteralExpr node) {

+    public virtual Expr VisitLiteralExpr(LiteralExpr node) {

       Contract.Requires(node != null);

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

       return node;

@@ -679,7 +679,7 @@ namespace Microsoft.Boogie {
           Contract.Ensures(Contract.Result<Type>() == node);

           return this.VisitType(node);

       }

-      public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node)

+      public override Expr VisitBvConcatExpr(BvConcatExpr node)

       {

           Contract.Ensures(Contract.Result<BvConcatExpr>() == node);

           this.VisitExpr(node.E0);

@@ -805,12 +805,12 @@ namespace Microsoft.Boogie {
           this.VisitVariableSeq(node.OutParams);

           return node;

       }

-      public override ExistsExpr VisitExistsExpr(ExistsExpr node)

+      public override Expr VisitExistsExpr(ExistsExpr node)

       {

           Contract.Ensures(Contract.Result<ExistsExpr>() == node);

           return (ExistsExpr)this.VisitQuantifierExpr(node);

       }

-      public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node)

+      public override Expr VisitBvExtractExpr(BvExtractExpr node)

       {

           Contract.Ensures(Contract.Result<BvExtractExpr>() == node);

           this.VisitExpr(node.Bitvector);

@@ -854,7 +854,7 @@ namespace Microsoft.Boogie {
               this.VisitEnsures(ensuresSeq[i]);

           return ensuresSeq;

       }

-      public override ForallExpr VisitForallExpr(ForallExpr node)

+      public override Expr VisitForallExpr(ForallExpr node)

       {

           Contract.Ensures(Contract.Result<ForallExpr>() == node);

           return (ForallExpr)this.VisitQuantifierExpr(node);

@@ -915,7 +915,7 @@ namespace Microsoft.Boogie {
           this.VisitProcedure(cce.NonNull(node.Proc));

           return (Implementation)this.VisitDeclWithFormals(node); // do this first or last?

       }

-      public override LiteralExpr VisitLiteralExpr(LiteralExpr node)

+      public override Expr VisitLiteralExpr(LiteralExpr node)

       {

           Contract.Ensures(Contract.Result<LiteralExpr>() == node);

           return node;

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index 73008742..4afd6f69 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -676,14 +676,13 @@ namespace Microsoft.Boogie {
       // any filename extension specified by the user.  We base our

       // calculations on that there is at most one occurrence of @PROC@.

       if (180 <= fileName.Length - 6 + pn.Length) {

-        pn = pn.Substring(0, Math.Max(180 - (fileName.Length - 6), 0)) + "-n" + sequenceNumber;

-        sequenceNumber++;

+        pn = pn.Substring(0, Math.Max(180 - (fileName.Length - 6), 0)) + "-n" + System.Threading.Interlocked.Increment(ref sequenceId);

       }

 

       return fileName.Replace("@PROC@", pn);

     }

 

-    private static int sequenceNumber = 0;

+    private static int sequenceId = -1;

 

   }

 }

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index c0d66720..0874addc 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1020,7 +1020,7 @@ namespace Microsoft.Boogie
         programCache.Set(programId, program, policy);

       }

 

-      if (0 <= CommandLineOptions.Clo.VerifySnapshots && 2 <= CommandLineOptions.Clo.TraceCaching)

+      if (0 <= CommandLineOptions.Clo.VerifySnapshots && CommandLineOptions.Clo.TraceCachingForBenchmarking)

       {

         var end = DateTime.UtcNow;

         if (TimePerRequest.Count == 0)

@@ -1030,7 +1030,7 @@ namespace Microsoft.Boogie
         TimePerRequest[requestId] = end.Subtract(start);

         StatisticsPerRequest[requestId] = stats;

 

-        var printTimes = 3 <= CommandLineOptions.Clo.TraceCaching;

+        var printTimes = true;

 

         Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(printTimes));

 

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 226efa21..5d20e6e8 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -247,7 +247,7 @@ namespace Microsoft.Boogie
         }

 

         node.ExtendDesugaring(before, beforePrecondtionCheck, after);

-        if (1 <= CommandLineOptions.Clo.TraceCaching)

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

         {

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

           {

@@ -336,8 +336,7 @@ namespace Microsoft.Boogie
       {

         var forallExpr = new ForallExpr(Token.NoToken, boundVars.ToList<Variable>(), new Trigger(Token.NoToken, true, new List<Expr> { axiomCall }), eq);

         body = forallExpr;

-        // TODO(wuestholz): Try assigning a higher weight to these quantifiers:

-        // forallExpr.Attributes = new QKeyValue(Token.NoToken, "weight", new List<object> { new LiteralExpr(Token.NoToken, Basetypes.BigNum.FromInt(20)) }, null);

+        forallExpr.Attributes = new QKeyValue(Token.NoToken, "weight", new List<object> { new LiteralExpr(Token.NoToken, Basetypes.BigNum.FromInt(30)) }, null);

         body.Type = Type.Bool;

       }

       else

@@ -377,7 +376,7 @@ namespace Microsoft.Boogie
       }

 

       var end = DateTime.UtcNow;

-      if (3 <= CommandLineOptions.Clo.TraceCaching)

+      if (CommandLineOptions.Clo.TraceCachingForDebugging)

       {

         Console.Out.WriteLine("Collected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);

       }

@@ -426,7 +425,7 @@ namespace Microsoft.Boogie
       dc.VisitProgram(program);

 

       var end = DateTime.UtcNow;

-      if (3 <= CommandLineOptions.Clo.TraceCaching)

+      if (CommandLineOptions.Clo.TraceCachingForDebugging)

       {

         Console.Out.WriteLine("Collected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);

       }

diff --git a/Source/Houdini/AnnotationDependenceAnalyser.cs b/Source/Houdini/AnnotationDependenceAnalyser.cs
index 1d12b6b1..e925d413 100644
--- a/Source/Houdini/AnnotationDependenceAnalyser.cs
+++ b/Source/Houdini/AnnotationDependenceAnalyser.cs
@@ -460,6 +460,7 @@ namespace Microsoft.Boogie.Houdini {
 

         if (NoStages())

         {

+          Debug.Assert(false);

           var TrivialGraph = new Graph<ScheduledStage>();

           TrivialGraph.AddSource(new ScheduledStage(0, new HashSet<string>()));

           return new StagedHoudiniPlan(TrivialGraph);

diff --git a/Source/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs
index f5ddc92a..27481e4f 100644
--- a/Source/Houdini/StagedHoudini.cs
+++ b/Source/Houdini/StagedHoudini.cs
@@ -33,6 +33,8 @@ namespace Microsoft.Boogie.Houdini
         houdiniInstances[i] = new List<Houdini>();

       }

 

+      BreakApartConjunctionsInAnnotations();

+

       var annotationDependenceAnalyser = new AnnotationDependenceAnalyser(program);

       annotationDependenceAnalyser.Analyse();

       this.plan = annotationDependenceAnalyser.ApplyStages();

@@ -53,6 +55,68 @@ namespace Microsoft.Boogie.Houdini
       }

     }

 

+    private void BreakApartConjunctionsInAnnotations()

+    {

+      // StagedHoudini works on a syntactic basis, so that

+      // if x and y occur in the same annotation, any annotation

+      // referring to either x or y will be in the same stage

+      // as this annotation.  It is thus desirable to separate

+      // conjunctive annotations into multiple annotations,

+      // to reduce these syntactic dependencies.

+

+      foreach(var b in program.Blocks()) {

+        List<Cmd> newCmds = new List<Cmd>();

+        foreach(var c in b.Cmds) {

+          var assertion = c as AssertCmd;

+          if (assertion != null) {

+            foreach(var e in BreakIntoConjuncts(assertion.Expr)) {

+              newCmds.Add(new AssertCmd(assertion.tok, e, assertion.Attributes));

+            }

+          } else {

+            newCmds.Add(c);

+          }

+        }

+        b.Cmds = newCmds;

+      }

+

+      foreach(var proc in program.Procedures) {

+        {

+          var newRequires = new List<Requires>();

+          foreach(var r in proc.Requires) {

+            foreach(var c in BreakIntoConjuncts(r.Condition)) {

+              newRequires.Add(new Requires(r.tok, r.Free, c, r.Comment, r.Attributes));

+            }

+          }

+          proc.Requires = newRequires;

+        }

+        {

+          var newEnsures = new List<Ensures>();

+          foreach(var e in proc.Ensures) {

+            foreach(var c in BreakIntoConjuncts(e.Condition)) {

+              newEnsures.Add(new Ensures(e.tok, e.Free, c, e.Comment, e.Attributes));

+            }

+          }

+          proc.Ensures = newEnsures;

+        }

+      }

+    }

+

+    private List<Expr> BreakIntoConjuncts(Expr expr)

+    {

+      var nary = expr as NAryExpr;

+      if(nary == null) {

+        return new List<Expr> { expr };

+      }

+      var fun = nary.Fun as BinaryOperator;

+      if(fun == null || (fun.Op != BinaryOperator.Opcode.And)) {

+        return new List<Expr> { expr };

+      }

+      var result = new List<Expr>();

+      result.AddRange(BreakIntoConjuncts(nary.Args[0]));

+      result.AddRange(BreakIntoConjuncts(nary.Args[1]));

+      return result;

+    }

+

     private bool NoStages() {

       return plan == null;

     }

@@ -124,6 +188,12 @@ namespace Microsoft.Boogie.Houdini
         Item => plan.GetDependences(s).Contains(Item.stage)).

           Select(Item => Item.parallelTask).ToArray());

 

+      if(s.Count() == 0) {

+        // This is the trivial first stage, so don't launch Houdini;

+        // give this a null outcome

+        return;

+      }

+

       List<Houdini> h = AcquireHoudiniInstance();

 

       if (h.Count() == 0)

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 91c17b23..49dbb7c8 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -314,7 +314,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

     ///////////////////////////////////////////////////////////////////////////////////

 

-    public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {

+    public override Expr VisitLiteralExpr(LiteralExpr node) {

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

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

       Push(TranslateLiteralExpr(node));

@@ -454,14 +454,14 @@ namespace Microsoft.Boogie.VCExprAST {
       return node;

     }

 

-    public override ExistsExpr VisitExistsExpr(ExistsExpr node) {

+    public override Expr VisitExistsExpr(ExistsExpr node) {

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

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

       node = (ExistsExpr)this.VisitQuantifierExpr(node);

       return node;

     }

 

-    public override ForallExpr VisitForallExpr(ForallExpr node) {

+    public override Expr VisitForallExpr(ForallExpr node) {

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

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

       node = (ForallExpr)this.VisitQuantifierExpr(node);

@@ -557,7 +557,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

     ///////////////////////////////////////////////////////////////////////////////////

 

-    public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) {

+    public override Expr VisitBvExtractExpr(BvExtractExpr node) {

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

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

       Push(TranslateBvExtractExpr(node));

@@ -574,7 +574,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

     ///////////////////////////////////////////////////////////////////////////////////

 

-    public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {

+    public override Expr VisitBvConcatExpr(BvConcatExpr node) {

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

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

       Push(TranslateBvConcatExpr(node));

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 454a2f30..d72a9d0e 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -608,19 +608,6 @@ namespace VC {
 

     protected Implementation currentImplementation;

 

-    private LocalVariable currentTemporaryVariableForAssertions;

-    protected LocalVariable CurrentTemporaryVariableForAssertions

-    {

-      get

-      {

-        if (currentTemporaryVariableForAssertions == null)

-        {

-          currentTemporaryVariableForAssertions = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "##assertion", Microsoft.Boogie.Type.Bool));

-        }

-        return currentTemporaryVariableForAssertions;

-      }

-    }

-

     protected List<Variable> CurrentLocalVariables = null;

 

     // shared across each implementation; created anew for each implementation

@@ -1334,7 +1321,6 @@ namespace VC {
       Contract.Requires(mvInfo != null);

 

       currentImplementation = impl;

-      currentTemporaryVariableForAssertions = null;

 

       var start = DateTime.UtcNow;

 

@@ -1342,12 +1328,12 @@ namespace VC {
       

       var end = DateTime.UtcNow;

 

-      if (3 <= CommandLineOptions.Clo.TraceCaching)

+      if (CommandLineOptions.Clo.TraceCachingForDebugging)

       {

         Console.Out.WriteLine("Turned implementation into passive commands within {0:F0} ms.\n", end.Subtract(start).TotalMilliseconds);

       }

 

-      if (2 <= CommandLineOptions.Clo.TraceCaching)

+      if (CommandLineOptions.Clo.TraceCachingForDebugging)

       {

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

         {

@@ -1361,7 +1347,6 @@ namespace VC {
         }

       }

 

-      currentTemporaryVariableForAssertions = null;

       currentImplementation = null;

 

       RestoreParamWhereClauses(impl);

@@ -1495,7 +1480,7 @@ namespace VC {
 

     void TraceCachingAction(Cmd cmd, CachingAction action)

     {

-      if (1 <= CommandLineOptions.Clo.TraceCaching)

+      if (CommandLineOptions.Clo.TraceCachingForTesting)

       {

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

         {

@@ -1504,10 +1489,11 @@ namespace VC {
           cmd.Emit(tokTxtWr, 0);

           Console.Out.WriteLine("  >>> {0}", action);

         }

-        if (CachingActionCounts != null)

-        {

-          Interlocked.Increment(ref CachingActionCounts[(int)action]);

-        }

+      }

+      

+      if (CommandLineOptions.Clo.TraceCachingForBenchmarking && CachingActionCounts != null)

+      {

+        Interlocked.Increment(ref CachingActionCounts[(int)action]);

       }

     }

 

@@ -1552,7 +1538,6 @@ namespace VC {
           ac.IncarnationMap = (Dictionary<Variable, Expr>)cce.NonNull(new Dictionary<Variable, Expr>(incarnationMap));

 

           var subsumption = Wlp.Subsumption(ac);

-          var alwaysUseSubsumption = subsumption == CommandLineOptions.SubsumptionOption.Always;

           if (relevantDoomedAssumpVars.Any())

           {

             TraceCachingAction(pc, CachingAction.DoNothingToAssert);

@@ -1573,59 +1558,15 @@ namespace VC {
             {

               bool isTrue;

               var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);

-              if (!isTrue && alwaysUseSubsumption)

-              {

-                TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);

-                var litExpr = ac.Expr as LiteralExpr;

-                if (litExpr == null || !litExpr.IsTrue)

-                {

-                  // Bind the assertion expression to a local variable.

-                  var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock);

-                  var identExpr = new IdentifierExpr(Token.NoToken, incarnation);

-                  incarnationMap[incarnation] = identExpr;

-                  ac.IncarnationMap[incarnation] = identExpr;

-                  passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));

-                  copy = identExpr;

-                  passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr)));

-

-                  // TODO(wuestholz): Try to use this instead:

-                  // ac.MarkAsVerifiedUnder(assmVars);

-                }

-                else

-                {

-                  dropCmd = true;

-                }

-              }

-              else if (isTrue)

+              TraceCachingAction(pc, !isTrue ? CachingAction.MarkAsPartiallyVerified : CachingAction.MarkAsFullyVerified);

+              var litExpr = ac.Expr as LiteralExpr;

+              if (litExpr == null || !litExpr.IsTrue)

               {

-                if (alwaysUseSubsumption)

-                {

-                  TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);

-                  var litExpr = ac.Expr as LiteralExpr;

-                  if (litExpr == null || !litExpr.IsTrue)

-                  {

-                    // Turn it into an assume statement.

-                    pc = new AssumeCmd(ac.tok, copy);

-                    pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);

-                  }

-                  else

-                  {

-                    dropCmd = true;

-                  }

-                }

-                else if (subsumption == CommandLineOptions.SubsumptionOption.Never)

-                {

-                  TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);

-                  dropCmd = true;

-                }

-                else

-                {

-                  TraceCachingAction(pc, CachingAction.DoNothingToAssert);

-                }

+                ac.MarkAsVerifiedUnder(assmVars);

               }

               else

               {

-                TraceCachingAction(pc, CachingAction.DoNothingToAssert);

+                dropCmd = true;

               }

             }

           }

@@ -1636,24 +1577,10 @@ namespace VC {
                    && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)

                    && currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))

           {

-            if (alwaysUseSubsumption)

-            {

-              // Turn it into an assume statement.

-              TraceCachingAction(pc, CachingAction.RecycleError);

-              pc = new AssumeCmd(ac.tok, copy);

-              pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);

-              currentImplementation.AddRecycledFailingAssertion(ac);

-            }

-            else if (subsumption == CommandLineOptions.SubsumptionOption.Never)

-            {

-              TraceCachingAction(pc, CachingAction.RecycleError);

-              dropCmd = true;

-              currentImplementation.AddRecycledFailingAssertion(ac);

-            }

-            else

-            {

-              TraceCachingAction(pc, CachingAction.DoNothingToAssert);

-            }

+            TraceCachingAction(pc, CachingAction.RecycleError);

+            ac.MarkAsVerifiedUnder(Expr.True);

+            currentImplementation.AddRecycledFailingAssertion(ac);

+            pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);

           }

           else

           {

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 8a549e9d..560f55b4 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -521,7 +521,7 @@ namespace VC {
       readonly List<Block> big_blocks = new List<Block>();

       readonly Dictionary<Block/*!*/, BlockStats/*!*/>/*!*/ stats = new Dictionary<Block/*!*/, BlockStats/*!*/>();

       readonly int id;

-      static int current_id;

+      static int current_id = -1;

       Block split_block;

       bool assert_to_assume;

       List<Block/*!*/>/*!*/ assumized_branches = new List<Block/*!*/>();

@@ -557,7 +557,7 @@ namespace VC {
         this.gotoCmdOrigins = gotoCmdOrigins;

         this.parent = par;

         this.impl = impl;

-        this.id = current_id++;

+        this.id = Interlocked.Increment(ref current_id);

       }

 

       public double Cost {

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 6f6326d1..cd735501 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -106,17 +106,12 @@ namespace VC {
         AssertCmd ac = (AssertCmd)cmd;

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

         VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);

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

-

-        VCExprLetBinding LB = null;

         VCExpr VU = null;

         if (ac.VerifiedUnder != null)

         {

-          var V = gen.Variable(ctxt.FreshLetBindingName(), Microsoft.Boogie.Type.Bool);

-          LB = gen.LetBinding(V, C);

-          C = V;

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

         }

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

 

         VCExpr R = null;

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

@@ -127,28 +122,24 @@ namespace VC {
             ctxt.Label2absy[id] = ac;

           }

 

-          switch (Subsumption(ac)) {

-            case CommandLineOptions.SubsumptionOption.Never:

-              break;

-            case CommandLineOptions.SubsumptionOption.Always:

-              N = gen.Implies(C, N);

-              break;

-            case CommandLineOptions.SubsumptionOption.NotForQuantifiers:

-              if (!(C is VCExprQuantifier)) {

-                N = gen.Implies(C, N);

-              }

-              break;

-            default:

-              Contract.Assert(false); throw new cce.UnreachableException();  // unexpected case

+          var subsumption = Subsumption(ac);

+          if (subsumption == CommandLineOptions.SubsumptionOption.Always

+              || (subsumption == CommandLineOptions.SubsumptionOption.NotForQuantifiers && !(C is VCExprQuantifier)))

+          {

+            N = gen.ImpliesSimp(C, N);

           }

 

-          ctxt.AssertionCount++;

+          if (VU != null)

+          {

+            var litExpr = ac.VerifiedUnder as LiteralExpr;

+            if (litExpr != null && litExpr.IsTrue)

+            {

+              return N;

+            }

+            C = gen.OrSimp(VU, C);

+          }

 

-          // TODO(wuestholz): Try to weaken the assertion instead of assuming the property that has already been verified:

-          // if (VU != null)

-          // {

-          //   C = gen.OrSimp(VU, C);

-          // }

+          ctxt.AssertionCount++;

 

           if (ctxt.ControlFlowVariableExpr == null) {

             Contract.Assert(ctxt.Label2absy != null);

@@ -164,16 +155,6 @@ namespace VC {
             }

           }

         }

-

-        if (VU != null)

-        {

-          R = gen.ImpliesSimp(gen.ImpliesSimp(VU, C), R);

-        }

-

-        if (LB != null)

-        {

-          R = gen.Let(R, LB);

-        }

         return R;

       } else if (cmd is AssumeCmd) {

         AssumeCmd ac = (AssumeCmd)cmd;

diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 88dd1a1f..8f3c2015 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -113,7 +113,7 @@ Processing command (at Snapshots6.v0.bpl(13,5)) assert y == 0;
 

 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 :: { ##extracted_function##1(y##old##0, y) } ##extracted_function##1(y##old##0, y) == (y##old##0 == y))

+  >>> 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);

@@ -128,7 +128,7 @@ Processing command (at Snapshots7.v0.bpl(14,5)) assert y < 0;
 

 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 :: { ##extracted_function##1(y, z) } ##extracted_function##1(y, z) == (y < z))

+  >>> 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);

@@ -144,8 +144,8 @@ Processing command (at Snapshots8.v0.bpl(10,5)) assert 0 <= x;
 

 Boogie program verifier finished with 1 verified, 0 errors

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

-  >>> added axiom: (forall call0formal#AT#n: int :: { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))

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

+  >>> 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);

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

@@ -167,8 +167,8 @@ Processing command (at Snapshots9.v0.bpl(10,5)) assert 0 <= x;
 

 Boogie program verifier finished with 1 verified, 0 errors

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

-  >>> added axiom: (forall call0formal#AT#n: int :: { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n && true))

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

+  >>> 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);

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

@@ -188,8 +188,8 @@ Processing command (at Snapshots10.v0.bpl(12,5)) assert 0 <= x;
 

 Boogie program verifier finished with 1 verified, 0 errors

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

-  >>> added axiom: (forall call0formal#AT#n: int :: { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))

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

+  >>> 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);

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

@@ -211,8 +211,8 @@ Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might
 

 Boogie program verifier finished with 0 verified, 1 error

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

-  >>> added axiom: (forall call0formal#AT#n: int :: { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))

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

+  >>> 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);

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

@@ -466,7 +466,7 @@ Processing command (at Snapshots24.v1.bpl(11,9)) assert {:subsumption 1} 5 == 5;
 Processing command (at Snapshots24.v1.bpl(15,9)) assert {:subsumption 2} 6 != 6;

   >>> RecycleError

 Processing command (at Snapshots24.v1.bpl(19,9)) assert {:subsumption 1} 2 == 2;

-  >>> DoNothingToAssert

+  >>> MarkAsFullyVerified

 Processing command (at Snapshots24.v1.bpl(20,9)) assert {:subsumption 2} 4 == 4;

   >>> MarkAsFullyVerified

 Processing command (at Snapshots24.v1.bpl(21,9)) assert 5 == 5;

@@ -566,7 +566,7 @@ 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 :: { ##extracted_function##1(call0old#AT#g, g) } ##extracted_function##1(call0old#AT#g, g) == (call0old#AT#g < g))

+  >>> 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);

   >>> AssumeNegationOfAssumptionVariable

@@ -580,7 +580,7 @@ Processing command (at Snapshots32.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 Snapshots32.v1.bpl(8,5)):

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

+  >>> 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);