From 4942546dd42b5ded43e51db08c3495606b5c5275 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 20 Jun 2024 19:05:10 -0700
Subject: [PATCH] reduce verbosity of runtime messages

The time taken for particular steps is statistics, not status.
---
 regression/cbmc/Failing_Assert1/dimacs.desc | 2 +-
 src/goto-checker/bmc_util.cpp               | 8 ++++----
 src/goto-symex/symex_target_equation.cpp    | 4 ++--
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/regression/cbmc/Failing_Assert1/dimacs.desc b/regression/cbmc/Failing_Assert1/dimacs.desc
index 75036ccd09d..e55c91be00e 100644
--- a/regression/cbmc/Failing_Assert1/dimacs.desc
+++ b/regression/cbmc/Failing_Assert1/dimacs.desc
@@ -1,6 +1,6 @@
 CORE no-new-smt
 main.c
---dimacs
+--dimacs --verbosity 8
 ^Runtime decision procedure: [0-9]+(\.[0-9]+)?(e-[0-9]+)?s$
 ^c main::1::i!0@1#1
 ^c main::1::j!0@1#1
diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp
index fcdd4f76142..6e31d312d77 100644
--- a/src/goto-checker/bmc_util.cpp
+++ b/src/goto-checker/bmc_util.cpp
@@ -407,16 +407,16 @@ void run_property_decider(
   auto const sat_solver_stop = std::chrono::steady_clock::now();
   std::chrono::duration<double> sat_solver_runtime =
     std::chrono::duration<double>(sat_solver_stop - sat_solver_start);
-  log.status() << "Runtime Solver: " << sat_solver_runtime.count() << "s"
-               << messaget::eom;
+  log.statistics() << "Runtime Solver: " << sat_solver_runtime.count() << "s"
+                   << messaget::eom;
 
   property_decider.update_properties_status_from_goals(
     properties, result.updated_properties, dec_result, set_pass);
 
   auto solver_stop = std::chrono::steady_clock::now();
   solver_runtime += std::chrono::duration<double>(solver_stop - solver_start);
-  log.status() << "Runtime decision procedure: " << solver_runtime.count()
-               << "s" << messaget::eom;
+  log.statistics() << "Runtime decision procedure: " << solver_runtime.count()
+                   << "s" << messaget::eom;
 
   if(dec_result == decision_proceduret::resultt::D_SATISFIABLE)
   {
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index f34146ed67e..0bb35155e01 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -354,8 +354,8 @@ void symex_target_equationt::convert(decision_proceduret &decision_procedure)
   const auto convert_SSA_stop = std::chrono::steady_clock::now();
   std::chrono::duration<double> convert_SSA_runtime =
     std::chrono::duration<double>(convert_SSA_stop - convert_SSA_start);
-  log.status() << "Runtime Convert SSA: " << convert_SSA_runtime.count() << "s"
-               << messaget::eom;
+  log.statistics() << "Runtime Convert SSA: " << convert_SSA_runtime.count()
+                   << "s" << messaget::eom;
 }
 
 void symex_target_equationt::convert_assignments(