diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp
index 70ccae582c8..39306b2ad7a 100644
--- a/src/goto-checker/multi_path_symex_checker.cpp
+++ b/src/goto-checker/multi_path_symex_checker.cpp
@@ -15,7 +15,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <util/ui_message.h>
 
-#include <solvers/hardness_collector.h>
+#include <goto-symex/solver_hardness.h>
 
 #include "bmc_util.h"
 #include "counterexample_beautification.h"
diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
index 77a18d124dc..df47f425c74 100644
--- a/src/goto-checker/solver_factory.cpp
+++ b/src/goto-checker/solver_factory.cpp
@@ -36,6 +36,8 @@ Author: Daniel Kroening, Peter Schrammel
 #include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/strings/string_refinement.h>
 
+#include <goto-symex/solver_hardness.h>
+
 solver_factoryt::solver_factoryt(
   const optionst &_options,
   const namespacet &_ns,
@@ -190,11 +192,10 @@ make_satcheck_prop(message_handlert &message_handler, const optionst &options)
     if(
       auto hardness_collector = dynamic_cast<hardness_collectort *>(&*satcheck))
     {
-      hardness_collector->enable_hardness_collection();
-      hardness_collector->with_solver_hardness(
-        [&options](solver_hardnesst &hardness) {
-          hardness.set_outfile(options.get_option("write-solver-stats-to"));
-        });
+      std::unique_ptr<solver_hardnesst> solver_hardness =
+        util_make_unique<solver_hardnesst>();
+      solver_hardness->set_outfile(options.get_option("write-solver-stats-to"));
+      hardness_collector->solver_hardness = std::move(solver_hardness);
     }
     else
     {
diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile
index 0047bc9acd9..232ca74dacb 100644
--- a/src/goto-symex/Makefile
+++ b/src/goto-symex/Makefile
@@ -17,6 +17,7 @@ SRC = auto_objects.cpp \
       show_program.cpp \
       show_vcc.cpp \
       slice.cpp \
+      solver_hardness.cpp \
       ssa_step.cpp \
       symex_assign.cpp \
       symex_atomic_section.cpp \
diff --git a/src/solvers/solver_hardness.cpp b/src/goto-symex/solver_hardness.cpp
similarity index 100%
rename from src/solvers/solver_hardness.cpp
rename to src/goto-symex/solver_hardness.cpp
diff --git a/src/solvers/solver_hardness.h b/src/goto-symex/solver_hardness.h
similarity index 87%
rename from src/solvers/solver_hardness.h
rename to src/goto-symex/solver_hardness.h
index d1aeabff778..3b80855dcd0 100644
--- a/src/solvers/solver_hardness.h
+++ b/src/goto-symex/solver_hardness.h
@@ -9,7 +9,8 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_SOLVERS_SOLVER_HARDNESS_H
 #define CPROVER_SOLVERS_SOLVER_HARDNESS_H
 
-#include <solvers/prop/literal.h>
+#include <solvers/hardness_collector.h>
+#include <solvers/prop/prop_conv_solver.h>
 
 #include <fstream>
 #include <string>
@@ -38,7 +39,7 @@ Author: Diffblue Ltd.
 /// derived class of \ref cnft for SAT solving). For this purpose the object
 /// lives in the \ref solver_factoryt::solvert and pointers are passed to both
 /// \ref decision_proceduret and \ref propt.
-struct solver_hardnesst
+struct solver_hardnesst : public clause_hardness_collectort
 {
   // From SAT solver we collect the number of clauses, the number of literals
   // and the number of distinct variables that were used in all clauses.
@@ -160,4 +161,26 @@ struct hash<solver_hardnesst::hardness_ssa_keyt>
 };
 } // namespace std
 
+static inline void with_solver_hardness(
+  decision_proceduret &maybe_hardness_collector,
+  std::function<void(solver_hardnesst &hardness)> handler)
+{
+  // FIXME I am wondering if there is a way to do this that is a bit less
+  // dynamically typed.
+  if(
+    auto prop_conv_solver =
+      dynamic_cast<prop_conv_solvert *>(&maybe_hardness_collector))
+  {
+    if(auto hardness_collector = prop_conv_solver->get_hardness_collector())
+    {
+      if(hardness_collector->solver_hardness)
+      {
+        auto &solver_hardness = static_cast<solver_hardnesst &>(
+          *(hardness_collector->solver_hardness));
+        handler(solver_hardness);
+      }
+    }
+  }
+}
+
 #endif // CPROVER_SOLVERS_SOLVER_HARDNESS_H
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 33927026753..02afd8fead1 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -16,12 +16,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_expr.h>
 
-#include <solvers/decision_procedure.h>
-#include <solvers/hardness_collector.h>
-
+#include "solver_hardness.h"
 #include "ssa_step.h"
 
-static hardness_collectort::handlert
+static std::function<void(solver_hardnesst &)>
 hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
 {
   return [step_index, &step](solver_hardnesst &hardness) {
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index 096fb56f4eb..32df4e0e92c 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -80,7 +80,6 @@ SRC = $(BOOLEFORCE_SRC) \
       $(SQUOLEM2_SRC) \
       $(CADICAL_SRC) \
       decision_procedure.cpp \
-      solver_hardness.cpp \
       flattening/arrays.cpp \
       flattening/boolbv.cpp \
       flattening/boolbv_abs.cpp \
diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h
index a7ee9096269..6641463de82 100644
--- a/src/solvers/flattening/arrays.h
+++ b/src/solvers/flattening/arrays.h
@@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "equality.h"
 
+class array_comprehension_exprt;
+class array_exprt;
 class array_of_exprt;
 class equal_exprt;
 class if_exprt;
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index 58b84da58ee..b023b026229 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/src/solvers/flattening/boolbv.h
@@ -37,6 +37,7 @@ class floatbv_typecast_exprt;
 class ieee_float_op_exprt;
 class member_exprt;
 class replication_exprt;
+class union_typet;
 
 class boolbvt:public arrayst
 {
diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp
index a4471aad3ef..9bbea947c78 100644
--- a/src/solvers/flattening/boolbv_get.cpp
+++ b/src/solvers/flattening/boolbv_get.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/namespace.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/threeval.h>
diff --git a/src/solvers/flattening/boolbv_member.cpp b/src/solvers/flattening/boolbv_member.cpp
index 3e4cd250585..18087ea0180 100644
--- a/src/solvers/flattening/boolbv_member.cpp
+++ b/src/solvers/flattening/boolbv_member.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "boolbv.h"
 
 #include <util/c_types.h>
+#include <util/namespace.h>
 
 static bvt convert_member_struct(
   const member_exprt &expr,
diff --git a/src/solvers/flattening/boolbv_struct.cpp b/src/solvers/flattening/boolbv_struct.cpp
index fc9222d1755..9b49a69eb09 100644
--- a/src/solvers/flattening/boolbv_struct.cpp
+++ b/src/solvers/flattening/boolbv_struct.cpp
@@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
+#include <util/namespace.h>
+
 bvt boolbvt::convert_struct(const struct_exprt &expr)
 {
   const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp
index 2fd21de7dfd..e8346ff3a12 100644
--- a/src/solvers/flattening/boolbv_typecast.cpp
+++ b/src/solvers/flattening/boolbv_typecast.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/bitvector_types.h>
 #include <util/c_types.h>
+#include <util/namespace.h>
 
 #include <solvers/floatbv/float_utils.h>
 
diff --git a/src/solvers/flattening/boolbv_update.cpp b/src/solvers/flattening/boolbv_update.cpp
index 058541e3adb..e8b0b40c57a 100644
--- a/src/solvers/flattening/boolbv_update.cpp
+++ b/src/solvers/flattening/boolbv_update.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/namespace.h>
 
 bvt boolbvt::convert_update(const update_exprt &expr)
 {
diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp
index 524b4b949e8..6743fa114bb 100644
--- a/src/solvers/flattening/boolbv_with.cpp
+++ b/src/solvers/flattening/boolbv_with.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/namespace.h>
 #include <util/std_expr.h>
 
 bvt boolbvt::convert_with(const with_exprt &expr)
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index cd0235eba75..01012b56255 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/exception_utils.h>
+#include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
diff --git a/src/solvers/hardness_collector.h b/src/solvers/hardness_collector.h
index 458cd33e17c..88a9e8e0087 100644
--- a/src/solvers/hardness_collector.h
+++ b/src/solvers/hardness_collector.h
@@ -14,32 +14,37 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_SOLVERS_HARDNESS_COLLECTOR_H
 #define CPROVER_SOLVERS_HARDNESS_COLLECTOR_H
 
-#include <functional>
-#include <solvers/solver_hardness.h>
+#include <solvers/prop/literal.h>
 
-class exprt;
+#include <memory>
 
-class hardness_collectort
+struct solver_hardnesst;
+
+class clause_hardness_collectort
 {
 public:
-  using handlert = std::function<void(solver_hardnesst &)>;
-  virtual void with_solver_hardness(handlert handler) = 0;
-  virtual void enable_hardness_collection() = 0;
-  virtual ~hardness_collectort() = default;
+  /// Called e.g. from the `satcheck_minisat2::lcnf`, this function adds the
+  ///   complexity statistics from the last SAT query to the `current_ssa_key`.
+  /// \param bv: the clause (vector of literals)
+  /// \param cnf: processed clause
+  /// \param cnf_clause_index: index of clause in dimacs output
+  /// \param register_cnf: negation of boolean variable tracking if the clause
+  /// can be eliminated
+  virtual void register_clause(
+    const bvt &bv,
+    const bvt &cnf,
+    const size_t cnf_clause_index,
+    bool register_cnf) = 0;
+
+  virtual ~clause_hardness_collectort()
+  {
+  }
 };
 
-template <typename T>
-void with_solver_hardness(
-  T &maybe_hardness_collector,
-  hardness_collectort::handlert handler)
+class hardness_collectort
 {
-  // FIXME I am wondering if there is a way to do this that is a bit less
-  // dynamically typed.
-  if(
-    auto hardness_collector =
-      dynamic_cast<hardness_collectort *>(&maybe_hardness_collector))
-  {
-    hardness_collector->with_solver_hardness(handler);
-  }
-}
+public:
+  std::unique_ptr<clause_hardness_collectort> solver_hardness;
+};
+
 #endif // CPROVER_SOLVERS_HARDNESS_COLLECTOR_H
diff --git a/src/solvers/module_dependencies.txt b/src/solvers/module_dependencies.txt
index 1352338989e..05a6bc0865a 100644
--- a/src/solvers/module_dependencies.txt
+++ b/src/solvers/module_dependencies.txt
@@ -1,5 +1,4 @@
 cplusplus # cudd
 cudd
-goto-programs
 solvers
 util
diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
index f9bcb0bd4de..14daf8d5540 100644
--- a/src/solvers/prop/prop_conv_solver.cpp
+++ b/src/solvers/prop/prop_conv_solver.cpp
@@ -559,16 +559,3 @@ std::string prop_conv_solvert::decision_procedure_text() const
 {
   return "propositional reduction";
 }
-
-void prop_conv_solvert::with_solver_hardness(
-  hardness_collectort::handlert handler)
-{
-  ::with_solver_hardness(prop, handler);
-}
-void prop_conv_solvert::enable_hardness_collection()
-{
-  if(auto hardness_collector = dynamic_cast<hardness_collectort *>(&prop))
-  {
-    hardness_collector->enable_hardness_collection();
-  }
-}
diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h
index 995ec6cdad7..3bbccf239ec 100644
--- a/src/solvers/prop/prop_conv_solver.h
+++ b/src/solvers/prop/prop_conv_solver.h
@@ -22,10 +22,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "prop_conv.h"
 #include "solver_resource_limits.h"
 
+class equal_exprt;
+
 class prop_conv_solvert : public conflict_providert,
                           public prop_convt,
-                          public solver_resource_limitst,
-                          public hardness_collectort
+                          public solver_resource_limitst
 {
 public:
   prop_conv_solvert(propt &_prop, message_handlert &message_handler)
@@ -95,8 +96,10 @@ class prop_conv_solvert : public conflict_providert,
 
   std::size_t get_number_of_solver_calls() const override;
 
-  void with_solver_hardness(handlert handler) override;
-  void enable_hardness_collection() override;
+  hardness_collectort *get_hardness_collector()
+  {
+    return dynamic_cast<hardness_collectort *>(&prop);
+  }
 
 protected:
   virtual void post_process();
diff --git a/src/solvers/sat/satcheck_cadical.cpp b/src/solvers/sat/satcheck_cadical.cpp
index 4b28f43bdea..567f03aeb3f 100644
--- a/src/solvers/sat/satcheck_cadical.cpp
+++ b/src/solvers/sat/satcheck_cadical.cpp
@@ -63,7 +63,8 @@ void satcheck_cadicalt::lcnf(const bvt &bv)
   }
   solver->add(0); // terminate clause
 
-  with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
+  if(solver_hardness)
+  {
     // To map clauses to lines of program code, track clause indices in the
     // dimacs cnf output. Dimacs output is generated after processing
     // clauses to remove duplicates and clauses that are trivially true.
@@ -77,8 +78,9 @@ void satcheck_cadicalt::lcnf(const bvt &bv)
     if(!clause_removed)
       cnf_clause_index++;
 
-    hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
-  });
+    solver_hardness->register_clause(
+      bv, cnf, cnf_clause_index, !clause_removed);
+  }
 
   clause_counter++;
 }
diff --git a/src/solvers/sat/satcheck_cadical.h b/src/solvers/sat/satcheck_cadical.h
index 02728ef183f..83e957a8a2e 100644
--- a/src/solvers/sat/satcheck_cadical.h
+++ b/src/solvers/sat/satcheck_cadical.h
@@ -42,20 +42,6 @@ class satcheck_cadicalt : public cnf_solvert, public hardness_collectort
   }
   bool is_in_conflict(literalt a) const override;
 
-  void
-  with_solver_hardness(std::function<void(solver_hardnesst &)> handler) override
-  {
-    if(solver_hardness.has_value())
-    {
-      handler(solver_hardness.value());
-    }
-  }
-
-  void enable_hardness_collection() override
-  {
-    solver_hardness = solver_hardnesst{};
-  }
-
 protected:
   resultt do_prop_solve() override;
 
@@ -63,8 +49,6 @@ class satcheck_cadicalt : public cnf_solvert, public hardness_collectort
   CaDiCaL::Solver * solver;
 
   bvt assumptions;
-
-  optionalt<solver_hardnesst> solver_hardness;
 };
 
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H
diff --git a/src/solvers/sat/satcheck_glucose.cpp b/src/solvers/sat/satcheck_glucose.cpp
index 90efb0074d5..7547f372421 100644
--- a/src/solvers/sat/satcheck_glucose.cpp
+++ b/src/solvers/sat/satcheck_glucose.cpp
@@ -123,7 +123,8 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
 
     solver->addClause_(c);
 
-    with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
+    if(solver_hardness)
+    {
       // To map clauses to lines of program code, track clause indices in the
       // dimacs cnf output. Dimacs output is generated after processing
       // clauses to remove duplicates and clauses that are trivially true.
@@ -137,8 +138,9 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
       if(!clause_removed)
         cnf_clause_index++;
 
-      hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
-    });
+      solver_hardness->register_clause(
+        bv, cnf, cnf_clause_index, !clause_removed);
+    }
 
     clause_counter++;
   }
