diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h
index b1ad279fa36..fdd6f26697e 100644
--- a/src/ansi-c/ansi_c_convert_type.h
+++ b/src/ansi-c/ansi_c_convert_type.h
@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
 #define CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
 
+#include <list>
+
 #include <util/message.h>
 
 #include "c_qualifiers.h"
diff --git a/src/assembler/assembler_parser.cpp b/src/assembler/assembler_parser.cpp
index 1ad30f95680..10200644d1d 100644
--- a/src/assembler/assembler_parser.cpp
+++ b/src/assembler/assembler_parser.cpp
@@ -8,8 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "assembler_parser.h"
 
-#include <iostream>
-
 assembler_parsert assembler_parser;
 
 extern char *yyassemblertext;
diff --git a/src/assembler/assembler_parser.h b/src/assembler/assembler_parser.h
index 4d3a160da25..76f03c71aaf 100644
--- a/src/assembler/assembler_parser.h
+++ b/src/assembler/assembler_parser.h
@@ -11,7 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_ASSEMBLER_ASSEMBLER_PARSER_H
 
 #include <util/parser.h>
-#include <util/expr.h>
+
+#include <list>
 
 int yyassemblerlex();
 int yyassemblererror(const std::string &error);
diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
index 632de57a779..f18f7044dc4 100644
--- a/src/cbmc/all_properties.cpp
+++ b/src/cbmc/all_properties.cpp
@@ -20,8 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/xml.h>
 #include <util/json.h>
 
+#include <solvers/prop/prop_conv.h>
 #include <solvers/sat/satcheck.h>
-#include <solvers/prop/literal_expr.h>
 
 #include <goto-symex/build_goto_trace.h>
 #include <goto-programs/xml_goto_trace.h>
diff --git a/src/cbmc/all_properties_class.h b/src/cbmc/all_properties_class.h
index 215ad4d3655..293babda092 100644
--- a/src/cbmc/all_properties_class.h
+++ b/src/cbmc/all_properties_class.h
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_CBMC_ALL_PROPERTIES_CLASS_H
 
 #include <solvers/prop/cover_goals.h>
+#include <solvers/prop/literal_expr.h>
 
 #include "bmc.h"
 
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
index 143fd922acd..98552f8ca73 100644
--- a/src/cbmc/bmc_cover.cpp
+++ b/src/cbmc/bmc_cover.cpp
@@ -21,7 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/xml_irep.h>
 
 #include <solvers/prop/cover_goals.h>
-#include <solvers/prop/literal_expr.h>
+#include <solvers/prop/prop_conv.h>
 
 #include <goto-symex/build_goto_trace.h>
 
diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h
index ac77594de36..ba7c3e3da33 100644
--- a/src/solvers/flattening/arrays.h
+++ b/src/solvers/flattening/arrays.h
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_FLATTENING_ARRAYS_H
 #define CPROVER_SOLVERS_FLATTENING_ARRAYS_H
 
+#include <list>
 #include <set>
 
 #include <util/union_find.h>
diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp
index aaf494169ed..0aa57c0b96a 100644
--- a/src/solvers/prop/cover_goals.cpp
+++ b/src/solvers/prop/cover_goals.cpp
@@ -11,9 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "cover_goals.h"
 
-#include <util/threeval.h>
-
 #include "literal_expr.h"
+#include "prop_conv.h"
 
 cover_goalst::~cover_goalst()
 {
diff --git a/src/solvers/prop/cover_goals.h b/src/solvers/prop/cover_goals.h
index 025e7b128f6..825b6366184 100644
--- a/src/solvers/prop/cover_goals.h
+++ b/src/solvers/prop/cover_goals.h
@@ -12,9 +12,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_PROP_COVER_GOALS_H
 #define CPROVER_SOLVERS_PROP_COVER_GOALS_H
 
+#include <list>
+
+#include <util/decision_procedure.h>
 #include <util/message.h>
 
-#include "prop_conv.h"
+#include "literal.h"
+
+class prop_convt;
 
 /// Try to cover some given set of goals incrementally. This can be seen as a
 /// heuristic variant of SAT-based set-cover. No minimality guarantee.
diff --git a/src/util/expr.h b/src/util/expr.h
index aeeb682dec8..9263be13a08 100644
--- a/src/util/expr.h
+++ b/src/util/expr.h
@@ -15,9 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "validate_types.h"
 #include "validation_mode.h"
 
-#include <functional>
-#include <list>
-
 #define forall_operands(it, expr) \
   if((expr).has_operands()) /* NOLINT(readability/braces) */ \
     for(exprt::operandst::const_iterator it=(expr).operands().begin(), \