diff --git a/doc/architectural/goto-program-transformations.md b/doc/architectural/goto-program-transformations.md
index cd3572c8f21..a0447b7a9af 100644
--- a/doc/architectural/goto-program-transformations.md
+++ b/doc/architectural/goto-program-transformations.md
@@ -310,6 +310,7 @@ line options. The reachability slicer is enabled by the `--reachability-slice`
 command line option. The implementation of this pass is called via the \ref
 reachability_slicer(goto_modelt &, message_handlert &) function. The full slicer
 is enabled by the `--full-slice` command line option. The implementation of this
-pass is called via the \ref full_slicer(goto_modelt &) function.
+pass is called via the \ref full_slicer(goto_modelt &, message_handlert &)
+function.
 
 <em>Predecessor pass is \ref properties-transform .</em>
diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
index 0b3eee5c96c..ef5f2b755f9 100644
--- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp
+++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -276,7 +276,7 @@ ai_baset *janalyzer_parse_optionst::build_analyzer(
     }
     else if(options.get_bool_option("dependence-graph"))
     {
-      domain = new dependence_grapht(ns);
+      domain = new dependence_grapht(ns, ui_message_handler);
     }
     else if(options.get_bool_option("intervals"))
     {
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index bbc225ca5f0..127d2baa290 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -897,9 +897,10 @@ bool jbmc_parse_optionst::process_goto_functions(
                   << messaget::eom;
     log.status() << "Performing a full slice" << messaget::eom;
     if(cmdline.isset("property"))
-      property_slicer(goto_model, cmdline.get_values("property"));
+      property_slicer(
+        goto_model, cmdline.get_values("property"), ui_message_handler);
     else
-      full_slicer(goto_model);
+      full_slicer(goto_model, ui_message_handler);
   }
 
   // remove any skips introduced
diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp
index 512e7320f12..3c2e515dd54 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.cpp
+++ b/jbmc/src/jdiff/jdiff_parse_options.cpp
@@ -144,7 +144,11 @@ int jdiff_parse_optionst::doit()
         : (cmdline.isset("backward-impact") ? impact_modet::BACKWARD
                                             : impact_modet::BOTH);
     change_impact(
-      goto_model1, goto_model2, impact_mode, cmdline.isset("compact-output"));
+      goto_model1,
+      goto_model2,
+      impact_mode,
+      cmdline.isset("compact-output"),
+      ui_message_handler);
 
     return CPROVER_EXIT_SUCCESS;
   }
diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
index 621dbdfeeb8..efb7c6ae8fc 100644
--- a/src/analyses/dependence_graph.cpp
+++ b/src/analyses/dependence_graph.cpp
@@ -164,7 +164,7 @@ void dep_graph_domaint::data_dependencies(
   // TODO use (future) reaching-definitions-dereferencing rw_set
   value_setst &value_sets=
     dep_graph.reaching_definitions().get_value_sets();
-  rw_range_set_value_sett rw_set(ns, value_sets);
+  rw_range_set_value_sett rw_set(ns, value_sets, message_handler);
   goto_rw(function_to, to, rw_set);
 
   for(const auto &read_object_entry : rw_set.get_r_set())
@@ -341,7 +341,10 @@ jsont dep_graph_domaint::output_json(
 class dep_graph_domain_factoryt : public ai_domain_factoryt<dep_graph_domaint>
 {
 public:
-  explicit dep_graph_domain_factoryt(dependence_grapht &_dg) : dg(_dg)
+  dep_graph_domain_factoryt(
+    dependence_grapht &_dg,
+    message_handlert &message_handler)
+    : dg(_dg), message_handler(message_handler)
   {
   }
 
@@ -349,7 +352,7 @@ class dep_graph_domain_factoryt : public ai_domain_factoryt<dep_graph_domaint>
   {
     auto node_id = dg.add_node();
     dg.nodes[node_id].PC = l;
-    auto p = std::make_unique<dep_graph_domaint>(node_id);
+    auto p = std::make_unique<dep_graph_domaint>(node_id, message_handler);
     CHECK_RETURN(p->is_bottom());
 
     return std::unique_ptr<statet>(p.release());
@@ -357,12 +360,16 @@ class dep_graph_domain_factoryt : public ai_domain_factoryt<dep_graph_domaint>
 
 private:
   dependence_grapht &dg;
+  message_handlert &message_handler;
 };
 
-dependence_grapht::dependence_grapht(const namespacet &_ns)
-  : ait<dep_graph_domaint>(std::make_unique<dep_graph_domain_factoryt>(*this)),
+dependence_grapht::dependence_grapht(
+  const namespacet &_ns,
+  message_handlert &message_handler)
+  : ait<dep_graph_domaint>(
+      std::make_unique<dep_graph_domain_factoryt>(*this, message_handler)),
     ns(_ns),
-    rd(ns)
+    rd(ns, message_handler)
 {
 }
 
diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h
index be2ed63a40b..c053dc2a699 100644
--- a/src/analyses/dependence_graph.h
+++ b/src/analyses/dependence_graph.h
@@ -68,8 +68,11 @@ class dep_graph_domaint:public ai_domain_baset
 public:
   typedef grapht<dep_nodet>::node_indext node_indext;
 
-  explicit dep_graph_domaint(node_indext id)
-    : has_values(false), node_id(id), has_changed(false)
+  dep_graph_domaint(node_indext id, message_handlert &message_handler)
+    : has_values(false),
+      node_id(id),
+      has_changed(false),
+      message_handler(message_handler)
   {
   }
 
@@ -189,6 +192,8 @@ class dep_graph_domaint:public ai_domain_baset
   // location has a data dependency on
   depst data_deps;
 
+  message_handlert &message_handler;
+
   friend const depst &
     dependence_graph_test_get_control_deps(const dep_graph_domaint &);
   friend const depst &
@@ -220,7 +225,7 @@ class dependence_grapht:
 
   typedef std::map<irep_idt, cfg_post_dominatorst> post_dominators_mapt;
 
-  explicit dependence_grapht(const namespacet &_ns);
+  dependence_grapht(const namespacet &_ns, message_handlert &);
 
   void initialize(const goto_functionst &goto_functions)
   {
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 0f81ecaf632..cbd36d3ccb6 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -682,7 +682,7 @@ void rw_range_set_value_sett::get_objects_dereference(
     size);
 
   exprt object=deref;
-  dereference(function, target, object, ns, value_sets);
+  dereference(function, target, object, ns, value_sets, message_handler);
 
   auto type_bits = pointer_offset_bits(object.type(), ns);
 
diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h
index fdb53deb314..a6c1bf227fb 100644
--- a/src/analyses/goto_rw.h
+++ b/src/analyses/goto_rw.h
@@ -21,7 +21,7 @@ Date: April 2010
 #include <goto-programs/goto_program.h>
 
 class goto_functionst;
-
+class message_handlert;
 class rw_range_sett;
 
 void goto_rw(
@@ -212,8 +212,8 @@ class rw_range_sett
 
   virtual ~rw_range_sett();
 
-  explicit rw_range_sett(const namespacet &_ns):
-    ns(_ns)
+  rw_range_sett(const namespacet &_ns, message_handlert &message_handler)
+    : ns(_ns), message_handler(message_handler)
   {
   }
 
@@ -263,6 +263,7 @@ class rw_range_sett
 
 protected:
   const namespacet &ns;
+  message_handlert &message_handler;
 
   objectst r_range_set, w_range_set;
 
@@ -370,9 +371,9 @@ class rw_range_set_value_sett:public rw_range_sett
 public:
   rw_range_set_value_sett(
     const namespacet &_ns,
-    value_setst &_value_sets):
-    rw_range_sett(_ns),
-    value_sets(_value_sets)
+    value_setst &_value_sets,
+    message_handlert &message_handler)
+    : rw_range_sett(_ns, message_handler), value_sets(_value_sets)
   {
   }
 
@@ -463,8 +464,9 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
   rw_guarded_range_set_value_sett(
     const namespacet &_ns,
     value_setst &_value_sets,
-    guard_managert &guard_manager)
-    : rw_range_set_value_sett(_ns, _value_sets),
+    guard_managert &guard_manager,
+    message_handlert &message_handler)
+    : rw_range_set_value_sett(_ns, _value_sets, message_handler),
       guard_manager(guard_manager),
       guard(true_exprt(), guard_manager)
   {
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index 5dc71d4aab4..f44562ed90f 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -32,27 +32,30 @@ class rd_range_domain_factoryt : public ai_domain_factoryt<rd_range_domaint>
 {
 public:
   rd_range_domain_factoryt(
-    sparse_bitvector_analysist<reaching_definitiont> *_bv_container)
-    : bv_container(_bv_container)
+    sparse_bitvector_analysist<reaching_definitiont> *_bv_container,
+    message_handlert &message_handler)
+    : bv_container(_bv_container), message_handler(message_handler)
   {
     PRECONDITION(bv_container != nullptr);
   }
 
   std::unique_ptr<statet> make(locationt) const override
   {
-    auto p = std::make_unique<rd_range_domaint>(bv_container);
+    auto p = std::make_unique<rd_range_domaint>(bv_container, message_handler);
     CHECK_RETURN(p->is_bottom());
     return std::unique_ptr<statet>(p.release());
   }
 
 private:
   sparse_bitvector_analysist<reaching_definitiont> *const bv_container;
+  message_handlert &message_handler;
 };
 
 reaching_definitions_analysist::reaching_definitions_analysist(
-  const namespacet &_ns)
+  const namespacet &_ns,
+  message_handlert &message_handler)
   : concurrency_aware_ait<rd_range_domaint>(
-      std::make_unique<rd_range_domain_factoryt>(this)),
+      std::make_unique<rd_range_domain_factoryt>(this, message_handler)),
     ns(_ns)
 {
 }
@@ -306,7 +309,7 @@ void rd_range_domaint::transform_assign(
   locationt to,
   reaching_definitions_analysist &rd)
 {
-  rw_range_set_value_sett rw_set(ns, rd.get_value_sets());
+  rw_range_set_value_sett rw_set(ns, rd.get_value_sets(), message_handler);
   goto_rw(function_to, to, rw_set);
   const bool is_must_alias=rw_set.get_w_set().size()==1;
 
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index 0421a0f4fca..fb8e0a78374 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -159,8 +159,12 @@ class rd_range_domaint:public ai_domain_baset
 {
 public:
   rd_range_domaint(
-    sparse_bitvector_analysist<reaching_definitiont> *_bv_container)
-    : ai_domain_baset(), has_values(false), bv_container(_bv_container)
+    sparse_bitvector_analysist<reaching_definitiont> *_bv_container,
+    message_handlert &message_handler)
+    : ai_domain_baset(),
+      has_values(false),
+      bv_container(_bv_container),
+      message_handler(message_handler)
   {
     PRECONDITION(bv_container != nullptr);
   }
@@ -346,6 +350,8 @@ class rd_range_domaint:public ai_domain_baset
   bool merge_inner(
     values_innert &dest,
     const values_innert &other);
+
+  message_handlert &message_handler;
 };
 
 class reaching_definitions_analysist:
@@ -354,7 +360,7 @@ class reaching_definitions_analysist:
 {
 public:
   // constructor
-  explicit reaching_definitions_analysist(const namespacet &_ns);
+  reaching_definitions_analysist(const namespacet &_ns, message_handlert &);
 
   virtual ~reaching_definitions_analysist();
 
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index e8579a519eb..a89d0ddd885 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -906,9 +906,12 @@ bool cbmc_parse_optionst::process_goto_program(
                   << messaget::eom;
     log.status() << "Performing a full slice" << messaget::eom;
     if(options.is_set("property"))
-      property_slicer(goto_model, options.get_list_option("property"));
+      property_slicer(
+        goto_model,
+        options.get_list_option("property"),
+        log.get_message_handler());
     else
-      full_slicer(goto_model);
+      full_slicer(goto_model, log.get_message_handler());
   }
 
   // remove any skips introduced since coverage instrumentation
diff --git a/src/goto-analyzer/build_analyzer.cpp b/src/goto-analyzer/build_analyzer.cpp
index 1b110e78dba..ac8dd224462 100644
--- a/src/goto-analyzer/build_analyzer.cpp
+++ b/src/goto-analyzer/build_analyzer.cpp
@@ -123,7 +123,7 @@ std::unique_ptr<ai_baset> build_analyzer(
     }
     else if(options.get_bool_option("dependence-graph"))
     {
-      return std::make_unique<dependence_grapht>(ns);
+      return std::make_unique<dependence_grapht>(ns, mh);
     }
     else if(options.get_bool_option("dependence-graph-vs"))
     {
diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp
index 2ef7f3d7240..1a0d7c1ffb2 100644
--- a/src/goto-diff/change_impact.cpp
+++ b/src/goto-diff/change_impact.cpp
@@ -207,7 +207,8 @@ class change_impactt
     const goto_modelt &model_old,
     const goto_modelt &model_new,
     impact_modet impact_mode,
-    bool compact_output);
+    bool compact_output,
+    message_handlert &message_handler);
 
   void operator()();
 
@@ -289,19 +290,20 @@ class change_impactt
 };
 
 change_impactt::change_impactt(
-    const goto_modelt &model_old,
-    const goto_modelt &model_new,
-    impact_modet _impact_mode,
-    bool _compact_output):
-  impact_mode(_impact_mode),
-  compact_output(_compact_output),
-  old_goto_functions(model_old.goto_functions),
-  ns_old(model_old.symbol_table),
-  new_goto_functions(model_new.goto_functions),
-  ns_new(model_new.symbol_table),
-  unified_diff(model_old, model_new),
-  old_dep_graph(ns_old),
-  new_dep_graph(ns_new)
+  const goto_modelt &model_old,
+  const goto_modelt &model_new,
+  impact_modet _impact_mode,
+  bool _compact_output,
+  message_handlert &message_handler)
+  : impact_mode(_impact_mode),
+    compact_output(_compact_output),
+    old_goto_functions(model_old.goto_functions),
+    ns_old(model_old.symbol_table),
+    new_goto_functions(model_new.goto_functions),
+    ns_new(model_new.symbol_table),
+    unified_diff(model_old, model_new),
+    old_dep_graph(ns_old, message_handler),
+    new_dep_graph(ns_new, message_handler)
 {
   // syntactic difference?
   if(!unified_diff())
@@ -757,8 +759,10 @@ void change_impact(
   const goto_modelt &model_old,
   const goto_modelt &model_new,
   impact_modet impact_mode,
-  bool compact_output)
+  bool compact_output,
+  message_handlert &message_handler)
 {
-  change_impactt c(model_old, model_new, impact_mode, compact_output);
+  change_impactt c(
+    model_old, model_new, impact_mode, compact_output, message_handler);
   c();
 }
