diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
index 77dd822eac5..5e661a8a38b 100644
--- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp
+++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -58,8 +58,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-analyzer/unreachable_instructions.h>
 
 janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
-  : parse_options_baset(JANALYZER_OPTIONS, argc, argv, ui_message_handler),
-    ui_message_handler(cmdline, std::string("JANALYZER ") + CBMC_VERSION)
+  : parse_options_baset(
+      JANALYZER_OPTIONS,
+      argc,
+      argv,
+      std::string("JANALYZER ") + CBMC_VERSION)
 {
 }
 
@@ -368,8 +371,7 @@ int janalyzer_parse_optionst::doit()
     return CPROVER_EXIT_USAGE_ERROR;
   }
 
-  goto_model =
-    initialize_goto_model(cmdline.args, log.get_message_handler(), options);
+  goto_model = initialize_goto_model(cmdline.args, ui_message_handler, options);
 
   if(process_goto_program(options))
     return CPROVER_EXIT_INTERNAL_ERROR;
@@ -387,10 +389,7 @@ int janalyzer_parse_optionst::doit()
     cmdline.isset("list-goto-functions"))
   {
     show_goto_functions(
-      goto_model,
-      log.get_message_handler(),
-      get_ui(),
-      cmdline.isset("list-goto-functions"));
+      goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -406,15 +405,14 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
 
     if(cmdline.isset("show-taint"))
     {
-      taint_analysis(
-        goto_model, taint_file, log.get_message_handler(), true, "");
+      taint_analysis(goto_model, taint_file, ui_message_handler, true, "");
       return CPROVER_EXIT_SUCCESS;
     }
     else
     {
       std::string json_file = cmdline.get_value("json");
       bool result = taint_analysis(
-        goto_model, taint_file, log.get_message_handler(), false, json_file);
+        goto_model, taint_file, ui_message_handler, false, json_file);
       return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS;
     }
   }
@@ -519,7 +517,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
 
   if(cmdline.isset("show-properties"))
   {
-    show_properties(goto_model, log.get_message_handler(), get_ui());
+    show_properties(goto_model, ui_message_handler);
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -570,12 +568,12 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
     else if(options.get_bool_option("verify"))
     {
       result = static_verifier(
-        goto_model, *analyzer, options, log.get_message_handler(), out);
+        goto_model, *analyzer, options, ui_message_handler, out);
     }
     else if(options.get_bool_option("simplify"))
     {
       result = static_simplifier(
-        goto_model, *analyzer, options, log.get_message_handler(), out);
+        goto_model, *analyzer, options, ui_message_handler, out);
     }
     else if(options.get_bool_option("unreachable-instructions"))
     {
@@ -616,18 +614,18 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
     log.status() << "Removing function pointers and virtual functions"
                  << messaget::eom;
     remove_function_pointers(
-      log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
+      ui_message_handler, goto_model, cmdline.isset("pointer-check"));
 
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
 
     // remove Java throw and catch
     // This introduces instanceof, so order is important:
-    remove_exceptions_using_instanceof(goto_model, log.get_message_handler());
+    remove_exceptions_using_instanceof(goto_model, ui_message_handler);
 
     // Java instanceof -> clsid comparison:
     class_hierarchyt class_hierarchy(goto_model.symbol_table);
-    remove_instanceof(goto_model, class_hierarchy, log.get_message_handler());
+    remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
 
     // do partial inlining
     log.status() << "Partial Inlining" << messaget::eom;
diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.h b/jbmc/src/janalyzer/janalyzer_parse_options.h
index 3140a94f72a..dc9af92502f 100644
--- a/jbmc/src/janalyzer/janalyzer_parse_options.h
+++ b/jbmc/src/janalyzer/janalyzer_parse_options.h
@@ -159,7 +159,6 @@ class janalyzer_parse_optionst : public parse_options_baset
   janalyzer_parse_optionst(int argc, const char **argv);
 
 protected:
-  ui_message_handlert ui_message_handler;
   goto_modelt goto_model;
 
   void register_languages();
@@ -171,11 +170,6 @@ class janalyzer_parse_optionst : public parse_options_baset
   virtual int perform_analysis(const optionst &options);
 
   ai_baset *build_analyzer(const optionst &, const namespacet &ns);
-
-  ui_message_handlert::uit get_ui()
-  {
-    return ui_message_handler.get_ui();
-  }
 };
 
 #endif // CPROVER_JANALYZER_JANALYZER_PARSE_OPTIONS_H
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 61dc2bef46f..bb00a58ea98 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -75,8 +75,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <java_bytecode/simple_method_stubbing.h>
 
 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
-  : parse_options_baset(JBMC_OPTIONS, argc, argv, ui_message_handler),
-    ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
+  : parse_options_baset(
+      JBMC_OPTIONS,
+      argc,
+      argv,
+      std::string("JBMC ") + CBMC_VERSION)
 {
 }
 
@@ -88,8 +91,7 @@ ::jbmc_parse_optionst::jbmc_parse_optionst(
       JBMC_OPTIONS + extra_options,
       argc,
       argv,
-      ui_message_handler),
-    ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
+      std::string("JBMC ") + CBMC_VERSION)
 {
 }
 
@@ -134,7 +136,7 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_SUCCESS);
   }
 
-  parse_path_strategy_options(cmdline, options, log.get_message_handler());
+  parse_path_strategy_options(cmdline, options, ui_message_handler);
 
   if(cmdline.isset("program-only"))
     options.set_option("program-only", true);
