Boogie: output number of proof obligations (asserts) along with timing information when using the /trace option

11 files changed, 153 insertions, 113 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index cffe3b5a..4ec10162 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -516,7 +516,7 @@ namespace Microsoft.Boogie {
         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

           vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

         } else if(CommandLineOptions.Clo.StratifiedInlining > 0) {

-            vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+          vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

         } else {

           vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

         }

@@ -529,6 +529,7 @@ namespace Microsoft.Boogie {
       var decls = program.TopLevelDeclarations.ToArray();

       foreach (Declaration decl in decls) {

         Contract.Assert(decl != null);

+        int prevAssertionCount = vcgen.CumulativeAssertionCount;

         Implementation impl = decl as Implementation;

         if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) {

           List<Counterexample/*!*/>/*?*/ errors;

@@ -550,7 +551,7 @@ namespace Microsoft.Boogie {
               if (CommandLineOptions.Clo.inferLeastForUnsat != null)

               {

                   var svcgen = vcgen as VC.StratifiedVCGen;

-                  Debug.Assert(svcgen != null);

+                  Contract.Assert(svcgen != null);

                   var ss = new HashSet<string>();

                   foreach (var tdecl in program.TopLevelDeclarations)

                   {

@@ -587,7 +588,7 @@ namespace Microsoft.Boogie {
           TimeSpan elapsed = end - start;

           if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {

             if (CommandLineOptions.Clo.Trace) {

-              timeIndication = string.Format("  [{0} s]  ", elapsed.TotalSeconds);

+              timeIndication = string.Format("  [{0} s, {1} proof obligations]  ", elapsed.TotalSeconds, vcgen.CumulativeAssertionCount - prevAssertionCount);

             }

           }

 

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 7ff0af6c..76eaf661 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -736,6 +736,7 @@ namespace Microsoft.Boogie {
           return g;

         }

         throw new IrreducibleLoopException();

+#if USED_CODE

         System.Diagnostics.Debug.Assert(g.SplitCandidates.Count > 0);

         Block splitCandidate = null;

         foreach (Block b in g.SplitCandidates) {

@@ -770,6 +771,7 @@ namespace Microsoft.Boogie {
           impl.Blocks.Add(copy);

           gotoCmd.AddTarget(copy);

         }

+#endif

       }

     }

 

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index ef24f07a..3fa678a8 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -590,7 +590,8 @@ namespace Microsoft.Dafny
 

       var decls = program.TopLevelDeclarations.ToArray();

       foreach (var decl in decls )

-      {Contract.Assert(decl != null);

+      {

+        Contract.Assert(decl != null);

         Implementation impl = decl as Implementation;

         if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification)

         {

@@ -612,6 +613,7 @@ namespace Microsoft.Dafny
             }

 

             ConditionGeneration.Outcome outcome;

+            int prevAssertionCount = vcgen.CumulativeAssertionCount;

             try

             {

                 outcome = vcgen.VerifyImplementation(impl, program, out errors);

@@ -636,7 +638,7 @@ namespace Microsoft.Dafny
             {

                 if (CommandLineOptions.Clo.Trace)

                 {

-                    timeIndication = string.Format("  [{0} s]  ", elapsed.TotalSeconds);

+                    timeIndication = string.Format("  [{0} s, {1} proof obligations]  ", elapsed.TotalSeconds, vcgen.CumulativeAssertionCount - prevAssertionCount);

                 }

             }

 

diff --git a/Source/Provers/TPTP/ProverInterface.cs b/Source/Provers/TPTP/ProverInterface.cs
index 424e36ac..662d45d3 100644
--- a/Source/Provers/TPTP/ProverInterface.cs
+++ b/Source/Provers/TPTP/ProverInterface.cs
@@ -240,7 +240,7 @@ USE_PREDICATES=<bool>     Try to use SMT predicates for functions returning bool
       if (CommandLineOptions.Clo.Trace) {

         DateTime end = DateTime.Now;

         TimeSpan elapsed = end - start;

-        Console.WriteLine("finished   [{0} s]  ", elapsed.TotalSeconds);

+        Console.WriteLine("finished   [{0} s]", elapsed.TotalSeconds);

       }

       return res;

     }

diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 388cf91b..45f2d098 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -350,7 +350,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
 

       if (CommandLineOptions.Clo.Trace) {

         TimeSpan elapsed = DateTime.Now - start;

-        Console.WriteLine("finished   [{0} s]  ", elapsed.TotalSeconds);

+        Console.WriteLine("finished   [{0} s]", elapsed.TotalSeconds);

       }

       return res;

     }

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index ed698d5f..bdbdd0f2 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -479,6 +479,8 @@ namespace VC {
       Contract.Invariant(program != null);

     }

 

+    public int CumulativeAssertionCount;  // for statistics

+

     protected readonly List<Checker>/*!>!*/ checkers = new List<Checker>();

     protected VariableSeq CurrentLocalVariables = null;

 

diff --git a/Source/VCGeneration/DoomCheck.cs b/Source/VCGeneration/DoomCheck.cs
index 9e1b2b1c..8571caee 100644
--- a/Source/VCGeneration/DoomCheck.cs
+++ b/Source/VCGeneration/DoomCheck.cs
@@ -170,7 +170,7 @@ void ObjectInvariant()
         }

 

         [NotDelayed]

-        public DoomCheck (Implementation passive_impl, Block unifiedExit, Checker check, List<Block> uncheckable) {

+        public DoomCheck (Implementation passive_impl, Block unifiedExit, Checker check, List<Block> uncheckable, out int assertionCount) {

           Contract.Requires(passive_impl != null);

           Contract.Requires(check != null);

           Contract.Requires(uncheckable != null);

@@ -217,7 +217,7 @@ void ObjectInvariant()
             Label2Absy = new Hashtable(); // This is only a dummy

             m_Evc = new Evc(check);

             Hashtable l2a = null;

-            VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check);

+            VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount);

             Contract.Assert(vce != null);

             Contract.Assert( l2a!=null);

             Label2Absy = l2a;

@@ -233,7 +233,8 @@ void ObjectInvariant()
             Label2Absy = new Hashtable(); // This is only a dummy

             m_Evc = new Evc(check);

             Hashtable l2a = null;

-            VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check);

+            int assertionCount;  // compute and then ignore

+            VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount);

             Contract.Assert(vce != null);

             Contract.Assert(l2a != null);

             Label2Absy = l2a;

@@ -293,42 +294,41 @@ void ObjectInvariant()
             CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Doomed;

             #endregion

 

-       */ 

-       

-        VCExpr GenerateEVC(Implementation impl, out Hashtable label2absy, Checker ch)

-        {

+       */

+

+        VCExpr GenerateEVC(Implementation impl, out Hashtable label2absy, Checker ch, out int assertionCount) {

           Contract.Requires(impl != null);

           Contract.Requires(ch != null);

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

 

-			    TypecheckingContext tc = new TypecheckingContext(null);

-			    impl.Typecheck(tc);

-			    label2absy = new Hashtable/*<int, Absy!>*/();

-			    VCExpr vc;

-			    switch (CommandLineOptions.Clo.vcVariety) {

-				    case CommandLineOptions.VCVariety.Doomed:

-                        

-                        vc = LetVC(cce.NonNull(impl.Blocks[0]), label2absy, ch.TheoremProver.Context);

-				    					    

-					    break;

-					    

-				    default:

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

-			    }

-			    return vc;

+          TypecheckingContext tc = new TypecheckingContext(null);

+          impl.Typecheck(tc);

+          label2absy = new Hashtable/*<int, Absy!>*/();

+          VCExpr vc;

+          switch (CommandLineOptions.Clo.vcVariety) {

+            case CommandLineOptions.VCVariety.Doomed:

+              vc = LetVC(cce.NonNull(impl.Blocks[0]), label2absy, ch.TheoremProver.Context, out assertionCount);

+              break;

+

+            default:

+              Contract.Assert(false); throw new cce.UnreachableException();  // unexpected enumeration value

+          }

+          return vc;

         }

 

         public VCExpr LetVC(Block startBlock,

-                             Hashtable/*<int, Absy!>*/ label2absy,

-                             ProverContext proverCtxt)

-        {Contract.Requires(startBlock != null);

+                            Hashtable/*<int, Absy!>*/ label2absy,

+                            ProverContext proverCtxt,

+                            out int assertionCount)

+        {

+          Contract.Requires(startBlock != null);

           Contract.Requires(label2absy != null);

           Contract.Requires(proverCtxt != null);

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

 

           Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();

           List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();

-          VCExpr startCorrect = LetVC(startBlock, label2absy, blockVariables, bindings, proverCtxt);

+          VCExpr startCorrect = LetVC(startBlock, label2absy, blockVariables, bindings, proverCtxt, out assertionCount);

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

             return proverCtxt.ExprGen.Let(bindings, proverCtxt.ExprGen.Not(startCorrect) );

           } else {

@@ -337,17 +337,19 @@ void ObjectInvariant()
         }

 

         VCExpr LetVC(Block block,

-                             Hashtable/*<int, Absy!>*/ label2absy,

-                             Hashtable/*<Block, VCExprVar!>*/ blockVariables,

-                             List<VCExprLetBinding> bindings,

-                             ProverContext proverCtxt)

+                     Hashtable/*<int, Absy!>*/ label2absy,

+                     Hashtable/*<Block, VCExprVar!>*/ blockVariables,

+                     List<VCExprLetBinding> bindings,

+                     ProverContext proverCtxt,

+                     out int assertionCount)

         {

-      Contract.Requires(label2absy != null);

-      Contract.Requires(blockVariables != null);

-      Contract.Requires(proverCtxt != null);

-      Contract.Requires(cce.NonNullElements(bindings));

+          Contract.Requires(label2absy != null);

+          Contract.Requires(blockVariables != null);

+          Contract.Requires(proverCtxt != null);

+          Contract.Requires(cce.NonNullElements(bindings));

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

 

+          assertionCount = 0;

           VCExpressionGenerator gen = proverCtxt.ExprGen;

           Contract.Assert(gen != null);

           VCExprVar v = (VCExprVar)blockVariables[block];

@@ -371,17 +373,19 @@ void ObjectInvariant()
               List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Length);

               foreach (Block successor in gotocmd.labelTargets) {

                 Contract.Assert(successor != null);

-                VCExpr s = LetVC(successor, label2absy, blockVariables, bindings, proverCtxt);

+                int ac;

+                VCExpr s = LetVC(successor, label2absy, blockVariables, bindings, proverCtxt, out ac);

+                assertionCount += ac;

                 SuccCorrectVars.Add(s);

               }

               SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars);

             }

 

             VCContext context = new VCContext(label2absy, proverCtxt);

