diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
index ee415768f18..2bb317164ac 100644
--- a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -6,6 +6,7 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com
 
 \*******************************************************************/
 
+#include <testing-utils/message.h>
 #include <testing-utils/use_catch.h>
 
 #include <java_bytecode/java_bytecode_language.h>
@@ -154,7 +155,7 @@ std::string create_info(std::vector<exprt> &lemmas, const namespacet &ns)
 /// \return SAT solver result
 decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
 {
-  satcheck_no_simplifiert sat_check;
+  satcheck_no_simplifiert sat_check(null_message_handler);
   bv_refinementt::infot info;
   info.ns = &ns;
   info.prop = &sat_check;
diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h
index 89dad7c5043..96653a29320 100644
--- a/src/goto-instrument/accelerate/scratch_program.h
+++ b/src/goto-instrument/accelerate/scratch_program.h
@@ -45,7 +45,7 @@ class scratch_programt:public goto_programt
       path_storage(),
       options(get_default_options()),
       symex(mh, symbol_table, equation, options, path_storage),
-      satcheck(util_make_unique<satcheckt>()),
+      satcheck(util_make_unique<satcheckt>(mh)),
       satchecker(ns, *satcheck),
       z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
       checker(&z3) // checker(&satchecker)
diff --git a/src/solvers/flattening/bv_minimize.h b/src/solvers/flattening/bv_minimize.h
index c6c8023501b..260a2a4c202 100644
--- a/src/solvers/flattening/bv_minimize.h
+++ b/src/solvers/flattening/bv_minimize.h
@@ -48,8 +48,8 @@ class bv_minimizing_dect:public bv_pointerst
     return "Bit vector minimizing SAT";
   }
 
-  explicit bv_minimizing_dect(const namespacet &_ns):
-    bv_pointerst(_ns, satcheck)
+  bv_minimizing_dect(const namespacet &_ns, message_handlert &message_handler)
+    : bv_pointerst(_ns, satcheck), satcheck(message_handler)
   {
   }
 
diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h
index 79fec011d64..e5078979e4e 100644
--- a/src/solvers/prop/prop.h
+++ b/src/solvers/prop/prop.h
@@ -24,7 +24,9 @@ Author: Daniel Kroening, kroening@kroening.com
 class propt
 {
 public:
-  propt() { }
+  explicit propt(message_handlert &message_handler) : log(message_handler)
+  {
+  }
 
   virtual ~propt() { }
 
diff --git a/src/solvers/qbf/qbf_quantor.cpp b/src/solvers/qbf/qbf_quantor.cpp
index 17c872b9180..8c2e7969982 100644
--- a/src/solvers/qbf/qbf_quantor.cpp
+++ b/src/solvers/qbf/qbf_quantor.cpp
@@ -13,7 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/invariant.h>
 
-qbf_quantort::qbf_quantort()
+qbf_quantort::qbf_quantort(message_handlert &message_handler)
+  : qdimacs_cnft(message_handler)
 {
 }
 
diff --git a/src/solvers/qbf/qbf_quantor.h b/src/solvers/qbf/qbf_quantor.h
index a6b8ec05d66..cc9faa6b62e 100644
--- a/src/solvers/qbf/qbf_quantor.h
+++ b/src/solvers/qbf/qbf_quantor.h
@@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 class qbf_quantort:public qdimacs_cnft
 {
 public:
-  qbf_quantort();
+  explicit qbf_quantort(message_handlert &message_handler);
   virtual ~qbf_quantort();
 
   virtual const std::string solver_text();
diff --git a/src/solvers/qbf/qbf_qube.cpp b/src/solvers/qbf/qbf_qube.cpp
index 905c42e08c8..c189c1d8f2e 100644
--- a/src/solvers/qbf/qbf_qube.cpp
+++ b/src/solvers/qbf/qbf_qube.cpp
@@ -13,7 +13,8 @@ Author: CM Wintersteiger
 
 #include <util/invariant.h>
 
-qbf_qubet::qbf_qubet()
+qbf_qubet::qbf_qubet(message_handlert &message_handler)
+  : qdimacs_cnft(message_handler)
 {
   // skizzo crashes on broken lines
   break_lines=false;
diff --git a/src/solvers/qbf/qbf_qube.h b/src/solvers/qbf/qbf_qube.h
index 062e664cb48..f64622e6b3c 100644
--- a/src/solvers/qbf/qbf_qube.h
+++ b/src/solvers/qbf/qbf_qube.h
@@ -15,7 +15,7 @@ Author: CM Wintersteiger
 class qbf_qubet:public qdimacs_cnft
 {
 public:
-  qbf_qubet();
+  explicit qbf_qubet(message_handlert &message_handler);
   virtual ~qbf_qubet();
 
   virtual const std::string solver_text();
diff --git a/src/solvers/qbf/qbf_qube_core.cpp b/src/solvers/qbf/qbf_qube_core.cpp
index cfd9e126c35..291cbe69cf3 100644
--- a/src/solvers/qbf/qbf_qube_core.cpp
+++ b/src/solvers/qbf/qbf_qube_core.cpp
@@ -15,7 +15,8 @@ Author: CM Wintersteiger
 #include <util/arith_tools.h>
 #include <util/invariant.h>
 
-qbf_qube_coret::qbf_qube_coret() : qdimacs_coret()
+qbf_qube_coret::qbf_qube_coret(message_handlert &message_handler)
+  : qdimacs_coret(message_handler)
 {
   break_lines=false;
   qbf_tmp_file="qube.qdimacs";
diff --git a/src/solvers/qbf/qbf_qube_core.h b/src/solvers/qbf/qbf_qube_core.h
index 21d295b5308..35b380cbd80 100644
--- a/src/solvers/qbf/qbf_qube_core.h
+++ b/src/solvers/qbf/qbf_qube_core.h
@@ -23,7 +23,7 @@ class qbf_qube_coret:public qdimacs_coret
   assignmentt assignment;
 
 public:
-  qbf_qube_coret();
+  explicit qbf_qube_coret(message_handlert &message_handler);
   virtual ~qbf_qube_coret();
 
   virtual const std::string solver_text();
diff --git a/src/solvers/qbf/qbf_skizzo.cpp b/src/solvers/qbf/qbf_skizzo.cpp
index 64f64c694cd..5202e763d19 100644
--- a/src/solvers/qbf/qbf_skizzo.cpp
+++ b/src/solvers/qbf/qbf_skizzo.cpp
@@ -13,7 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/invariant.h>
 
-qbf_skizzot::qbf_skizzot()
+qbf_skizzot::qbf_skizzot(message_handlert &message_handler)
+  : qdimacs_cnft(message_handler)
 {
   // skizzo crashes on broken lines
   break_lines=false;
diff --git a/src/solvers/qbf/qbf_skizzo.h b/src/solvers/qbf/qbf_skizzo.h
index 62bf604582e..9568826e0d6 100644
--- a/src/solvers/qbf/qbf_skizzo.h
+++ b/src/solvers/qbf/qbf_skizzo.h
@@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 class qbf_skizzot:public qdimacs_cnft
 {
 public:
-  qbf_skizzot();
+  explicit qbf_skizzot(message_handlert &message_handler);
   virtual ~qbf_skizzot();
 
   virtual const std::string solver_text();
diff --git a/src/solvers/qbf/qdimacs_cnf.h b/src/solvers/qbf/qdimacs_cnf.h
index 7cecbb90c1d..f394d0efa79 100644
--- a/src/solvers/qbf/qdimacs_cnf.h
+++ b/src/solvers/qbf/qdimacs_cnf.h
@@ -18,7 +18,10 @@ Author: Daniel Kroening, kroening@kroening.com
 class qdimacs_cnft:public dimacs_cnft
 {
 public:
-  qdimacs_cnft() { }
+  explicit qdimacs_cnft(message_handlert &message_handler)
+    : dimacs_cnft(message_handler)
+  {
+  }
   virtual ~qdimacs_cnft() { }
 
   virtual void write_qdimacs_cnf(std::ostream &out);
diff --git a/src/solvers/qbf/qdimacs_core.h b/src/solvers/qbf/qdimacs_core.h
index 5cb144585f2..82784ed5484 100644
--- a/src/solvers/qbf/qdimacs_core.h
+++ b/src/solvers/qbf/qdimacs_core.h
@@ -19,6 +19,11 @@ Author: CM Wintersteiger
 class qdimacs_coret:public qdimacs_cnft
 {
 public:
+  explicit qdimacs_coret(message_handlert &message_handler)
+    : qdimacs_cnft(message_handler)
+  {
+  }
+
   virtual tvt l_get(literalt a) const=0;
   virtual bool is_in_core(literalt l) const=0;
 
diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp
index fc6cefbfb7b..06c6664525b 100644
--- a/src/solvers/refinement/refine_arrays.cpp
+++ b/src/solvers/refinement/refine_arrays.cpp
@@ -43,7 +43,7 @@ void bv_refinementt::arrays_overapproximated()
   std::list<lazy_constraintt>::iterator it=lazy_array_constraints.begin();
   while(it!=lazy_array_constraints.end())
   {
-    satcheck_no_simplifiert sat_check;
+    satcheck_no_simplifiert sat_check(get_message_handler());
     bv_pointerst solver(ns, sat_check);
     solver.unbounded_array=bv_pointerst::unbounded_arrayt::U_ALL;
 
diff --git a/src/solvers/sat/cnf.h b/src/solvers/sat/cnf.h
index 236de673374..e83a55d675b 100644
--- a/src/solvers/sat/cnf.h
+++ b/src/solvers/sat/cnf.h
@@ -19,7 +19,10 @@ class cnft:public propt
 public:
   // For CNF, we don't use index 0 as a matter of principle,
   // so we'll start counting variables at 1.
-  cnft():_no_variables(1) { }
+  explicit cnft(message_handlert &message_handler)
+    : propt(message_handler), _no_variables(1)
+  {
+  }
   virtual ~cnft() { }
 
   virtual literalt land(literalt a, literalt b) override;
@@ -66,7 +69,8 @@ class cnft:public propt
 class cnf_solvert:public cnft
 {
 public:
-  cnf_solvert():status(statust::INIT), clause_counter(0)
+  explicit cnf_solvert(message_handlert &message_handler)
+    : cnft(message_handler), status(statust::INIT), clause_counter(0)
   {
   }
 
diff --git a/src/solvers/sat/cnf_clause_list.h b/src/solvers/sat/cnf_clause_list.h
index aa95681612a..22d89d15aeb 100644
--- a/src/solvers/sat/cnf_clause_list.h
+++ b/src/solvers/sat/cnf_clause_list.h
@@ -23,7 +23,10 @@ Author: Daniel Kroening, kroening@kroening.com
 class cnf_clause_listt:public cnft
 {
 public:
-  cnf_clause_listt() { }
+  explicit cnf_clause_listt(message_handlert &message_handler)
+    : cnft(message_handler)
+  {
+  }
   virtual ~cnf_clause_listt() { }
 
   virtual void lcnf(const bvt &bv);
@@ -82,6 +85,11 @@ class cnf_clause_listt:public cnft
 class cnf_clause_list_assignmentt:public cnf_clause_listt
 {
 public:
+  explicit cnf_clause_list_assignmentt(message_handlert &message_handler)
+    : cnf_clause_listt(message_handler)
+  {
+  }
+
   typedef std::vector<tvt> assignmentt;
 
   assignmentt &get_assignment()
diff --git a/src/solvers/sat/dimacs_cnf.cpp b/src/solvers/sat/dimacs_cnf.cpp
index cb384f89bf3..1109b75a74d 100644
--- a/src/solvers/sat/dimacs_cnf.cpp
+++ b/src/solvers/sat/dimacs_cnf.cpp
@@ -15,15 +15,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 #include <sstream>
 
-dimacs_cnft::dimacs_cnft():break_lines(false)
+dimacs_cnft::dimacs_cnft(message_handlert &message_handler)
+  : cnf_clause_listt(message_handler), break_lines(false)
 {
 }
 
-dimacs_cnft::dimacs_cnft(message_handlert &message_handler) : dimacs_cnft()
-{
-  log.set_message_handler(message_handler);
-}
-
 void dimacs_cnft::set_assignment(literalt, bool)
 {
   UNIMPLEMENTED;
@@ -35,7 +31,10 @@ bool dimacs_cnft::is_in_conflict(literalt) const
   return false;
 }
 
-dimacs_cnf_dumpt::dimacs_cnf_dumpt(std::ostream &_out):out(_out)
+dimacs_cnf_dumpt::dimacs_cnf_dumpt(
+  std::ostream &_out,
+  message_handlert &message_handler)
+  : cnft(message_handler), out(_out)
 {
 }
 
diff --git a/src/solvers/sat/dimacs_cnf.h b/src/solvers/sat/dimacs_cnf.h
index eaa3b41e70a..0677f8ffd2c 100644
--- a/src/solvers/sat/dimacs_cnf.h
+++ b/src/solvers/sat/dimacs_cnf.h
@@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
 class dimacs_cnft:public cnf_clause_listt
 {
 public:
-  dimacs_cnft();
   explicit dimacs_cnft(message_handlert &);
   virtual ~dimacs_cnft() { }
 
@@ -43,7 +42,7 @@ class dimacs_cnft:public cnf_clause_listt
 class dimacs_cnf_dumpt:public cnft
 {
 public:
-  explicit dimacs_cnf_dumpt(std::ostream &_out);
+  dimacs_cnf_dumpt(std::ostream &_out, message_handlert &message_handler);
   virtual ~dimacs_cnf_dumpt() { }
 
   virtual const std::string solver_text()
diff --git a/src/solvers/sat/pbs_dimacs_cnf.h b/src/solvers/sat/pbs_dimacs_cnf.h
index f257746b8c4..1d331dc71ba 100644
--- a/src/solvers/sat/pbs_dimacs_cnf.h
+++ b/src/solvers/sat/pbs_dimacs_cnf.h
@@ -19,12 +19,13 @@ Author: Alex Groce
 class pbs_dimacs_cnft:public dimacs_cnft
 {
 public:
-  pbs_dimacs_cnft():
-    optimize(false),
-    maximize(false),
-    binary_search(false),
-    goal(0),
-    opt_sum(0)
+  explicit pbs_dimacs_cnft(message_handlert &message_handler)
+    : dimacs_cnft(message_handler),
+      optimize(false),
+      maximize(false),
+      binary_search(false),
+      goal(0),
+      opt_sum(0)
   {
   }
 
diff --git a/src/solvers/sat/satcheck_glucose.cpp b/src/solvers/sat/satcheck_glucose.cpp
index 01ea148fb87..0b7439c9553 100644
--- a/src/solvers/sat/satcheck_glucose.cpp
+++ b/src/solvers/sat/satcheck_glucose.cpp
@@ -215,9 +215,11 @@ void satcheck_glucose_baset<T>::set_assignment(literalt a, bool value)
   }
 }
 
-template<typename T>
-satcheck_glucose_baset<T>::satcheck_glucose_baset(T *_solver):
-  solver(_solver)
+template <typename T>
+satcheck_glucose_baset<T>::satcheck_glucose_baset(
+  T *_solver,
+  message_handlert &message_handler)
+  : cnf_solvert(message_handler), solver(_solver)
 {
 }
 
@@ -254,13 +256,19 @@ void satcheck_glucose_baset<T>::set_assumptions(const bvt &bv)
     INVARIANT(!it->is_constant(), "assumption literals must not be constant");
 }
 
-satcheck_glucose_no_simplifiert::satcheck_glucose_no_simplifiert():
-  satcheck_glucose_baset<Glucose::Solver>(new Glucose::Solver)
+satcheck_glucose_no_simplifiert::satcheck_glucose_no_simplifiert(
+  message_handlert &message_handler)
+  : satcheck_glucose_baset<Glucose::Solver>(
+      new Glucose::Solver,
+      message_handler)
 {
 }
 
-satcheck_glucose_simplifiert::satcheck_glucose_simplifiert():
-  satcheck_glucose_baset<Glucose::SimpSolver>(new Glucose::SimpSolver)
+satcheck_glucose_simplifiert::satcheck_glucose_simplifiert(
+  message_handlert &message_handler)
+  : satcheck_glucose_baset<Glucose::SimpSolver>(
+      new Glucose::SimpSolver,
+      message_handler)
 {
 }
 
diff --git a/src/solvers/sat/satcheck_glucose.h b/src/solvers/sat/satcheck_glucose.h
index 8f849630db5..9b6c22e08bb 100644
--- a/src/solvers/sat/satcheck_glucose.h
+++ b/src/solvers/sat/satcheck_glucose.h
@@ -27,7 +27,7 @@ template<typename T>
 class satcheck_glucose_baset:public cnf_solvert
 {
 public:
-  explicit satcheck_glucose_baset(T *);
+  satcheck_glucose_baset(T *, message_handlert &message_handler);
   virtual ~satcheck_glucose_baset();
 
   virtual resultt prop_solve();
@@ -57,7 +57,7 @@ class satcheck_glucose_no_simplifiert:
   public satcheck_glucose_baset<Glucose::Solver>
 {
 public:
-  satcheck_glucose_no_simplifiert();
+  explicit satcheck_glucose_no_simplifiert(message_handlert &message_handler);
   virtual const std::string solver_text();
 };
 
@@ -65,7 +65,7 @@ class satcheck_glucose_simplifiert:
   public satcheck_glucose_baset<Glucose::SimpSolver>
 {
 public:
-  satcheck_glucose_simplifiert();
+  explicit satcheck_glucose_simplifiert(message_handlert &message_handler);
   virtual const std::string solver_text();
   virtual void set_frozen(literalt a);
   bool is_eliminated(literalt a) const;
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
index 1246ced7ac4..7c5b25a707a 100644
--- a/src/solvers/sat/satcheck_minisat2.cpp
+++ b/src/solvers/sat/satcheck_minisat2.cpp
@@ -293,9 +293,11 @@ void satcheck_minisat2_baset<T>::set_assignment(literalt a, bool value)
   }
 }
 
-template<typename T>
-satcheck_minisat2_baset<T>::satcheck_minisat2_baset(T *_solver):
-  solver(_solver), time_limit_seconds(0)
+template <typename T>
+satcheck_minisat2_baset<T>::satcheck_minisat2_baset(
+  T *_solver,
+  message_handlert &message_handler)
+  : cnf_solvert(message_handler), solver(_solver), time_limit_seconds(0)
 {
 }
 
@@ -336,28 +338,20 @@ void satcheck_minisat2_baset<T>::set_assumptions(const bvt &bv)
     }
 }
 
-satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert():
-  satcheck_minisat2_baset<Minisat::Solver>(new Minisat::Solver)
-{
-}
-
 satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert(
   message_handlert &message_handler)
-  : satcheck_minisat_no_simplifiert()
-{
-  log.set_message_handler(message_handler);
-}
-
-satcheck_minisat_simplifiert::satcheck_minisat_simplifiert():
-  satcheck_minisat2_baset<Minisat::SimpSolver>(new Minisat::SimpSolver)
+  : satcheck_minisat2_baset<Minisat::Solver>(
+      new Minisat::Solver,
+      message_handler)
 {
 }
 
 satcheck_minisat_simplifiert::satcheck_minisat_simplifiert(
   message_handlert &message_handler)
-  : satcheck_minisat_simplifiert()
+  : satcheck_minisat2_baset<Minisat::SimpSolver>(
+      new Minisat::SimpSolver,
+      message_handler)
 {
-  log.set_message_handler(message_handler);
 }
 
 void satcheck_minisat_simplifiert::set_frozen(literalt a)
diff --git a/src/solvers/sat/satcheck_minisat2.h b/src/solvers/sat/satcheck_minisat2.h
index 340bc955220..6a53ff468d7 100644
--- a/src/solvers/sat/satcheck_minisat2.h
+++ b/src/solvers/sat/satcheck_minisat2.h
@@ -27,7 +27,7 @@ template<typename T>
 class satcheck_minisat2_baset:public cnf_solvert
 {
 public:
-  explicit satcheck_minisat2_baset(T *);
+  satcheck_minisat2_baset(T *, message_handlert &message_handler);
   virtual ~satcheck_minisat2_baset();
 
   virtual resultt prop_solve() override;
@@ -69,7 +69,6 @@ class satcheck_minisat_no_simplifiert:
   public satcheck_minisat2_baset<Minisat::Solver>
 {
 public:
-  satcheck_minisat_no_simplifiert();
   explicit satcheck_minisat_no_simplifiert(message_handlert &message_handler);
   virtual const std::string solver_text();
 };
@@ -78,7 +77,6 @@ class satcheck_minisat_simplifiert:
   public satcheck_minisat2_baset<Minisat::SimpSolver>
 {
 public:
-  satcheck_minisat_simplifiert();
   explicit satcheck_minisat_simplifiert(message_handlert &message_handler);
   virtual const std::string solver_text() final;
   virtual void set_frozen(literalt a) final;
diff --git a/src/solvers/strings/string_constraint.cpp b/src/solvers/strings/string_constraint.cpp
index 0441daeabfd..93cf61942ec 100644
--- a/src/solvers/strings/string_constraint.cpp
+++ b/src/solvers/strings/string_constraint.cpp
@@ -17,7 +17,9 @@ Author: Diffblue Ltd.
 /// \return true if `expr < 0` is unsatisfiable, false otherwise
 static bool cannot_be_neg(const exprt &expr)
 {
-  satcheck_no_simplifiert sat_check;
+  // this is an internal check, no need for user visibility
+  null_message_handlert null_message_handler;
+  satcheck_no_simplifiert sat_check(null_message_handler);
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
   boolbvt solver(ns, sat_check);
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp
index 4e680d35568..661d1d4e649 100644
--- a/src/solvers/strings/string_refinement.cpp
+++ b/src/solvers/strings/string_refinement.cpp
@@ -38,7 +38,8 @@ static bool is_valid_string_constraint(
 static optionalt<exprt> find_counter_example(
   const namespacet &ns,
   const exprt &axiom,
-  const symbol_exprt &var);
+  const symbol_exprt &var,
+  message_handlert &message_handler);
 
 /// Check axioms takes the model given by the underlying solver and answers
 /// whether it satisfies the string constraints.
@@ -1304,8 +1305,11 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
       stream, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
 
     if(
-      const auto &witness =
-        find_counter_example(ns, with_concretized_arrays, axiom.univ_var))
+      const auto &witness = find_counter_example(
+        ns,
+        with_concretized_arrays,
+        axiom.univ_var,
+        stream.message.get_message_handler()))
     {
       stream << std::string(4, ' ')
              << "- violated_for: " << format(axiom.univ_var) << "="
@@ -1335,7 +1339,9 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
     debug_check_axioms_step(
       stream, nc_axiom, nc_axiom, negated_axiom, negated_axiom);
 
-    if(const auto witness = find_counter_example(ns, negated_axiom, univ_var))
+    if(
+      const auto witness = find_counter_example(
+        ns, negated_axiom, univ_var, stream.message.get_message_handler()))
     {
       stream << std::string(4, ' ')
              << "- violated_for: " << univ_var.get_identifier() << "="
@@ -2043,14 +2049,16 @@ exprt string_refinementt::get(const exprt &expr) const
 /// \param ns: namespace
 /// \param [in] axiom: the axiom to be checked
 /// \param [in] var: the variable whose evaluation will be stored in witness
+/// \param message_handler: message handler
 /// \return the witness of the satisfying assignment if one
 ///   exists. If UNSAT, then behaviour is undefined.
 static optionalt<exprt> find_counter_example(
   const namespacet &ns,
   const exprt &axiom,
-  const symbol_exprt &var)
+  const symbol_exprt &var,
+  message_handlert &message_handler)
 {
-  satcheck_no_simplifiert sat_check;
+  satcheck_no_simplifiert sat_check(message_handler);
   boolbvt solver(ns, sat_check);
   solver << axiom;
 
diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp
index 271799cdfee..3720e8edd68 100644
--- a/unit/solvers/bdd/miniBDD/miniBDD.cpp
+++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp
@@ -9,6 +9,7 @@ Author: Diffblue Ltd.
 /// \file
 /// Unit tests for miniBDD
 
+#include <testing-utils/message.h>
 #include <testing-utils/use_catch.h>
 
 #include <solvers/bdd/miniBDD/miniBDD.h>
@@ -25,7 +26,8 @@ class bdd_propt : public propt
 public:
   mini_bdd_mgrt &mgr;
 
-  explicit bdd_propt(mini_bdd_mgrt &_mgr) : mgr(_mgr)
+  explicit bdd_propt(mini_bdd_mgrt &_mgr)
+    : propt(null_message_handler), mgr(_mgr)
   {
     // True and False
     bdd_map.push_back(mgr.False());
diff --git a/unit/solvers/floatbv/float_utils.cpp b/unit/solvers/floatbv/float_utils.cpp
index be7bbf4bea9..b7cdcce9b6a 100644
--- a/unit/solvers/floatbv/float_utils.cpp
+++ b/unit/solvers/floatbv/float_utils.cpp
@@ -6,6 +6,7 @@ Author: Daniel Kroening
 
 \*******************************************************************/
 
+#include <testing-utils/message.h>
 #include <testing-utils/use_catch.h>
 
 // for debug output in case of failure
@@ -155,7 +156,7 @@ SCENARIO("float_utils", "[core][solvers][floatbv][float_utils]")
 
   for(unsigned i = 0; i < 200; i++)
   {
-    satcheckt satcheck;
+    satcheckt satcheck(null_message_handler);
     float_utilst float_utils(satcheck);
 
     GIVEN("Two random floating point numbers")
@@ -192,7 +193,7 @@ SCENARIO("float_approximation", "[core][solvers][floatbv][float_approximation]")
 
   for(unsigned i = 0; i < 200; i++)
   {
-    satcheckt satcheck;
+    satcheckt satcheck(null_message_handler);
     float_approximationt float_utils(satcheck);
 
     GIVEN("Two random floating point numbers")