@@ -421,9 +423,7 @@ int jbmc_parse_optionst::doit()
   }
 
   messaget::eval_verbosity(
-    cmdline.get_value("verbosity"),
-    messaget::M_STATISTICS,
-    log.get_message_handler());
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // command line options
@@ -498,7 +498,7 @@ int jbmc_parse_optionst::doit()
     }
 
     language->set_language_options(options);
-    language->set_message_handler(log.get_message_handler());
+    language->set_message_handler(ui_message_handler);
 
     log.status() << "Parsing " << filename << messaget::eom;
 
@@ -747,7 +747,7 @@ void jbmc_parse_optionst::process_goto_function(
     goto_function,
     symbol_table,
     *class_hierarchy,
-    log.get_message_handler());
+    ui_message_handler);
   // Java virtual functions -> explicit dispatch tables:
   remove_virtual_functions(function);
 
@@ -851,7 +851,6 @@ bool jbmc_parse_optionst::show_loaded_functions(
     show_goto_functions(
       ns,
       ui_message_handler,
-      ui_message_handler.get_ui(),
       goto_model.get_goto_functions(),
       cmdline.isset("list-goto-functions"));
     return true;
@@ -860,11 +859,7 @@ bool jbmc_parse_optionst::show_loaded_functions(
   if(cmdline.isset("show-properties"))
   {
     namespacet ns(goto_model.get_symbol_table());
-    show_properties(
-      ns,
-      log.get_message_handler(),
-      ui_message_handler.get_ui(),
-      goto_model.get_goto_functions());
+    show_properties(ns, ui_message_handler, goto_model.get_goto_functions());
     return true;
   }
 
@@ -887,8 +882,7 @@ bool jbmc_parse_optionst::process_goto_functions(
     return false;
 
   // remove catch and throw
-  remove_exceptions(
-    goto_model, *class_hierarchy.get(), log.get_message_handler());
+  remove_exceptions(goto_model, *class_hierarchy.get(), ui_message_handler);
 
   // instrument library preconditions
   instrument_preconditions(goto_model);
@@ -910,7 +904,7 @@ bool jbmc_parse_optionst::process_goto_functions(
   {
     // Entry point will have been set before and function pointers removed
     log.status() << "Removing unused functions" << messaget::eom;
-    remove_unused_functions(goto_model, log.get_message_handler());
+    remove_unused_functions(goto_model, ui_message_handler);
   }
 
   // remove skips such that trivial GOTOs are deleted
diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
index b2685cab415..2fa213baf1a 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.h
+++ b/jbmc/src/jbmc/jbmc_parse_options.h
@@ -117,7 +117,6 @@ class jbmc_parse_optionst : public parse_options_baset
     bool body_available);
 
 protected:
-  ui_message_handlert ui_message_handler;
   java_object_factory_parameterst object_factory_params;
   bool stub_objects_are_not_null;
 
diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp
index 61e13fe60a9..627d324152d 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.cpp
+++ b/jbmc/src/jdiff/jdiff_parse_options.cpp
@@ -62,8 +62,11 @@ Author: Peter Schrammel
 #include <goto-diff/unified_diff.h>
 
 jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
-  : parse_options_baset(JDIFF_OPTIONS, argc, argv, ui_message_handler),
-    ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION)
+  : parse_options_baset(
+      JDIFF_OPTIONS,
+      argc,
+      argv,
+      std::string("JDIFF ") + CBMC_VERSION)
 {
 }
 
@@ -224,15 +227,9 @@ int jdiff_parse_optionst::doit()
     cmdline.isset("list-goto-functions"))
   {
     show_goto_functions(
-      goto_model1,
-      log.get_message_handler(),
-      ui_message_handler.get_ui(),
-      cmdline.isset("list-goto-functions"));
+      goto_model1, ui_message_handler, cmdline.isset("list-goto-functions"));
     show_goto_functions(
-      goto_model2,
-      log.get_message_handler(),
-      ui_message_handler.get_ui(),
-      cmdline.isset("list-goto-functions"));
+      goto_model2, ui_message_handler, cmdline.isset("list-goto-functions"));
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -277,18 +274,18 @@ bool jdiff_parse_optionst::process_goto_program(
     log.status() << "Removing function pointers and virtual functions"
                  << messaget::eom;
     remove_function_pointers(
-      log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
+      ui_message_handler, goto_model, cmdline.isset("pointer-check"));
 
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
 
     // remove Java throw and catch
     // This introduces instanceof, so order is important:
-    remove_exceptions_using_instanceof(goto_model, log.get_message_handler());
+    remove_exceptions_using_instanceof(goto_model, ui_message_handler);
 
     // Java instanceof -> clsid comparison:
     class_hierarchyt class_hierarchy(goto_model.symbol_table);
-    remove_instanceof(goto_model, class_hierarchy, log.get_message_handler());
+    remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
 
     mm_io(goto_model);
 
@@ -321,10 +318,9 @@ bool jdiff_parse_optionst::process_goto_program(
     // instrument cover goals
     if(cmdline.isset("cover"))
     {
-      const auto cover_config = get_cover_config(
-        options, goto_model.symbol_table, log.get_message_handler());
-      if(instrument_cover_goals(
-           cover_config, goto_model, log.get_message_handler()))
+      const auto cover_config =
+        get_cover_config(options, goto_model.symbol_table, ui_message_handler);
+      if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
         return true;
     }
 
diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h
index fcb144b43b0..c5d4fe736f4 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.h
+++ b/jbmc/src/jdiff/jdiff_parse_options.h
@@ -49,7 +49,6 @@ class jdiff_parse_optionst : public parse_options_baset
   jdiff_parse_optionst(int argc, const char **argv);
 
 protected:
-  ui_message_handlert ui_message_handler;
   void register_languages();
 
   void get_command_line_options(optionst &options);
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 2558212b9b0..9f8a85d91a6 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -83,9 +83,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "xml_interface.h"
 
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
-  : parse_options_baset(CBMC_OPTIONS, argc, argv, ui_message_handler),
-    xml_interfacet(cmdline),
-    ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION)
+  : parse_options_baset(
+      CBMC_OPTIONS,
+      argc,
+      argv,
+      std::string("CBMC ") + CBMC_VERSION),
+    xml_interfacet(cmdline)
 {
 }
 
@@ -97,9 +100,8 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
       CBMC_OPTIONS + extra_options,
       argc,
       argv,
-      ui_message_handler),
-    xml_interfacet(cmdline),
-    ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION)
+      std::string("CBMC ") + CBMC_VERSION),
+    xml_interfacet(cmdline)
 {
 }
 
