diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h
index bc1c848413fa..d84c6da19642 100644
--- a/src/analyses/goto_rw.h
+++ b/src/analyses/goto_rw.h
@@ -12,9 +12,9 @@ Date: April 2010
 #ifndef CPROVER_ANALYSES_GOTO_RW_H
 #define CPROVER_ANALYSES_GOTO_RW_H
 
-#include <map>
 #include <iosfwd>
 #include <limits>
+#include <map>
 #include <memory> // unique_ptr
 
 #include <util/guard.h>
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index 04da61316088..f15a3124f555 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -8,19 +8,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "ansi_c_entry_point.h"
 
-#include <cassert>
-#include <cstdlib>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
-#include <util/cprover_prefix.h>
-#include <util/namespace.h>
-#include <util/prefix.h>
-#include <util/std_code.h>
-#include <util/std_expr.h>
 #include <util/string_constant.h>
-#include <util/symbol.h>
 
 #include <goto-programs/goto_functions.h>
 
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index 9b7d88d2bfbc..8200e70a84e5 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -11,22 +11,14 @@ Author: Diffblue Ltd.
 
 #include "c_nondet_symbol_factory.h"
 
-#include <set>
-#include <sstream>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/fresh_symbol.h>
 #include <util/namespace.h>
-#include <util/pointer_offset_size.h>
-#include <util/prefix.h>
-#include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>
 
-#include <linking/zero_initializer.h>
-
 #include <goto-programs/goto_functions.h>
 
 /// Create a new temporary static symbol
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 5a8eb6cfb4e7..fb27e0653e32 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -14,17 +14,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 
 #include <util/arith_tools.h>
-#include <util/c_types.h>
-#include <util/config.h>
-#include <util/std_types.h>
-#include <util/prefix.h>
-#include <util/cprover_prefix.h>
-#include <util/simplify_expr.h>
 #include <util/base_type.h>
-#include <util/std_expr.h>
-#include <util/string_constant.h>
+#include <util/cprover_prefix.h>
+#include <util/c_types.h>
+#include <util/ieee_float.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
+#include <util/string_constant.h>
 
 #include "builtin_factory.h"
 #include "c_typecast.h"
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 1acc58d2f20d..dcb40a0e897e 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -13,19 +13,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <unordered_set>
 
+#include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
-#include <util/invariant.h>
-#include <util/simplify_expr.h>
-#include <util/arith_tools.h>
-#include <util/std_types.h>
 #include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 
+#include "ansi_c_convert_type.h"
 #include "c_qualifiers.h"
-#include "ansi_c_declaration.h"
 #include "padding.h"
 #include "type2name.h"
