diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 9b8e2e4500c..63b53e394b2 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -340,7 +340,6 @@ void bmct::get_memory_model()
 void bmct::setup()
 {
   get_memory_model();
-  symex.set_message_handler(get_message_handler());
   symex.options=options;
 
   {
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index c81ee66e74b..f45d7ab5e4c 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -38,14 +38,14 @@ class bmct:public safety_checkert
     const optionst &_options,
     const symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
-    prop_convt &_prop_conv):
-    safety_checkert(ns, _message_handler),
-    options(_options),
-    ns(_symbol_table, new_symbol_table),
-    equation(ns),
-    symex(ns, new_symbol_table, equation),
-    prop_conv(_prop_conv),
-    ui(ui_message_handlert::uit::PLAIN)
+    prop_convt &_prop_conv)
+    : safety_checkert(ns, _message_handler),
+      options(_options),
+      ns(_symbol_table, new_symbol_table),
+      equation(ns),
+      symex(_message_handler, ns, new_symbol_table, equation),
+      prop_conv(_prop_conv),
+      ui(ui_message_handlert::uit::PLAIN)
   {
     symex.constant_propagation=options.get_bool_option("propagation");
     symex.record_coverage=
diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp
index 4a1c59096b5..fdc34de4b1c 100644
--- a/src/cbmc/symex_bmc.cpp
+++ b/src/cbmc/symex_bmc.cpp
@@ -17,14 +17,15 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 
 symex_bmct::symex_bmct(
+  message_handlert &mh,
   const namespacet &_ns,
   symbol_tablet &_new_symbol_table,
-  symex_targett &_target):
-  goto_symext(_ns, _new_symbol_table, _target),
-  record_coverage(false),
-  max_unwind(0),
-  max_unwind_is_set(false),
-  symex_coverage(_ns)
+  symex_targett &_target)
+  : goto_symext(mh, _ns, _new_symbol_table, _target),
+    record_coverage(false),
+    max_unwind(0),
+    max_unwind_is_set(false),
+    symex_coverage(_ns)
 {
 }
 