@@ -484,7 +486,7 @@ int cbmc_parse_optionst::doit()
   register_languages();
 
   if(cmdline.isset("test-preprocessor"))
-    return test_c_preprocessor(log.get_message_handler())
+    return test_c_preprocessor(ui_message_handler)
              ? CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
              : CPROVER_EXIT_SUCCESS;
 
@@ -530,7 +532,7 @@ int cbmc_parse_optionst::doit()
     }
 
     language->set_language_options(options);
-    language->set_message_handler(log.get_message_handler());
+    language->set_message_handler(ui_message_handler);
 
     log.status() << "Parsing " << filename << messaget::eom;
 
@@ -545,7 +547,7 @@ int cbmc_parse_optionst::doit()
   }
 
   int get_goto_program_ret =
-    get_goto_program(goto_model, options, cmdline, log, ui_message_handler);
+    get_goto_program(goto_model, options, cmdline, ui_message_handler);
 
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
@@ -553,8 +555,7 @@ int cbmc_parse_optionst::doit()
   if(cmdline.isset("show-claims") || // will go away
      cmdline.isset("show-properties")) // use this one
   {
-    show_properties(
-      goto_model, log.get_message_handler(), ui_message_handler.get_ui());
+    show_properties(goto_model, ui_message_handler);
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -690,12 +691,12 @@ int cbmc_parse_optionst::get_goto_program(
   goto_modelt &goto_model,
   const optionst &options,
   const cmdlinet &cmdline,
-  messaget &log,
   ui_message_handlert &ui_message_handler)
 {
+  messaget log{ui_message_handler};
   if(cmdline.args.empty())
   {
-    log.error() << "Please provide a program to verify" << log.eom;
+    log.error() << "Please provide a program to verify" << messaget::eom;
     return CPROVER_EXIT_INCORRECT_TASK;
   }
 
@@ -732,12 +733,11 @@ int cbmc_parse_optionst::get_goto_program(
       show_goto_functions(
         goto_model,
         ui_message_handler,
-        ui_message_handler.get_ui(),
         cmdline.isset("list-goto-functions"));
       return CPROVER_EXIT_SUCCESS;
     }
 
-    log.status() << config.object_bits_info() << log.eom;
+    log.status() << config.object_bits_info() << messaget::eom;
   }
 
   return -1; // no error, continue
@@ -772,7 +772,7 @@ void cbmc_parse_optionst::preprocessing(const optionst &options)
       return;
     }
 
-    language->set_message_handler(log.get_message_handler());
+    language->set_message_handler(ui_message_handler);
 
     if(language->preprocess(infile, filename, std::cout))
       log.error() << "PREPROCESSING ERROR" << messaget::eom;
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index bc9ef50440c..c5cae07c4c6 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -106,12 +106,10 @@ class cbmc_parse_optionst : public parse_options_baset, public xml_interfacet
     goto_modelt &,
     const optionst &,
     const cmdlinet &,
-    messaget &,
     ui_message_handlert &);
 
 protected:
   goto_modelt goto_model;
-  ui_message_handlert ui_message_handler;
 
   void register_languages();
   void get_command_line_options(optionst &);
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 0bda5470a06..8b38b9188e6 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -69,8 +69,11 @@ Author: Daniel Kroening, kroening@kroening.com
 goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
   int argc,
   const char **argv)
-  : parse_options_baset(GOTO_ANALYSER_OPTIONS, argc, argv, ui_message_handler),
-    ui_message_handler(cmdline, std::string("GOTO-ANALYZER ") + CBMC_VERSION)
+  : parse_options_baset(
+      GOTO_ANALYSER_OPTIONS,
+      argc,
+      argv,
+      std::string("GOTO-ANALYZER "))
 {
 }
 
@@ -398,8 +401,7 @@ int goto_analyzer_parse_optionst::doit()
 
   register_languages();
 
-  goto_model =
-    initialize_goto_model(cmdline.args, log.get_message_handler(), options);
+  goto_model = initialize_goto_model(cmdline.args, ui_message_handler, options);
 
   if(process_goto_program(options))
     return CPROVER_EXIT_INTERNAL_ERROR;