diff --git a/src/solvers/sat/satcheck_glucose.h b/src/solvers/sat/satcheck_glucose.h
index a8e627ab344..ada40c034b9 100644
--- a/src/solvers/sat/satcheck_glucose.h
+++ b/src/solvers/sat/satcheck_glucose.h
@@ -57,20 +57,6 @@ class satcheck_glucose_baset : public cnf_solvert, public hardness_collectort
     return true;
   }
 
-  void
-  with_solver_hardness(std::function<void(solver_hardnesst &)> handler) override
-  {
-    if(solver_hardness.has_value())
-    {
-      handler(solver_hardness.value());
-    }
-  }
-
-  void enable_hardness_collection() override
-  {
-    solver_hardness = solver_hardnesst{};
-  }
-
 protected:
   resultt do_prop_solve() override;
 
@@ -78,8 +64,6 @@ class satcheck_glucose_baset : public cnf_solvert, public hardness_collectort
 
   void add_variables();
   bvt assumptions;
-
-  optionalt<solver_hardnesst> solver_hardness;
 };
 
 class satcheck_glucose_no_simplifiert:
diff --git a/src/solvers/sat/satcheck_ipasir.cpp b/src/solvers/sat/satcheck_ipasir.cpp
index a75e0489e88..d0eee8a04f3 100644
--- a/src/solvers/sat/satcheck_ipasir.cpp
+++ b/src/solvers/sat/satcheck_ipasir.cpp
@@ -88,7 +88,8 @@ void satcheck_ipasirt::lcnf(const bvt &bv)
   }
   ipasir_add(solver, 0); // terminate clause
 