-    //        m_Context = context;

+            //        m_Context = context;

 

             VCExpr vc = Wlp.Block(block, SuccCorrect, context);

-

+            assertionCount += context.AssertionCount;

             v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool);

             

             bindings.Add(gen.LetBinding(v, vc));

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index e1c5ce13..27237a51 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -1692,7 +1692,9 @@ namespace VC
                         }

                     }

                     if (toExpand.Count == 0) expand = false;

-                    else DoExpansion(incrementalSearch, toExpand, vState);

+                    else {

+                      DoExpansion(incrementalSearch, toExpand, vState);

+                    }

                 }

             }

             #endregion

@@ -2402,14 +2404,13 @@ namespace VC
         static int newVarCnt = 0;

 

         // Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.

-        private void DoExpansion(bool incremental, List<int>/*!*/ candidates, VerificationState vState)

-        {

-            vState.expansionCount += candidates.Count;

+        private void DoExpansion(bool incremental, List<int>/*!*/ candidates, VerificationState vState) {

+          vState.expansionCount += candidates.Count;

 

-            if (incremental)

-                DoExpansionAndPush(candidates, vState);

-            else

-                DoExpansionAndInline(candidates, vState);

+          if (incremental)

+            DoExpansionAndPush(candidates, vState);

+          else

+            DoExpansionAndInline(candidates, vState);

         }

 

         // Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 36b9edc2..351591df 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -271,7 +271,9 @@ namespace VC {
 

       TypecheckingContext tc = new TypecheckingContext(null);

       impl.Typecheck(tc);

-      VCExpr vcexpr = gen.Not(LetVC(impl.Blocks[0], info.controlFlowVariable, null, checker.TheoremProver.Context));

+      int assertionCount;

+      VCExpr vcexpr = gen.Not(LetVC(impl.Blocks[0], info.controlFlowVariable, null, checker.TheoremProver.Context, out assertionCount));

+      CumulativeAssertionCount += assertionCount;

       Contract.Assert(vcexpr != null);

       ResetPredecessors(impl.Blocks);

       VCExpr reachvcexpr = GenerateReachVC(impl, info, checker);

@@ -1484,7 +1486,7 @@ namespace VC {
         }

       }

 