diff --git a/src/goto-diff/change_impact.h b/src/goto-diff/change_impact.h
index d56e57184e1..bb26edafe45 100644
--- a/src/goto-diff/change_impact.h
+++ b/src/goto-diff/change_impact.h
@@ -15,12 +15,14 @@ Date: April 2016
 #define CPROVER_GOTO_DIFF_CHANGE_IMPACT_H
 
 class goto_modelt;
+class message_handlert;
 enum class impact_modet { FORWARD, BACKWARD, BOTH };
 
 void change_impact(
   const goto_modelt &model_old,
   const goto_modelt &model_new,
   impact_modet impact_mode,
-  bool compact_output);
+  bool compact_output,
+  message_handlert &message_handler);
 
 #endif // CPROVER_GOTO_DIFF_CHANGE_IMPACT_H
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index b30a71df7d3..39f37c784f8 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -147,7 +147,8 @@ int goto_diff_parse_optionst::doit()
       goto_model1,
       goto_model2,
       impact_mode,
-      cmdline.isset("compact-output"));
+      cmdline.isset("compact-output"),
+      ui_message_handler);
 
     return CPROVER_EXIT_SUCCESS;
   }
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 9516bdaf060..f8b8c8a6414 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -254,7 +254,8 @@ static bool implicit(goto_programt::const_targett target)
 void full_slicert::operator()(
   goto_functionst &goto_functions,
   const namespacet &ns,
-  const slicing_criteriont &criterion)
+  const slicing_criteriont &criterion,
+  message_handlert &message_handler)
 {
   // build the CFG data structure
   cfg(goto_functions);
@@ -296,7 +297,7 @@ void full_slicert::operator()(
   }
 
   // compute program dependence graph (and post-dominators)
-  dependence_grapht dep_graph(ns);
+  dependence_grapht dep_graph(ns, message_handler);
   dep_graph(goto_functions, ns);
 
   // compute the fixedpoint
@@ -347,41 +348,45 @@ void full_slicert::operator()(
 void full_slicer(
   goto_functionst &goto_functions,
   const namespacet &ns,
-  const slicing_criteriont &criterion)
+  const slicing_criteriont &criterion,
+  message_handlert &message_handler)
 {
-  full_slicert()(goto_functions, ns, criterion);
+  full_slicert()(goto_functions, ns, criterion, message_handler);
 }
 
 void full_slicer(
   goto_functionst &goto_functions,
-  const namespacet &ns)
+  const namespacet &ns,
+  message_handlert &message_handler)
 {
   assert_criteriont a;
-  full_slicert()(goto_functions, ns, a);
+  full_slicert()(goto_functions, ns, a, message_handler);
 }
 
-void full_slicer(goto_modelt &goto_model)
+void full_slicer(goto_modelt &goto_model, message_handlert &message_handler)
 {
   assert_criteriont a;
   const namespacet ns(goto_model.symbol_table);
-  full_slicert()(goto_model.goto_functions, ns, a);
+  full_slicert()(goto_model.goto_functions, ns, a, message_handler);
 }
 
 void property_slicer(
   goto_functionst &goto_functions,
   const namespacet &ns,
-  const std::list<std::string> &properties)
+  const std::list<std::string> &properties,
+  message_handlert &message_handler)
 {
   properties_criteriont p(properties);
-  full_slicert()(goto_functions, ns, p);
+  full_slicert()(goto_functions, ns, p, message_handler);
 }
 
 void property_slicer(
   goto_modelt &goto_model,
-  const std::list<std::string> &properties)
+  const std::list<std::string> &properties,
+  message_handlert &message_handler)
 {
   const namespacet ns(goto_model.symbol_table);
-  property_slicer(goto_model.goto_functions, ns, properties);
+  property_slicer(goto_model.goto_functions, ns, properties, message_handler);
 }
 
 slicing_criteriont::~slicing_criteriont()
diff --git a/src/goto-instrument/full_slicer.h b/src/goto-instrument/full_slicer.h
index 630d7ec8243..e18f37f1103 100644
--- a/src/goto-instrument/full_slicer.h
+++ b/src/goto-instrument/full_slicer.h
@@ -16,21 +16,22 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class goto_functionst;
 class goto_modelt;
