From 812d8d8bfb3a11dc40c485ffa05be154678134c3 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Thu, 8 Feb 2024 16:12:06 -0800
Subject: [PATCH] Print resource counts when using -smoke

---
 Source/ExecutionEngine/CommandLineOptions.cs | 6 +++++-
 Source/VCGeneration/SmokeTester.cs           | 8 ++++++--
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs
index f00d024e4..faf89dc7b 100644
--- 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
index 71621da0f..340dfff58 100644
--- 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);
     }
   }
-}
\ No newline at end of file
+}