@@ -422,10 +424,7 @@ int goto_analyzer_parse_optionst::doit()
     cmdline.isset("list-goto-functions"))
   {
     show_goto_functions(
-      goto_model,
-      log.get_message_handler(),
-      get_ui(),
-      cmdline.isset("list-goto-functions"));
+      goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -443,15 +442,14 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
     if(cmdline.isset("show-taint"))
     {
-      taint_analysis(
-        goto_model, taint_file, log.get_message_handler(), true, "");
+      taint_analysis(goto_model, taint_file, ui_message_handler, true, "");
       return CPROVER_EXIT_SUCCESS;
     }
     else
     {
       std::string json_file=cmdline.get_value("json");
       bool result = taint_analysis(
-        goto_model, taint_file, log.get_message_handler(), false, json_file);
+        goto_model, taint_file, ui_message_handler, false, json_file);
       return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS;
     }
   }
@@ -553,7 +551,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
   if(cmdline.isset("show-properties"))
   {
-    show_properties(goto_model, log.get_message_handler(), get_ui());
+    show_properties(goto_model, ui_message_handler);
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -607,13 +605,13 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
     }
     else if(options.get_bool_option("show-on-source"))
     {
-      show_on_source(goto_model, *analyzer, log.get_message_handler());
+      show_on_source(goto_model, *analyzer, ui_message_handler);
       return CPROVER_EXIT_SUCCESS;
     }
     else if(options.get_bool_option("verify"))
     {
       result = static_verifier(
-        goto_model, *analyzer, options, log.get_message_handler(), out);
+        goto_model, *analyzer, options, ui_message_handler, out);
     }
     else if(options.get_bool_option("simplify"))
     {
@@ -621,7 +619,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
       output_stream.close();
       output_stream.open(outfile, std::ios::binary);
       result = static_simplifier(
-        goto_model, *analyzer, options, log.get_message_handler(), out);
+        goto_model, *analyzer, options, ui_message_handler, out);
     }
     else if(options.get_bool_option("unreachable-instructions"))
     {
@@ -681,7 +679,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     log.status() << "Removing function pointers and virtual functions"
                  << messaget::eom;
     remove_function_pointers(
-      log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
+      ui_message_handler, goto_model, cmdline.isset("pointer-check"));
 
     // do partial inlining
     log.status() << "Partial Inlining" << messaget::eom;
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index ee063e657e4..3ef39630b76 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -162,7 +162,6 @@ class goto_analyzer_parse_optionst: public parse_options_baset
   goto_analyzer_parse_optionst(int argc, const char **argv);
 
 protected:
-  ui_message_handlert ui_message_handler;
   goto_modelt goto_model;
 
   virtual void register_languages();
@@ -174,11 +173,6 @@ class goto_analyzer_parse_optionst: public parse_options_baset
   virtual int perform_analysis(const optionst &options);
 
   ai_baset *build_analyzer(const optionst &, const namespacet &ns);
-
-  ui_message_handlert::uit get_ui()
-  {
-    return ui_message_handler.get_ui();
-  }
 };
 
 #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index a85ed2c1c78..2753ec1d1ba 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -64,8 +64,11 @@ Author: Peter Schrammel
 #include "change_impact.h"
 
 goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv)
-  : parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv, ui_message_handler),
-    ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION)
+  : parse_options_baset(
+      GOTO_DIFF_OPTIONS,
+      argc,
+      argv,
+      std::string("GOTO-DIFF ") + CBMC_VERSION)
 {
 }
 
@@ -262,15 +265,9 @@ int goto_diff_parse_optionst::doit()
     cmdline.isset("list-goto-functions"))
   {
     show_goto_functions(
-      goto_model1,
-      log.get_message_handler(),
-      ui_message_handler.get_ui(),
-      cmdline.isset("list-goto-functions"));
+      goto_model1, ui_message_handler, cmdline.isset("list-goto-functions"));
     show_goto_functions(
-      goto_model2,
-      log.get_message_handler(),
-      ui_message_handler.get_ui(),
-      cmdline.isset("list-goto-functions"));
+      goto_model2, ui_message_handler, cmdline.isset("list-goto-functions"));
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -323,15 +320,14 @@ bool goto_diff_parse_optionst::process_goto_program(
     log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
                  << messaget::eom;
     link_to_library(
-      goto_model, log.get_message_handler(), cprover_cpp_library_factory);
-    link_to_library(
-      goto_model, log.get_message_handler(), cprover_c_library_factory);
+      goto_model, ui_message_handler, cprover_cpp_library_factory);
+    link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
 
     // remove function pointers
     log.status() << "Removal of function pointers and virtual functions"
                  << messaget::eom;
     remove_function_pointers(
-      log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
+      ui_message_handler, goto_model, cmdline.isset("pointer-check"));
 
     mm_io(goto_model);
 
@@ -364,10 +360,9 @@ bool goto_diff_parse_optionst::process_goto_program(
       // for coverage annotation:
       remove_skip(goto_model);
 
-      const auto cover_config = get_cover_config(
-        options, goto_model.symbol_table, log.get_message_handler());
-      if(instrument_cover_goals(
-           cover_config, goto_model, log.get_message_handler()))
+      const auto cover_config =
+        get_cover_config(options, goto_model.symbol_table, ui_message_handler);
+      if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
         return true;
     }
 
diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h
index a350d061bf5..e46977d2fac 100644
--- a/src/goto-diff/goto_diff_parse_options.h
+++ b/src/goto-diff/goto_diff_parse_options.h
@@ -48,7 +48,6 @@ class goto_diff_parse_optionst : public parse_options_baset
   goto_diff_parse_optionst(int argc, const char **argv);
 
 protected:
