Merge pull request #1870 from diffblue/chrono-precision

do not round reported durations to seconds

Author: Daniel Kroening

src/cbmc/all_properties.cpp

@@ -57,8 +57,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 
   solver.set_message_handler(get_message_handler());
 
-  auto now = std::chrono::steady_clock::now();
-  auto sat_start = std::chrono::time_point_cast<std::chrono::seconds>(now);
+  auto solver_start=std::chrono::steady_clock::now();
 
   bmc.do_conversion();
 
@@ -133,10 +132,10 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
   }
 
   {
-    now = std::chrono::steady_clock::now();
-    auto sat_stop = std::chrono::time_point_cast<std::chrono::seconds>(now);
+    auto solver_stop = std::chrono::steady_clock::now();
 
-    status() << "Runtime decision procedure: " << (sat_stop - sat_start).count()
+    status() << "Runtime decision procedure: "
+             << std::chrono::duration<double>(solver_stop-solver_start).count()
              << "s" << eom;
   }
 

src/cbmc/bmc.cpp

@@ -159,8 +159,7 @@ bmct::run_decision_procedure(prop_convt &prop_conv)
 
   prop_conv.set_message_handler(get_message_handler());
 
-  auto now = std::chrono::steady_clock::now();
-  auto sat_start = std::chrono::time_point_cast<std::chrono::seconds>(now);
+  auto solver_start = std::chrono::steady_clock::now();
 
   do_conversion();
 
@@ -169,9 +168,9 @@ bmct::run_decision_procedure(prop_convt &prop_conv)
   decision_proceduret::resultt dec_result=prop_conv.dec_solve();
 
   {
-    now = std::chrono::steady_clock::now();
-    auto sat_stop = std::chrono::time_point_cast<std::chrono::seconds>(now);
-    status() << "Runtime decision procedure: " << (sat_stop - sat_start).count()
+    auto solver_stop = std::chrono::steady_clock::now();
+    status() << "Runtime decision procedure: "
+             << std::chrono::duration<double>(solver_start-solver_stop).count()
              << "s" << eom;
   }
 

src/cbmc/bmc_cover.cpp

@@ -195,8 +195,7 @@ bool bmc_covert::operator()()
 
   solver.set_message_handler(get_message_handler());
 
-  auto now = std::chrono::steady_clock::now();
-  auto sat_start = std::chrono::time_point_cast<std::chrono::seconds>(now);
+  auto solver_start=std::chrono::steady_clock::now();
 
   // Collect _all_ goals in `goal_map'.
   // This maps property IDs to 'goalt'
@@ -256,9 +255,9 @@ bool bmc_covert::operator()()
   cover_goals();
 
   {
-    now = std::chrono::steady_clock::now();
-    auto sat_stop = std::chrono::time_point_cast<std::chrono::seconds>(now);
-    status() << "Runtime decision procedure: " << (sat_stop - sat_start).count()
+    auto solver_stop=std::chrono::steady_clock::now();
+    status() << "Runtime decision procedure: "
+             << std::chrono::duration<double>(solver_stop-solver_start).count()
              << "s" << eom;
   }
 

src/cbmc/fault_localization.cpp

@@ -246,8 +246,7 @@ fault_localizationt::run_decision_procedure(prop_convt &prop_conv)
 
   prop_conv.set_message_handler(bmc.get_message_handler());
 
-  auto now = std::chrono::steady_clock::now();
-  auto sat_start = std::chrono::time_point_cast<std::chrono::seconds>(now);
+  auto solver_start=std::chrono::steady_clock::now();
 
   bmc.do_conversion();
 
@@ -260,9 +259,9 @@ fault_localizationt::run_decision_procedure(prop_convt &prop_conv)
   // output runtime
 
   {
-    now = std::chrono::steady_clock::now();
-    auto sat_stop = std::chrono::time_point_cast<std::chrono::seconds>(now);
-    status() << "Runtime decision procedure: " << (sat_stop - sat_start).count()
+    auto solver_stop=std::chrono::steady_clock::now();
+    status() << "Runtime decision procedure: "
+             << std::chrono::duration<double>(solver_stop-solver_start).count()
              << "s" << eom;
   }