diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h
index 570d405de39..40a6f5bd03c 100644
--- a/src/goto-checker/bmc_util.h
+++ b/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;
diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp
index 39306b2ad7a..76c72b203c2 100644
--- a/src/goto-checker/multi_path_symex_checker.cpp
+++ b/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>
diff --git a/src/goto-checker/multi_path_symex_checker.h b/src/goto-checker/multi_path_symex_checker.h
index 550c59944f9..b604681a32b 100644
--- a/src/goto-checker/multi_path_symex_checker.h
+++ b/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,
diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp
index 11d03e18bcd..95596b3820c 100644
--- a/src/goto-checker/multi_path_symex_only_checker.cpp
+++ b/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(
diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/src/goto-checker/single_loop_incremental_symex_checker.cpp
index 6369847c30b..ed3eedbe96c 100644
--- a/src/goto-checker/single_loop_incremental_symex_checker.cpp
+++ b/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>
diff --git a/src/goto-checker/single_path_symex_checker.h b/src/goto-checker/single_path_symex_checker.h
index fef0d160734..eca9ad0af80 100644
--- a/src/goto-checker/single_path_symex_checker.h
+++ b/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"
diff --git a/src/goto-checker/single_path_symex_only_checker.cpp b/src/goto-checker/single_path_symex_only_checker.cpp
index 01a65fb5011..f86d590882c 100644
--- a/src/goto-checker/single_path_symex_only_checker.cpp
+++ b/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>
diff --git a/src/goto-checker/single_path_symex_only_checker.h b/src/goto-checker/single_path_symex_only_checker.h
index 1732a76881a..325459e919c 100644
--- a/src/goto-checker/single_path_symex_only_checker.h
+++ b/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;
 
diff --git a/src/goto-checker/symex_coverage.cpp b/src/goto-checker/symex_coverage.cpp
index cd6f3552b95..f5df2f85df6 100644
--- a/src/goto-checker/symex_coverage.cpp
+++ b/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>
 
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 216a3bd97df..1bf93dc87a0 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -12,13 +12,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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)
 {
diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
index df911ebbe78..66830cbea17 100644
--- a/src/solvers/prop/prop_conv_solver.cpp
+++ b/src/solvers/prop/prop_conv_solver.cpp
@@ -8,11 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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());