Print resource counts when using -smoke

boogie-org · Feb 9, 2024 · 812d8d8 · 812d8d8
1 parent fbf1aa2
commit 812d8d8
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 3 deletions.
diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs
@@ -1288,7 +1288,11 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
               ps.CheckBooleanFlag("checkInfer", x => InstrumentWithAsserts = x) ||
               ps.CheckBooleanFlag("restartProver", x => restartProverPerVc = x) ||
               ps.CheckBooleanFlag("printInlined", x => printInlined = x) ||
-              ps.CheckBooleanFlag("smoke", x => SoundnessSmokeTest = x) ||
+              ps.CheckBooleanFlag("smoke", x =>
+              {
+                SoundnessSmokeTest = x;
+                Prune = false;
+              }) ||
               ps.CheckBooleanFlag("vcsDumpSplits", x => VcsDumpSplits = x) ||
               ps.CheckBooleanFlag("dbgRefuted", x => DebugRefuted = x) ||
               ps.CheckBooleanFlag("reflectAdd", x => ReflectAdd = x) ||

diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs
@@ -279,6 +279,7 @@ async Task<bool> CheckUnreachable(TextWriter traceWriter, Block cur, List<Cmd> s
     Contract.Assert(checker != null);
 
     SolverOutcome outcome = SolverOutcome.Undetermined;
+    var resourceCount = 0;
     try
     {
       VCExpr vc;
@@ -309,6 +310,7 @@ async Task<bool> CheckUnreachable(TextWriter traceWriter, Block cur, List<Cmd> s
         Options.SmokeTimeout, Options.ResourceLimit, CancellationToken.None);
 
       await checker.ProverTask;
+      resourceCount = checker.GetProverResourceCount();
 
       lock (checker)
       {
@@ -326,7 +328,9 @@ async Task<bool> CheckUnreachable(TextWriter traceWriter, Block cur, List<Cmd> s
     TimeSpan elapsed = end - start;
     if (Options.Trace)
     {
-      traceWriter.WriteLine("  [{0} s] {1}", elapsed.TotalSeconds,
+      traceWriter.WriteLine("  [{0} s, resource count: {1}] {2}",
+        elapsed.TotalSeconds,
+        resourceCount,
         outcome == SolverOutcome.Valid
           ? "OOPS"
           : "OK" + (outcome == SolverOutcome.Invalid ? "" : " (" + outcome + ")"));
@@ -492,4 +496,4 @@ public override void OnProverWarning(string msg)
       callback.OnWarning(options, msg);
     }
   }
-}
+}