-  ui_message_handlert ui_message_handler;
   void register_languages();
 
   void get_command_line_options(optionst &options);
diff --git a/src/goto-harness/goto_harness_main.cpp b/src/goto-harness/goto_harness_main.cpp
index 285970764df..7e9eb28fa5f 100644
--- a/src/goto-harness/goto_harness_main.cpp
+++ b/src/goto-harness/goto_harness_main.cpp
@@ -10,6 +10,5 @@ Author: Diffblue Ltd.
 
 int main(int argc, const char *argv[])
 {
-  auto parse_options = goto_harness_parse_optionst(argc, argv);
-  return parse_options.main();
+  return goto_harness_parse_optionst{argc, argv}.main();
 }
diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp
index 4a55b659cf0..343e88e8402 100644
--- a/src/goto-harness/goto_harness_parse_options.cpp
+++ b/src/goto-harness/goto_harness_parse_options.cpp
@@ -55,7 +55,7 @@ int goto_harness_parse_optionst::doit()
 
   // Read goto binary into goto-model
   auto read_goto_binary_result =
-    read_goto_binary(got_harness_config.in_file, log.get_message_handler());
+    read_goto_binary(got_harness_config.in_file, ui_message_handler);
   if(!read_goto_binary_result.has_value())
   {
     throw deserialization_exceptiont{"failed to read goto program from file `" +
@@ -89,7 +89,7 @@ int goto_harness_parse_optionst::doit()
 
   // Write end result to new goto-binary
   if(write_goto_binary(
-       got_harness_config.out_file, goto_model, log.get_message_handler()))
+       got_harness_config.out_file, goto_model, ui_message_handler))
   {
     throw system_exceptiont{"failed to write goto program from file `" +
                             got_harness_config.out_file + "'"};
@@ -126,8 +126,10 @@ void goto_harness_parse_optionst::help()
 goto_harness_parse_optionst::goto_harness_parse_optionst(
   int argc,
   const char *argv[])
-  : parse_options_baset{GOTO_HARNESS_OPTIONS, argc, argv, ui_message_handler},
-    ui_message_handler(cmdline, std::string("GOTO-HARNESS ") + CBMC_VERSION)
+  : parse_options_baset{GOTO_HARNESS_OPTIONS,
+                        argc,
+                        argv,
+                        std::string("GOTO-HARNESS ") + CBMC_VERSION}
 {
 }
 
diff --git a/src/goto-harness/goto_harness_parse_options.h b/src/goto-harness/goto_harness_parse_options.h
index c611d75e70b..edcf045bff8 100644
--- a/src/goto-harness/goto_harness_parse_options.h
+++ b/src/goto-harness/goto_harness_parse_options.h
@@ -45,8 +45,6 @@ class goto_harness_parse_optionst : public parse_options_baset
     irep_idt harness_function_name;
   };
 
-  ui_message_handlert ui_message_handler;
-
   /// Handle command line arguments that are common to all
   /// harness generators.
   goto_harness_configt handle_common_options();
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index a16a95021cc..c21c8935dc6 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -268,7 +268,8 @@ int goto_instrument_parse_optionst::doit()
       namespacet ns(goto_model.symbol_table);
       value_set_analysist value_set_analysis(ns);
       value_set_analysis(goto_model.goto_functions);
-      show_value_sets(get_ui(), goto_model, value_set_analysis);
+      show_value_sets(
+        ui_message_handler.get_ui(), goto_model, value_set_analysis);
       return CPROVER_EXIT_SUCCESS;
     }
 
@@ -345,7 +346,7 @@ int goto_instrument_parse_optionst::doit()
       do_remove_returns();
       parameter_assignments(goto_model);
 
-      remove_unused_functions(goto_model, log.get_message_handler());
+      remove_unused_functions(goto_model, ui_message_handler);
 
       if(!cmdline.isset("inline"))
       {
@@ -385,7 +386,7 @@ int goto_instrument_parse_optionst::doit()
       do_remove_returns();
       parameter_assignments(goto_model);
 
-      remove_unused_functions(goto_model, log.get_message_handler());
+      remove_unused_functions(goto_model, ui_message_handler);
 
       if(!cmdline.isset("inline"))
       {
@@ -556,7 +557,7 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("interpreter"))
     {
       log.status() << "Starting interpreter" << messaget::eom;
-      interpreter(goto_model, log.get_message_handler());
+      interpreter(goto_model, ui_message_handler);
       return CPROVER_EXIT_SUCCESS;
     }
 
@@ -564,7 +565,7 @@ int goto_instrument_parse_optionst::doit()
        cmdline.isset("show-properties"))
     {
       const namespacet ns(goto_model.symbol_table);
-      show_properties(goto_model, log.get_message_handler(), get_ui());
+      show_properties(goto_model, ui_message_handler);
       return CPROVER_EXIT_SUCCESS;
     }
 
@@ -584,7 +585,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-loops"))
     {
-      show_loop_ids(get_ui(), goto_model);
+      show_loop_ids(ui_message_handler.get_ui(), goto_model);
       return CPROVER_EXIT_SUCCESS;
     }
 
@@ -615,10 +616,7 @@ int goto_instrument_parse_optionst::doit()
       cmdline.isset("list-goto-functions"))
     {
       show_goto_functions(
-        goto_model,
-        log.get_message_handler(),
-        ui_message_handler.get_ui(),
-        cmdline.isset("list-goto-functions"));
+        goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
       return CPROVER_EXIT_SUCCESS;
     }
 