-  with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
+  if(solver_hardness)
+  {
     // To map clauses to lines of program code, track clause indices in the
     // dimacs cnf output. Dimacs output is generated after processing
     // clauses to remove duplicates and clauses that are trivially true.
@@ -102,8 +103,9 @@ void satcheck_ipasirt::lcnf(const bvt &bv)
     if(!clause_removed)
       cnf_clause_index++;
 
-    hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
-  });
+    solver_hardness->register_clause(
+      bv, cnf, cnf_clause_index, !clause_removed);
+  }
 
   clause_counter++;
 }
diff --git a/src/solvers/sat/satcheck_ipasir.h b/src/solvers/sat/satcheck_ipasir.h
index 0ab6192a6b8..60a07010186 100644
--- a/src/solvers/sat/satcheck_ipasir.h
+++ b/src/solvers/sat/satcheck_ipasir.h
@@ -46,28 +46,12 @@ class satcheck_ipasirt : public cnf_solvert, public hardness_collectort
     return true;
   }
 
-  void
-  with_solver_hardness(std::function<void(solver_hardnesst &)> handler) override
-  {
-    if(solver_hardness.has_value())
-    {
-      handler(solver_hardness.value());
-    }
-  }
-
-  void enable_hardness_collection() override
-  {
-    solver_hardness = solver_hardnesst{};
-  }
-
 protected:
   resultt do_prop_solve() override;
 
   void *solver;
 
   bvt assumptions;
