Record the SMT input size for each split

Source/Core/Xml.cs

@@ -112,7 +112,7 @@ public void WriteEndMethod(string outcome, DateTime endTime, TimeSpan elapsed, i
     }
 
     public void WriteSplit(int splitNum, int iteration, IEnumerable<AssertCmd> asserts, DateTime startTime,
-                           string outcome, TimeSpan elapsed, int? resourceCount)
+                           string outcome, TimeSpan elapsed, int? resourceCount, int? smtInputSize)
     {
       Contract.Requires(splitNum > 0);
       Contract.Requires(outcome != null);
@@ -145,6 +145,10 @@ public void WriteSplit(int splitNum, int iteration, IEnumerable<AssertCmd> asser
         {
           wr.WriteAttributeString("resourceCount", resourceCount.ToString());
         }
+        if (smtInputSize is not null)
+        {
+          wr.WriteAttributeString("smtInputSize", smtInputSize.ToString());
+        }
         wr.WriteEndElement(); // conclusion
 
         wr.WriteEndElement(); // assertionBatch

Source/ExecutionEngine/ImplementationRunResult.cs

@@ -78,7 +78,7 @@ public void ProcessXml(ExecutionEngine engine) {
 
       foreach (var vcResult in RunResults.OrderBy(s => (vcNum: s.VcNum, iteration: s.Iteration))) {
         engine.Options.XmlSink.WriteSplit(vcResult.VcNum, vcResult.Iteration, vcResult.Asserts, vcResult.StartTime,
-          vcResult.Outcome.ToString().ToLowerInvariant(), vcResult.RunTime, vcResult.ResourceCount);
+          vcResult.Outcome.ToString().ToLowerInvariant(), vcResult.RunTime, vcResult.ResourceCount, vcResult.SmtInputSize);
       }
 
       engine.Options.XmlSink.WriteEndMethod(VcOutcome.ToString().ToLowerInvariant(),

Source/Provers/SMTLib/ProverInterface.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Text;
 using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Boogie.SMTLib;
@@ -21,6 +22,8 @@ public enum SolverOutcome
 
 public abstract class ProverInterface
 {
+  public int SentSize { get; protected set; }
+
   public static ProverInterface CreateProver(SMTLibOptions libOptions, Program prog,
     string /*?*/ logFilePath, bool appendLogFile, uint timeout,
     int taskID = -1)

Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs

@@ -71,9 +71,9 @@ public override async Task<SolverOutcome> Check(string descriptiveName, VCExpr v
         SetupProcess();
         checkSatSent = false;
         FullReset(gen);
-
         if (options.LogFilename != null && currentLogFile == null)
         {
+
           currentLogFile = OpenOutputFile(descriptiveName);
           await currentLogFile.WriteAsync(common.ToString());
         }
@@ -123,6 +123,7 @@ public override void FullReset(VCExpressionGenerator generator)
       AxiomsAreSetup = false;
       DeclCollector.Reset();
       NamedAssumes.Clear();
+      SentSize = 0;
     }
 
     private Task<IReadOnlyList<SExpr>> SendRequestsAndClose(IReadOnlyList<string> requests, CancellationToken cancellationToken) {
@@ -284,7 +285,9 @@ protected override void Send(string s, bool isCommon)
       // Boogie emits comments after the solver has responded. In batch
       // mode, sending these to the solver is problematic. But they'll
       // still get sent to the log below.
-      if (Process != null && !checkSatSent) {
+      if (Process != null && !checkSatSent)
+      {
+        SentSize += s.Length;
         Process.Send(s);
       }
 

Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs

@@ -46,7 +46,9 @@ private void PossiblyRestart()
       if (Process != null && processNeedsRestart) {
         processNeedsRestart = false;
         SetupProcess();
-        Process.Send(common.ToString());
+        var c = common.ToString();
+        SentSize += c.Length;
+        Process.Send(c);
       }
     }
 
@@ -124,6 +126,7 @@ public override async Task<SolverOutcome> Check(string descriptiveName, VCExpr v
         }
 
         var result = await CheckSat(cancellationToken, errorLimit);
+        SentSize = 0;
         SendThisVC("(pop 1)");
 
         return result;
@@ -142,10 +145,11 @@ public override async Task Reset(VCExpressionGenerator generator)
       if (0 < common.Length)
       {
         var c = common.ToString();
+        SentSize += c.Length;
         Process.Send(c);
         if (currentLogFile != null)
         {
-          currentLogFile.WriteLine(c);
+          await currentLogFile.WriteLineAsync(c);
         }
       }
 
@@ -264,6 +268,7 @@ public async Task<SolverOutcome> CheckSat(CancellationToken cancellationToken,
         {
           if (popLater)
           {
+            SentSize = 0;
             SendThisVC("(pop 1)");
           }
         }
@@ -301,6 +306,7 @@ private T WrapInPushPop<T>(ref bool popLater, Func<T> action)
     {
       if (popLater)
       {
+        SentSize = 0;
         SendThisVC("(pop 1)");
       }
       SendThisVC("(push 1)");
@@ -647,6 +653,7 @@ protected override void Send(string s, bool isCommon)
 
       if (Process != null)
       {
+        SentSize += s.Length;
         Process.Send(s);
       }
 

Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs

@@ -1111,6 +1111,7 @@ public override void PushVCExpression(VCExpr vc)
 
     public override void Pop()
     {
+      SentSize = 0;
       SendThisVC("(pop 1)");
       DeclCollector.Pop();
     }

Source/VCGeneration/Checker.cs

@@ -259,6 +259,8 @@ public TimeSpan ProverRunTime
       get { return proverRunTime; }
     }
 
+    public int SmtInputSize => thmProver.SentSize;
+
     public int GetProverResourceCount()
     {
       return thmProver.GetRCount();

Source/VCGeneration/Split.cs

@@ -39,16 +39,14 @@ public IReadOnlyList<Declaration> PrunedDeclarations {
         }
       }
 
-      readonly Dictionary<Block /*!*/, BlockStats /*!*/> /*!*/
-        stats = new Dictionary<Block /*!*/, BlockStats /*!*/>();
+      readonly Dictionary<Block /*!*/, BlockStats /*!*/> /*!*/ stats = new();
 
       static int currentId = -1;
 
       Block splitBlock;
       bool assertToAssume;
 
-      List<Block /*!*/> /*!*/
-        assumizedBranches = new List<Block /*!*/>();
+      List<Block /*!*/> /*!*/ assumizedBranches = new();
 
       double score;
       bool scoreComputed;
@@ -58,8 +56,7 @@ public IReadOnlyList<Declaration> PrunedDeclarations {
 
       public Dictionary<TransferCmd, ReturnCmd> GotoCmdOrigins { get; }
 
-      public readonly VerificationConditionGenerator /*!*/
-        parent;
+      public readonly VerificationConditionGenerator /*!*/ parent;
 
       public Implementation /*!*/ Implementation => Run.Implementation;
 
@@ -78,6 +75,7 @@ public readonly VerificationConditionGenerator /*!*/
       // async interface
       public int SplitIndex { get; set; }
       public VerificationConditionGenerator.ErrorReporter reporter;
+      public int SmtInputSize { get; set; }
 
       public Split(VCGenOptions options, List<Block /*!*/> /*!*/ blocks,
         Dictionary<TransferCmd, ReturnCmd> /*!*/ gotoCmdOrigins,
@@ -915,6 +913,7 @@ public VerificationRunResult ReadOutcome(int iteration, Checker checker, Verifie
           Asserts: Asserts,
           CoveredElements: CoveredElements,
           ResourceCount: resourceCount,
+          SmtInputSize,
           SolverUsed: (Options as SMTLibSolverOptions)?.Solver);
         callback.OnVCResult(result);
 
@@ -981,6 +980,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa
         checker.TheoremProver.SetAdditionalSmtOptions(Implementation.GetExtraSMTOptions()
           .Select(kv => new OptionValue(kv.Key, kv.Value)));
         await checker.BeginCheck(Description, vc, reporter, timeout, rlimit, cancellationToken);
+        SmtInputSize = checker.SmtInputSize;
       }
 
       public string Description

Source/VCGeneration/VerificationRunResult.cs

@@ -18,6 +18,7 @@ public record VerificationRunResult
     List<AssertCmd> Asserts,
     IEnumerable<TrackedNodeComponent> CoveredElements,
     int ResourceCount,
+    int SmtInputSize,
     SolverKind? SolverUsed
   ) {
     public void ComputePerAssertOutcomes(out Dictionary<AssertCmd, SolverOutcome> perAssertOutcome,

Test/commandline/xml.bpl

@@ -1,5 +1,5 @@
-// RUN: %parallel-boogie -randomSeed:0 -xml:"%t-1.xml" "%s"
-// RUN: %parallel-boogie -randomSeed:0 -xml:"%t-2.xml" "%s"
+// RUN: %parallel-boogie -randomSeed:0 -proverLog:%t-1.smt -xml:"%t-1.xml" "%s"
+// RUN: %parallel-boogie -randomSeed:0 -proverLog:%t-2.smt -xml:"%t-2.xml" "%s"
 // RUN: grep -Eo "resourceCount=\"[0-9]+\"" "%t-1.xml" | sort -g > "%t-res1"
 // RUN: grep -Eo "resourceCount=\"[0-9]+\"" "%t-2.xml" | sort -g > "%t-res2"
 // RUN: diff "%t-res1" "%t-res2"
@@ -11,11 +11,11 @@
 // CHECK: \<method name="ExampleWithSplits" startTime=".*"\>
 // CHECK:   \<assertionBatch number="1" iteration="0" startTime=".*"\>
 // CHECK:     \<assertion file="xml.bpl" line="25" column="3" /\>
-// CHECK:     \<conclusion duration=".*" outcome="valid" resourceCount=".*" /\>
+// CHECK:     \<conclusion duration=".*" outcome="valid" resourceCount=".*" smtInputSize="865" /\>
 // CHECK:   \</assertionBatch\>
 // CHECK:   \<assertionBatch number="2" iteration="0" startTime=".*"\>
 // CHECK:     \<assertion file="xml.bpl" line="27" column="3" /\>
-// CHECK:     \<conclusion duration=".*" outcome="valid" resourceCount=".*" /\>
+// CHECK:     \<conclusion duration=".*" outcome="valid" resourceCount=".*" smtInputSize="881" /\>
 // CHECK:   \</assertionBatch\>
 // CHECK:   \<conclusion endTime=".*" duration=".*" resourceCount=".*" outcome="correct" /\>
 // CHECK: \</method\>