@@ -37,10 +38,9 @@ void symex_bmct::symex_step(
 
   if(!source_location.is_nil() && last_source_location!=source_location)
   {
-    debug() << "BMC at file " << source_location.get_file()
-            << " line " << source_location.get_line()
-            << " function " << source_location.get_function()
-            << eom;
+    log.debug() << "BMC at file " << source_location.get_file() << " line "
+                << source_location.get_line() << " function "
+                << source_location.get_function() << log.eom;
 
     last_source_location=source_location;
   }
@@ -52,15 +52,15 @@ void symex_bmct::symex_step(
      state.source.pc->is_assume() &&
      simplify_expr(state.source.pc->guard, ns).is_false())
   {
-    statistics() << "aborting path on assume(false) at "
-                 << state.source.pc->source_location
-                 << " thread " << state.source.thread_nr;
+    log.statistics() << "aborting path on assume(false) at "
+                     << state.source.pc->source_location << " thread "
+                     << state.source.thread_nr;
 
     const irep_idt &c=state.source.pc->source_location.get_comment();
     if(!c.empty())
-      statistics() << ": " << c;
+      log.statistics() << ": " << c;
 
-    statistics() << eom;
+    log.statistics() << log.eom;
   }
 
   goto_symext::symex_step(goto_functions, state);
@@ -94,7 +94,7 @@ void symex_bmct::merge_goto(
 
   goto_symext::merge_goto(goto_state, state);
 
-  assert(prev_pc->is_goto());
+  PRECONDITION(prev_pc->is_goto());
   if(record_coverage &&
      // could the branch possibly be taken?
      !prev_guard.is_false() &&
@@ -132,15 +132,14 @@ bool symex_bmct::get_unwind(
 
   bool abort=unwind>=this_loop_limit;
 
-  statistics() << (abort?"Not unwinding":"Unwinding")
-               << " loop " << id << " iteration "
-               << unwind;
+  log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
+                   << " iteration " << unwind;
 
   if(this_loop_limit!=std::numeric_limits<unsigned>::max())
-    statistics() << " (" << this_loop_limit << " max)";
+    log.statistics() << " (" << this_loop_limit << " max)";
 
-  statistics() << " " << source.pc->source_location
-               << " thread " << source.thread_nr << eom;
+  log.statistics() << " " << source.pc->source_location << " thread "
+                   << source.thread_nr << log.eom;
 
   return abort;
 }
@@ -176,15 +175,13 @@ bool symex_bmct::get_unwind_recursion(
   {
     const symbolt &symbol=ns.lookup(id);
 
-    statistics() << (abort?"Not unwinding":"Unwinding")
-                 << " recursion "
-                 << symbol.display_name()
-                 << " iteration " << unwind;
+    log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " recursion "
+                     << symbol.display_name() << " iteration " << unwind;
 
     if(this_loop_limit!=std::numeric_limits<unsigned>::max())
-      statistics() << " (" << this_loop_limit << " max)";
+      log.statistics() << " (" << this_loop_limit << " max)";
 
-    statistics() << eom;
+    log.statistics() << log.eom;
   }
 
   return abort;
@@ -194,7 +191,7 @@ void symex_bmct::no_body(const irep_idt &identifier)
 {
   if(body_warnings.insert(identifier).second)
   {
-    warning() <<
-      "**** WARNING: no body for function " << identifier << eom;
+    log.warning() << "**** WARNING: no body for function " << identifier
+                  << log.eom;
   }
 }
diff --git a/src/cbmc/symex_bmc.h b/src/cbmc/symex_bmc.h
index b8d23a52719..ba483840be2 100644
--- a/src/cbmc/symex_bmc.h
+++ b/src/cbmc/symex_bmc.h
@@ -18,12 +18,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "symex_coverage.h"
 
-class symex_bmct:
-  public goto_symext,
-  public messaget
+class symex_bmct: public goto_symext
 {
 public:
   symex_bmct(
+    message_handlert &mh,
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
     symex_targett &_target);
diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp
index 518765e11ab..0359d926e2a 100644
--- a/src/goto-instrument/accelerate/accelerate.cpp
+++ b/src/goto-instrument/accelerate/accelerate.cpp
@@ -109,14 +109,14 @@ int acceleratet::accelerate_loop(goto_programt::targett &loop_header)
   program.update();
 
 #if 1
-  enumerating_loop_accelerationt
-    acceleration(
-      symbol_table,
-      goto_functions,
-      program,
-      loop,
-      loop_header,
-      accelerate_limit);
+  enumerating_loop_accelerationt acceleration(
+    message_handler,
+    symbol_table,
+    goto_functions,
+    program,
+    loop,
+    loop_header,
+    accelerate_limit);
 #else
   disjunctive_polynomial_accelerationt
     acceleration(symbol_table, goto_functions, program, loop, loop_header);
@@ -333,7 +333,7 @@ void acceleratet::set_dirty_vars(path_acceleratort &accelerator)
 
     if(jt==dirty_vars_map.end())
     {
-      scratch_programt scratch(symbol_table);
+      scratch_programt scratch(symbol_table, message_handler);
       symbolt new_sym=utils.fresh_symbol("accelerate::dirty", bool_typet());
       dirty_var=new_sym.symbol_expr();
       dirty_vars_map[*it]=dirty_var;
@@ -512,7 +512,7 @@ void acceleratet::insert_automaton(trace_automatont &automaton)
   // machine.
   for(const auto &sym : automaton.alphabet)
   {
-    scratch_programt state_machine(symbol_table);
+    scratch_programt state_machine(symbol_table, message_handler);
     trace_automatont::sym_range_pairt p=transitions.equal_range(sym);
 
     build_state_machine(p.first, p.second, accept_states, state, next_state,
@@ -648,15 +648,16 @@ int acceleratet::accelerate_loops()
   return num_accelerated;
 }
 
-
 void accelerate_functions(
   goto_modelt &goto_model,
+  message_handlert &message_handler,
   bool use_z3)
 {
   Forall_goto_functions(it, goto_model.goto_functions)
   {
     std::cout << "Accelerating function " << it->first << '\n';
-    acceleratet accelerate(it->second.body, goto_model, use_z3);
+    acceleratet accelerate(
+      it->second.body, goto_model, message_handler, use_z3);
 
     int num_accelerated=accelerate.accelerate_loops();
 
diff --git a/src/goto-instrument/accelerate/accelerate.h b/src/goto-instrument/accelerate/accelerate.h
index 000fec39dbb..05dec188f28 100644
--- a/src/goto-instrument/accelerate/accelerate.h
+++ b/src/goto-instrument/accelerate/accelerate.h
@@ -14,6 +14,7 @@ Author: Matt Lewis
 
 #include <util/namespace.h>
 #include <util/expr.h>
+#include <util/message.h>
 
 #include <analyses/natural_loops.h>
 
@@ -28,15 +29,18 @@ Author: Matt Lewis
 
 class acceleratet
 {
- public:
-  acceleratet(goto_programt &_program,
-              goto_modelt &_goto_model,
-              bool _use_z3):
+public:
+  acceleratet(
+    goto_programt &_program,
+    goto_modelt &_goto_model,
+    message_handlert &message_handler,
+    bool _use_z3)
+    : message_handler(message_handler),
       program(_program),
       goto_functions(_goto_model.goto_functions),
       symbol_table(_goto_model.symbol_table),
       ns(_goto_model.symbol_table),
-      utils(symbol_table, goto_functions),
+      utils(symbol_table, message_handler, goto_functions),
       use_z3(_use_z3)
   {
     natural_loops(program);
@@ -51,46 +55,54 @@ class acceleratet
 
   static const int accelerate_limit = -1;
 
- protected:
-  void find_paths(goto_programt::targett &loop_header,
-                  pathst &loop_paths,
-                  pathst &exit_paths,
-                  goto_programt::targett &back_jump);
+protected:
+  message_handlert &message_handler;
 
-  void extend_path(goto_programt::targett &t,
-                   goto_programt::targett &loop_header,
-                   natural_loops_mutablet::natural_loopt &loop,
-                   patht &prefix,
-                   pathst &loop_paths,
-                   pathst &exit_paths,
-                   goto_programt::targett &back_jump);
+  void find_paths(
+    goto_programt::targett &loop_header,
+    pathst &loop_paths,
+    pathst &exit_paths,
+    goto_programt::targett &back_jump);
+
+  void extend_path(
+    goto_programt::targett &t,
+    goto_programt::targett &loop_header,
+    natural_loops_mutablet::natural_loopt &loop,
+    patht &prefix,
+    pathst &loop_paths,
+    pathst &exit_paths,
+    goto_programt::targett &back_jump);
 
   goto_programt::targett find_back_jump(goto_programt::targett loop_header);
 
-  void insert_looping_path(goto_programt::targett &loop_header,
-                           goto_programt::targett &back_jump,
-                           goto_programt &looping_path,
-                           patht &inserted_path);
-  void insert_accelerator(goto_programt::targett &loop_header,
-                          goto_programt::targett &back_jump,
-                          path_acceleratort &accelerator,
-                          subsumed_patht &subsumed);
+  void insert_looping_path(
+    goto_programt::targett &loop_header,
+    goto_programt::targett &back_jump,
+    goto_programt &looping_path,
+    patht &inserted_path);
+  void insert_accelerator(
+    goto_programt::targett &loop_header,
+    goto_programt::targett &back_jump,
+    path_acceleratort &accelerator,
+    subsumed_patht &subsumed);
 
   void set_dirty_vars(path_acceleratort &accelerator);
   void add_dirty_checks();
   bool is_underapproximate(path_acceleratort &accelerator);
 
-  void make_overflow_loc(goto_programt::targett loop_header,
-                         goto_programt::targett &loop_end,
-                         goto_programt::targett &overflow_loc);
+  void make_overflow_loc(
+    goto_programt::targett loop_header,
+    goto_programt::targett &loop_end,
+    goto_programt::targett &overflow_loc);
 
   void insert_automaton(trace_automatont &automaton);
-  void build_state_machine(trace_automatont::sym_mapt::iterator p,
-                           trace_automatont::sym_mapt::iterator end,
-                           state_sett &accept_states,
-                           symbol_exprt state,
-                           symbol_exprt next_state,
-                           scratch_programt &state_machine);
+  void build_state_machine(
+    trace_automatont::sym_mapt::iterator p,
+    trace_automatont::sym_mapt::iterator end,
+    state_sett &accept_states,
+    symbol_exprt state,
+    symbol_exprt next_state,
+    scratch_programt &state_machine);
 
   symbolt make_symbol(std::string name, typet type);
   void decl(symbol_exprt &sym, goto_programt::targett t);
@@ -117,6 +129,7 @@ class acceleratet
 
 void accelerate_functions(
   goto_modelt &,
+  message_handlert &message_handler,
   bool use_z3);
 
 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H
diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp
index b6089b22aa0..f9439941d93 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.cpp
+++ b/src/goto-instrument/accelerate/acceleration_utils.cpp
@@ -128,7 +128,7 @@ bool acceleration_utilst::check_inductive(
   // assert (target1==polynomial1);
   // assert (target2==polynomial2);
   // ...
-  scratch_programt program(symbol_table);
+  scratch_programt program(symbol_table, message_handler);
   std::vector<exprt> polynomials_hold;
   substitutiont substitution;
 
@@ -386,7 +386,7 @@ bool acceleration_utilst::do_assumptions(
   // assert(!precondition);
 
   exprt condition=precondition(path);
-  scratch_programt program(symbol_table);
+  scratch_programt program(symbol_table, message_handler);
 
   substitutiont substitution;
   stash_polynomials(program, polynomials, substitution, path);
diff --git a/src/goto-instrument/accelerate/acceleration_utils.h b/src/goto-instrument/accelerate/acceleration_utils.h
index e05c7ed48da..8d9046768ee 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.h
+++ b/src/goto-instrument/accelerate/acceleration_utils.h
@@ -16,6 +16,7 @@ Author: Matt Lewis
 #include <set>
 
 #include <util/symbol_table.h>
+#include <util/message.h>
 
 #include <goto-programs/goto_program.h>
 #include <goto-programs/goto_functions.h>
@@ -32,10 +33,16 @@ typedef std::unordered_map<exprt, exprt, irep_hash> expr_mapt;
 
 class acceleration_utilst
 {
- public:
-  acceleration_utilst(symbol_tablet &_symbol_table,
-                      const goto_functionst &_goto_functions,
-                      exprt &_loop_counter) :
+protected:
+  message_handlert &message_handler;
+
+public:
+  acceleration_utilst(
+    symbol_tablet &_symbol_table,
+    message_handlert &message_handler,
+    const goto_functionst &_goto_functions,
+    exprt &_loop_counter)
+    : message_handler(message_handler),
       symbol_table(_symbol_table),
       ns(symbol_table),
       goto_functions(_goto_functions),
@@ -43,8 +50,11 @@ class acceleration_utilst
   {
   }
 
-  acceleration_utilst(symbol_tablet &_symbol_table,
-                      const goto_functionst &_goto_functions) :
+  acceleration_utilst(
+    symbol_tablet &_symbol_table,
+    message_handlert &message_handler,
+    const goto_functionst &_goto_functions)
+    : message_handler(message_handler),
       symbol_table(_symbol_table),
       ns(symbol_table),
       goto_functions(_goto_functions),
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
index cbd10ccc48c..01da74d20f8 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -51,7 +51,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
   path_acceleratort &accelerator)
 {
   std::map<exprt, polynomialt> polynomials;
-  scratch_programt program(symbol_table);
+  scratch_programt program(symbol_table, message_handler);
 
   accelerator.clear();
 
@@ -144,7 +144,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
   expr_sett dirty;
   utils.find_modified(accelerator.path, dirty);
   polynomial_acceleratort path_acceleration(
-    symbol_table, goto_functions, loop_counter);
+    message_handler, symbol_table, goto_functions, loop_counter);
   goto_programt::instructionst assigns;
 
   for(patht::iterator it=accelerator.path.begin();
@@ -342,7 +342,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
 
 bool disjunctive_polynomial_accelerationt::find_path(patht &path)
 {
-  scratch_programt program(symbol_table);
+  scratch_programt program(symbol_table, message_handler);
 
   program.append(fixed);
   program.append(fixed);
@@ -410,7 +410,7 @@ bool disjunctive_polynomial_accelerationt::fit_polynomial(
   std::vector<expr_listt> parameters;
   std::set<std::pair<expr_listt, exprt> > coefficients;
   expr_listt exprs;
-  scratch_programt program(symbol_table);
+  scratch_programt program(symbol_table, message_handler);
   expr_sett influence;
 
   cone_of_influence(var, influence);
@@ -713,7 +713,7 @@ void disjunctive_polynomial_accelerationt::assert_for_values(
       {
         std::map<exprt, exprt>::iterator v_it=values.find(e);
 
-        assert(v_it!=values.end());
+        PRECONDITION(v_it!=values.end());
 
         mult_exprt mult(concrete_value, v_it->second);
         mult.swap(concrete_value);
@@ -791,9 +791,9 @@ void disjunctive_polynomial_accelerationt::build_path(
 
     const auto succs=goto_program.get_successors(t);
 
-    // We should have a looping path, so we should never hit a location
-    // with no successors.
-    assert(succs.size() > 0);
+    INVARIANT(succs.size() > 0,
+        "we should have a looping path, so we should never hit a location "
+        "with no successors.");
 
     if(succs.size()==1)
     {
@@ -824,7 +824,7 @@ void disjunctive_polynomial_accelerationt::build_path(
       }
     }
 
-    assert(found_branch);
+    PRECONDITION(found_branch);
 
     exprt cond=nil_exprt();
 
@@ -861,7 +861,7 @@ void disjunctive_polynomial_accelerationt::build_path(
  */
 void disjunctive_polynomial_accelerationt::build_fixed()
 {
-  scratch_programt scratch(symbol_table);
+  scratch_programt scratch(symbol_table, message_handler);
   std::map<exprt, exprt> shadow_distinguishers;
 
   fixed.copy_from(goto_program);
@@ -941,7 +941,7 @@ void disjunctive_polynomial_accelerationt::build_fixed()
 
     if(t->is_goto())
     {
-      assert(fixedt->is_goto());
+      PRECONDITION(fixedt->is_goto());
       // If this is a forwards jump, it's either jumping inside the loop
       // (in which case we leave it alone), or it jumps outside the loop.
       // If it jumps out of the loop, it's on a path we don't care about
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h
index 168c2c99888..c1888158359 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h
@@ -16,6 +16,7 @@ Author: Matt Lewis
 #include <set>
 
 #include <util/symbol_table.h>
+#include <util/message.h>
 
 #include <goto-programs/goto_program.h>
 #include <goto-programs/goto_functions.h>
@@ -34,18 +35,20 @@ class disjunctive_polynomial_accelerationt:public loop_accelerationt
 {
 public:
   disjunctive_polynomial_accelerationt(
+    message_handlert &message_handler,
     symbol_tablet &_symbol_table,
     goto_functionst &_goto_functions,
     goto_programt &_goto_program,
     natural_loops_mutablet::natural_loopt &_loop,
-    goto_programt::targett _loop_header):
-    symbol_table(_symbol_table),
-    ns(symbol_table),
-    goto_functions(_goto_functions),
-    goto_program(_goto_program),
-    loop(_loop),
-    loop_header(_loop_header),
-    utils(symbol_table, goto_functions, loop_counter)
+    goto_programt::targett _loop_header)
+    : message_handler(message_handler),
+      symbol_table(_symbol_table),
+      ns(symbol_table),
+      goto_functions(_goto_functions),
+      goto_program(_goto_program),
+      loop(_loop),
+      loop_header(_loop_header),
+      utils(symbol_table, message_handler, goto_functions, loop_counter)
   {
     loop_counter = nil_exprt();
     find_distinguishing_points();
@@ -63,6 +66,8 @@ class disjunctive_polynomial_accelerationt:public loop_accelerationt
   bool find_path(patht &path);
 
 protected:
+  message_handlert &message_handler;
+
   void assert_for_values(
     scratch_programt &program,
     std::map<exprt, exprt> &values,
diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h
index a9d03b7ad69..3a47032387a 100644
--- a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h
+++ b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h
@@ -31,21 +31,28 @@ class enumerating_loop_accelerationt:public loop_accelerationt
 {
 public:
   enumerating_loop_accelerationt(
+    message_handlert &message_handler,
     symbol_tablet &_symbol_table,
     goto_functionst &_goto_functions,
     goto_programt &_goto_program,
     natural_loops_mutablet::natural_loopt &_loop,
     goto_programt::targett _loop_header,
-    int _path_limit):
-    symbol_table(_symbol_table),
-    goto_functions(_goto_functions),
-    goto_program(_goto_program),
-    loop(_loop),
-    loop_header(_loop_header),
-    polynomial_accelerator(symbol_table, goto_functions),
-    path_limit(_path_limit),
-    path_enumerator(util_make_unique<sat_path_enumeratort>(
-      symbol_table, goto_functions, goto_program, loop, loop_header))
+    int _path_limit)
+    : symbol_table(_symbol_table),
+      goto_functions(_goto_functions),
+      goto_program(_goto_program),
+      loop(_loop),
+      loop_header(_loop_header),
+      polynomial_accelerator(message_handler, symbol_table, goto_functions),
+      path_limit(_path_limit),
+      path_enumerator(
+        util_make_unique<sat_path_enumeratort>(
+          message_handler,
+          symbol_table,
+          goto_functions,
+          goto_program,
+          loop,
+          loop_header))
   {
   }
 
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index 17ab6d79ab4..76f9345b425 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -59,7 +59,7 @@ bool polynomial_acceleratort::accelerate(
 
   expr_sett targets;
   std::map<exprt, polynomialt> polynomials;
-  scratch_programt program(symbol_table);
+  scratch_programt program(symbol_table, message_handler);
   goto_programt::instructionst assigns;
 
   utils.find_modified(body, targets);
@@ -288,7 +288,7 @@ bool polynomial_acceleratort::fit_polynomial_sliced(
   std::vector<expr_listt> parameters;
   std::set<std::pair<expr_listt, exprt> > coefficients;
   expr_listt exprs;
-  scratch_programt program(symbol_table);
+  scratch_programt program(symbol_table, message_handler);
   exprt overflow_var =
     utils.fresh_symbol("polynomial::overflow", bool_typet()).symbol_expr();
   overflow_instrumentert overflow(program, overflow_var, symbol_table);
@@ -457,7 +457,7 @@ bool polynomial_acceleratort::fit_const(
   return false;
 
 #if 0
-  scratch_programt program(symbol_table);
+  scratch_programt program(symbol_table, message_handler);
 
   program.append(body);
   program.add_instruction(ASSERT)->guard=equal_exprt(target, not_exprt(target));
@@ -668,7 +668,7 @@ bool polynomial_acceleratort::check_inductive(
   // assert (target1==polynomial1);
   // assert (target2==polynomial2);
   // ...
-  scratch_programt program(symbol_table);
+  scratch_programt program(symbol_table, message_handler);
   std::vector<exprt> polynomials_hold;
   substitutiont substitution;
 
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.h b/src/goto-instrument/accelerate/polynomial_accelerator.h
index 7530b66b849..3489e5ef941 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.h
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.h
@@ -33,25 +33,29 @@ class polynomial_acceleratort:public path_accelerationt
 {
 public:
   polynomial_acceleratort(
+    message_handlert &message_handler,
     const symbol_tablet &_symbol_table,
-    const goto_functionst &_goto_functions):
-    symbol_table(const_cast<symbol_tablet &>(_symbol_table)),
-    ns(symbol_table),
-    goto_functions(_goto_functions),
-    utils(symbol_table, goto_functions, loop_counter)
+    const goto_functionst &_goto_functions)
+    : message_handler(message_handler),
+      symbol_table(const_cast<symbol_tablet &>(_symbol_table)),
+      ns(symbol_table),
+      goto_functions(_goto_functions),
+      utils(symbol_table, message_handler, goto_functions, loop_counter)
   {
     loop_counter=nil_exprt();
   }
 
   polynomial_acceleratort(
+    message_handlert &message_handler,
     const symbol_tablet &_symbol_table,
     const goto_functionst &_goto_functions,
-    exprt &_loop_counter):
-    symbol_table(const_cast<symbol_tablet &>(_symbol_table)),
-    ns(symbol_table),
-    goto_functions(_goto_functions),
-    utils(symbol_table, goto_functions, loop_counter),
-    loop_counter(_loop_counter)
+    exprt &_loop_counter)
+    : message_handler(message_handler),
+      symbol_table(const_cast<symbol_tablet &>(_symbol_table)),
+      ns(symbol_table),
+      goto_functions(_goto_functions),
+      utils(symbol_table, message_handler, goto_functions, loop_counter),
+      loop_counter(_loop_counter)
   {
   }
 
@@ -63,6 +67,8 @@ class polynomial_acceleratort:public path_accelerationt
     polynomialt &polynomial);
 
 protected:
+  message_handlert &message_handler;
+
   bool fit_polynomial_sliced(
     goto_programt::instructionst &sliced_body,
     exprt &target,
diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
index 0d9c6a4eebc..40d3eca8b7a 100644
--- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp
+++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
@@ -48,7 +48,7 @@ Author: Matt Lewis
 
 bool sat_path_enumeratort::next(patht &path)
 {
-  scratch_programt program(symbol_table);
+  scratch_programt program(symbol_table, message_handler);
 
   program.append(fixed);
   program.append(fixed);
@@ -213,7 +213,7 @@ void sat_path_enumeratort::build_path(
  */
 void sat_path_enumeratort::build_fixed()
 {
-  scratch_programt scratch(symbol_table);
+  scratch_programt scratch(symbol_table, message_handler);
   std::map<exprt, exprt> shadow_distinguishers;
 
   fixed.copy_from(goto_program);
diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.h b/src/goto-instrument/accelerate/sat_path_enumerator.h
index c8b8b1747e9..7e086e22b39 100644
--- a/src/goto-instrument/accelerate/sat_path_enumerator.h
+++ b/src/goto-instrument/accelerate/sat_path_enumerator.h
@@ -35,18 +35,20 @@ class sat_path_enumeratort:public path_enumeratort
 {
 public:
   sat_path_enumeratort(
+    message_handlert &message_handler,
     symbol_tablet &_symbol_table,
     goto_functionst &_goto_functions,
     goto_programt &_goto_program,
     natural_loops_mutablet::natural_loopt &_loop,
-    goto_programt::targett _loop_header):
-    symbol_table(_symbol_table),
-    ns(symbol_table),
-    goto_functions(_goto_functions),
-    goto_program(_goto_program),
-    loop(_loop),
-    loop_header(_loop_header),
-    utils(symbol_table, goto_functions, loop_counter)
+    goto_programt::targett _loop_header)
+    : message_handler(message_handler),
+      symbol_table(_symbol_table),
+      ns(symbol_table),
+      goto_functions(_goto_functions),
+      goto_program(_goto_program),
+      loop(_loop),
+      loop_header(_loop_header),
+      utils(symbol_table, message_handler, goto_functions, loop_counter)
   {
     find_distinguishing_points();
     build_fixed();
@@ -55,6 +57,7 @@ class sat_path_enumeratort:public path_enumeratort
   bool next(patht &path);
 
 protected:
+  message_handlert &message_handler;
   void find_distinguishing_points();
 
   void build_path(scratch_programt &scratch_program, patht &path);
diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h
index a132f597c3a..86a0323d139 100644
--- a/src/goto-instrument/accelerate/scratch_program.h
+++ b/src/goto-instrument/accelerate/scratch_program.h
@@ -16,6 +16,7 @@ Author: Matt Lewis
 #include <string>
 
 #include <util/make_unique.h>
+#include <util/message.h>
 #include <util/symbol_table.h>
 
 #include <goto-programs/goto_program.h>
@@ -34,16 +35,16 @@ Author: Matt Lewis
 class scratch_programt:public goto_programt
 {
 public:
-  explicit scratch_programt(symbol_tablet &_symbol_table):
-    constant_propagation(true),
-    symbol_table(_symbol_table),
-    ns(symbol_table),
-    equation(ns),
-    symex(ns, symbol_table, equation),
-    satcheck(util_make_unique<satcheckt>()),
-    satchecker(ns, *satcheck),
-    z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
-    checker(&z3) // checker(&satchecker)
+  scratch_programt(symbol_tablet &_symbol_table, message_handlert &mh)
+    : constant_propagation(true),
+      symbol_table(_symbol_table),
+      ns(symbol_table),
+      equation(ns),
+      symex(mh, ns, symbol_table, equation),
+      satcheck(util_make_unique<satcheckt>()),
+      satchecker(ns, *satcheck),
+      z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
+      checker(&z3) // checker(&satchecker)
   {
   }
 
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 2218fd68235..a0562e33d73 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -694,7 +694,8 @@ int goto_instrument_parse_optionst::doit()
       goto_inline(goto_model, get_message_handler());
 
       status() << "Accelerating" << eom;
-      accelerate_functions(goto_model, cmdline.isset("z3"));
+      accelerate_functions(
+        goto_model, get_message_handler(), cmdline.isset("z3"));
       remove_skip(goto_model);
       goto_model.goto_functions.update();
     }
@@ -1018,7 +1019,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   if(cmdline.isset("function-inline"))
   {
     std::string function=cmdline.get_value("function-inline");
-    assert(!function.empty());
+    PRECONDITION(!function.empty());
 
     bool caching=!cmdline.isset("no-caching");
 
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 5535791e0aa..d300b3b25d4 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
 
 #include <util/options.h>
+#include <util/message.h>
 #include <util/byte_operators.h>
 
 #include <goto-programs/goto_functions.h>
@@ -42,18 +43,20 @@ class goto_symext
 {
 public:
   goto_symext(
+    message_handlert &mh,
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
-    symex_targett &_target):
-    total_vccs(0),
-    remaining_vccs(0),
-    constant_propagation(true),
-    new_symbol_table(_new_symbol_table),
-    language_mode(),
-    ns(_ns),
-    target(_target),
-    atomic_section_counter(0),
-    guard_identifier("goto_symex::\\guard")
+    symex_targett &_target)
+    : total_vccs(0),
+      remaining_vccs(0),
+      constant_propagation(true),
+      new_symbol_table(_new_symbol_table),
+      language_mode(),
+      ns(_ns),
+      target(_target),
+      atomic_section_counter(0),
+      log(mh),
+      guard_identifier("goto_symex::\\guard")
   {
     options.set_option("simplify", true);
     options.set_option("assertions", true);
@@ -139,6 +142,8 @@ class goto_symext
   symex_targett &target;
   unsigned atomic_section_counter;
 
+  mutable messaget log;
+
   friend class symex_dereference_statet;
 
   void new_name(symbolt &symbol);
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 0243f1487c2..9e88e8ab8e8 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-#include <iostream>
 #include <sstream>
 #include <cassert>
 
@@ -73,10 +72,13 @@ void goto_symext::parameter_assignments(
     // if you run out of actual arguments there was a mismatch
     if(it1==arguments.end())
     {
-      std::string warn=
-        "call to `"+id2string(function_identifier)+"': "
-        "not enough arguments, inserting non-deterministic value\n";
-      std::cerr << state.source.pc->source_location.as_string()+": "+warn;
+      log.warning() << state.source.pc->source_location.as_string()
+                    << ": "
+                       "call to `"
+                    << id2string(function_identifier)
+                    << "': "
+                       "not enough arguments, inserting non-deterministic value"
+                    << log.eom;
 
       rhs=side_effect_expr_nondett(parameter_type);
     }
@@ -193,7 +195,7 @@ void goto_symext::symex_function_call_symbol(
 {
   target.location(state.guard.as_expr(), state.source);
 
-  assert(code.function().id()==ID_symbol);
+  PRECONDITION(code.function().id() == ID_symbol);
 
   const irep_idt &identifier=
     to_symbol_expr(code.function()).get_identifier();
@@ -286,7 +288,7 @@ void goto_symext::symex_function_call_code(
     state.rename(a, ns);
 
   // produce a new frame
-  assert(!state.call_stack().empty());
+  PRECONDITION(!state.call_stack().empty());
   goto_symex_statet::framet &frame=state.new_frame();
 
   // preserve locality of local variables
@@ -320,7 +322,7 @@ void goto_symext::symex_function_call_code(
 /// pop one call frame
 void goto_symext::pop_frame(statet &state)
 {
-  assert(!state.call_stack().empty());
+  PRECONDITION(!state.call_stack().empty());
 
   {
     statet::framet &frame=state.top();
@@ -332,7 +334,7 @@ void goto_symext::pop_frame(statet &state)
     state.level1.restore_from(frame.old_level1);
 
     // clear function-locals from L2 renaming
-    assert(state.dirty);
+    PRECONDITION(state.dirty);
     for(goto_symex_statet::renaming_levelt::current_namest::iterator
         c_it=state.level2.current_names.begin();
         c_it!=state.level2.current_names.end();
@@ -432,7 +434,7 @@ void goto_symext::return_assignment(statet &state)
   statet::framet &frame=state.top();
 
   const goto_programt::instructiont &instruction=*state.source.pc;
-  assert(instruction.is_return());
+  PRECONDITION(instruction.is_return());
   const code_returnt &code=to_code_return(instruction.code);
 
   target.location(state.guard.as_expr(), state.source);