@@ -637,7 +635,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-locations"))
     {
-      show_locations(get_ui(), goto_model);
+      show_locations(ui_message_handler.get_ui(), goto_model);
       return CPROVER_EXIT_SUCCESS;
     }
 
@@ -760,7 +758,7 @@ int goto_instrument_parse_optionst::doit()
       namespacet ns(goto_model.symbol_table);
 
       log.status() << "Performing full inlining" << messaget::eom;
-      goto_inline(goto_model, log.get_message_handler());
+      goto_inline(goto_model, ui_message_handler);
 
       log.status() << "Removing calls to functions without a body"
                    << messaget::eom;
@@ -770,10 +768,7 @@ int goto_instrument_parse_optionst::doit()
       log.status() << "Accelerating" << messaget::eom;
       guard_managert guard_manager;
       accelerate_functions(
-        goto_model,
-        log.get_message_handler(),
-        cmdline.isset("z3"),
-        guard_manager);
+        goto_model, ui_message_handler, cmdline.isset("z3"), guard_manager);
       remove_skip(goto_model);
     }
 
@@ -810,8 +805,7 @@ int goto_instrument_parse_optionst::doit()
       do_indirect_call_and_rtti_removal();
 
       log.status() << "Removing unused functions" << messaget::eom;
-      remove_unused_functions(
-        goto_model.goto_functions, log.get_message_handler());
+      remove_unused_functions(goto_model.goto_functions, ui_message_handler);
     }
 
     if(cmdline.isset("undefined-function-is-assume-false"))
@@ -826,8 +820,7 @@ int goto_instrument_parse_optionst::doit()
       log.status() << "Writing GOTO program to `" << cmdline.args[1] << "'"
                    << messaget::eom;
 
-      if(write_goto_binary(
-           cmdline.args[1], goto_model, log.get_message_handler()))
+      if(write_goto_binary(cmdline.args[1], goto_model, ui_message_handler))
         return CPROVER_EXIT_CONVERSION_FAILED;
       else
         return CPROVER_EXIT_SUCCESS;
@@ -857,7 +850,7 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
 
   log.status() << "Function Pointer Removal" << messaget::eom;
   remove_function_pointers(
-    log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
+    ui_message_handler, goto_model, cmdline.isset("pointer-check"));
   log.status() << "Virtual function removal" << messaget::eom;
   remove_virtual_functions(goto_model);
   log.status() << "Cleaning inline assembler statements" << messaget::eom;
@@ -878,7 +871,7 @@ void goto_instrument_parse_optionst::do_remove_const_function_pointers_only()
 
   log.status() << "Removing const function pointers only" << messaget::eom;
   remove_function_pointers(
-    log.get_message_handler(),
+    ui_message_handler,
     goto_model,
     cmdline.isset("pointer-check"),
     true); // abort if we can't resolve via const pointers
@@ -916,7 +909,7 @@ void goto_instrument_parse_optionst::get_goto_program()
 
   config.set(cmdline);
 
-  auto result = read_goto_binary(cmdline.args[0], log.get_message_handler());
+  auto result = read_goto_binary(cmdline.args[0], ui_message_handler);
 
   if(!result.has_value())
     throw 0;
@@ -973,9 +966,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   {
     log.status() << "Adding gotos to skip loops" << messaget::eom;
     if(skip_loops(
-         goto_model,
-         cmdline.get_value("skip-loops"),
-         log.get_message_handler()))
+         goto_model, cmdline.get_value("skip-loops"), ui_message_handler))
       throw 0;
   }
 
@@ -989,7 +980,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
     log.status() << "Adding up to " << max_argc << " command line arguments"
                  << messaget::eom;
-    if(model_argc_argv(goto_model, max_argc, log.get_message_handler()))
+    if(model_argc_argv(goto_model, max_argc, ui_message_handler))
       throw 0;
   }
 
@@ -998,7 +989,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     remove_functions(
       goto_model,
       cmdline.get_values("remove-function-body"),
-      log.get_message_handler());
+      ui_message_handler);
   }
 
   // we add the library in some cases, as some analyses benefit
@@ -1017,9 +1008,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
                  << messaget::eom;
     link_to_library(
-      goto_model, log.get_message_handler(), cprover_cpp_library_factory);
-    link_to_library(
-      goto_model, log.get_message_handler(), cprover_c_library_factory);
+      goto_model, ui_message_handler, cprover_cpp_library_factory);
+    link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
   }
 
   // now do full inlining, if requested
@@ -1036,7 +1026,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     }
 
     log.status() << "Performing full inlining" << messaget::eom;