-
-  optionalt<solver_hardnesst> solver_hardness;
 };
 
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
index f42b029aa11..25a82e6f8df 100644
--- a/src/solvers/sat/satcheck_minisat2.cpp
+++ b/src/solvers/sat/satcheck_minisat2.cpp
@@ -144,7 +144,8 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
 
     solver->addClause_(c);
 
-    with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
+    if(solver_hardness)
+    {
       // To map clauses to lines of program code, track clause indices in the
       // dimacs cnf output. Dimacs output is generated after processing
       // clauses to remove duplicates and clauses that are trivially true.
@@ -158,8 +159,9 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
       if(!clause_removed)
         cnf_clause_index++;
 
-      hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
-    });
+      solver_hardness->register_clause(
+        bv, cnf, cnf_clause_index, !clause_removed);
+    }
 
     clause_counter++;
   }
diff --git a/src/solvers/sat/satcheck_minisat2.h b/src/solvers/sat/satcheck_minisat2.h
index 1375d8d4f92..bfba9c3f164 100644
--- a/src/solvers/sat/satcheck_minisat2.h
+++ b/src/solvers/sat/satcheck_minisat2.h
@@ -68,20 +68,6 @@ class satcheck_minisat2_baset : public cnf_solvert, public hardness_collectort
     time_limit_seconds=lim;
   }
 