+class message_handlert;
 
-void full_slicer(
-  goto_functionst &,
-  const namespacet &);
+void full_slicer(goto_functionst &, const namespacet &, message_handlert &);
 
-void full_slicer(goto_modelt &);
+void full_slicer(goto_modelt &, message_handlert &);
 
 void property_slicer(
   goto_functionst &,
   const namespacet &,
-  const std::list<std::string> &properties);
+  const std::list<std::string> &properties,
+  message_handlert &);
 
 void property_slicer(
   goto_modelt &,
-  const std::list<std::string> &properties);
+  const std::list<std::string> &properties,
+  message_handlert &);
 
 class slicing_criteriont
 {
@@ -44,6 +45,7 @@ class slicing_criteriont
 void full_slicer(
   goto_functionst &goto_functions,
   const namespacet &ns,
-  const slicing_criteriont &criterion);
+  const slicing_criteriont &criterion,
+  message_handlert &);
 
 #endif // CPROVER_GOTO_INSTRUMENT_FULL_SLICER_H
diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-instrument/full_slicer_class.h
index c4abd515610..4ad06772ce6 100644
--- a/src/goto-instrument/full_slicer_class.h
+++ b/src/goto-instrument/full_slicer_class.h
@@ -41,7 +41,8 @@ class full_slicert
   void operator()(
     goto_functionst &goto_functions,
     const namespacet &ns,
-    const slicing_criteriont &criterion);
+    const slicing_criteriont &criterion,
+    message_handlert &message_handler);
 
 protected:
   struct cfg_nodet
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 55721374ce6..81dacb0d438 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -550,8 +550,8 @@ int goto_instrument_parse_optionst::doit()
       const symbolt &symbol=ns.lookup(ID_main);
       symbol_exprt main(symbol.name, symbol.type);
 
-      std::cout <<
-        rw_set_functiont(value_set_analysis, goto_model, main);
+      std::cout << rw_set_functiont(
+        value_set_analysis, goto_model, main, ui_message_handler);
       return CPROVER_EXIT_SUCCESS;
     }
 
@@ -567,7 +567,7 @@ int goto_instrument_parse_optionst::doit()
       rewrite_rw_ok(goto_model);
 
       const namespacet ns(goto_model.symbol_table);
-      reaching_definitions_analysist rd_analysis(ns);
+      reaching_definitions_analysist rd_analysis(ns, ui_message_handler);
       rd_analysis(goto_model);
       rd_analysis.output(goto_model, std::cout);
 
@@ -580,7 +580,7 @@ int goto_instrument_parse_optionst::doit()
       rewrite_rw_ok(goto_model);
 
       const namespacet ns(goto_model.symbol_table);
-      dependence_grapht dependence_graph(ns);
+      dependence_grapht dependence_graph(ns, ui_message_handler);
       dependence_graph(goto_model);
       dependence_graph.output(goto_model, std::cout);
       dependence_graph.output_dot(std::cout);
@@ -1524,13 +1524,13 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     {
       // removing pointers
       log.status() << "Removing Pointers" << messaget::eom;
-      remove_pointers(goto_model, value_set_analysis);
+      remove_pointers(goto_model, value_set_analysis, ui_message_handler);
     }
 
     if(cmdline.isset("race-check"))
     {
       log.status() << "Adding Race Checks" << messaget::eom;
-      race_check(value_set_analysis, goto_model);
+      race_check(value_set_analysis, goto_model, ui_message_handler);
     }
 
     if(cmdline.isset("mm"))
@@ -1627,14 +1627,15 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       interrupt(
         value_set_analysis,
         goto_model,
-        cmdline.get_value("isr"));
+        cmdline.get_value("isr"),
+        ui_message_handler);
     }
 
     // Memory-mapped I/O
     if(cmdline.isset("mmio"))
     {
       log.status() << "Instrumenting memory-mapped I/O" << messaget::eom;
-      mmio(value_set_analysis, goto_model);
+      mmio(value_set_analysis, goto_model, ui_message_handler);
     }
 
     if(cmdline.isset("concurrency"))
@@ -1759,12 +1760,13 @@ void goto_instrument_parse_optionst::instrument_goto_program()
                   << messaget::eom;
     log.status() << "Performing a full slice" << messaget::eom;
     if(cmdline.isset("property"))
-      property_slicer(goto_model, cmdline.get_values("property"));
+      property_slicer(
+        goto_model, cmdline.get_values("property"), ui_message_handler);
     else
     {
       // full_slicer requires that the model has unique location numbers:
       goto_model.goto_functions.update();
-      full_slicer(goto_model);
+      full_slicer(goto_model, ui_message_handler);
     }
   }
 
diff --git a/src/goto-instrument/interrupt.cpp b/src/goto-instrument/interrupt.cpp
index acd6a01211c..4f082d05ac7 100644
--- a/src/goto-instrument/interrupt.cpp
+++ b/src/goto-instrument/interrupt.cpp
@@ -64,7 +64,8 @@ static void interrupt(
 #endif
   goto_programt &goto_program,
   const symbol_exprt &interrupt_handler,
-  const rw_set_baset &isr_rw_set)
+  const rw_set_baset &isr_rw_set,
+  message_handlert &message_handler)
 {
   namespacet ns(symbol_table);
 
@@ -79,12 +80,11 @@ static void interrupt(
     ns,
     value_sets,
     function_id,
-    i_it
+    i_it,
 #ifdef LOCAL_MAY
-    ,
-    local_may
+    local_may,
 #endif
-  ); // NOLINT(whitespace/parens)
+    message_handler); // NOLINT(whitespace/parens)
 
     // potential race?
     bool race_on_read=potential_race_on_read(rw_set, isr_rw_set);
@@ -188,15 +188,15 @@ get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
 void interrupt(
   value_setst &value_sets,
   goto_modelt &goto_model,
-  const irep_idt &interrupt_handler)
+  const irep_idt &interrupt_handler,
+  message_handlert &message_handler)
 {
   // look up the ISR
   symbol_exprt isr=
     get_isr(goto_model.symbol_table, interrupt_handler);
 
   // we first figure out which objects are read/written by the ISR
-  rw_set_functiont isr_rw_set(
-    value_sets, goto_model, isr);
+  rw_set_functiont isr_rw_set(value_sets, goto_model, isr, message_handler);
 
   // now instrument
 
@@ -216,7 +216,8 @@ void interrupt(
 #endif
         gf_entry.second.body,
         isr,
-        isr_rw_set);
+        isr_rw_set,
+        message_handler);
     }
   }
 