-    goto_inline(goto_model, log.get_message_handler(), true);
+    goto_inline(goto_model, ui_message_handler, true);
   }
 
   if(cmdline.isset("show-custom-bitvector-analysis") ||
@@ -1062,7 +1052,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     escape_analysis.instrument(goto_model);
 
     // inline added functions, they are often small
-    goto_partial_inline(goto_model, log.get_message_handler());
+    goto_partial_inline(goto_model, ui_message_handler);
 
     // recalculate numbers, etc.
     goto_model.goto_functions.update();
@@ -1108,24 +1098,15 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     if(!cmdline.isset("log"))
     {
       goto_function_inline(
-        goto_model,
-        function,
-        ui_message_handler,
-        true,
-        caching);
+        goto_model, function, ui_message_handler, true, caching);
     }
     else
     {
       std::string filename=cmdline.get_value("log");
       bool have_file=!filename.empty() && filename!="-";
 
-      jsont result=
-        goto_function_inline_and_log(
-          goto_model,
-          function,
-          ui_message_handler,
-          true,
-          caching);
+      jsont result = goto_function_inline_and_log(
+        goto_model, function, ui_message_handler, true, caching);
 
       if(have_file)
       {
@@ -1194,12 +1175,12 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       cmdline.get_value("generate-function-body-options"),
       object_factory_parameters,
       goto_model.symbol_table,
-      log.get_message_handler());
+      ui_message_handler);
     generate_function_bodies(
       std::regex(cmdline.get_value("generate-function-body")),
       *generate_implementation,
       goto_model,
-      log.get_message_handler());
+      ui_message_handler);
   }
 
   // add generic checks, if needed
@@ -1245,7 +1226,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     do_remove_returns();
 
     log.status() << "String Abstraction" << messaget::eom;
-    string_abstraction(goto_model, log.get_message_handler());
+    string_abstraction(goto_model, ui_message_handler);
   }
 
   // some analyses require function pointer removal and partial inlining
@@ -1358,7 +1339,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
           cmdline.isset("render-cluster-function"),
           cmdline.isset("cav11"),
           cmdline.isset("hide-internals"),
-          log.get_message_handler(),
+          ui_message_handler,
           cmdline.isset("ignore-arrays"));
     }
 
@@ -1507,7 +1488,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
          goto_model.goto_functions,
          callercallee,
          goto_model.symbol_table,
-         log.get_message_handler()))
+         ui_message_handler))
       throw 0;
   }
 
@@ -1521,7 +1502,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     slice_global_inits(goto_model);
 
     log.status() << "Performing an aggressive slice" << messaget::eom;
-    aggressive_slicert aggressive_slicer(goto_model, log.get_message_handler());
+    aggressive_slicert aggressive_slicer(goto_model, ui_message_handler);
 
     if(cmdline.isset("aggressive-slice-call-depth"))
       aggressive_slicer.call_depth =
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index e5b0b6c9e4c..ba46d872ed9 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -122,8 +122,7 @@ class goto_instrument_parse_optionst : public parse_options_baset
         GOTO_INSTRUMENT_OPTIONS,
         argc,
         argv,
-        ui_message_handler),
-      ui_message_handler(cmdline, "goto-instrument"),
+        "goto-instrument"),
       function_pointer_removal_done(false),
       partial_inlining_done(false),
       remove_returns_done(false)
@@ -131,7 +130,6 @@ class goto_instrument_parse_optionst : public parse_options_baset
   }
 
 protected:
-  ui_message_handlert ui_message_handler;
   void register_languages();
 
   void get_goto_program();
@@ -147,11 +145,6 @@ class goto_instrument_parse_optionst : public parse_options_baset
   bool remove_returns_done;
 
   goto_modelt goto_model;
-
-  ui_message_handlert::uit get_ui()
-  {
-    return ui_message_handler.get_ui();
-  }
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp
index 087a57bcbfd..d1f5c2a1b60 100644
--- a/src/goto-programs/show_goto_functions.cpp
+++ b/src/goto-programs/show_goto_functions.cpp
@@ -25,12 +25,12 @@ Author: Peter Schrammel
 
 void show_goto_functions(
   const namespacet &ns,
-  message_handlert &message_handler,
-  ui_message_handlert::uit ui,
+  ui_message_handlert &ui_message_handler,
   const goto_functionst &goto_functions,
   bool list_only)
 {
-  messaget msg(message_handler);
+  ui_message_handlert::uit ui = ui_message_handler.get_ui();
+  messaget msg(ui_message_handler);
   switch(ui)
   {
   case ui_message_handlert::uit::XML_UI:
@@ -82,11 +82,10 @@ void show_goto_functions(
 
 void show_goto_functions(
   const goto_modelt &goto_model,
-  message_handlert &message_handler,
-  ui_message_handlert::uit ui,
+  ui_message_handlert &ui_message_handler,
   bool list_only)
 {
   const namespacet ns(goto_model.symbol_table);
   show_goto_functions(
-    ns, message_handler, ui, goto_model.goto_functions, list_only);
+    ns, ui_message_handler, goto_model.goto_functions, list_only);
 }
diff --git a/src/goto-programs/show_goto_functions.h b/src/goto-programs/show_goto_functions.h
index db1510db64b..aec8c352c76 100644
--- a/src/goto-programs/show_goto_functions.h
+++ b/src/goto-programs/show_goto_functions.h
@@ -30,15 +30,13 @@ class goto_functionst;
 
 void show_goto_functions(
   const namespacet &ns,
-  message_handlert &message_handler,
-  ui_message_handlert::uit ui,
+  ui_message_handlert &ui_message_handler,
   const goto_functionst &goto_functions,
-  bool list_only = false);
+  bool list_only);
 
 void show_goto_functions(
   const goto_modelt &,
-  message_handlert &message_handler,
-  ui_message_handlert::uit ui,
-  bool list_only = false);
+  ui_message_handlert &ui_message_handler,
+  bool list_only);
 
 #endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_H
diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp
index b7172871445..a8cf43df408 100644
--- a/src/goto-programs/show_properties.cpp
+++ b/src/goto-programs/show_properties.cpp
@@ -163,25 +163,25 @@ void show_properties_json(
 
 void show_properties(
   const namespacet &ns,
-  message_handlert &message_handler,
-  ui_message_handlert::uit ui,
+  ui_message_handlert &ui_message_handler,
   const goto_functionst &goto_functions)
 {
+  ui_message_handlert::uit ui = ui_message_handler.get_ui();
   if(ui == ui_message_handlert::uit::JSON_UI)
-    show_properties_json(ns, message_handler, goto_functions);
+    show_properties_json(ns, ui_message_handler, goto_functions);
   else
     for(const auto &fct : goto_functions.function_map)
-      show_properties(ns, fct.first, message_handler, ui, fct.second.body);
+      show_properties(ns, fct.first, ui_message_handler, ui, fct.second.body);
 }
 
 void show_properties(
   const goto_modelt &goto_model,
-  message_handlert &message_handler,
-  ui_message_handlert::uit ui)
+  ui_message_handlert &ui_message_handler)
 {
+  ui_message_handlert::uit ui = ui_message_handler.get_ui();
   const namespacet ns(goto_model.symbol_table);
   if(ui == ui_message_handlert::uit::JSON_UI)
-    show_properties_json(ns, message_handler, goto_model.goto_functions);
+    show_properties_json(ns, ui_message_handler, goto_model.goto_functions);
   else
-    show_properties(ns, message_handler, ui, goto_model.goto_functions);
+    show_properties(ns, ui_message_handler, goto_model.goto_functions);
 }
diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h
index ea8cc46e4a7..f444f8d3e77 100644
--- a/src/goto-programs/show_properties.h
+++ b/src/goto-programs/show_properties.h
@@ -32,13 +32,11 @@ class message_handlert;
 
 void show_properties(
   const goto_modelt &,
-  message_handlert &message_handler,
-  ui_message_handlert::uit ui);
+  ui_message_handlert &ui_message_handler);
 
 void show_properties(
   const namespacet &ns,
-  message_handlert &message_handler,
-  ui_message_handlert::uit ui,
+  ui_message_handlert &ui_message_handler,
   const goto_functionst &goto_functions);
 
 /// \brief Returns a source_locationt that corresponds
diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp
index 67d04c6b697..c1bece29bab 100644
--- a/src/util/parse_options.cpp
+++ b/src/util/parse_options.cpp
@@ -28,23 +28,14 @@ parse_options_baset::parse_options_baset(
   const std::string &_optstring,
   int argc,
   const char **argv,
-  message_handlert &mh)
-  : log(mh)
+  const std::string &program)
+  : parse_result(cmdline.parse(
+      argc,
+      argv,
+      (std::string("?h(help)") + _optstring).c_str())),
+    ui_message_handler(cmdline, program),
+    log(ui_message_handler)
 {
-  std::string optstring=std::string("?h(help)")+_optstring;
-  parse_result=cmdline.parse(argc, argv, optstring.c_str());
-
-  // DO NOT USE log HERE!
-  //
-  // The usual pattern of use is that the application class inherits from
-  // messaget and parse_options_baset using a member variable of type
-  // message_handlert to construct the messaget part.
-  //
-  // C++'s rules of initialisation mean that the constructors for
-  // messaget and then parse_options_base run before those of message_handlert.
-  // This means that the message_handlert object is uninitialised.
-  // Using it here will likely cause a hard to debug failure somewhere in
-  // the messaget code.
 }
 
 void parse_options_baset::help()
diff --git a/src/util/parse_options.h b/src/util/parse_options.h
index 54bac8c4bc8..6cfdbcf9ad9 100644
--- a/src/util/parse_options.h
+++ b/src/util/parse_options.h
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "cmdline.h"
 #include "message.h"
+#include "ui_message.h"
 
 class parse_options_baset
 {
@@ -22,7 +23,7 @@ class parse_options_baset
     const std::string &optstring,
     int argc,
     const char **argv,
-    message_handlert &mh);
+    const std::string &program);
 
   cmdlinet cmdline;
 
@@ -34,12 +35,15 @@ class parse_options_baset
   virtual int main();
   virtual ~parse_options_baset() { }
 
+private:
+  bool parse_result;
+
 protected:
+  ui_message_handlert ui_message_handler;
   messaget log;
 
 private:
   void unknown_option_msg();
-  bool parse_result;
 };
 
 std::string
diff --git a/unit/compound_block_locations.cpp b/unit/compound_block_locations.cpp
index 1365ab8e51e..e71679b04ba 100644
--- a/unit/compound_block_locations.cpp
+++ b/unit/compound_block_locations.cpp
@@ -289,7 +289,7 @@ void compound_block_locationst::check_compound_block_locations(
 
   goto_modelt gm;
   int ret;
-  ret = cbmc_parse_optionst::get_goto_program(gm, opts, cmdline, log, mh);
+  ret = cbmc_parse_optionst::get_goto_program(gm, opts, cmdline, mh);
   REQUIRE(ret == -1);
 
   const auto found = gm.goto_functions.function_map.find("main");
diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp
index 6061077a615..6d8ddd0248c 100644
--- a/unit/path_strategies.cpp
+++ b/unit/path_strategies.cpp
@@ -398,7 +398,7 @@ void _check_with_strategy(
   goto_modelt goto_model;
   int ret;
   ret = cbmc_parse_optionst::get_goto_program(
-    goto_model, options, cmdline, log, ui_message_handler);
+    goto_model, options, cmdline, ui_message_handler);
   REQUIRE(ret == -1);
 
   symbol_tablet symex_symbol_table;