diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 63bfaa3fff0..5f1ff633ed2 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -9,10 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// ANSI-C Language Type Checking
 
-#include "c_typecheck_base.h"
-
-#include <sstream>
-
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/c_types.h>
@@ -39,10 +35,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "builtin_factory.h"
 #include "c_expr.h"
 #include "c_qualifiers.h"
+#include "c_typecheck_base.h"
 #include "expr2c.h"
 #include "padding.h"
 #include "type2name.h"
 
+#include <cassert>
+#include <sstream>
+
 void c_typecheck_baset::typecheck_expr(exprt &expr)
 {
   if(expr.id()==ID_already_typechecked)
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index a1af1242dc2..98f5e4ce5a5 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -23,6 +23,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "c_typecheck_base.h"
 #include "type2name.h"
 
+#include <cassert>
+
 void c_typecheck_baset::do_initializer(
   exprt &initializer,
   const typet &type,
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 26bf7d194f0..90b5a84040c 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -9,12 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// C++ Language Type Checking
 
-#include "c_typecheck_base.h"
-
-#include <unordered_set>
-
-#include <goto-programs/goto_instruction_code.h>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
@@ -24,14 +18,20 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include "ansi_c_convert_type.h"
 #include "ansi_c_declaration.h"
 #include "c_qualifiers.h"
+#include "c_typecheck_base.h"
 #include "gcc_types.h"
 #include "padding.h"
 #include "type2name.h"
 #include "typedef_type.h"
 
+#include <cassert>
+#include <unordered_set>
+
 void c_typecheck_baset::typecheck_type(typet &type)
 {
   // we first convert, and then check
diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp
index d133283b1c0..99369d9879d 100644
--- a/src/cpp/cpp_instantiate_template.cpp
+++ b/src/cpp/cpp_instantiate_template.cpp
@@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_type2name.h"
 
+#include <cassert>
+
 std::string cpp_typecheckt::template_suffix(
   const cpp_template_args_tct &template_args)
 {
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
index 7687c1303ac..e697ed82eae 100644
--- a/src/cpp/cpp_typecheck.cpp
+++ b/src/cpp/cpp_typecheck.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_typecheck.h"
 
-#include <algorithm>
-
 #include <util/pointer_expr.h>
 #include <util/source_location.h>
 #include <util/symbol.h>
@@ -23,6 +21,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include "cpp_util.h"
 #include "expr2cpp.h"
 
+#include <algorithm>
+#include <cassert>
+
 void cpp_typecheckt::convert(cpp_itemt &item)
 {
   if(item.is_declaration())
diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp
index 15e4e32a0e2..d43aa0f3998 100644
--- a/src/cpp/cpp_typecheck_code.cpp
+++ b/src/cpp/cpp_typecheck_code.cpp
@@ -9,8 +9,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 /// \file
 /// C++ Language Type Checking
 
-#include "cpp_typecheck.h"
-
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/pointer_expr.h>
@@ -18,9 +16,12 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_declarator_converter.h"
 #include "cpp_exception_id.h"
+#include "cpp_typecheck.h"
 #include "cpp_typecheck_fargs.h"
 #include "cpp_util.h"
 
+#include <cassert>
+
 void cpp_typecheckt::typecheck_code(codet &code)
 {
   const irep_idt &statement=code.get_statement();
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
index 193f1515dfc..c450f223b57 100644
--- a/src/cpp/cpp_typecheck_compound_type.cpp
+++ b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -15,11 +15,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <iostream>
 #endif
 
-#include <algorithm>
-
 #include <util/arith_tools.h>
-#include <util/std_types.h>
 #include <util/c_types.h>
+#include <util/std_types.h>
 
 #include <ansi-c/c_qualifiers.h>
 
@@ -28,6 +26,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include "cpp_type2name.h"
 #include "cpp_util.h"
 
+#include <algorithm>
+#include <cassert>
+
 bool cpp_typecheckt::has_const(const typet &type)
 {
   if(type.id()==ID_const)
diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp
index 2879af7662c..056fa4e64db 100644
--- a/src/cpp/cpp_typecheck_constructor.cpp
+++ b/src/cpp/cpp_typecheck_constructor.cpp
@@ -9,15 +9,17 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 /// \file
 /// C++ Language Type Checking
 
-#include "cpp_typecheck.h"
-
-#include <goto-programs/goto_instruction_code.h>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
 
+#include <goto-programs/goto_instruction_code.h>
+
+#include "cpp_typecheck.h"
+
+#include <cassert>
+
 /// Generate code to copy the parent.
 /// \param source_location: location for generated code
 /// \param parent_base_name: base name of typechecked parent
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
index 607f02ee78b..5805b4eb525 100644
--- a/src/cpp/cpp_typecheck_conversions.cpp
+++ b/src/cpp/cpp_typecheck_conversions.cpp
@@ -9,8 +9,6 @@ Module: C++ Language Type Checking
 /// \file
 /// C++ Language Type Checking
 
-#include "cpp_typecheck.h"
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
@@ -21,8 +19,11 @@ Module: C++ Language Type Checking
 
 #include <ansi-c/c_qualifiers.h>
 
+#include "cpp_typecheck.h"
 #include "cpp_util.h"
 
+#include <cassert>
+
 /// Lvalue-to-rvalue conversion
 ///
 ///  An lvalue (3.10) of a non-function, non-array type T can be
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 10d112a0508..52c46ad5c71 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -31,6 +31,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include "cpp_util.h"
 #include "expr2cpp.h"
 
+#include <cassert>
+
 bool cpp_typecheckt::find_parent(
   const symbolt &symb,
   const irep_idt &base_name,
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
index de26dd0dc78..cff8508a18e 100644
--- a/src/cpp/cpp_typecheck_resolve.cpp
+++ b/src/cpp/cpp_typecheck_resolve.cpp
@@ -15,8 +15,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <iostream>
 #endif
 
-#include <algorithm>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/mathematical_types.h>
@@ -34,6 +32,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include "cpp_typecheck_fargs.h"
 #include "cpp_util.h"
 
+#include <algorithm>
+#include <cassert>
+
 cpp_typecheck_resolvet::cpp_typecheck_resolvet(cpp_typecheckt &_cpp_typecheck):
   cpp_typecheck(_cpp_typecheck),
   original_scope(nullptr) // set in resolve_scope()
diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp
index c454a649920..9b0417d8a91 100644
--- a/src/cpp/cpp_typecheck_template.cpp
+++ b/src/cpp/cpp_typecheck_template.cpp
@@ -9,16 +9,17 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 /// \file
 /// C++ Language Type Checking
 
-#include "cpp_typecheck.h"
-
 #include <util/base_exceptions.h>
 #include <util/simplify_expr.h>
 
-#include "cpp_type2name.h"
-#include "cpp_declarator_converter.h"
-#include "cpp_template_type.h"
 #include "cpp_convert_type.h"
+#include "cpp_declarator_converter.h"
 #include "cpp_template_args.h"
+#include "cpp_template_type.h"
+#include "cpp_type2name.h"
+#include "cpp_typecheck.h"
+
+#include <cassert>
 
 void cpp_typecheckt::salvage_default_arguments(
   const template_typet &old_type,
diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp
index 83bd51f609f..b39f2be0236 100644
--- a/src/cpp/cpp_typecheck_type.cpp
+++ b/src/cpp/cpp_typecheck_type.cpp
@@ -9,17 +9,18 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 /// \file
 /// C++ Language Type Checking
 
-#include "cpp_typecheck.h"
-
-#include <util/source_location.h>
-#include <util/simplify_expr.h>
 #include <util/c_types.h>
+#include <util/simplify_expr.h>
+#include <util/source_location.h>
 
 #include <ansi-c/c_qualifiers.h>
 
 #include "cpp_convert_type.h"
+#include "cpp_typecheck.h"
 #include "cpp_typecheck_fargs.h"
 
+#include <cassert>
+
 void cpp_typecheckt::typecheck_type(typet &type)
 {
   assert(!type.id().empty());
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index f6728ed6763..a7770dfc794 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -9,19 +9,19 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 /// \file
 /// C++ Language Parsing
 
-#include "cpp_parser.h"
-
-#include <map>
-
 #include <util/c_types.h>
 #include <util/std_code.h>
 
 #include <ansi-c/ansi_c_y.tab.h>
 #include <ansi-c/merged_type.h>
 
-#include "cpp_token_buffer.h"
-#include "cpp_member_spec.h"
 #include "cpp_enum_type.h"
+#include "cpp_member_spec.h"
+#include "cpp_parser.h"
+#include "cpp_token_buffer.h"
+
+#include <cassert>
+#include <map>
 
 #ifdef DEBUG
 #include <iostream>
diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp
index cdf9eb7f1c8..8b9e38d4c1a 100644
--- a/src/goto-diff/change_impact.cpp
+++ b/src/goto-diff/change_impact.cpp
@@ -13,14 +13,15 @@ Date: April 2016
 
 #include "change_impact.h"
 
-#include <iostream>
-
 #include <goto-programs/goto_model.h>
 
 #include <analyses/dependence_graph.h>
 
 #include "unified_diff.h"
 
+#include <cassert>
+#include <iostream>
+
 #if 0
   struct cfg_nodet
   {
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index 2bd751e2480..6681f2f8c57 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_program2code.h"
 
-#include <sstream>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_util.h>
@@ -21,6 +19,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
 
+#include <cassert>
+#include <sstream>
+
 void goto_program2codet::operator()()
 {
   // labels stored for cleanup
diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-instrument/k_induction.cpp
index 5ed91b4317e..fae1ab4be8c 100644
--- a/src/goto-instrument/k_induction.cpp
+++ b/src/goto-instrument/k_induction.cpp
@@ -11,15 +11,17 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "k_induction.h"
 
-#include <analyses/natural_loops.h>
-#include <analyses/local_may_alias.h>
-
 #include <goto-programs/remove_skip.h>
 
+#include <analyses/local_may_alias.h>
+#include <analyses/natural_loops.h>
+
 #include "havoc_utils.h"
 #include "loop_utils.h"
 #include "unwind.h"
 
+#include <cassert>
+
 class k_inductiont
 {
 public:
diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp
index dcfca5417d6..4fd02f1e609 100644
--- a/src/goto-instrument/unwind.cpp
+++ b/src/goto-instrument/unwind.cpp
@@ -23,6 +23,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "unwindset.h"
 
+#include <cassert>
+
 void goto_unwindt::copy_segment(
   const goto_programt::const_targett start,
   const goto_programt::const_targett end, // exclusive
diff --git a/src/goto-instrument/wmm/cycle_collection.cpp b/src/goto-instrument/wmm/cycle_collection.cpp
index a36ac99b851..1ace99775b2 100644
--- a/src/goto-instrument/wmm/cycle_collection.cpp
+++ b/src/goto-instrument/wmm/cycle_collection.cpp
@@ -11,9 +11,11 @@ Date: 2012
 /// \file
 /// collection of cycles in graph of abstract events
 
+#include <util/message.h>
+
 #include "event_graph.h"
 
-#include <util/message.h>
+#include <cassert>
 
 /// after the collection, eliminates the executions forbidden by an indirect
 /// thin-air
diff --git a/src/goto-instrument/wmm/event_graph.cpp b/src/goto-instrument/wmm/event_graph.cpp
index 95e2a3712ba..4142d1a3dc6 100644
--- a/src/goto-instrument/wmm/event_graph.cpp
+++ b/src/goto-instrument/wmm/event_graph.cpp
@@ -15,6 +15,7 @@ Date: 2012
 
 #include <util/message.h>
 
+#include <cassert>
 #include <fstream>
 
 
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
index 19e941cf308..b08e03d361e 100644
--- a/src/goto-instrument/wmm/goto2graph.cpp
+++ b/src/goto-instrument/wmm/goto2graph.cpp
@@ -13,19 +13,19 @@ Date: 2012
 
 #include "goto2graph.h"
 
-#include <vector>
-#include <string>
-#include <fstream>
-
 #include <util/options.h>
 #include <util/prefix.h>
 
-#include <linking/static_lifetime_init.h>
-
 #include <goto-instrument/rw_set.h>
+#include <linking/static_lifetime_init.h>
 
 #include "fence.h"
 
+#include <cassert>
+#include <fstream>
+#include <string>
+#include <vector>
+
 // #define PRINT_UNSAFES