Merge pull request #8354 from diffblue/message-statistics

reduce verbosity of runtime messages

Author: tautschnig

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

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)
   {

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(