increase verbosity level of various messages

CBMC generates too much console output.  This commit increases the verbosity
level required for various progress and performance statistics messages.

Author: kroening

regression/cbmc/export-symex-ready-goto/test-correct.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---export-symex-ready-goto exported.symex.ready.goto
+--export-symex-ready-goto exported.symex.ready.goto --verbosity 10
 ^Parsing test.c$
 ^Converting$
 ^Type-checking test$

regression/cbmc/json1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---json-ui --stop-on-fail
+--json-ui --stop-on-fail --verbosity 10
 activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/sat-solver/test.desc

@@ -1,6 +1,6 @@
 CORE broken-z3-smt-backend broken-cprover-smt-backend no-new-smt
 test.c
---sat-solver cadical
+--sat-solver cadical --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 Solving with CaDiCaL|The specified solver, 'cadical', is not available. The default solver will be used instead.

src/cbmc/cbmc_parse_options.cpp

@@ -838,7 +838,7 @@ int cbmc_parse_optionst::get_goto_program(
     return CPROVER_EXIT_SUCCESS;
   }
 
-  log.status() << config.object_bits_info() << messaget::eom;
+  log.statistics() << config.object_bits_info() << messaget::eom;
 
   return -1; // no error, continue
 }

src/goto-checker/bmc_util.cpp

@@ -350,8 +350,9 @@ void postprocess_equation(
   std::chrono::duration<double> postprocess_equation_runtime =
     std::chrono::duration<double>(
       postprocess_equation_stop - postprocess_equation_start);
-  log.status() << "Runtime Postprocess Equation: "
-               << postprocess_equation_runtime.count() << "s" << messaget::eom;
+  log.statistics() << "Runtime Postprocess Equation: "
+                   << postprocess_equation_runtime.count() << "s"
+                   << messaget::eom;
 }
 
 std::chrono::duration<double> prepare_property_decider(

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -85,8 +85,8 @@ void multi_path_symex_only_checkert::generate_equation()
   const auto symex_stop = std::chrono::steady_clock::now();
   std::chrono::duration<double> symex_runtime =
     std::chrono::duration<double>(symex_stop - symex_start);
-  log.status() << "Runtime Symex: " << symex_runtime.count() << "s"
-               << messaget::eom;
+  log.statistics() << "Runtime Symex: " << symex_runtime.count() << "s"
+                   << messaget::eom;
 
   postprocess_equation(symex, equation, options, ns, ui_message_handler);
 }

src/goto-checker/single_path_symex_checker.cpp

@@ -82,8 +82,8 @@ operator()(propertiest &properties)
     worklist->pop();
   }
 
-  log.status() << "Runtime Symex: " << symex_runtime.count() << "s"
-               << messaget::eom;
+  log.statistics() << "Runtime Symex: " << symex_runtime.count() << "s"
+                   << messaget::eom;
 
   final_update_properties(properties, result.updated_properties);
 

src/goto-checker/single_path_symex_only_checker.cpp

@@ -52,8 +52,8 @@ operator()(propertiest &properties)
     worklist->pop();
   }
 
-  log.status() << "Runtime Symex: " << symex_runtime.count() << "s"
-               << messaget::eom;
+  log.statistics() << "Runtime Symex: " << symex_runtime.count() << "s"
+                   << messaget::eom;
 
   final_update_properties(properties, result.updated_properties);
 

src/goto-programs/initialize_goto_model.cpp

@@ -93,7 +93,7 @@ void initialize_from_source_files(
     languaget &language = *lf.language;
     language.set_language_options(options, message_handler);
 
-    msg.status() << "Parsing " << filename << messaget::eom;
+    msg.progress() << "Parsing " << filename << messaget::eom;
 
     if(language.parse(infile, filename, message_handler))
     {
@@ -103,7 +103,7 @@ void initialize_from_source_files(
     lf.get_modules();
   }
 
-  msg.status() << "Converting" << messaget::eom;
+  msg.progress() << "Converting" << messaget::eom;
 
   if(language_files.typecheck(symbol_table, message_handler))
   {

src/solvers/prop/prop_conv_solver.cpp

@@ -447,18 +447,18 @@ prop_conv_solvert::dec_solve(const exprt &assumption)
   {
     const auto post_process_start = std::chrono::steady_clock::now();
 
-    log.statistics() << "Post-processing" << messaget::eom;
+    log.progress() << "Post-processing" << messaget::eom;
     finish_eager_conversion();
     post_processing_done = true;
 
     const auto post_process_stop = std::chrono::steady_clock::now();
     std::chrono::duration<double> post_process_runtime =
       std::chrono::duration<double>(post_process_stop - post_process_start);
-    log.status() << "Runtime Post-process: " << post_process_runtime.count()
-                 << "s" << messaget::eom;
+    log.statistics() << "Runtime Post-process: " << post_process_runtime.count()
+                     << "s" << messaget::eom;
   }
 
-  log.statistics() << "Solving with " << prop.solver_text() << messaget::eom;
+  log.progress() << "Solving with " << prop.solver_text() << messaget::eom;
 
   if(assumption.is_nil())
     push();

src/solvers/refinement/bv_refinement_loop.cpp

@@ -24,7 +24,7 @@ bv_refinementt::bv_refinementt(const infot &info)
 decision_proceduret::resultt bv_refinementt::dec_solve(const exprt &assumption)
 {
   // do the usual post-processing
-  log.status() << "BV-Refinement: post-processing" << messaget::eom;
+  log.progress() << "BV-Refinement: post-processing" << messaget::eom;
   finish_eager_conversion();
 
   log.debug() << "Solving with " << prop.solver_text() << messaget::eom;
@@ -36,7 +36,7 @@ decision_proceduret::resultt bv_refinementt::dec_solve(const exprt &assumption)
   {
     iteration++;
 
-    log.status() << "BV-Refinement: iteration " << iteration << messaget::eom;
+    log.progress() << "BV-Refinement: iteration " << iteration << messaget::eom;
 
     // output the very same information in a structured fashion
     if(config_.output_xml)
@@ -54,12 +54,12 @@ decision_proceduret::resultt bv_refinementt::dec_solve(const exprt &assumption)
       {
         log.status() << "BV-Refinement: got SAT, and it simulates => SAT"
                      << messaget::eom;
-        log.status() << "Total iterations: " << iteration << messaget::eom;
+        log.statistics() << "Total iterations: " << iteration << messaget::eom;
         return resultt::D_SATISFIABLE;
       }
       else
-        log.status() << "BV-Refinement: got SAT, and it is spurious, refining"
-                     << messaget::eom;
+        log.progress() << "BV-Refinement: got SAT, and it is spurious, refining"
+                       << messaget::eom;
       break;
 
     case resultt::D_UNSATISFIABLE:
@@ -69,11 +69,11 @@ decision_proceduret::resultt bv_refinementt::dec_solve(const exprt &assumption)
         log.status()
           << "BV-Refinement: got UNSAT, and the proof passes => UNSAT"
           << messaget::eom;
-        log.status() << "Total iterations: " << iteration << messaget::eom;
+        log.statistics() << "Total iterations: " << iteration << messaget::eom;
         return resultt::D_UNSATISFIABLE;
       }
       else
-        log.status()
+        log.progress()
           << "BV-Refinement: got UNSAT, and the proof fails, refining"
           << messaget::eom;
       break;