-#include "ansi_c_convert_type.h"
 
 void c_typecheck_baset::typecheck_type(typet &type)
 {
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index f309f9be7ece..305a38e008f0 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -13,23 +13,18 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <sstream>
 
 #include <map>
-#include <set>
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
-#include <util/std_types.h>
-#include <util/std_code.h>
-#include <util/ieee_float.h>
+#include <util/find_symbols.h>
 #include <util/fixedbv.h>
-#include <util/prefix.h>
-#include <util/lispirep.h>
 #include <util/lispexpr.h>
+#include <util/lispirep.h>
 #include <util/namespace.h>
-#include <util/symbol.h>
-#include <util/suffix.h>
-#include <util/find_symbols.h>
 #include <util/pointer_offset_size.h>
+#include <util/suffix.h>
+#include <util/symbol.h>
 
 #include "c_misc.h"
 #include "c_qualifiers.h"
diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp
index 3f1b6e859050..614b46b7ea06 100644
--- a/src/ansi-c/type2name.cpp
+++ b/src/ansi-c/type2name.cpp
@@ -11,13 +11,12 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "type2name.h"
 
-#include <util/std_types.h>
 #include <util/arith_tools.h>
+#include <util/invariant.h>
 #include <util/namespace.h>
-#include <util/symbol.h>
-#include <util/symbol_table.h>
 #include <util/pointer_offset_size.h>
-#include <util/invariant.h>
+#include <util/std_types.h>
+#include <util/symbol_table.h>
 
 typedef std::unordered_map<irep_idt, std::pair<size_t, bool>> symbol_numbert;
 
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index e0af60274f54..545ab8a54f16 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -12,35 +12,22 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "bmc.h"
 
 #include <chrono>
-#include <exception>
-#include <fstream>
 #include <iostream>
-#include <memory>
 
 #include <util/exit_codes.h>
 #include <util/string2int.h>
-#include <util/source_location.h>
 #include <util/string_utils.h>
-#include <util/memory_info.h>
-#include <util/message.h>
-#include <util/json.h>
-#include <util/json_stream.h>
-#include <util/cprover_prefix.h>
 
-#include <langapi/mode.h>
 #include <langapi/language_util.h>
 
-#include <goto-programs/goto_model.h>
-#include <goto-programs/xml_goto_trace.h>
-#include <goto-programs/json_goto_trace.h>
 #include <goto-programs/graphml_witness.h>
+#include <goto-programs/json_goto_trace.h>
+#include <goto-programs/xml_goto_trace.h>
 
 #include <goto-symex/build_goto_trace.h>
+#include <goto-symex/memory_model_pso.h>
 #include <goto-symex/slice.h>
 #include <goto-symex/slice_by_trace.h>
-#include <goto-symex/memory_model_sc.h>
-#include <goto-symex/memory_model_tso.h>
-#include <goto-symex/memory_model_pso.h>
 
 #include <linking/static_lifetime_init.h>
 
diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp
index 77f7fe93ba61..0ecd58b10833 100644
--- a/src/cbmc/symex_coverage.cpp
+++ b/src/cbmc/symex_coverage.cpp
@@ -13,16 +13,13 @@ Date: March 2016
 
 #include "symex_coverage.h"
 
-#include <ctime>
 #include <chrono>
-#include <iostream>
+#include <ctime>
 #include <fstream>
-#include <sstream>
+#include <iostream>
 
-#include <util/xml.h>
 #include <util/string2int.h>
-#include <util/cprover_prefix.h>
-#include <util/prefix.h>
+#include <util/xml.h>
 
 #include <langapi/language_util.h>
 
diff --git a/src/cbmc/symex_coverage.h b/src/cbmc/symex_coverage.h
index 9bba52fd84b5..6eac2cf4ef73 100644
--- a/src/cbmc/symex_coverage.h
+++ b/src/cbmc/symex_coverage.h
@@ -14,9 +14,9 @@ Date: March 2016
 #ifndef CPROVER_CBMC_SYMEX_COVERAGE_H
 #define CPROVER_CBMC_SYMEX_COVERAGE_H
 
-#include <string>
 #include <iosfwd>
 #include <map>
+#include <string>
 
 #include <goto-programs/goto_program.h>
 
diff --git a/src/cpp/cpp_template_type.h b/src/cpp/cpp_template_type.h
index de472b41a485..9c69e6208def 100644
--- a/src/cpp/cpp_template_type.h
+++ b/src/cpp/cpp_template_type.h
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <util/invariant.h>
 #include <util/type.h>
-#include <util/expr.h>
 
 #include "cpp_template_parameter.h"
 
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index a6502391c3e8..45d7c8727596 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -15,23 +15,18 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <iostream>
 #endif
 
-#include <util/pointer_offset_size.h>
-#include <util/std_types.h>
 #include <util/arith_tools.h>
-#include <util/std_expr.h>
-#include <util/config.h>
-#include <util/simplify_expr.h>
 #include <util/base_type.h>
-#include <util/invariant.h>
-
 #include <util/c_types.h>
+#include <util/config.h>
+#include <util/pointer_offset_size.h>
+
 #include <ansi-c/c_qualifiers.h>
 
 #include <linking/zero_initializer.h>
 
-#include "cpp_type2name.h"
-#include "cpp_convert_type.h"
 #include "cpp_exception_id.h"
+#include "cpp_type2name.h"
 #include "expr2cpp.h"
 
 bool cpp_typecheckt::find_parent(
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
index 565bca8a4bbd..c4c856378783 100644
--- a/src/cpp/cpp_typecheck_initializer.cpp
+++ b/src/cpp/cpp_typecheck_initializer.cpp
@@ -14,12 +14,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
-#include <util/std_expr.h>
 
 #include <linking/zero_initializer.h>
 
-#include "cpp_util.h"
-
 /// Initialize an object with a value
 void cpp_typecheckt::convert_initializer(symbolt &symbol)
 {
diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp
index 99c8d63cefd1..835311faf096 100644
--- a/src/goto-analyzer/static_show_domain.cpp
+++ b/src/goto-analyzer/static_show_domain.cpp
@@ -8,6 +8,8 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 
 #include "static_show_domain.h"
 
+#include <util/options.h>
+
 #include <analyses/dependence_graph.h>
 
 /// Runs the analyzer and then prints out the domain
diff --git a/src/goto-analyzer/static_show_domain.h b/src/goto-analyzer/static_show_domain.h
index 1b2c3ee3772f..71a6e90ef92d 100644
--- a/src/goto-analyzer/static_show_domain.h
+++ b/src/goto-analyzer/static_show_domain.h
@@ -11,12 +11,10 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 
 #include <iosfwd>
 
-#include <util/message.h>
-#include <util/options.h>
-
-#include <goto-programs/goto_model.h>
-
-#include <analyses/ai.h>
+class ai_baset;
+class goto_modelt;
+class message_handlert;
+class optionst;
 
 bool static_show_domain(
   const goto_modelt &,
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index 9e6ffa578223..08e29037c703 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -6,17 +6,17 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 
 \*******************************************************************/
 
+#include "static_simplifier.h"
+
+#include <util/message.h>
+#include <util/options.h>
+
+#include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unreachable.h>
 #include <goto-programs/write_goto_binary.h>
 
-#include <util/xml.h>
-#include <util/xml_expr.h>
-#include <util/json.h>
-#include <util/json_expr.h>
-
-#include "static_simplifier.h"
-
+#include <analyses/ai.h>
 
 /// Simplifies the program using the information in the abstract domain.
 /// \param goto_model: the program analyzed
diff --git a/src/goto-analyzer/static_simplifier.h b/src/goto-analyzer/static_simplifier.h
index 59e741fba83c..557d94737c0a 100644
--- a/src/goto-analyzer/static_simplifier.h
+++ b/src/goto-analyzer/static_simplifier.h
@@ -11,12 +11,10 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 
 #include <iosfwd>
 
-#include <util/message.h>
-#include <util/options.h>
-
-#include <goto-programs/goto_model.h>
-
-#include <analyses/ai.h>
+class ai_baset;
+class goto_modelt;
+class message_handlert;
+class optionst;
 
 bool static_simplifier(
   goto_modelt &,
diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp
index 660d20bd37e2..f4fbc6320b7d 100644
--- a/src/goto-analyzer/static_verifier.cpp
+++ b/src/goto-analyzer/static_verifier.cpp
@@ -8,11 +8,14 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 
 #include "static_verifier.h"
 
-#include <util/xml.h>
-#include <util/xml_expr.h>
-#include <util/json.h>
 #include <util/json_expr.h>
+#include <util/message.h>
+#include <util/namespace.h>
+#include <util/options.h>
 
+#include <goto-programs/goto_model.h>
+
+#include <analyses/ai.h>
 
 /// Runs the analyzer and then prints out the domain
 /// \param goto_model: the program analyzed
diff --git a/src/goto-analyzer/static_verifier.h b/src/goto-analyzer/static_verifier.h
index e71bdfbb45c0..87358a309586 100644
--- a/src/goto-analyzer/static_verifier.h
+++ b/src/goto-analyzer/static_verifier.h
@@ -11,12 +11,10 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 
 #include <iosfwd>
 
-#include <util/message.h>
-#include <util/options.h>
-
-#include <goto-programs/goto_model.h>
-
-#include <analyses/ai.h>
+class ai_baset;
+class goto_modelt;
+class message_handlert;
+class optionst;
 
 bool static_verifier(
   const goto_modelt &,
diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp
index 0e783baaba5f..c691142aeadc 100644
--- a/src/goto-analyzer/unreachable_instructions.cpp
+++ b/src/goto-analyzer/unreachable_instructions.cpp
@@ -13,18 +13,16 @@ Date: April 2016
 
 #include "unreachable_instructions.h"
 
-#include <sstream>
-
-#include <util/json.h>
-#include <util/json_expr.h>
 #include <util/file_util.h>
+#include <util/json_expr.h>
+#include <util/options.h>
 #include <util/xml.h>
 
-#include <analyses/cfg_dominators.h>
-
-#include <goto-programs/goto_model.h>
 #include <goto-programs/compute_called_functions.h>
 
+#include <analyses/ai.h>
+#include <analyses/cfg_dominators.h>
+
 typedef std::map<unsigned, goto_programt::const_targett> dead_mapt;
 
 static void unreachable_instructions(
diff --git a/src/goto-analyzer/unreachable_instructions.h b/src/goto-analyzer/unreachable_instructions.h
index edffd0f7b1c9..eeee658ea524 100644
--- a/src/goto-analyzer/unreachable_instructions.h
+++ b/src/goto-analyzer/unreachable_instructions.h
@@ -14,14 +14,12 @@ Date: April 2016
 #ifndef CPROVER_GOTO_ANALYZER_UNREACHABLE_INSTRUCTIONS_H
 #define CPROVER_GOTO_ANALYZER_UNREACHABLE_INSTRUCTIONS_H
 
-#include <ostream>
-
-#include <analyses/ai.h>
-
-#include <util/options.h>
-#include <util/message.h>
+#include <iosfwd>
 
+class ai_baset;
 class goto_modelt;
+class message_handlert;
+class optionst;
 
 void unreachable_instructions(
   const goto_modelt &,
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index c092f940f952..98550ce73750 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -15,27 +15,21 @@ Date: June 2006
 
 #include <cstring>
 #include <fstream>
-#include <sstream>
 #include <iostream>
-#include <cstdlib>
-#include <algorithm>
 
-#include <util/config.h>
-#include <util/tempdir.h>
-#include <util/base_type.h>
 #include <util/cmdline.h>
+#include <util/config.h>
 #include <util/file_util.h>
-#include <util/unicode.h>
-#include <util/irep_serialization.h>
-#include <util/suffix.h>
 #include <util/get_base_name.h>
+#include <util/suffix.h>
+#include <util/tempdir.h>
+#include <util/unicode.h>
 
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/ansi_c_entry_point.h>
 
 #include <goto-programs/goto_convert.h>
 #include <goto-programs/goto_convert_functions.h>
-#include <goto-programs/goto_inline.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/write_goto_binary.h>
 
diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
index c7ede9677682..d89900d11f31 100644
--- a/src/goto-cc/linker_script_merge.cpp
+++ b/src/goto-cc/linker_script_merge.cpp
@@ -6,32 +6,25 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>, 2017
 
 \*******************************************************************/
 
-#include <json/json_parser.h>
+#include "linker_script_merge.h"
 
 #include <algorithm>
-#include <cstdio>
-#include <iostream>
-#include <iterator>
 #include <fstream>
+#include <iterator>
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
-#include <util/expr.h>
-#include <util/get_base_name.h>
 #include <util/magic.h>
-#include <util/prefix.h>
 #include <util/run.h>
-#include <util/string2int.h>
 #include <util/tempfile.h>
 
+#include <json/json_parser.h>
+
 #include <linking/static_lifetime_init.h>
 #include <linking/zero_initializer.h>
 
 #include <goto-programs/read_goto_binary.h>
 
-#include "compile.h"
-#include "linker_script_merge.h"
-
 int linker_script_merget::add_linker_script_definitions()
 {
   if(!cmdline.isset('T') || elf_binaries.size()!=1)
diff --git a/src/goto-diff/goto_diff.h b/src/goto-diff/goto_diff.h
index 72171a76b316..efb90d1ed1d4 100644
--- a/src/goto-diff/goto_diff.h
+++ b/src/goto-diff/goto_diff.h
@@ -12,13 +12,14 @@ Author: Peter Schrammel
 #ifndef CPROVER_GOTO_DIFF_GOTO_DIFF_H
 #define CPROVER_GOTO_DIFF_GOTO_DIFF_H
 
-#include <goto-programs/goto_model.h>
-
-#include <util/json.h>
 #include <util/ui_message.h>
 
-#include <ostream>
+#include <iosfwd>
+#include <set>
 
+class goto_modelt;
+class json_arrayt;
+class json_objectt;
 class optionst;
 
 class goto_difft:public messaget
diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp
index db3b925d7027..a06b13edf2b7 100644
--- a/src/goto-diff/goto_diff_base.cpp
+++ b/src/goto-diff/goto_diff_base.cpp
@@ -11,11 +11,12 @@ Author: Peter Schrammel
 
 #include "goto_diff.h"
 
-#include <goto-programs/show_properties.h>
-
 #include <util/json_expr.h>
 #include <util/options.h>
 
+#include <goto-programs/goto_model.h>
+#include <goto-programs/show_properties.h>
+
 /// Output diff result
 void goto_difft::output_functions() const
 {
diff --git a/src/goto-diff/syntactic_diff.cpp b/src/goto-diff/syntactic_diff.cpp
index 83f4ef04a78d..558bf1a8eb8d 100644
--- a/src/goto-diff/syntactic_diff.cpp
+++ b/src/goto-diff/syntactic_diff.cpp
@@ -11,6 +11,8 @@ Author: Peter Schrammel
 
 #include "syntactic_diff.h"
 
+#include <goto-programs/goto_model.h>
+
 bool syntactic_difft::operator()()
 {
   forall_goto_functions(it, goto_model1.goto_functions)
diff --git a/src/goto-instrument/alignment_checks.cpp b/src/goto-instrument/alignment_checks.cpp
index 68c173bda7aa..758539c68beb 100644
--- a/src/goto-instrument/alignment_checks.cpp
+++ b/src/goto-instrument/alignment_checks.cpp
@@ -11,9 +11,8 @@ Module: Alignment Checks
 
 #include "alignment_checks.h"
 
-#include <util/pointer_offset_size.h>
 #include <util/config.h>
-#include <util/symbol_table.h>
+#include <util/pointer_offset_size.h>
 
 void print_struct_alignment_problems(
   const symbol_tablet &symbol_table,
diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp
index 82da31087b8d..ca36d43ee991 100644
--- a/src/goto-instrument/call_sequences.cpp
+++ b/src/goto-instrument/call_sequences.cpp
@@ -15,9 +15,7 @@ Date: April 2013
 
 #include <stack>
 #include <iostream>
-#include <unordered_set>
 
-#include <util/std_expr.h>
 #include <util/simplify_expr.h>
 
 #include <goto-programs/goto_model.h>
diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp
index 16f3ebe83122..98d0d1248ebb 100644
--- a/src/goto-instrument/code_contracts.cpp
+++ b/src/goto-instrument/code_contracts.cpp
@@ -13,7 +13,6 @@ Date: February 2016
 
 #include "code_contracts.h"
 
-#include <util/cprover_prefix.h>
 #include <util/fresh_symbol.h>
 #include <util/replace_symbol.h>
 
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index c51a6859d3e5..2715f303063a 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -11,16 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "dump_c.h"
 
-#include <sstream>
-#include <cctype>
-
+#include <util/base_type.h>
 #include <util/config.h>
-#include <util/invariant.h>
-#include <util/prefix.h>
-#include <util/suffix.h>
 #include <util/find_symbols.h>
-#include <util/base_type.h>
-#include <util/cprover_prefix.h>
+#include <util/invariant.h>
 #include <util/replace_symbol.h>
 
 #include <ansi-c/ansi_c_language.h>
@@ -28,8 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <linking/static_lifetime_init.h>
 
-#include "goto_program2code.h"
 #include "dump_c_class.h"
+#include "goto_program2code.h"
 
 inline std::ostream &operator << (std::ostream &out, dump_ct &src)
 {
diff --git a/src/goto-instrument/mmio.cpp b/src/goto-instrument/mmio.cpp
index db9df4293fe4..0e0a2a03693b 100644
--- a/src/goto-instrument/mmio.cpp
+++ b/src/goto-instrument/mmio.cpp
@@ -15,18 +15,6 @@ Date: September 2011
 
 #include <linking/static_lifetime_init.h>
 
-#include <goto-programs/goto_program.h>
-#include <goto-programs/goto_functions.h>
-
-#if 0
-#include <util/std_expr.h>
-#include <util/guard.h>
-#include <util/prefix.h>
-
-#include <goto-programs/remove_skip.h>
-#endif
-
-#include "interrupt.h"
 #include "rw_set.h"
 
 #ifdef LOCAL_MAY
diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp
index 2dce04f9d221..51cbf5034fec 100644
--- a/src/goto-instrument/nondet_static.cpp
+++ b/src/goto-instrument/nondet_static.cpp
@@ -14,13 +14,7 @@ Date: November 2011
 
 #include "nondet_static.h"
 
-#include <util/namespace.h>
-#include <util/std_expr.h>
-#include <util/cprover_prefix.h>
-#include <util/prefix.h>
-
 #include <goto-programs/goto_model.h>
-#include <goto-programs/goto_functions.h>
 
 #include <linking/static_lifetime_init.h>
 
diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp
index 8517e90f1aeb..0289148f1eca 100644
--- a/src/goto-instrument/race_check.cpp
+++ b/src/goto-instrument/race_check.cpp
@@ -13,16 +13,6 @@ Date: February 2006
 
 #include "race_check.h"
 
-#include <util/std_expr.h>
-#include <util/guard.h>
-#include <util/symbol_table.h>
-#include <util/prefix.h>
-#include <util/cprover_prefix.h>
-
-#include <goto-programs/goto_program.h>
-#include <goto-programs/goto_functions.h>
-
-#include <pointer-analysis/value_sets.h>
 #include <goto-programs/remove_skip.h>
 
 #include <linking/static_lifetime_init.h>
diff --git a/src/goto-instrument/rw_set.h b/src/goto-instrument/rw_set.h
index 69072389347d..3dd99a9a7db0 100644
--- a/src/goto-instrument/rw_set.h
+++ b/src/goto-instrument/rw_set.h
@@ -19,17 +19,17 @@ Date: February 2006
 #include <set>
 
 #include <util/guard.h>
-#include <util/std_code.h>
-#include <util/namespace.h>
 #include <util/std_expr.h>
 
 #include <goto-programs/goto_model.h>
-#include <pointer-analysis/value_sets.h>
 
 #ifdef LOCAL_MAY
 #include <analyses/local_may_alias.h>
 #endif
 
+class namespacet;
+class value_setst;
+
 // a container for read/write sets
 
 class rw_set_baset
diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp
index a0e0457fa24b..9784d648f392 100644
--- a/src/goto-instrument/stack_depth.cpp
+++ b/src/goto-instrument/stack_depth.cpp
@@ -13,12 +13,7 @@ Date: November 2011
 
 #include "stack_depth.h"
 
-#include <util/c_types.h>
-#include <util/symbol_table.h>
-#include <util/std_expr.h>
-#include <util/std_types.h>
 #include <util/arith_tools.h>
-#include <util/cprover_prefix.h>
 
 #include <goto-programs/goto_model.h>
 
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
index 9611f56d2f7c..6d130be954b8 100644
--- a/src/goto-instrument/wmm/goto2graph.cpp
+++ b/src/goto-instrument/wmm/goto2graph.cpp
@@ -16,17 +16,8 @@ Date: 2012
 #include <vector>
 #include <string>
 #include <fstream>
-#include <limits>
 
-#ifndef _WIN32
-#include <cstdlib>
-#endif
-
-#include <util/prefix.h>
-#include <util/cprover_prefix.h>
 #include <util/options.h>
-#include <util/message.h>
-#include <util/std_expr.h>
 
 #include <linking/static_lifetime_init.h>
 
diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
index 4f8a5e65247a..feadf6af1ad8 100644
--- a/src/goto-instrument/wmm/shared_buffers.cpp
+++ b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -8,12 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "shared_buffers.h"
 
+#include <util/c_types.h>
+
 #include <linking/static_lifetime_init.h>
 
-#include "fence.h"
 #include "../rw_set.h"
-
-#include <util/c_types.h>
+#include "fence.h"
 
 /// returns a unique id (for fresh variables)
 std::string shared_bufferst::unique(void)
diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp
index 1f2e38b61daa..155e20643839 100644
--- a/src/goto-instrument/wmm/weak_memory.cpp
+++ b/src/goto-instrument/wmm/weak_memory.cpp
@@ -23,10 +23,6 @@ Date: September 2011
 
 #include <set>
 
-#include <util/cprover_prefix.h>
-#include <util/prefix.h>
-#include <util/message.h>
-
 #include <goto-programs/remove_skip.h>
 
 #include <linking/static_lifetime_init.h>
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index ba1dfb7c685b..13685785d712 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -17,17 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
 #include <util/pointer_offset_size.h>
-#include <util/pointer_predicates.h>
-#include <util/prefix.h>
 #include <util/rational.h>
 #include <util/rational_tools.h>
-#include <util/replace_expr.h>
-#include <util/simplify_expr.h>
-#include <util/source_location.h>
-#include <util/std_code.h>
-#include <util/std_expr.h>
-#include <util/string_constant.h>
-#include <util/symbol.h>
 
 #include <linking/zero_initializer.h>
 
diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h
index 9b926d25e18b..1d1803697659 100644
--- a/src/goto-programs/class_hierarchy.h
+++ b/src/goto-programs/class_hierarchy.h
@@ -19,7 +19,9 @@ Date: April 2016
 #include <unordered_map>
 
 #include <util/graph.h>
-#include <util/namespace.h>
+#include <util/irep.h>
+
+class symbol_tablet;
 
 class class_hierarchyt
 {
diff --git a/src/goto-programs/generate_function_bodies.cpp b/src/goto-programs/generate_function_bodies.cpp
index 64d12ce0d4a8..aca0ed19abad 100644
--- a/src/goto-programs/generate_function_bodies.cpp
+++ b/src/goto-programs/generate_function_bodies.cpp
@@ -8,17 +8,10 @@ Author: Diffblue Ltd.
 
 #include "generate_function_bodies.h"
 
-#include <memory>
-#include <sstream>
-#include <utility>
-#include <functional>
-
+#include <util/arith_tools.h>
 #include <util/format_expr.h>
 #include <util/make_unique.h>
-#include <util/message.h>
 #include <util/string_utils.h>
-#include <util/pointer_offset_size.h>
-#include <util/arith_tools.h>
 
 void generate_function_bodiest::generate_function_body(
   goto_functiont &function,
diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h
index 12b6b8c98be2..0289fbdfcc24 100644
--- a/src/goto-programs/goto_functions.h
+++ b/src/goto-programs/goto_functions.h
@@ -14,14 +14,12 @@ Date: June 2003
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
 
-#include "goto_program.h"
-
-#include <ostream>
-#include <cassert>
+#include <iosfwd>
 
-#include <util/std_types.h>
-#include <util/symbol.h>
 #include <util/cprover_prefix.h>
+#include <util/std_types.h>
+
+#include "goto_program.h"
 
 class goto_functiont
 {
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
index aa53dfd97d81..88c84258b2f2 100644
--- a/src/goto-programs/goto_program.h
+++ b/src/goto-programs/goto_program.h
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
 
-#include <cassert>
 #include <iosfwd>
 #include <set>
 #include <limits>
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index a4a0ca7179bb..616f5308cb2c 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -11,15 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "interpreter_class.h"
 
-#include <iostream>
-#include <sstream>
-#include <cstring>
-
-#include <util/ieee_float.h>
-#include <util/invariant.h>
 #include <util/fixedbv.h>
-#include <util/std_expr.h>
-#include <util/string_container.h>
+#include <util/ieee_float.h>
 #include <util/pointer_offset_size.h>
 
 #include <langapi/language_util.h>
diff --git a/src/goto-programs/remove_asm.cpp b/src/goto-programs/remove_asm.cpp
index d93032a33aa4..8df9d6429e86 100644
--- a/src/goto-programs/remove_asm.cpp
+++ b/src/goto-programs/remove_asm.cpp
@@ -14,14 +14,13 @@ Date:   December 2014
 
 #include "remove_asm.h"
 
-#include <sstream>
-
 #include <util/c_types.h>
-#include <util/std_expr.h>
 #include <util/string_constant.h>
 
 #include <assembler/assembler_parser.h>
 
+#include "goto_model.h"
+
 class remove_asmt
 {
 public:
diff --git a/src/goto-programs/remove_asm.h b/src/goto-programs/remove_asm.h
index 913fe85c336f..49d668c74d9f 100644
--- a/src/goto-programs/remove_asm.h
+++ b/src/goto-programs/remove_asm.h
@@ -15,7 +15,10 @@ Date:   December 2014
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_ASM_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_ASM_H
 
-#include <goto-programs/goto_model.h>
+#include <goto-programs/goto_functions.h>
+
+class goto_modelt;
+class symbol_tablet;
 
 void remove_asm(
   goto_functionst::goto_functiont &goto_function,
diff --git a/src/goto-programs/remove_calls_no_body.cpp b/src/goto-programs/remove_calls_no_body.cpp
index b8e46c41edf6..62121dcfe175 100644
--- a/src/goto-programs/remove_calls_no_body.cpp
+++ b/src/goto-programs/remove_calls_no_body.cpp
@@ -9,9 +9,12 @@ Author: Daniel Poetzl
 /// \file
 /// Remove calls to functions without a body
 
-#include <util/invariant.h>
 #include "remove_calls_no_body.h"
 
+#include <util/invariant.h>
+
+#include "goto_functions.h"
+
 /// Remove a single call
 /// \param goto_program: goto program to modify
 /// \param target: iterator pointing to the call
diff --git a/src/goto-programs/remove_calls_no_body.h b/src/goto-programs/remove_calls_no_body.h
index de10c426f2e9..9b7382328ce3 100644
--- a/src/goto-programs/remove_calls_no_body.h
+++ b/src/goto-programs/remove_calls_no_body.h
@@ -12,7 +12,9 @@ Author: Daniel Poetzl
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_CALLS_NO_BODY_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_CALLS_NO_BODY_H
 
-#include "goto_functions.h"
+#include "goto_program.h"
+
+class goto_functionst;
 
 class remove_calls_no_bodyt
 {
diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp
index 141fc4709fc6..ef5b351f54d5 100644
--- a/src/goto-programs/remove_complex.cpp
+++ b/src/goto-programs/remove_complex.cpp
@@ -14,6 +14,10 @@ Date:   September 2014
 #include "remove_complex.h"
 
 #include <util/arith_tools.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+
+#include "goto_model.h"
 
 static exprt complex_member(const exprt &expr, irep_idt id)
 {
diff --git a/src/goto-programs/remove_complex.h b/src/goto-programs/remove_complex.h
index 098470ecc1a8..c448f4a15e72 100644
--- a/src/goto-programs/remove_complex.h
+++ b/src/goto-programs/remove_complex.h
@@ -14,7 +14,9 @@ Date:   September 2014
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_COMPLEX_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_COMPLEX_H
 
-#include <goto-programs/goto_model.h>
+class goto_functionst;
+class goto_modelt;
+class symbol_tablet;
 
 void remove_complex(symbol_tablet &, goto_functionst &);
 
diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp
index 9b8e67c8b680..81e2812136b7 100644
--- a/src/goto-programs/remove_const_function_pointers.cpp
+++ b/src/goto-programs/remove_const_function_pointers.cpp
@@ -11,9 +11,14 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com
 
 #include "remove_const_function_pointers.h"
 
-#include <ansi-c/c_qualifiers.h>
-#include <util/simplify_expr.h>
 #include <util/arith_tools.h>
+#include <util/simplify_expr.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+#include <ansi-c/c_qualifiers.h>
+
+#include "goto_functions.h"
 
 #define LOG(message, irep) \
   debug() << "Case " << __LINE__ << " : " << message << "\n" \
diff --git a/src/goto-programs/remove_const_function_pointers.h b/src/goto-programs/remove_const_function_pointers.h
index 469deaec0327..0299de8b3834 100644
--- a/src/goto-programs/remove_const_function_pointers.h
+++ b/src/goto-programs/remove_const_function_pointers.h
@@ -12,13 +12,22 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H
 
+#include <list>
 #include <unordered_set>
 
-#include "goto_model.h"
-#include <util/message.h>
 #include <util/expr.h>
-#include <util/namespace.h>
-
+#include <util/message.h>
+#include <util/mp_arith.h>
+
+class address_of_exprt;
+class dereference_exprt;
+class index_exprt;
+class member_exprt;
+class namespacet;
+class struct_exprt;
+class symbol_exprt;
+class symbol_tablet;
+class typecast_exprt;
 
 class remove_const_function_pointerst:public messaget
 {
diff --git a/src/goto-programs/remove_function_pointers.h b/src/goto-programs/remove_function_pointers.h
index 3038a9406371..4a7bbfb09b53 100644
--- a/src/goto-programs/remove_function_pointers.h
+++ b/src/goto-programs/remove_function_pointers.h
@@ -14,8 +14,11 @@ Date: June 2003
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
 
-#include "goto_model.h"
-#include <util/message.h>
+class goto_functionst;
+class goto_programt;
+class goto_modelt;
+class message_handlert;
+class symbol_tablet;
 
 // remove indirect function calls
 // and replace by case-split
diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
index 4c275ff9bbb2..5257c83ea0af 100644
--- a/src/goto-programs/remove_returns.cpp
+++ b/src/goto-programs/remove_returns.cpp
@@ -14,7 +14,8 @@ Date:   September 2009
 #include "remove_returns.h"
 
 #include <util/std_expr.h>
-#include <util/symbol_table.h>
+
+#include "goto_model.h"
 
 class remove_returnst
 {
diff --git a/src/goto-programs/remove_returns.h b/src/goto-programs/remove_returns.h
index f20171114783..32d2a81c8240 100644
--- a/src/goto-programs/remove_returns.h
+++ b/src/goto-programs/remove_returns.h
@@ -14,10 +14,17 @@ Date:   September 2009
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
 
-#include <goto-programs/goto_model.h>
+#include <functional>
+
+#include <util/std_types.h>
 
 #define RETURN_VALUE_SUFFIX "#return_value"
 
+class goto_functionst;
+class goto_model_functiont;
+class goto_modelt;
+class symbol_table_baset;
+
 // Turns 'return x' into an assignment to fkt#return_value,
 // unless the function returns void,
 // and a 'goto the_end_of_the_function'.
diff --git a/src/goto-programs/remove_skip.h b/src/goto-programs/remove_skip.h
index 68f9a833994d..6ff55bf3e034 100644
--- a/src/goto-programs/remove_skip.h
+++ b/src/goto-programs/remove_skip.h
@@ -12,8 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H
 
-#include "goto_functions.h"
+#include "goto_program.h"
 
+class goto_functionst;
 class goto_modelt;
 
 bool is_skip(const goto_programt &, goto_programt::const_targett);
diff --git a/src/goto-programs/remove_unreachable.cpp b/src/goto-programs/remove_unreachable.cpp
index 562546f377b1..07d71adf471b 100644
--- a/src/goto-programs/remove_unreachable.cpp
+++ b/src/goto-programs/remove_unreachable.cpp
@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <set>
 #include <stack>
 
+#include "goto_functions.h"
+
 /// remove unreachable code
 void remove_unreachable(goto_programt &goto_program)
 {
diff --git a/src/goto-programs/remove_unreachable.h b/src/goto-programs/remove_unreachable.h
index 5267529d3647..ec8ac9bb9fb2 100644
--- a/src/goto-programs/remove_unreachable.h
+++ b/src/goto-programs/remove_unreachable.h
@@ -12,7 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_UNREACHABLE_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_UNREACHABLE_H
 
-#include "goto_functions.h"
+class goto_functionst;
+class goto_programt;
 
 void remove_unreachable(goto_programt &goto_program);
 void remove_unreachable(goto_functionst &goto_functions);
diff --git a/src/goto-programs/remove_unused_functions.cpp b/src/goto-programs/remove_unused_functions.cpp
index 3092e1147965..edb4c712ec2c 100644
--- a/src/goto-programs/remove_unused_functions.cpp
+++ b/src/goto-programs/remove_unused_functions.cpp
@@ -13,6 +13,8 @@ Author: CM Wintersteiger
 
 #include <util/message.h>
 
+#include "goto_model.h"
+
 void remove_unused_functions(
   goto_modelt &goto_model,
   message_handlert &message_handler)
diff --git a/src/goto-programs/remove_unused_functions.h b/src/goto-programs/remove_unused_functions.h
index 8c8b1739a984..d7fd2569e185 100644
--- a/src/goto-programs/remove_unused_functions.h
+++ b/src/goto-programs/remove_unused_functions.h
@@ -12,9 +12,14 @@ Author: CM Wintersteiger
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_UNUSED_FUNCTIONS_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_UNUSED_FUNCTIONS_H
 
-#include <util/message.h>
+#include <set>
 
-#include <goto-programs/goto_model.h>
+#include <util/irep.h>
+
+class goto_functionst;
+class goto_modelt;
+class message_handlert;
+class symbol_tablet;
 
 void remove_unused_functions(
   goto_functionst &,
diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp
index f2e7f5b9fe4f..cabd5100698d 100644
--- a/src/goto-programs/remove_vector.cpp
+++ b/src/goto-programs/remove_vector.cpp
@@ -14,6 +14,10 @@ Date:   September 2014
 #include "remove_vector.h"
 
 #include <util/arith_tools.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+
+#include "goto_model.h"
 
 static bool have_to_remove_vector(const typet &type);
 
diff --git a/src/goto-programs/remove_vector.h b/src/goto-programs/remove_vector.h
index 960d75953a84..2bd1f623e953 100644
--- a/src/goto-programs/remove_vector.h
+++ b/src/goto-programs/remove_vector.h
@@ -14,7 +14,9 @@ Date:   September 2014
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_VECTOR_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_VECTOR_H
 
-#include <goto-programs/goto_model.h>
+class goto_functionst;
+class goto_modelt;
+class symbol_tablet;
 
 void remove_vector(symbol_tablet &, goto_functionst &);
 
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index 86e19e7de810..a242577e8cdb 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -8,18 +8,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 /// \file
 /// Remove Virtual Function (Method) Calls
-#include <algorithm>
-
 #include "remove_virtual_functions.h"
-#include "class_hierarchy.h"
-#include "class_identifier.h"
 
-#include <goto-programs/resolve_inherited_component.h>
+#include <algorithm>
 
-#include <util/c_types.h>
-#include <util/prefix.h>
 #include <util/type_eq.h>
 
+#include "class_identifier.h"
+#include "goto_model.h"
+#include "resolve_inherited_component.h"
+
 class remove_virtual_functionst
 {
 public:
diff --git a/src/goto-programs/remove_virtual_functions.h b/src/goto-programs/remove_virtual_functions.h
index 43bd0f2fea88..ae5d257f6fdc 100644
--- a/src/goto-programs/remove_virtual_functions.h
+++ b/src/goto-programs/remove_virtual_functions.h
@@ -14,8 +14,15 @@ Date: April 2016
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
 
-#include "goto_model.h"
+#include <util/std_expr.h>
+
 #include "class_hierarchy.h"
+#include "goto_program.h"
+
+class goto_functionst;
+class goto_model_functiont;
+class goto_modelt;
+class symbol_table_baset;
 
 // remove virtual function calls
 // and replace by case-split
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
index adbfa9b96b6c..60329fe62ae6 100644
--- a/src/goto-programs/string_abstraction.cpp
+++ b/src/goto-programs/string_abstraction.cpp
@@ -11,16 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "string_abstraction.h"
 
-#include <cstring>
-
-#include <util/pointer_predicates.h>
-#include <util/std_expr.h>
-#include <util/std_code.h>
-#include <util/message.h>
 #include <util/arith_tools.h>
-#include <util/type_eq.h>
-
 #include <util/c_types.h>
+#include <util/pointer_predicates.h>
+#include <util/type_eq.h>
 
 #include "pointer_arithmetic.h"
 
diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp
index 7acc15e890ba..9e736033df17 100644
--- a/src/goto-programs/vcd_goto_trace.cpp
+++ b/src/goto-programs/vcd_goto_trace.cpp
@@ -13,13 +13,11 @@ Date: June 2011
 
 #include "vcd_goto_trace.h"
 
-#include <ctime>
-#include <ostream>
 #include <cassert>
+#include <ctime>
 
-#include <util/arith_tools.h>
-#include <util/pointer_offset_size.h>
 #include <util/numbering.h>
+#include <util/pointer_offset_size.h>
 
 std::string as_vcd_binary(
   const exprt &expr,
diff --git a/src/goto-symex/equation_conversion_exceptions.h b/src/goto-symex/equation_conversion_exceptions.h
index f2055c1c9ec5..ffa57abefe07 100644
--- a/src/goto-symex/equation_conversion_exceptions.h
+++ b/src/goto-symex/equation_conversion_exceptions.h
@@ -12,7 +12,7 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
 #define CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
 
-#include <ostream>
+#include <sstream>
 
 #include <util/format_expr.h>
 
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 7d7edb8891f6..117693b83912 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -14,13 +14,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/options.h>
 #include <util/message.h>
-#include <util/byte_operators.h>
 
 #include <goto-programs/goto_functions.h>
 
 #include "goto_symex_state.h"
 #include "symex_target_equation.h"
 
+class byte_extract_exprt;
 class typet;
 class code_typet;
 class symbol_tablet;
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 6294e47b3a1d..f827f1ecaeaa 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -11,25 +11,15 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-#include <util/expr_util.h>
-#include <util/message.h>
 #include <util/arith_tools.h>
-#include <util/cprover_prefix.h>
-#include <util/std_types.h>
+#include <util/c_types.h>
+#include <util/invariant_utils.h>
 #include <util/pointer_offset_size.h>
-#include <util/symbol_table.h>
-#include <util/std_expr.h>
-#include <util/std_code.h>
 #include <util/simplify_expr.h>
-#include <util/prefix.h>
 #include <util/string2int.h>
-#include <util/invariant_utils.h>
-#include <util/c_types.h>
 
 #include <linking/zero_initializer.h>
 
-#include "goto_symex_state.h"
-
 inline static typet c_sizeof_type_rec(const exprt &expr)
 {
   const irept &sizeof_type=expr.find(ID_C_c_sizeof_type);
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 5e1e0cf4c913..ce6265e1c20e 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -12,11 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_symex.h"
 
 #include <util/arith_tools.h>
-#include <util/std_expr.h>
-#include <util/cprover_prefix.h>
 #include <util/base_type.h>
-#include <util/pointer_offset_size.h>
+#include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/pointer_offset_size.h>
 
 /// Given an expression, find the root object and the offset into it.
 ///
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 95b8866865e8..e259a515489d 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -11,16 +11,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-#include <util/invariant.h>
-#include <util/pointer_offset_size.h>
 #include <util/arith_tools.h>
 #include <util/base_type.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
+#include <util/invariant.h>
+#include <util/pointer_offset_size.h>
 
 #include <pointer-analysis/value_set_dereference.h>
-#include <pointer-analysis/rewrite_index.h>
-
-#include <util/c_types.h>
 
 #include "symex_dereference_state.h"
 
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 37e173928c47..6de8995364d4 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -11,19 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-#include <sstream>
-
-#include <util/cprover_prefix.h>
-#include <util/invariant.h>
-#include <util/prefix.h>
 #include <util/arith_tools.h>
 #include <util/base_type.h>
-#include <util/std_expr.h>
-#include <util/symbol_table.h>
-
+#include <util/byte_operators.h>
 #include <util/c_types.h>
-
-#include <analyses/dirty.h>
+#include <util/invariant.h>
 
 bool goto_symext::get_unwind_recursion(
   const irep_idt &identifier,
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index f3cc50c32bb6..30ca539f4290 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -12,14 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_symex.h"
 
 #include <util/arith_tools.h>
-#include <util/invariant.h>
-#include <util/rename.h>
 #include <util/base_type.h>
-#include <util/std_expr.h>
-#include <util/std_code.h>
 #include <util/byte_operators.h>
-#include <util/pointer_offset_size.h>
 #include <util/c_types.h>
+#include <util/pointer_offset_size.h>
 
 void goto_symext::havoc_rec(
   statet &state,
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index ef4a4e70cc82..2556ee4d7e99 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -8,31 +8,15 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "java_entry_point.h"
 
-#include <algorithm>
-#include <set>
-#include <unordered_set>
-#include <iostream>
-
-#include <linking/static_lifetime_init.h>
-
-#include <util/arith_tools.h>
-#include <util/c_types.h>
 #include <util/config.h>
-#include <util/cprover_prefix.h>
-#include <util/message.h>
-#include <util/namespace.h>
-#include <util/pointer_offset_size.h>
-#include <util/prefix.h>
-#include <util/std_code.h>
-#include <util/std_expr.h>
-#include <util/std_types.h>
 #include <util/string_constant.h>
 #include <util/suffix.h>
 
+#include <goto-programs/goto_functions.h>
+
 #include <linking/static_lifetime_init.h>
 
 #include "java_object_factory.h"
-#include "java_types.h"
 #include "java_utils.h"
 
 static void create_initialize(symbol_table_baset &symbol_table)
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index feaeb218f6ce..612a66f9ce53 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -8,32 +8,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "java_object_factory.h"
 
-#include <unordered_set>
-#include <sstream>
-
-#include <util/arith_tools.h>
 #include <util/fresh_symbol.h>
-#include <util/c_types.h>
-#include <util/std_code.h>
-#include <util/std_expr.h>
-#include <util/namespace.h>
 #include <util/nondet_bool.h>
-#include <util/nondet_ifthenelse.h>
 #include <util/pointer_offset_size.h>
-#include <util/prefix.h>
-#include <util/invariant.h>
-
-#include <linking/zero_initializer.h>
 
 #include <goto-programs/goto_functions.h>
 
-#include <java_bytecode/select_pointer_type.h>
-
-#include "java_types.h"
-#include "java_utils.h"
-#include "java_string_library_preprocess.h"
-#include "java_root_class.h"
 #include "generic_parameter_specialization_map_keys.h"
+#include "java_root_class.h"
 
 class java_object_factoryt
 {
diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp
index a8f1278e961d..43f60bd19504 100644
--- a/src/jsil/jsil_entry_point.cpp
+++ b/src/jsil/jsil_entry_point.cpp
@@ -13,10 +13,7 @@ Author: Michael Tautschnig, tautschn@amazon.com
 
 #include <util/arith_tools.h>
 #include <util/config.h>
-#include <util/symbol_table.h>
 #include <util/message.h>
-#include <util/std_types.h>
-#include <util/cprover_prefix.h>
 
 #include <goto-programs/goto_functions.h>
 
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index 5b5a1d36fd21..a93e0919e648 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -12,15 +12,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "linking.h"
 
 #include <cassert>
-#include <stack>
+#include <deque>
+#include <unordered_set>
 
-#include <util/find_symbols.h>
-#include <util/source_location.h>
 #include <util/base_type.h>
-#include <util/std_expr.h>
-#include <util/std_types.h>
-#include <util/simplify_expr.h>
+#include <util/find_symbols.h>
 #include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 
 #include <langapi/language_util.h>
 
diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp
index 91f6e3c411d8..d563278ff52a 100644
--- a/src/linking/remove_internal_symbols.cpp
+++ b/src/linking/remove_internal_symbols.cpp
@@ -11,12 +11,11 @@ Author: Daniel Kroening
 
 #include "remove_internal_symbols.h"
 
-#include <util/symbol_table.h>
-#include <util/namespace.h>
+#include <util/config.h>
 #include <util/find_symbols.h>
+#include <util/namespace.h>
 #include <util/std_types.h>
-#include <util/cprover_prefix.h>
-#include <util/config.h>
+#include <util/symbol_table.h>
 
 #include "static_lifetime_init.h"
 
diff --git a/src/linking/static_lifetime_init.h b/src/linking/static_lifetime_init.h
index 0955fc1f57cd..829e2e16a05c 100644
--- a/src/linking/static_lifetime_init.h
+++ b/src/linking/static_lifetime_init.h
@@ -10,11 +10,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_LINKING_STATIC_LIFETIME_INIT_H
 #define CPROVER_LINKING_STATIC_LIFETIME_INIT_H
 
-#include <util/symbol_table.h>
-#include <util/message.h>
-#include <util/source_location.h>
 #include <util/cprover_prefix.h>
 
+class message_handlert;
+class source_locationt;
+class symbol_tablet;
+
 bool static_lifetime_init(
   symbol_tablet &symbol_table,
   const source_locationt &source_location,
diff --git a/src/linking/zero_initializer.cpp b/src/linking/zero_initializer.cpp
index 0916256ab5d7..675cdb7dd7f8 100644
--- a/src/linking/zero_initializer.cpp
+++ b/src/linking/zero_initializer.cpp
@@ -11,16 +11,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "zero_initializer.h"
 
-#include <sstream>
-
-#include <util/namespace.h>
-#include <util/message.h>
 #include <util/arith_tools.h>
-#include <util/std_types.h>
-#include <util/std_expr.h>
+#include <util/c_types.h>
+#include <util/message.h>
+#include <util/namespace.h>
 #include <util/pointer_offset_size.h>
+#include <util/std_expr.h>
 
-#include <util/c_types.h>
 #include <ansi-c/expr2c.h>
 
 class zero_initializert:public messaget
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 0e528f5760bf..7cd08339d7a9 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -14,17 +14,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 #include <ostream>
 
-#include <util/symbol_table.h>
-#include <util/simplify_expr.h>
-#include <util/base_type.h>
-#include <util/std_expr.h>
-#include <util/prefix.h>
-#include <util/std_code.h>
 #include <util/arith_tools.h>
-#include <util/pointer_offset_size.h>
-#include <util/cprover_prefix.h>
-
+#include <util/base_type.h>
 #include <util/c_types.h>
+#include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 
 #include <langapi/language_util.h>
 
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 4e437ede5ea2..cca2293bd708 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -17,34 +17,24 @@ Author: Daniel Kroening, kroening@kroening.com
 #endif
 
 #include <cassert>
-#include <sstream>
 
-#include <util/format_type.h>
-#include <util/invariant.h>
-#include <util/string2int.h>
-#include <util/expr_util.h>
-#include <util/base_type.h>
 #include <util/arith_tools.h>
-#include <util/rename.h>
 #include <util/array_name.h>
+#include <util/base_type.h>
+#include <util/byte_operators.h>
 #include <util/config.h>
-#include <util/std_expr.h>
 #include <util/cprover_prefix.h>
-#include <util/pointer_offset_size.h>
-#include <util/symbol_table.h>
+#include <util/c_types.h>
+#include <util/format_type.h>
 #include <util/guard.h>
 #include <util/options.h>
+#include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
-#include <util/byte_operators.h>
+#include <util/rename.h>
 #include <util/ssa_expr.h>
-#include <util/c_types.h>
 
 #include <ansi-c/c_typecast.h>
 
-#include <pointer-analysis/value_set.h>
-
-#include "pointer_offset_sum.h"
-
 // global data, horrible
 unsigned int value_set_dereferencet::invalid_counter=0;
 
diff --git a/src/solvers/flattening/boolbv_update.cpp b/src/solvers/flattening/boolbv_update.cpp
index f5121f8bf91d..668b8cc8fdc7 100644
--- a/src/solvers/flattening/boolbv_update.cpp
+++ b/src/solvers/flattening/boolbv_update.cpp
@@ -8,13 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
-#include <util/std_types.h>
-#include <util/std_expr.h>
 #include <util/arith_tools.h>
-#include <util/base_type.h>
-#include <util/pointer_offset_size.h>
-
-#include <util/c_types.h>
 
 bvt boolbvt::convert_update(const exprt &expr)
 {
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index b82a54ac615c..7043938eccff 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -8,14 +8,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "bv_pointers.h"
 
+#include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
-#include <util/arith_tools.h>
-#include <util/invariant.h>
-#include <util/prefix.h>
-#include <util/std_expr.h>
 #include <util/pointer_offset_size.h>
-#include <util/threeval.h>
 
 literalt bv_pointerst::convert_rest(const exprt &expr)
 {
diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp
index 42054cc61dc7..2cc586c7c024 100644
--- a/src/solvers/flattening/flatten_byte_operators.cpp
+++ b/src/solvers/flattening/flatten_byte_operators.cpp
@@ -6,19 +6,17 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <util/c_types.h>
-#include <util/expr.h>
-#include <util/std_types.h>
-#include <util/std_expr.h>
+#include "flatten_byte_operators.h"
+
 #include <util/arith_tools.h>
-#include <util/pointer_offset_size.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 #include <util/namespace.h>
+#include <util/pointer_offset_size.h>
 #include <util/replace_symbol.h>
 #include <util/simplify_expr.h>
 
 #include "flatten_byte_extract_exceptions.h"
-#include "flatten_byte_operators.h"
 
 /// rewrite an object into its individual bytes
 /// \par parameters: src  object to unpack
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index 5bbbad458f2e..d0a2a8669032 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -15,9 +15,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
-#include <util/std_expr.h>
-#include <util/prefix.h>
+#include <util/invariant.h>
 #include <util/pointer_offset_size.h>
+#include <util/prefix.h>
+#include <util/std_expr.h>
 
 bool pointer_logict::is_dynamic_object(const exprt &expr) const
 {
diff --git a/src/util/fresh_symbol.cpp b/src/util/fresh_symbol.cpp
index 0f7c3a9daf29..c77c7e33e47e 100644
--- a/src/util/fresh_symbol.cpp
+++ b/src/util/fresh_symbol.cpp
@@ -13,6 +13,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 
 #include "namespace.h"
 #include "rename.h"
+#include "symbol.h"
+#include "symbol_table_base.h"
 
 /// Installs a fresh-named symbol with the requested name pattern
 /// \par parameters: `type`: type of new symbol
diff --git a/src/util/fresh_symbol.h b/src/util/fresh_symbol.h
index 8cdedc56977f..0d1601ad1805 100644
--- a/src/util/fresh_symbol.h
+++ b/src/util/fresh_symbol.h
@@ -14,10 +14,12 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 
 #include <string>
 
-#include <util/irep.h>
-#include <util/source_location.h>
-#include <util/symbol_table.h>
-#include <util/type.h>
+#include "irep.h"
+
+class source_locationt;
+class symbolt;
+class symbol_table_baset;
+class typet;
 
 symbolt &get_fresh_aux_symbol(
   const typet &type,
diff --git a/src/util/graph.h b/src/util/graph.h
index 85ad33c448d3..6b7fd6e07f72 100644
--- a/src/util/graph.h
+++ b/src/util/graph.h
@@ -12,15 +12,15 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_GRAPH_H
 #define CPROVER_UTIL_GRAPH_H
 
+#include <algorithm>
+#include <cassert>
+#include <functional>
+#include <iosfwd>
 #include <list>
-#include <stack>
 #include <map>
-#include <vector>
-#include <iosfwd>
-#include <cassert>
-#include <algorithm>
 #include <queue>
-#include <functional>
+#include <stack>
+#include <vector>
 
 #include "invariant.h"
 
diff --git a/src/util/invariant_utils.h b/src/util/invariant_utils.h
index d448fedfeb35..3dd9d386418a 100644
--- a/src/util/invariant_utils.h
+++ b/src/util/invariant_utils.h
@@ -10,8 +10,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 #define CPROVER_UTIL_INVARIANT_TYPES_H
 
 #include "invariant.h"
-
-#include <util/irep.h>
+#include "irep.h"
 
 #include <string>
 
diff --git a/src/util/irep.h b/src/util/irep.h
index fbaf0ad5a949..2365989bfaab 100644
--- a/src/util/irep.h
+++ b/src/util/irep.h
@@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <vector>
 #include <string>
-#include <cassert>
-#include <iosfwd>
 
 #include "irep_ids.h"
 
diff --git a/src/util/irep_hash_container.h b/src/util/irep_hash_container.h
index 382130659e03..65342ba99b13 100644
--- a/src/util/irep_hash_container.h
+++ b/src/util/irep_hash_container.h
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_IREP_HASH_CONTAINER_H
 #define CPROVER_UTIL_IREP_HASH_CONTAINER_H
 
-#include <cstdlib>  // for size_t
 #include <vector>
 
 #include "numbering.h"
@@ -22,7 +21,7 @@ class irept;
 class irep_hash_container_baset
 {
 public:
-  size_t number(const irept &irep);
+  std::size_t number(const irept &irep);
 
   explicit irep_hash_container_baset(bool _full):full(_full)
   {
@@ -41,23 +40,23 @@ class irep_hash_container_baset
 
   struct pointer_hasht
   {
-    size_t operator()(const void *p) const
+    std::size_t operator()(const void *p) const
     {
-      return (size_t)p;
+      return (std::size_t)p;
     }
   };
 
-  typedef std::unordered_map<const void *, size_t, pointer_hasht>
+  typedef std::unordered_map<const void *, std::size_t, pointer_hasht>
     ptr_hasht;
   ptr_hasht ptr_hash;
 
   // this is the second level: content
 
-  typedef std::vector<size_t> packedt;
+  typedef std::vector<std::size_t> packedt;
 
   struct vector_hasht
   {
-    size_t operator()(const packedt &p) const;
+    std::size_t operator()(const packedt &p) const;
   };
 
   typedef hash_numbering<packedt, vector_hasht> numberingt;
diff --git a/src/util/json_irep.h b/src/util/json_irep.h
index 6fdc3dfc92d5..6e6fe6b1a55f 100644
--- a/src/util/json_irep.h
+++ b/src/util/json_irep.h
@@ -12,7 +12,7 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com
 #ifndef CPROVER_UTIL_JSON_IREP_H
 #define CPROVER_UTIL_JSON_IREP_H
 
-#include <util/irep.h>
+#include "irep.h"
 
 class jsont;
 class json_objectt;
diff --git a/src/util/json_stream.h b/src/util/json_stream.h
index f27e360c9a3f..cbb4689a5de8 100644
--- a/src/util/json_stream.h
+++ b/src/util/json_stream.h
@@ -9,8 +9,8 @@ Author: Peter Schrammel
 #ifndef CPROVER_UTIL_JSON_STREAM_H
 #define CPROVER_UTIL_JSON_STREAM_H
 
-#include <memory>
 #include <iosfwd>
+#include <memory>
 
 #include "json.h"
 #include "invariant.h"
diff --git a/src/util/nondet_bool.h b/src/util/nondet_bool.h
index af628d3456e5..700b85ec5b09 100644
--- a/src/util/nondet_bool.h
+++ b/src/util/nondet_bool.h
@@ -12,8 +12,8 @@ Author: Chris Smowton, chris@smowton.net
 #ifndef CPROVER_UTIL_NONDET_BOOL_H
 #define CPROVER_UTIL_NONDET_BOOL_H
 
-#include <util/std_types.h>
-#include <util/std_expr.h>
+#include "std_expr.h"
+#include "std_types.h"
 
 /// \par parameters: Desired type (C_bool or plain bool)
 /// \return nondet expr of that type
diff --git a/src/util/nondet_ifthenelse.h b/src/util/nondet_ifthenelse.h
index 664a6bdf1b23..cf1966526ef6 100644
--- a/src/util/nondet_ifthenelse.h
+++ b/src/util/nondet_ifthenelse.h
@@ -12,7 +12,7 @@ Author: Chris Smowton, chris@smowton.net
 #ifndef CPROVER_UTIL_NONDET_IFTHENELSE_H
 #define CPROVER_UTIL_NONDET_IFTHENELSE_H
 
-#include <util/std_code.h>
+#include "std_code.h"
 
 class symbol_tablet;
 class source_locationt;
diff --git a/src/util/numbering.h b/src/util/numbering.h
index f932874695a3..42e18354e219 100644
--- a/src/util/numbering.h
+++ b/src/util/numbering.h
@@ -9,13 +9,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_NUMBERING_H
 #define CPROVER_UTIL_NUMBERING_H
 
-#include <cassert>
 #include <map>
 #include <unordered_map>
 #include <vector>
 
-#include <util/invariant.h>
-#include <util/optional.h>
+#include "invariant.h"
+#include "optional.h"
 
 /// \tparam Map a map from a key type to some numeric type
 template <typename Map>
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index 21dbdbb23f7a..2e315ba242fd 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -11,17 +11,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "pointer_offset_size.h"
 
+#include "arith_tools.h"
 #include "c_types.h"
-#include "expr.h"
 #include "invariant.h"
-#include "arith_tools.h"
-#include "std_types.h"
-#include "std_expr.h"
-#include "expr_util.h"
-#include "simplify_expr.h"
 #include "namespace.h"
-#include "symbol.h"
+#include "simplify_expr.h"
 #include "ssa_expr.h"
+#include "std_expr.h"
 
 member_offset_iterator::member_offset_iterator(
   const struct_typet &_type,
diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp
index 312166f00888..966ebdae021d 100644
--- a/src/util/pointer_predicates.cpp
+++ b/src/util/pointer_predicates.cpp
@@ -11,14 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "pointer_predicates.h"
 
+#include "arith_tools.h"
 #include "c_types.h"
 #include "cprover_prefix.h"
 #include "namespace.h"
-#include "std_expr.h"
-#include "expr_util.h"
-#include "arith_tools.h"
 #include "pointer_offset_size.h"
-#include "config.h"
+#include "std_expr.h"
 #include "symbol.h"
 
 exprt pointer_object(const exprt &p)
diff --git a/src/util/rational.h b/src/util/rational.h
index 809f237c95ae..a043ed0923df 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -10,9 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_RATIONAL_H
 #define CPROVER_UTIL_RATIONAL_H
 
-#include <cassert>
-#include <vector>
-
 #include "mp_arith.h"
 
 class constant_exprt;
diff --git a/src/util/refined_string_type.cpp b/src/util/refined_string_type.cpp
index 818eb9e4391f..91cbc7ff090f 100644
--- a/src/util/refined_string_type.cpp
+++ b/src/util/refined_string_type.cpp
@@ -18,6 +18,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 #include "refined_string_type.h"
 
+#include "std_expr.h"
+
 refined_string_typet::refined_string_typet(
   const typet &index_type, const typet &char_type)
 {
diff --git a/src/util/refined_string_type.h b/src/util/refined_string_type.h
index ecef73288ea5..bc597556b2d9 100644
--- a/src/util/refined_string_type.h
+++ b/src/util/refined_string_type.h
@@ -19,11 +19,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #ifndef CPROVER_UTIL_REFINED_STRING_TYPE_H
 #define CPROVER_UTIL_REFINED_STRING_TYPE_H
 
-#include <util/std_types.h>
-#include <util/std_expr.h>
-#include <util/arith_tools.h>
-#include <util/cprover_prefix.h>
-#include <util/expr_util.h>
+#include "cprover_prefix.h"
+#include "std_types.h"
 
 // Internal type used for string refinement
 class refined_string_typet: public struct_typet
diff --git a/src/util/sharing_map.h b/src/util/sharing_map.h
index a558ec429017..1c8943ae1ac6 100644
--- a/src/util/sharing_map.h
+++ b/src/util/sharing_map.h
@@ -15,17 +15,15 @@ Author: Daniel Poetzl
 #include <string>
 #include <stack>
 #include <vector>
-#include <map>
 #include <stdexcept>
 #include <functional>
 #include <memory>
 #include <iosfwd>
 #include <cassert>
 
-#include <util/string2int.h>
-#include <util/threeval.h>
-#include <util/irep.h>
-#include <util/sharing_node.h>
+#include "irep.h"
+#include "sharing_node.h"
+#include "threeval.h"
 
 #define _sm_assert(b) assert(b)
 //#define _sm_assert(b)
diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h
index 9cec1cd2f3af..2ecebabb4677 100644
--- a/src/util/sharing_node.h
+++ b/src/util/sharing_node.h
@@ -15,7 +15,6 @@ Author: Daniel Poetzl
 #include <list>
 #include <map>
 #include <memory>
-#include <cassert>
 
 #include "invariant.h"
 
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 4a0e2855d290..c2e07be9630f 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -11,29 +11,21 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 #include <algorithm>
 
-#include "c_types.h"
-#include "rational.h"
-#include "simplify_expr_class.h"
-#include "mp_arith.h"
 #include "arith_tools.h"
-#include "replace_expr.h"
-#include "std_types.h"
+#include "base_type.h"
+#include "byte_operators.h"
+#include "c_types.h"
+#include "config.h"
+#include "endianness_map.h"
 #include "expr_util.h"
-#include "std_expr.h"
 #include "fixedbv.h"
+#include "namespace.h"
 #include "pointer_offset_size.h"
+#include "rational.h"
 #include "rational_tools.h"
-#include "config.h"
-#include "base_type.h"
-#include "type_eq.h"
-#include "namespace.h"
-#include "threeval.h"
-#include "pointer_predicates.h"
-#include "prefix.h"
-#include "byte_operators.h"
-#include "bv_arithmetic.h"
-#include "endianness_map.h"
 #include "simplify_utils.h"
+#include "std_expr.h"
+#include "type_eq.h"
 
 // #define DEBUGX
 
@@ -41,6 +33,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 #endif
 
+#include "simplify_expr_class.h"
+
 // #define USE_CACHE
 
 #ifdef USE_CACHE
diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp
index 026cb84105f9..db64a51b2436 100644
--- a/src/util/simplify_expr_array.cpp
+++ b/src/util/simplify_expr_array.cpp
@@ -8,14 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "simplify_expr_class.h"
 
-#include <cassert>
-
-#include "expr.h"
-#include "namespace.h"
-#include "std_expr.h"
-#include "replace_expr.h"
 #include "arith_tools.h"
+#include "namespace.h"
 #include "pointer_offset_size.h"
+#include "replace_expr.h"
+#include "std_expr.h"
 
 bool simplify_exprt::simplify_index(exprt &expr)
 {
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index c225997d2c89..da3c03da4488 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "base_type.h"
 #include "bv_arithmetic.h"
 #include "config.h"
-#include "expr.h"
 #include "expr_util.h"
 #include "fixedbv.h"
 #include "ieee_float.h"
@@ -24,7 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "rational.h"
 #include "rational_tools.h"
 #include "std_expr.h"
-#include "string2int.h"
 
 bool simplify_exprt::simplify_bswap(bswap_exprt &expr)
 {
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index a1e26187897c..fff9ba57f521 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -10,17 +10,15 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cassert>
 
-#include "c_types.h"
-#include "expr.h"
-#include "namespace.h"
-#include "std_expr.h"
-#include "pointer_offset_size.h"
 #include "arith_tools.h"
+#include "c_types.h"
 #include "config.h"
 #include "expr_util.h"
-#include "threeval.h"
-#include "prefix.h"
+#include "namespace.h"
+#include "pointer_offset_size.h"
 #include "pointer_predicates.h"
+#include "std_expr.h"
+#include "threeval.h"
 
 static bool is_dereference_integer_object(
   const exprt &expr,
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index e6195f2cb544..331d04c3001f 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -8,15 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "simplify_expr_class.h"
 
-#include <cassert>
-
+#include "arith_tools.h"
+#include "base_type.h"
 #include "byte_operators.h"
-#include "expr.h"
 #include "namespace.h"
-#include "std_expr.h"
 #include "pointer_offset_size.h"
-#include "arith_tools.h"
-#include "base_type.h"
+#include "std_expr.h"
 
 bool simplify_exprt::simplify_member(exprt &expr)
 {
diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h
index 63e6dfaf7d7c..3a0e3b151d6b 100644
--- a/src/util/ssa_expr.h
+++ b/src/util/ssa_expr.h
@@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_SSA_EXPR_H
 #define CPROVER_UTIL_SSA_EXPR_H
 
-#include <util/std_expr.h>
+#include "std_expr.h"
 
 /*! \brief Expression providing an SSA-renamed symbol of expressions
 */
diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp
index 445c31c3c278..431ca3875305 100644
--- a/src/util/std_expr.cpp
+++ b/src/util/std_expr.cpp
@@ -13,9 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "arith_tools.h"
 #include "byte_operators.h"
 #include "c_types.h"
-#include "namespace.h"
 #include "pointer_offset_size.h"
-#include "std_types.h"
 
 bool constant_exprt::value_is_zero_string() const
 {
diff --git a/src/util/string_expr.h b/src/util/string_expr.h
index c9d54470d3b7..dd44684140ff 100644
--- a/src/util/string_expr.h
+++ b/src/util/string_expr.h
@@ -12,9 +12,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #ifndef CPROVER_UTIL_STRING_EXPR_H
 #define CPROVER_UTIL_STRING_EXPR_H
 
-#include <util/std_expr.h>
-#include <util/arith_tools.h>
-#include <util/refined_string_type.h>
+#include "arith_tools.h"
+#include "refined_string_type.h"
+#include "std_expr.h"
 
 // Given an representation of strings as exprt that implements `length` and
 // `content` this provides additional useful methods.
diff --git a/src/util/symbol_table_base.h b/src/util/symbol_table_base.h
index 62db57c024cc..6a51a34a8639 100644
--- a/src/util/symbol_table_base.h
+++ b/src/util/symbol_table_base.h
@@ -6,13 +6,9 @@
 #ifndef CPROVER_UTIL_SYMBOL_TABLE_BASE_H
 #define CPROVER_UTIL_SYMBOL_TABLE_BASE_H
 
-#include <functional>
-#include <iosfwd>
 #include <map>
 #include <unordered_map>
 
-#include <util/optional.h>
-
 #include "symbol.h"
 
 typedef std::multimap<irep_idt, irep_idt> symbol_base_mapt;
diff --git a/src/util/union_find_replace.h b/src/util/union_find_replace.h
index 37f86604f1bd..b7630db11edf 100644
--- a/src/util/union_find_replace.h
+++ b/src/util/union_find_replace.h
@@ -9,7 +9,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #ifndef CPROVER_UTIL_UNION_FIND_REPLACE_H
 #define CPROVER_UTIL_UNION_FIND_REPLACE_H
 
-#include <util/replace_expr.h>
+#include "replace_expr.h"
 
 /// Similar interface to union-find for expressions, with a function for
 /// replacing sub-expressions by their result for find.