Skip to content

Commit b86b8ac

Browse files
committed
reduce verbosity of runtime messages
The time taken for particular steps is statistics, not status.
1 parent ef327f6 commit b86b8ac

File tree

2 files changed

+6
-6
lines changed

2 files changed

+6
-6
lines changed

src/goto-checker/bmc_util.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -407,16 +407,16 @@ void run_property_decider(
407407
auto const sat_solver_stop = std::chrono::steady_clock::now();
408408
std::chrono::duration<double> sat_solver_runtime =
409409
std::chrono::duration<double>(sat_solver_stop - sat_solver_start);
410-
log.status() << "Runtime Solver: " << sat_solver_runtime.count() << "s"
411-
<< messaget::eom;
410+
log.statistics() << "Runtime Solver: " << sat_solver_runtime.count() << "s"
411+
<< messaget::eom;
412412

413413
property_decider.update_properties_status_from_goals(
414414
properties, result.updated_properties, dec_result, set_pass);
415415

416416
auto solver_stop = std::chrono::steady_clock::now();
417417
solver_runtime += std::chrono::duration<double>(solver_stop - solver_start);
418-
log.status() << "Runtime decision procedure: " << solver_runtime.count()
419-
<< "s" << messaget::eom;
418+
log.statistics() << "Runtime decision procedure: " << solver_runtime.count()
419+
<< "s" << messaget::eom;
420420

421421
if(dec_result == decision_proceduret::resultt::D_SATISFIABLE)
422422
{

src/goto-symex/symex_target_equation.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -354,8 +354,8 @@ void symex_target_equationt::convert(decision_proceduret &decision_procedure)
354354
const auto convert_SSA_stop = std::chrono::steady_clock::now();
355355
std::chrono::duration<double> convert_SSA_runtime =
356356
std::chrono::duration<double>(convert_SSA_stop - convert_SSA_start);
357-
log.status() << "Runtime Convert SSA: " << convert_SSA_runtime.count() << "s"
358-
<< messaget::eom;
357+
log.statistics() << "Runtime Convert SSA: " << convert_SSA_runtime.count()
358+
<< "s" << messaget::eom;
359359
}
360360

361361
void symex_target_equationt::convert_assignments(

0 commit comments

Comments
 (0)