-      public void BeginCheck(VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout) {

+      public void BeginCheck(VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout, out int assertionCount) {

         Contract.Requires(callback != null);

         splitNo = no;

 

@@ -1508,13 +1510,8 @@ namespace VC {
             ResetPredecessors(codeExpr.Blocks);

             vcgen.AddBlocksBetween(codeExpr.Blocks);

             Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr));

-            VCExpr startCorrect = VCGen.LetVC(

-		      codeExpr.Blocks[0],

-              null,

-              label2absy,

-		      blockVariables,

-		      bindings,

-		      ctx);

+            int ac;  // computed, but then ignored for this CodeExpr

+            VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);

             VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);

 

             if (vcgen.CurrentLocalVariables.Length != 0) {

@@ -1536,8 +1533,10 @@ namespace VC {
           }

 		  ));

 

+        int prev = parent.CumulativeAssertionCount;

         VCExpr vc = parent.GenerateVCAux(impl, null, label2absy, checker);

         Contract.Assert(vc != null);

+        assertionCount = parent.CumulativeAssertionCount - prev;

 

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

           reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, parent.implName2LazyInliningInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program);

@@ -1630,42 +1629,44 @@ namespace VC {
       impl.Typecheck(tc);

 

       VCExpr vc;

+      int assertionCount;

       switch (CommandLineOptions.Clo.vcVariety) {

         case CommandLineOptions.VCVariety.Structured:

-          vc = VCViaStructuredProgram(impl, label2absy, ch.TheoremProver.Context);

+          vc = VCViaStructuredProgram(impl, label2absy, ch.TheoremProver.Context, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.Block:

-          vc = FlatBlockVC(impl, label2absy, false, false, false, ch.TheoremProver.Context);

+          vc = FlatBlockVC(impl, label2absy, false, false, false, ch.TheoremProver.Context, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.BlockReach:

-          vc = FlatBlockVC(impl, label2absy, false, true, false, ch.TheoremProver.Context);

+          vc = FlatBlockVC(impl, label2absy, false, true, false, ch.TheoremProver.Context, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.Local:

-          vc = FlatBlockVC(impl, label2absy, true, false, false, ch.TheoremProver.Context);

+          vc = FlatBlockVC(impl, label2absy, true, false, false, ch.TheoremProver.Context, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.BlockNested:

-          vc = NestedBlockVC(impl, label2absy, false, ch.TheoremProver.Context);

+          vc = NestedBlockVC(impl, label2absy, false, ch.TheoremProver.Context, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.BlockNestedReach:

-          vc = NestedBlockVC(impl, label2absy, true, ch.TheoremProver.Context);

+          vc = NestedBlockVC(impl, label2absy, true, ch.TheoremProver.Context, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.Dag:

           if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags) {

-            vc = DagVC(cce.NonNull(impl.Blocks[0]), label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context);

+            vc = DagVC(cce.NonNull(impl.Blocks[0]), label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context, out assertionCount);

           } else {

-            vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariable, label2absy, ch.TheoremProver.Context);

+            vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariable, label2absy, ch.TheoremProver.Context, out assertionCount);

           }

           break;

         case CommandLineOptions.VCVariety.DagIterative:

-          vc = LetVCIterative(impl.Blocks, controlFlowVariable, label2absy, ch.TheoremProver.Context);

+          vc = LetVCIterative(impl.Blocks, controlFlowVariable, label2absy, ch.TheoremProver.Context, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.Doomed:

-          vc = FlatBlockVC(impl, label2absy, false, false, true, ch.TheoremProver.Context);

+          vc = FlatBlockVC(impl, label2absy, false, false, true, ch.TheoremProver.Context, out assertionCount);

           break;

         default:

           Contract.Assert(false);

           throw new cce.UnreachableException();  // unexpected enumeration value

       }

+      CumulativeAssertionCount += assertionCount;

       return vc;

     }

 

@@ -1677,11 +1678,12 @@ namespace VC {
       }

     }

 

-    public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback){

+    public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback) {

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

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

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

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

+

       if (impl.SkipVerification) {

         return Outcome.Inconclusive; // not sure about this one

       }

@@ -1756,10 +1758,13 @@ namespace VC {
             }

             callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));

 

+            int assertionCount;

             s.BeginCheck(callback, mvInfo, no, 

               (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :

                 keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :

-                             CommandLineOptions.Clo.ProverKillTime);

+                             CommandLineOptions.Clo.ProverKillTime,

+              out assertionCount);

+            CumulativeAssertionCount += assertionCount;

 

             no++;

 

@@ -3421,7 +3426,8 @@ namespace VC {
     static VCExpr LetVC(Block startBlock,

                         Variable controlFlowVariable,

                         Hashtable/*<int, Absy!>*/ label2absy,

-                        ProverContext proverCtxt) {

+                        ProverContext proverCtxt,

+                        out int assertionCount) {

       Contract.Requires(startBlock != null);

       Contract.Requires(proverCtxt != null);

 

@@ -3429,18 +3435,21 @@ namespace VC {
 

       Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();

       List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();

-      VCExpr startCorrect = LetVC(startBlock, controlFlowVariable, label2absy, blockVariables, bindings, proverCtxt);

+      VCExpr startCorrect = LetVC(startBlock, controlFlowVariable, label2absy, blockVariables, bindings, proverCtxt, out assertionCount);

       return proverCtxt.ExprGen.Let(bindings, startCorrect);

     }

 

     static VCExpr LetVCIterative(List<Block> blocks,

                                  Variable controlFlowVariable,

                                  Hashtable label2absy,

-                                 ProverContext proverCtxt) {

+                                 ProverContext proverCtxt,

+                                 out int assertionCount) {

       Contract.Requires(blocks != null);

       Contract.Requires(proverCtxt != null);

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

 

+      assertionCount = 0;

+

       Graph<Block> dag = new Graph<Block>();

       dag.AddSource(blocks[0]); 

       foreach (Block b in blocks) {

@@ -3491,6 +3500,7 @@ namespace VC {
 

         VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariable);

         VCExpr vc = Wlp.Block(block, SuccCorrect, context);

+        assertionCount += context.AssertionCount;

 

         VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool);

         bindings.Add(gen.LetBinding(v, vc));

@@ -3505,7 +3515,8 @@ namespace VC {
                         Hashtable/*<int, Absy!>*/ label2absy,

                         Hashtable/*<Block, VCExprVar!>*/ blockVariables,

                         List<VCExprLetBinding/*!*/>/*!*/ bindings,

-                        ProverContext proverCtxt)

+                        ProverContext proverCtxt,

+                        out int assertionCount)

     {

       Contract.Requires(block != null);

       Contract.Requires(blockVariables!= null);

@@ -3514,6 +3525,8 @@ namespace VC {
 

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

 

+      assertionCount = 0;

+

       VCExpressionGenerator gen = proverCtxt.ExprGen;

       Contract.Assert(gen != null);

       VCExprVar v = (VCExprVar)blockVariables[block];

@@ -3536,8 +3549,11 @@ namespace VC {
         } else {

           Contract.Assert( gotocmd.labelTargets != null);

           List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Length);

-          foreach (Block successor in gotocmd.labelTargets) {Contract.Assert(successor != null);

-            VCExpr s = LetVC(successor, controlFlowVariable, label2absy, blockVariables, bindings, proverCtxt);

+          foreach (Block successor in gotocmd.labelTargets) {

+            Contract.Assert(successor != null);

+            int ac;

+            VCExpr s = LetVC(successor, controlFlowVariable, label2absy, blockVariables, bindings, proverCtxt, out ac);

+            assertionCount += ac;

             if (controlFlowVariable != null) 

             {

               VCExprVar controlFlowVariableExpr = proverCtxt.BoogieExprTranslator.LookupVariable(controlFlowVariable);

@@ -3553,6 +3569,7 @@ namespace VC {
         

         VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariable);

         VCExpr vc = Wlp.Block(block, SuccCorrect, context);

+        assertionCount += context.AssertionCount;

         

         v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool);

         bindings.Add(gen.LetBinding(v, vc));

@@ -3564,7 +3581,8 @@ namespace VC {
     static VCExpr DagVC(Block block,

                          Hashtable/*<int, Absy!>*/ label2absy,

                          Hashtable/*<Block, VCExpr!>*/ blockEquations,

-                         ProverContext proverCtxt)

+                         ProverContext proverCtxt,

+                         out int assertionCount)

     {

       Contract.Requires(block != null);

       Contract.Requires(label2absy != null);

@@ -3572,6 +3590,7 @@ namespace VC {
       Contract.Requires(proverCtxt != null);

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

 

+      assertionCount = 0;

       VCExpressionGenerator gen = proverCtxt.ExprGen;

       Contract.Assert(gen != null);

       VCExpr vc = (VCExpr)blockEquations[block];

@@ -3589,7 +3608,9 @@ namespace VC {
       {

         foreach (Block successor in cce.NonNull(gotocmd.labelTargets)) {

           Contract.Assert(successor != null);

-          VCExpr c = DagVC(successor, label2absy, blockEquations, proverCtxt);

+          int ac;

+          VCExpr c = DagVC(successor, label2absy, blockEquations, proverCtxt, out ac);

+          assertionCount += ac;

           SuccCorrect = SuccCorrect == null ? c : gen.And(SuccCorrect, c);

         }

       }

@@ -3599,6 +3620,7 @@ namespace VC {
 

       VCContext context = new VCContext(label2absy, proverCtxt);

       vc = Wlp.Block(block, SuccCorrect, context);

+      assertionCount += context.AssertionCount;

       

       //  gen.MarkAsSharedFormula(vc);  PR: don't know yet what to do with this guy

 

@@ -3609,7 +3631,8 @@ namespace VC {
     static VCExpr FlatBlockVC(Implementation impl,

                               Hashtable/*<int, Absy!>*/ label2absy,

                               bool local, bool reach, bool doomed,

-                              ProverContext proverCtxt)

+                              ProverContext proverCtxt,

+                              out int assertionCount)

     {

       Contract.Requires(impl != null);

       Contract.Requires(label2absy != null);

@@ -3680,6 +3703,7 @@ namespace VC {
         programSemantics.Add(binding);

       }

 

+      assertionCount = context.AssertionCount;

       return gen.Let(programSemantics, proofObligation);

     }

 

@@ -3743,7 +3767,8 @@ namespace VC {
     static VCExpr NestedBlockVC(Implementation impl,

                                 Hashtable/*<int, Absy!>*/ label2absy,

                                 bool reach,

-                                ProverContext proverCtxt){

+                                ProverContext proverCtxt,

+                                out int assertionCount){

       Contract.Requires(impl != null);

       Contract.Requires(label2absy != null);

       Contract.Requires(proverCtxt != null);

@@ -3766,10 +3791,10 @@ namespace VC {
       {

         List<Block> blocks = impl.Blocks;

         

-     // block sorting is now done on the VCExpr

-     //   if (((!)CommandLineOptions.Clo.TheProverFactory).NeedsBlockSorting) {

-     //     blocks = SortBlocks(blocks);

-     //   }

+        // block sorting is now done on the VCExpr

+        //   if (((!)CommandLineOptions.Clo.TheProverFactory).NeedsBlockSorting) {

+        //     blocks = SortBlocks(blocks);

+        //   }

         int i = 0;

         foreach (Block b in blocks) {

           Contract.Assert(b != null);

@@ -3781,7 +3806,8 @@ namespace VC {
       VCExprLetBinding programSemantics = NestedBlockEquation(cce.NonNull(impl.Blocks[0]), BlkCorrect, BlkReached, totalOrder, context, g, gen);

       List<VCExprLetBinding> ps = new List<VCExprLetBinding>(1);

       ps.Add(programSemantics);

-      

+

+      assertionCount = context.AssertionCount;

       return gen.Let(ps, proofObligation);

     }

 

@@ -3863,12 +3889,13 @@ namespace VC {
 

     static VCExpr VCViaStructuredProgram

                   (Implementation impl, Hashtable/*<int, Absy!>*/ label2absy,

-                   ProverContext proverCtxt)

+                   ProverContext proverCtxt,

+                   out int assertionCount)

     {

-    Contract.Requires(impl != null);

-    Contract.Requires(label2absy != null);

-    Contract.Requires(proverCtxt != null);

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

+      Contract.Requires(impl != null);

+      Contract.Requires(label2absy != null);

+      Contract.Requires(proverCtxt != null);

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

 

       #region Convert block structure back to a "regular expression"

       RE r = DAG2RE.Transform(cce.NonNull(impl.Blocks[0]));

@@ -3878,7 +3905,9 @@ namespace VC {
       VCContext ctxt = new VCContext(label2absy, proverCtxt);

       Contract.Assert(ctxt != null);

       #region Send wlp(program,true) to Simplify

-      return Wlp.RegExpr(r, VCExpressionGenerator.True, ctxt);

+      var vcexp = Wlp.RegExpr(r, VCExpressionGenerator.True, ctxt);

+      assertionCount = ctxt.AssertionCount;

+      return vcexp;

       #endregion

     }

 

diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs
index 734d81d6..4d2e0775 100644
--- a/Source/VCGeneration/VCDoomed.cs
+++ b/Source/VCGeneration/VCDoomed.cs
@@ -121,7 +121,9 @@ namespace VC {
     

       Checker checker = FindCheckerFor(impl, 1000);

       Contract.Assert(checker != null);

-      DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks);

+      int assertionCount;

+      DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks, out assertionCount);

+      CumulativeAssertionCount += assertionCount;

 

       //EmitImpl(impl, false);

       

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index c3134c09..b84df433 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -23,6 +23,7 @@ namespace VC {
     [Rep] public readonly Hashtable/*<int, Absy!>*/ Label2absy;

     [Rep] public readonly ProverContext Ctxt;

     public readonly Variable ControlFlowVariable;

+    public int AssertionCount;  // counts the number of assertions for which Wlp has been computed

     

     public VCContext(Hashtable/*<int, Absy!>*/ label2absy, ProverContext ctxt)

     {

@@ -85,9 +86,8 @@ namespace VC {
     /// <summary>

     /// Computes the wlp for an assert or assume command "cmd".

     /// </summary>

-    public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt)

-    {

-      Contract.Requires(cmd!= null);

+    public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) {

+      Contract.Requires(cmd != null);

       Contract.Requires(N != null);

       Contract.Requires(ctxt != null);

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

@@ -99,8 +99,7 @@ namespace VC {
         VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);

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

           return gen.Implies(C, N);

-        }

-        else {

+        } else {

           int id = ac.UniqueId;

           if (ctxt.Label2absy != null) {

             ctxt.Label2absy[id] = ac;

@@ -126,11 +125,11 @@ namespace VC {
           if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)

             return gen.Implies(C, N);

 

+          ctxt.AssertionCount++;

           if (ctxt.ControlFlowVariable == null) {

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

             return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), C), N);

-          }

-          else {

+          } else {

             VCExpr controlFlowVariableExpr = ctxt.Ctxt.BoogieExprTranslator.LookupVariable(ctxt.ControlFlowVariable);

             Contract.Assert(controlFlowVariableExpr != null);

             VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(b.UniqueId)));

@@ -138,8 +137,7 @@ namespace VC {
             VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(ac.UniqueId)));

             if (ctxt.Label2absy == null) {

               return gen.AndSimp(gen.Implies(assertFailure, C), gen.Implies(C, N));

-            }

-            else {

+            } else {

               return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), gen.Implies(assertFailure, C)), gen.Implies(C, N));

             }

           }

@@ -148,12 +146,11 @@ namespace VC {
       } else if (cmd is AssumeCmd) {

         AssumeCmd ac = (AssumeCmd)cmd;

 

-        if(CommandLineOptions.Clo.StratifiedInlining > 0) {

-            var pname = QKeyValue.FindStringAttribute(ac.Attributes, "candidate");

-            if(pname != null)

-            {

-                return gen.ImpliesSimp(gen.LabelPos("candidate_" + pname.ToString(), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);

-            }

+        if (CommandLineOptions.Clo.StratifiedInlining > 0) {

+          var pname = QKeyValue.FindStringAttribute(ac.Attributes, "candidate");

+          if (pname != null) {

+            return gen.ImpliesSimp(gen.LabelPos("candidate_" + pname.ToString(), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);

+          }

 

           // Label the assume if it is a procedure call

           NAryExpr naryExpr = ac.Expr as NAryExpr;

@@ -165,12 +162,12 @@ namespace VC {
             }

           }

         }

-        

+

         return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);

 

       } else {

-      Console.WriteLine(cmd.ToString());

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

+        Console.WriteLine(cmd.ToString());

+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected command

       }

     }