-  void
-  with_solver_hardness(std::function<void(solver_hardnesst &)> handler) override
-  {
-    if(solver_hardness.has_value())
-    {
-      handler(solver_hardness.value());
-    }
-  }
-
-  void enable_hardness_collection() override
-  {
-    solver_hardness = solver_hardnesst{};
-  }
-
 protected:
   resultt do_prop_solve() override;
 
@@ -90,8 +76,6 @@ class satcheck_minisat2_baset : public cnf_solvert, public hardness_collectort
 
   void add_variables();
   bvt assumptions;
-
-  optionalt<solver_hardnesst> solver_hardness;
 };
 
 class satcheck_minisat_no_simplifiert:
diff --git a/src/solvers/strings/string_constraint.cpp b/src/solvers/strings/string_constraint.cpp
index 2a3459c12b6..9bdef3a8813 100644
--- a/src/solvers/strings/string_constraint.cpp
+++ b/src/solvers/strings/string_constraint.cpp
@@ -8,10 +8,11 @@ Author: Diffblue Ltd.
 
 #include "string_constraint.h"
 
-#include <solvers/sat/satcheck.h>
+#include <util/namespace.h>
 #include <util/symbol_table.h>
 
 #include <solvers/flattening/boolbv.h>
+#include <solvers/sat/satcheck.h>
 
 /// Runs a solver instance to verify whether an expression can only be
 /// non-negative.
diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp
index a715228269e..c3292761576 100644
--- a/unit/solvers/bdd/miniBDD/miniBDD.cpp
+++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp
@@ -21,6 +21,7 @@ Author: Diffblue Ltd.
 #include <util/bitvector_types.h>
 #include <util/expanding_vector.h>
 #include <util/format_expr.h>
+#include <util/namespace.h>
 #include <util/symbol_table.h>
 
 class bdd_propt : public propt