diff --git a/src/goto-instrument/interrupt.h b/src/goto-instrument/interrupt.h
index 082b4e0b4f5..9d2446a60b0 100644
--- a/src/goto-instrument/interrupt.h
+++ b/src/goto-instrument/interrupt.h
@@ -17,11 +17,13 @@ Date: September 2011
 #include <util/irep.h>
 
 class goto_modelt;
+class message_handlert;
 class value_setst;
 
 void interrupt(
   value_setst &,
   goto_modelt &,
-  const irep_idt &interrupt_handler);
+  const irep_idt &interrupt_handler,
+  message_handlert &);
 
 #endif // CPROVER_GOTO_INSTRUMENT_INTERRUPT_H
diff --git a/src/goto-instrument/mmio.cpp b/src/goto-instrument/mmio.cpp
index a067c79f4bb..65ecad0c63b 100644
--- a/src/goto-instrument/mmio.cpp
+++ b/src/goto-instrument/mmio.cpp
@@ -28,7 +28,8 @@ static void mmio(
 #ifdef LOCAL_MAY
   const goto_functionst::goto_functiont &goto_function,
 #endif
-  goto_programt &goto_program)
+  goto_programt &goto_program,
+  message_handlert &message_handler)
 {
   namespacet ns(symbol_table);
 
@@ -46,12 +47,11 @@ static void mmio(
         ns,
         value_sets,
         function_id,
-        i_it
+        i_it,
 #ifdef LOCAL_MAY
-        ,
-        local_may
+        local_may,
 #endif
-      ); // NOLINT(whitespace/parens)
+        message_handler); // NOLINT(whitespace/parens)
 
       if(rw_set.empty())
         continue;
@@ -158,7 +158,8 @@ static void mmio(
 
 void mmio(
   value_setst &value_sets,
-  goto_modelt &goto_model)
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
 {
   // now instrument
 
@@ -175,7 +176,8 @@ void mmio(
 #ifdef LOCAL_MAY
         gf_entry.second,
 #endif
-        gf_entry.second.body);
+        gf_entry.second.body,
+        message_handler);
     }
   }
 
diff --git a/src/goto-instrument/mmio.h b/src/goto-instrument/mmio.h
index f2fbec84fa1..1e671b4a42b 100644
--- a/src/goto-instrument/mmio.h
+++ b/src/goto-instrument/mmio.h
@@ -14,11 +14,10 @@ Date: September 2011
 #ifndef CPROVER_GOTO_INSTRUMENT_MMIO_H
 #define CPROVER_GOTO_INSTRUMENT_MMIO_H
 
+class message_handlert;
 class value_setst;
 class goto_modelt;
 
-void mmio(
-  value_setst &,
-  goto_modelt &);
+void mmio(value_setst &, goto_modelt &, message_handlert &);
 
 #endif // CPROVER_GOTO_INSTRUMENT_MMIO_H
diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp
index 85bc08ff0f1..7dccfe38fed 100644
--- a/src/goto-instrument/race_check.cpp
+++ b/src/goto-instrument/race_check.cpp
@@ -164,7 +164,8 @@ static void race_check(
   const irep_idt &function_id,
   L_M_ARG(const goto_functionst::goto_functiont &goto_function)
   goto_programt &goto_program,
-  w_guardst &w_guards)
+  w_guardst &w_guards,
+  message_handlert &message_handler)
 // clang-format on
 {
   namespacet ns(symbol_table);
@@ -180,7 +181,11 @@ static void race_check(
     if(instruction.is_assign())
     {
       rw_set_loct rw_set(
-        ns, value_sets, function_id, i_it L_M_LAST_ARG(local_may));
+        ns,
+        value_sets,
+        function_id,
+        i_it L_M_LAST_ARG(local_may),
+        message_handler);
 
       if(!has_shared_entries(ns, rw_set))
         continue;
@@ -269,7 +274,8 @@ void race_check(
 #ifdef LOCAL_MAY
   const goto_functionst::goto_functiont &goto_function,
 #endif
-  goto_programt &goto_program)
+  goto_programt &goto_program,
+  message_handlert &message_handler)
 {
   w_guardst w_guards(symbol_table);
 
@@ -278,7 +284,8 @@ void race_check(
     symbol_table,
     function_id,
     L_M_ARG(goto_function) goto_program,
-    w_guards);
+    w_guards,
+    message_handler);
 
   w_guards.add_initialization(goto_program);
   goto_program.update();
@@ -286,7 +293,8 @@ void race_check(
 
 void race_check(
   value_setst &value_sets,
-  goto_modelt &goto_model)
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
 {
   w_guardst w_guards(goto_model.symbol_table);
 
@@ -301,7 +309,8 @@ void race_check(
         goto_model.symbol_table,
         gf_entry.first,
         L_M_ARG(gf_entry.second) gf_entry.second.body,
-        w_guards);
+        w_guards,
+        message_handler);
     }
   }
 
diff --git a/src/goto-instrument/race_check.h b/src/goto-instrument/race_check.h
index 98e9bfd52d9..e4d6daa3443 100644
--- a/src/goto-instrument/race_check.h
+++ b/src/goto-instrument/race_check.h
@@ -22,6 +22,7 @@ Date: February 2006
 
 class goto_modelt;
 class goto_programt;
+class message_handlert;
 class value_setst;
 
 void race_check(
@@ -31,8 +32,9 @@ void race_check(
 #ifdef LOCAL_MAY
   const goto_functionst::goto_functiont &goto_function,
 #endif
-  goto_programt &goto_program);
+  goto_programt &goto_program,
+  message_handlert &);
 
-void race_check(value_setst &, goto_modelt &);
+void race_check(value_setst &, goto_modelt &, message_handlert &);
 
 #endif // CPROVER_GOTO_INSTRUMENT_RACE_CHECK_H
diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp
index ca98c2ef60a..b1c03a6c273 100644
--- a/src/goto-instrument/rw_set.cpp
+++ b/src/goto-instrument/rw_set.cpp
@@ -155,7 +155,7 @@ void _rw_set_loct::read_write_rec(
       read_write_rec(*it, r, w, suffix, guard_conjuncts);
     }
     #else
-    dereference(function_id, target, tmp, ns, value_sets);
+    dereference(function_id, target, tmp, ns, value_sets, message_handler);
 
     read_write_rec(tmp, r, w, suffix, guard_conjuncts);
 #endif
@@ -219,12 +219,11 @@ void rw_set_functiont::compute_rec(const exprt &function)
           ns,
           value_sets,
           function_id,
-          i_it
+          i_it,
 #ifdef LOCAL_MAY
-          ,
-          local_may
+          local_may,
 #endif
-        ); // NOLINT(whitespace/parens)
+          message_handler); // NOLINT(whitespace/parens)
       }
     }
   }
diff --git a/src/goto-instrument/rw_set.h b/src/goto-instrument/rw_set.h
index aea64226697..3eefa66b554 100644
--- a/src/goto-instrument/rw_set.h
+++ b/src/goto-instrument/rw_set.h
@@ -26,6 +26,7 @@ Date: February 2006
 #include <analyses/local_may_alias.h>
 #endif
 
+class message_handlert;
 class value_setst;
 
 // a container for read/write sets
@@ -33,8 +34,8 @@ class value_setst;
 class rw_set_baset
 {
 public:
-  explicit rw_set_baset(const namespacet &_ns)
-    :ns(_ns)
+  rw_set_baset(const namespacet &_ns, message_handlert &message_handler)
+    : ns(_ns), message_handler(message_handler)
   {
   }
 
@@ -97,6 +98,7 @@ class rw_set_baset
   virtual void reset_track_deref() {}
 
   const namespacet &ns;
+  message_handlert &message_handler;
 };
 
 inline std::ostream &operator<<(
@@ -117,8 +119,9 @@ class _rw_set_loct:public rw_set_baset
     value_setst &_value_sets,
     const irep_idt &_function_id,
     goto_programt::const_targett _target,
-    local_may_aliast &may)
-    : rw_set_baset(_ns),
+    local_may_aliast &may,
+    message_handlert &message_handler)
+    : rw_set_baset(_ns, message_handler),
       value_sets(_value_sets),
       function_id(_function_id),
       target(_target),
@@ -128,8 +131,9 @@ class _rw_set_loct:public rw_set_baset
     const namespacet &_ns,
     value_setst &_value_sets,
     const irep_idt &_function_id,
-    goto_programt::const_targett _target)
-    : rw_set_baset(_ns),
+    goto_programt::const_targett _target,
+    message_handlert &message_handler)
+    : rw_set_baset(_ns, message_handler),
       value_sets(_value_sets),
       function_id(_function_id),
       target(_target)
@@ -182,15 +186,23 @@ class rw_set_loct:public _rw_set_loct
     value_setst &_value_sets,
     const irep_idt &_function_id,
     goto_programt::const_targett _target,
-    local_may_aliast &may)
-    : _rw_set_loct(_ns, _value_sets, _function_id, _target, may)
+    local_may_aliast &may,
+    message_handlert &message_handler)
+    : _rw_set_loct(
+        _ns,
+        _value_sets,
+        _function_id,
+        _target,
+        may,
+        message_handler)
 #else
   rw_set_loct(
     const namespacet &_ns,
     value_setst &_value_sets,
     const irep_idt &_function_id,
-    goto_programt::const_targett _target)
-    : _rw_set_loct(_ns, _value_sets, _function_id, _target)
+    goto_programt::const_targett _target,
+    message_handlert &message_handler)
+    : _rw_set_loct(_ns, _value_sets, _function_id, _target, message_handler)
 #endif
   {
     compute();
@@ -205,11 +217,12 @@ class rw_set_functiont:public rw_set_baset
   rw_set_functiont(
     value_setst &_value_sets,
     const goto_modelt &_goto_model,
-    const exprt &function):
-    rw_set_baset(ns),
-    ns(_goto_model.symbol_table),
-    value_sets(_value_sets),
-    goto_functions(_goto_model.goto_functions)
+    const exprt &function,
+    message_handlert &message_handler)
+    : rw_set_baset(ns, message_handler),
+      ns(_goto_model.symbol_table),
+      value_sets(_value_sets),
+      goto_functions(_goto_model.goto_functions)
   {
     compute_rec(function);
   }
@@ -243,16 +256,24 @@ class rw_set_with_trackt:public _rw_set_loct
     value_setst &_value_sets,
     const irep_idt &_function_id,
     goto_programt::const_targett _target,
-    local_may_aliast &may)
-    : _rw_set_loct(_ns, _value_sets, _function_id, _target, may),
+    local_may_aliast &may,
+    message_handlert &message_handler)
+    : _rw_set_loct(
+        _ns,
+        _value_sets,
+        _function_id,
+        _target,
+        may,
+        message_handler),
       dereferencing(false)
 #else
   rw_set_with_trackt(
     const namespacet &_ns,
     value_setst &_value_sets,
     const irep_idt &_function_id,
-    goto_programt::const_targett _target)
-    : _rw_set_loct(_ns, _value_sets, _function_id, _target),
+    goto_programt::const_targett _target,
+    message_handlert &message_handler)
+    : _rw_set_loct(_ns, _value_sets, _function_id, _target, message_handler),
       dereferencing(false)
 #endif
   {
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
index 3850c969da6..fc33f29f75b 100644
--- a/src/goto-instrument/wmm/goto2graph.cpp
+++ b/src/goto-instrument/wmm/goto2graph.cpp
@@ -428,12 +428,11 @@ bool instrumentert::cfg_visitort::contains_shared_array(
       ns,
       value_sets,
       function_id,
-      cur
+      cur,
 #ifdef LOCAL_MAY
-      ,
-      local_may
+      local_may,
 #endif
-    ); // NOLINT(whitespace/parens)
+      instrumenter.message.get_message_handler()); // NOLINT(whitespace/parens)
     instrumenter.message.debug() << "Writes: "<<rw_set.w_entries.size()
       <<"; Reads:"<<rw_set.r_entries.size() << messaget::eom;
 
@@ -857,12 +856,11 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
     ns,
     value_sets,
     function_id,
-    i_it
+    i_it,
 #ifdef LOCAL_MAY
