Cleanup chrono includes

With Ubuntu 22.04 GitHub runner image 20221119.2 there appears to be
some libclang difference so that include-what-you-use newly started
suggesting `bits/chrono` instead of `chrono` (which is spurious);
nevertheless, some of the uses of `#include <chrono>` indeed were
unnecessary.

Fixes: #7383

Author: tautschnig

src/goto-checker/bmc_util.h

@@ -12,16 +12,15 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_BMC_UTIL_H
 #define CPROVER_GOTO_CHECKER_BMC_UTIL_H
 
-#include <chrono>
-#include <memory>
-
-#include <goto-symex/build_goto_trace.h>
-
 #include <goto-instrument/unwindset.h>
+#include <goto-symex/build_goto_trace.h>
 
 #include "incremental_goto_checker.h"
 #include "properties.h"
 
+#include <chrono> // IWYU pragma: keep
+#include <memory>
+
 class decision_proceduret;
 class goto_symex_property_decidert;
 class goto_tracet;

src/goto-checker/multi_path_symex_checker.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "multi_path_symex_checker.h"
 
-#include <chrono>
-
 #include <util/ui_message.h>
 
 #include <goto-symex/solver_hardness.h>

src/goto-checker/multi_path_symex_checker.h

@@ -12,14 +12,14 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H
 #define CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H
 
-#include <chrono>
-
 #include "fault_localization_provider.h"
 #include "goto_symex_property_decider.h"
 #include "goto_trace_provider.h"
 #include "multi_path_symex_only_checker.h"
 #include "witness_provider.h"
 
+#include <chrono> // IWYU pragma: keep
+
 /// Performs a multi-path symbolic execution using goto-symex
 /// and calls a SAT/SMT solver to check the status of the properties.
 class multi_path_symex_checkert : public multi_path_symex_only_checkert,

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -16,8 +16,6 @@ Author: Daniel Kroening, Peter Schrammel
 #include <goto-symex/show_program.h>
 #include <goto-symex/show_vcc.h>
 
-#include <chrono>
-
 #include "bmc_util.h"
 
 multi_path_symex_only_checkert::multi_path_symex_only_checkert(

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -13,8 +13,6 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "single_loop_incremental_symex_checker.h"
 
-#include <chrono>
-
 #include <util/structured_data.h>
 
 #include <goto-symex/slice.h>

src/goto-checker/single_path_symex_checker.h

@@ -12,8 +12,6 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_CHECKER_H
 #define CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_CHECKER_H
 
-#include <chrono>
-
 #include "goto_symex_property_decider.h"
 #include "goto_trace_provider.h"
 #include "single_path_symex_only_checker.h"

src/goto-checker/single_path_symex_only_checker.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "single_path_symex_only_checker.h"
 
-#include <chrono>
-
 #include <util/ui_message.h>
 
 #include <goto-symex/path_storage.h>

src/goto-checker/single_path_symex_only_checker.h

@@ -12,13 +12,12 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
 #define CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
 
-#include "incremental_goto_checker.h"
-
+#include <goto-instrument/unwindset.h>
 #include <goto-symex/path_storage.h>
 
-#include <goto-instrument/unwindset.h>
+#include "incremental_goto_checker.h"
 
-#include <chrono>
+#include <chrono> // IWYU pragma: keep
 
 class symex_bmct;
 

src/goto-checker/symex_coverage.cpp

@@ -23,8 +23,7 @@ Date: March 2016
 #include <langapi/language_util.h>
 #include <linking/static_lifetime_init.h>
 
-#include <chrono>
-#include <ctime>
+#include <chrono> // IWYU pragma: keep
 #include <fstream> // IWYU pragma: keep
 #include <iostream>
 

src/goto-symex/symex_target_equation.cpp

@@ -12,13 +12,13 @@ Author: Daniel Kroening, [email protected]
 
 #include "symex_target_equation.h"
 
-#include <chrono>
-
 #include <util/std_expr.h>
 
 #include "solver_hardness.h"
 #include "ssa_step.h"
 
+#include <chrono> // IWYU pragma: keep
+
 static std::function<void(solver_hardnesst &)>
 hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
 {

src/solvers/prop/prop_conv_solver.cpp

@@ -8,11 +8,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "prop_conv_solver.h"
 
-#include <algorithm>
-#include <chrono>
-
 #include "literal_expr.h"
 
+#include <algorithm>
+#include <chrono> // IWYU pragma: keep
+
 bool prop_conv_solvert::is_in_conflict(const exprt &expr) const
 {
   return prop.is_in_conflict(to_literal_expr(expr).get_literal());