chrono

Author: Daniel Kroening

src/ebmc/cegar/bmc_cegar.cpp

@@ -6,17 +6,16 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <cassert>
-
-#include <util/time_stopping.h>
+#include "bmc_cegar.h"
 
 #include <trans-netlist/instantiate_netlist.h>
 #include <trans-netlist/unwind_netlist.h>
 #include <trans-netlist/ldg.h>
 #include <trans-netlist/trans_to_netlist.h>
 #include <trans-netlist/compute_ct.h>
 
-#include "bmc_cegar.h"
+#include <cassert>
+#include <chrono>
 
 /*******************************************************************\
 
@@ -40,16 +39,20 @@ void bmc_cegart::bmc_cegar()
     return;
   }
 
-  absolute_timet start_time=current_time();
+  auto start_time=std::chrono::steady_clock::now();
 
   try { cegar_loop(); }
 
   catch(int)
   {
   }
 
-  statistics() << "CEGAR time: "
-               << (current_time()-start_time) << eom;
+  auto stop_time = std::chrono::steady_clock::now();
+
+  statistics()
+    << "CEGAR time: "
+    << std::chrono::duration<double>(stop_time-start_time).count()
+    << eom;
 }
 
 /*******************************************************************\

src/ebmc/ebmc_base.cpp

@@ -9,7 +9,6 @@ Author: Daniel Kroening, [email protected]
 #include <fstream>
 #include <iostream>
 
-#include <util/time_stopping.h>
 #include <util/get_module.h>
 #include <util/xml.h>
 #include <util/find_macros.h>
@@ -34,7 +33,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language_util.h>
 #include <langapi/mode.h>
-#include <langapi/languages.h>
 
 #include "ebmc_base.h"
 #include "ebmc_version.h"
@@ -99,7 +97,7 @@ int ebmc_baset::finish_bmc(prop_convt &solver)
   status() << "Solving with "
            << solver.decision_procedure_text() << eom;
 
-  absolute_timet sat_start_time=current_time();
+  auto sat_start_time = std::chrono::steady_clock::now();
 
   // Use assumptions to check the properties separately
 
@@ -159,8 +157,12 @@ int ebmc_baset::finish_bmc(prop_convt &solver)
     }
   }
 
-  statistics() << "Solver time: " << (current_time()-sat_start_time)
-               << eom;
+  auto sat_stop_time = std::chrono::steady_clock::now();
+
+  statistics()
+     << "Solver time: "
+     << std::chrono::duration<double>(current_time()-sat_start_time).count()
+     << eom;
 
   // We return '0' if the property holds,
   // and '10' if it is violated.