-    ,
-    local_may
+    local_may,
 #endif
-  ); // NOLINT(whitespace/parens)
+    instrumenter.message.get_message_handler()); // NOLINT(whitespace/parens)
 
   event_idt previous=std::numeric_limits<event_idt>::max();
   event_idt previous_gnode=std::numeric_limits<event_idt>::max();
diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
index 05e279cbfe4..4d73b57efd2 100644
--- a/src/goto-instrument/wmm/shared_buffers.cpp
+++ b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -1023,12 +1023,11 @@ void shared_bufferst::affected_by_delay(
         ns,
         value_sets,
         gf_entry.first,
-        i_it
+        i_it,
 #ifdef LOCAL_MAY
-        ,
-        local_may
+        local_may,
 #endif
-      ); // NOLINT(whitespace/parens)
+        message.get_message_handler()); // NOLINT(whitespace/parens)
       for(const auto &w_entry : rw_set.w_entries)
       {
         for(const auto &r_entry : rw_set.r_entries)
@@ -1090,12 +1089,12 @@ void shared_bufferst::cfg_visitort::weak_memory(
           ns,
           value_sets,
           function_id,
-          i_it
+          i_it,
 #ifdef LOCAL_MAY
-          ,
-          local_may
+          local_may,
 #endif
-        ); // NOLINT(whitespace/parens)
+          shared_buffers.message
+            .get_message_handler()); // NOLINT(whitespace/parens)
 
         if(rw_set.empty())
           continue;
diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp
index 0e4946b5337..bf4b85c69fe 100644
--- a/src/goto-instrument/wmm/weak_memory.cpp
+++ b/src/goto-instrument/wmm/weak_memory.cpp
@@ -65,12 +65,11 @@ void introduce_temporaries(
         ns,
         value_sets,
         function_id,
-        i_it
+        i_it,
 #ifdef LOCAL_MAY
-        ,
-        local_may
+        local_may,
 #endif
-      ); // NOLINT(whitespace/parens)
+        message.get_message_handler()); // NOLINT(whitespace/parens)
       if(rw_set.empty())
         continue;
 
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index afe0677f989..76fc7f48a83 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -27,12 +27,14 @@ class preconditiont
     value_setst &_value_sets,
     const goto_programt::const_targett _target,
     const SSA_stept &_SSA_step,
-    const goto_symex_statet &_s)
+    const goto_symex_statet &_s,
+    message_handlert &message_handler)
     : ns(_ns),
       value_sets(_value_sets),
       target(_target),
       SSA_step(_SSA_step),
-      s(_s)
+      s(_s),
+      message_handler(message_handler)
   {
   }
 
@@ -42,6 +44,7 @@ class preconditiont
   const goto_programt::const_targett target;
   const SSA_stept &SSA_step;
   const goto_symex_statet &s;
+  message_handlert &message_handler;
   void compute_rec(exprt &dest);
 
 public:
@@ -57,14 +60,15 @@ void precondition(
   const goto_programt::const_targett target,
   const symex_target_equationt &equation,
   const goto_symex_statet &s,
-  exprt &dest)
+  exprt &dest,
+  message_handlert &message_handler)
 {
   for(symex_target_equationt::SSA_stepst::const_reverse_iterator
       it=equation.SSA_steps.rbegin();
       it!=equation.SSA_steps.rend();
       it++)
   {
-    preconditiont precondition(ns, value_sets, target, *it, s);
+    preconditiont precondition(ns, value_sets, target, *it, s, message_handler);
     precondition.compute(dest);
     if(dest.is_false())
       return;
@@ -128,7 +132,13 @@ void preconditiont::compute_rec(exprt &dest)
     {
       exprt tmp;
       tmp.swap(deref_expr.pointer());
-      dereference(SSA_step.source.function_id, target, tmp, ns, value_sets);
+      dereference(
+        SSA_step.source.function_id,
+        target,
+        tmp,
+        ns,
+        value_sets,
+        message_handler);
       deref_expr.swap(tmp);
       compute_rec(deref_expr);
     }
diff --git a/src/goto-symex/precondition.h b/src/goto-symex/precondition.h
index aef6d5cf5ba..11501147c4e 100644
--- a/src/goto-symex/precondition.h
+++ b/src/goto-symex/precondition.h
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto-programs/goto_program.h"
 
 class exprt;
+class message_handlert;
 class namespacet;
 class symex_target_equationt;
 class value_setst;
@@ -25,6 +26,7 @@ void precondition(
   const goto_programt::const_targett target,
   const symex_target_equationt &equation,
   const class goto_symex_statet &s,
-  exprt &dest);
+  exprt &dest,
+  message_handlert &message_handler);
 
 #endif // CPROVER_GOTO_SYMEX_PRECONDITION_H
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 7806a720269..5c1ff7134a9 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -131,7 +131,12 @@ void goto_symext::process_array_expr(statet &state, exprt &expr)
   symex_dereference_statet symex_dereference_state(state, ns);
 
   value_set_dereferencet dereference(
-    ns, state.symbol_table, symex_dereference_state, language_mode, false, log);
+    ns,
+    state.symbol_table,
+    symex_dereference_state,
+    language_mode,
+    false,
+    log.get_message_handler());
 
   expr = dereference.dereference(expr, symex_config.show_points_to_sets);
   lift_lets(state, expr);
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 51d64fb3e24..f4beccfb669 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -329,7 +329,7 @@ void goto_symext::dereference_rec(
       symex_dereference_state,
       language_mode,
       expr_is_not_null,
-      log);
+      log.get_message_handler());
 
     // std::cout << "**** " << format(tmp1) << '\n';
     exprt tmp2 =
diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp
index 176343c6152..2f1d15c5bf3 100644
--- a/src/goto-synthesizer/cegis_verifier.cpp
+++ b/src/goto-synthesizer/cegis_verifier.cpp
@@ -178,7 +178,7 @@ std::list<loop_idt> cegis_verifiert::get_cause_loop_id(
   std::list<loop_idt> result;
 
   // build the dependence graph
-  dependence_grapht dependence_graph(ns);
+  dependence_grapht dependence_graph(ns, log.get_message_handler());
   dependence_graph(goto_model);
 
   // Checking if `to` is dependent on `from`.
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp
index 672f749c576..efa02a89046 100644
--- a/src/pointer-analysis/goto_program_dereference.cpp
+++ b/src/pointer-analysis/goto_program_dereference.cpp
@@ -259,15 +259,15 @@ void goto_program_dereferencet::dereference_expression(
 /// may be pointing to.
 void remove_pointers(
   goto_modelt &goto_model,
-  value_setst &value_sets)
+  value_setst &value_sets,
+  message_handlert &message_handler)
 {
   namespacet ns(goto_model.symbol_table);
 
   optionst options;
 
-  goto_program_dereferencet
-    goto_program_dereference(
-      ns, goto_model.symbol_table, options, value_sets);
+  goto_program_dereferencet goto_program_dereference(
+    ns, goto_model.symbol_table, options, value_sets, message_handler);
 
   for(auto &gf_entry : goto_model.goto_functions.function_map)
     goto_program_dereference.dereference_program(gf_entry.second.body);
@@ -280,11 +280,12 @@ void dereference(
   goto_programt::const_targett target,
   exprt &expr,
   const namespacet &ns,
-  value_setst &value_sets)
+  value_setst &value_sets,
+  message_handlert &message_handler)
 {
   optionst options;
   symbol_tablet new_symbol_table;
-  goto_program_dereferencet
-    goto_program_dereference(ns, new_symbol_table, options, value_sets);
+  goto_program_dereferencet goto_program_dereference(
+    ns, new_symbol_table, options, value_sets, message_handler);
   goto_program_dereference.dereference_expression(function_id, target, expr);
 }
diff --git a/src/pointer-analysis/goto_program_dereference.h b/src/pointer-analysis/goto_program_dereference.h
index a77e8483e1f..1818323d0de 100644
--- a/src/pointer-analysis/goto_program_dereference.h
+++ b/src/pointer-analysis/goto_program_dereference.h
@@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
 #define CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
 
-#include <util/message.h>
-
 #include "dereference_callback.h"
 #include "value_set_dereference.h"
 
@@ -35,24 +33,23 @@ class goto_program_dereferencet:protected dereference_callbackt
   // for the final argument to value_set_dereferencet.
   // This means that language-inappropriate values such as
   // (struct A*)some_integer_value in Java, may be returned.
-  // Note: value_set_dereferencet requires a messaget instance
-  // as on of its arguments to display the points-to set
+  // Note: value_set_dereferencet requires a message_handlert instance
+  // as one of its arguments to display the points-to set
   // during symex. Display is not done during goto-program
   // conversion. To ensure this the display_points_to_sets
   // parameter in value_set_dereferencet::dereference()
   // is set to false by default and is not changed by the
-  // goto program conversion modules. Similarly, here we set
-  // _log to be a default messaget instance.
+  // goto program conversion modules.
   goto_program_dereferencet(
     const namespacet &_ns,
     symbol_table_baset &_new_symbol_table,
     const optionst &_options,
     value_setst &_value_sets,
-    const messaget &_log = messaget())
+    message_handlert &message_handler)
     : options(_options),
       ns(_ns),
       value_sets(_value_sets),
-      dereference(_ns, _new_symbol_table, *this, ID_nil, false, _log)
+      dereference(_ns, _new_symbol_table, *this, ID_nil, false, message_handler)
   {
   }
 
@@ -101,11 +98,10 @@ void dereference(
   goto_programt::const_targett target,
   exprt &expr,
   const namespacet &,
-  value_setst &);
+  value_setst &,
+  message_handlert &);
 
-void remove_pointers(
-  goto_modelt &,
-  value_setst &);
+void remove_pointers(goto_modelt &, value_setst &, message_handlert &);
 
 #define OPT_REMOVE_POINTERS "(remove-pointers)"
 
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 924480fbe25..1441fce7fdd 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -282,6 +282,7 @@ exprt value_set_dereferencet::handle_dereference_base_case(
 
   if(display_points_to_sets)
   {
+    messaget log{message_handler};
     log.status() << value_set_dereference_stats_to_json(
       pointer, points_to_set, retained_values, result_value);
   }
diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h
index d33abf35f04..96552e66af9 100644
--- a/src/pointer-analysis/value_set_dereference.h
+++ b/src/pointer-analysis/value_set_dereference.h
@@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 
 class dereference_callbackt;
-class messaget;
+class message_handlert;
 class symbol_table_baset;
 
 /// Wrapper for a function dereferencing pointer expressions using a value set.
@@ -30,20 +30,20 @@ class value_set_dereferencet final
   ///   dereference failure
   /// \param _exclude_null_derefs: Ignore value-set entries that indicate a
   //    given dereference may follow a null pointer
-  /// \param _log: Messaget object for displaying points-to set
+  /// \param _message_handler: Message handler for displaying points-to set
   value_set_dereferencet(
     const namespacet &_ns,
     symbol_table_baset &_new_symbol_table,
     dereference_callbackt &_dereference_callback,
     const irep_idt _language_mode,
     bool _exclude_null_derefs,
-    const messaget &_log)
+    message_handlert &_message_handler)
     : ns(_ns),
       new_symbol_table(_new_symbol_table),
       dereference_callback(_dereference_callback),
       language_mode(_language_mode),
       exclude_null_derefs(_exclude_null_derefs),
-      log(_log)
+      message_handler(_message_handler)
   { }
 
   virtual ~value_set_dereferencet() { }
@@ -105,7 +105,7 @@ class value_set_dereferencet final
   /// Flag indicating whether `value_set_dereferencet::dereference` should
   /// disregard an apparent attempt to dereference NULL
   const bool exclude_null_derefs;
-  const messaget &log;
+  message_handlert &message_handler;
   valuet get_failure_value(const exprt &pointer, const typet &type);
   exprt handle_dereference_base_case(
     const exprt &pointer,
diff --git a/unit/analyses/dependence_graph.cpp b/unit/analyses/dependence_graph.cpp
index ab67479d312..ddcd12af2e7 100644
--- a/unit/analyses/dependence_graph.cpp
+++ b/unit/analyses/dependence_graph.cpp
@@ -87,7 +87,7 @@ SCENARIO("dependence_graph", "[core][analyses][dependence_graph]")
 
     WHEN("Constructing a dependence graph")
     {
-      dependence_grapht dep_graph(ns);
+      dependence_grapht dep_graph(ns, null_message_handler);
       dep_graph(goto_model.goto_functions, ns);
 
       THEN("The function call and assignment instructions "