diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
index 90fc5790998..d41ce83d7b0 100644
--- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp
+++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -58,8 +58,8 @@ 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),
-    messaget(ui_message_handler),
+  : messaget(ui_message_handler),
+    parse_options_baset(JANALYZER_OPTIONS, argc, argv, *this),
     ui_message_handler(cmdline, std::string("JANALYZER ") + CBMC_VERSION)
 {
 }
@@ -355,29 +355,8 @@ int janalyzer_parse_optionst::doit()
 
   register_languages();
 
-  try
-  {
-    goto_model =
-      initialize_goto_model(cmdline.args, get_message_handler(), options);
-  }
-
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(int e)
-  {
-    error() << "Numeric exception: " << e << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
+  goto_model =
+    initialize_goto_model(cmdline.args, get_message_handler(), options);
 
   if(process_goto_program(options))
     return CPROVER_EXIT_INTERNAL_ERROR;
@@ -402,34 +381,7 @@ int janalyzer_parse_optionst::doit()
     return CPROVER_EXIT_SUCCESS;
   }
 
-  try
-  {
-    return perform_analysis(options);
-  }
-
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(int e)
-  {
-    error() << "Numeric exception: " << e << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
-  }
+  return perform_analysis(options);
 }
 
 /// Depending on the command line mode, run one of the analysis tasks
@@ -554,8 +506,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
     return CPROVER_EXIT_SUCCESS;
   }
 
-  if(set_properties())
-    return CPROVER_EXIT_SET_PROPERTIES_FAILED;
+  if(cmdline.isset("property"))
+    ::set_properties(goto_model, cmdline.get_values("property"));
 
   if(options.get_bool_option("general-analysis"))
   {
@@ -637,34 +589,6 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
   return CPROVER_EXIT_USAGE_ERROR;
 }
 
-bool janalyzer_parse_optionst::set_properties()
-{
-  try
-  {
-    if(cmdline.isset("property"))
-      ::set_properties(goto_model, cmdline.get_values("property"));
-  }
-
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(int)
-  {
-    return true;
-  }
-
-  return false;
-}
-
 bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
 {
   try
diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.h b/jbmc/src/janalyzer/janalyzer_parse_options.h
index cd3ac664ae2..d0ce84724ed 100644
--- a/jbmc/src/janalyzer/janalyzer_parse_options.h
+++ b/jbmc/src/janalyzer/janalyzer_parse_options.h
@@ -150,7 +150,7 @@ class optionst;
   JAVA_BYTECODE_LANGUAGE_OPTIONS
 // clang-format on
 
-class janalyzer_parse_optionst : public parse_options_baset, public messaget
+class janalyzer_parse_optionst : public messaget, public parse_options_baset
 {
 public:
   virtual int doit() override;
@@ -167,7 +167,6 @@ class janalyzer_parse_optionst : public parse_options_baset, public messaget
   virtual void get_command_line_options(optionst &options);
 
   virtual bool process_goto_program(const optionst &options);
-  bool set_properties();
 
   virtual int perform_analysis(const optionst &options);
 
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 4ab56be7ee1..03472a92767 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -70,8 +70,8 @@ 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),
-    messaget(ui_message_handler),
+  : messaget(ui_message_handler),
+    parse_options_baset(JBMC_OPTIONS, argc, argv, *this),
     ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
 {
 }
@@ -80,8 +80,8 @@ ::jbmc_parse_optionst::jbmc_parse_optionst(
   int argc,
   const char **argv,
   const std::string &extra_options)
-  : parse_options_baset(JBMC_OPTIONS + extra_options, argc, argv),
-    messaget(ui_message_handler),
+  : messaget(ui_message_handler),
+    parse_options_baset(JBMC_OPTIONS + extra_options, argc, argv, *this),
     ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
 {
 }
@@ -425,22 +425,7 @@ int jbmc_parse_optionst::doit()
   //
 
   optionst options;
-  try
-  {
-    get_command_line_options(options);
-  }
-
-  catch(const char *error_msg)
-  {
-    error() << error_msg << eom;
-    return 6; // should contemplate EX_SOFTWARE from sysexits.h
-  }
-
-  catch(const std::string &error_msg)
-  {
-    error() << error_msg << eom;
-    return 6; // should contemplate EX_SOFTWARE from sysexits.h
-  }
+  get_command_line_options(options);
 
   //
   // Print a banner
@@ -636,28 +621,8 @@ int jbmc_parse_optionst::doit()
 
 bool jbmc_parse_optionst::set_properties(goto_modelt &goto_model)
 {
-  try
-  {
-    if(cmdline.isset("property"))
-      ::set_properties(goto_model, cmdline.get_values("property"));
-  }
-
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(int)
-  {
-    return true;
-  }
+  if(cmdline.isset("property"))
+    ::set_properties(goto_model, cmdline.get_values("property"));
 
   return false;
 }
@@ -672,7 +637,6 @@ int jbmc_parse_optionst::get_goto_program(
     return 6;
   }
 
-  try
   {
     lazy_goto_modelt lazy_goto_model=lazy_goto_modelt::from_handler_object(
       *this, options, get_message_handler());
@@ -738,29 +702,6 @@ int jbmc_parse_optionst::get_goto_program(
     status() << config.object_bits_info() << eom;
   }
 
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return 6;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return 6;
-  }
-
-  catch(int)
-  {
-    return 6;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    return 6;
-  }
-
   return -1; // no error, continue
 }
 
@@ -776,7 +717,6 @@ void jbmc_parse_optionst::process_goto_function(
   bool using_symex_driven_loading =
     options.get_bool_option("symex-driven-lazy-loading");
 
-  try
   {
     // Removal of RTTI inspection:
     remove_instanceof(
@@ -861,24 +801,6 @@ void jbmc_parse_optionst::process_goto_function(
     // update the function member in each instruction
     function.update_instructions_function();
   }
-
-  catch(const char *e)
-  {
-    error() << e << eom;
-    throw;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    throw;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    throw;
-  }
 }
 
 bool jbmc_parse_optionst::show_loaded_functions(
@@ -933,7 +855,6 @@ bool jbmc_parse_optionst::process_goto_functions(
   goto_modelt &goto_model,
   const optionst &options)
 {
-  try
   {
     status() << "Running GOTO functions transformation passes" << eom;
 
@@ -1021,29 +942,6 @@ bool jbmc_parse_optionst::process_goto_functions(
     remove_skip(goto_model);
   }
 
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(int)
-  {
-    return true;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    return true;
-  }
-
   return false;
 }
 
diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
index 5e9b39f5f68..3d5493a128f 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.h
+++ b/jbmc/src/jbmc/jbmc_parse_options.h
@@ -84,9 +84,7 @@ class optionst;
   "(symex-driven-lazy-loading)"
 // clang-format on
 
-class jbmc_parse_optionst:
-  public parse_options_baset,
-  public messaget
+class jbmc_parse_optionst : public messaget, public parse_options_baset
 {
 public:
   virtual int doit() override;
diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp
index 683a8d1f7c7..526ccedbefd 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.cpp
+++ b/jbmc/src/jdiff/jdiff_parse_options.cpp
@@ -63,8 +63,8 @@ Author: Peter Schrammel
 // TODO: do not use language_uit for this; requires a refactoring of
 //   initialize_goto_model to support parsing specific command line files
 jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
-  : parse_options_baset(JDIFF_OPTIONS, argc, argv),
-    jdiff_languagest(cmdline, ui_message_handler, &options),
+  : jdiff_languagest(cmdline, ui_message_handler, &options),
+    parse_options_baset(JDIFF_OPTIONS, argc, argv, *this),
     ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION),
     languages2(cmdline, ui_message_handler, &options)
 {
@@ -74,8 +74,8 @@ ::jdiff_parse_optionst::jdiff_parse_optionst(
   int argc,
   const char **argv,
   const std::string &extra_options)
-  : parse_options_baset(JDIFF_OPTIONS + extra_options, argc, argv),
-    jdiff_languagest(cmdline, ui_message_handler, &options),
+  : jdiff_languagest(cmdline, ui_message_handler, &options),
+    parse_options_baset(JDIFF_OPTIONS + extra_options, argc, argv, *this),
     ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION),
     languages2(cmdline, ui_message_handler, &options)
 {
@@ -342,7 +342,6 @@ bool jdiff_parse_optionst::process_goto_program(
   const optionst &options,
   goto_modelt &goto_model)
 {
-  try
   {
     // remove function pointers
     status() << "Removing function pointers and virtual functions" << eom;
@@ -407,31 +406,6 @@ bool jdiff_parse_optionst::process_goto_program(
     goto_model.goto_functions.update();
   }
 
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(int e)
-  {
-    error() << "Numeric exception: " << e << eom;
-    return true;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
-    return true;
-  }
-
   return false;
 }
 
diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h
index e56f44633ee..41f4ddf6c58 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.h
+++ b/jbmc/src/jdiff/jdiff_parse_options.h
@@ -42,7 +42,7 @@ class goto_modelt;
   "(compact-output)"
 // clang-format on
 
-class jdiff_parse_optionst : public parse_options_baset, public jdiff_languagest
+class jdiff_parse_optionst : public jdiff_languagest, public parse_options_baset
 {
 public:
   virtual int doit();
diff --git a/regression/cbmc/json-ui/no_entry.desc b/regression/cbmc/json-ui/no_entry.desc
index 949d5e73631..ea376532787 100644
--- a/regression/cbmc/json-ui/no_entry.desc
+++ b/regression/cbmc/json-ui/no_entry.desc
@@ -1,10 +1,10 @@
-KNOWNBUG
+CORE
 no_entry.c
 --json-ui
 activate-multi-line-match
 ^EXIT=6$
 ^SIGNAL=0$
-"messageText": "the program has no entry point",[\n ]*"messageType": "ERROR",
+"messageText": "the program has no entry point",[\n ]*"messageType": "ERROR"
 --
 ^warning: ignoring
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/json-ui/syntax_error.desc b/regression/cbmc/json-ui/syntax_error.desc
index 7c35f907dfb..b7c3530a7bc 100644
--- a/regression/cbmc/json-ui/syntax_error.desc
+++ b/regression/cbmc/json-ui/syntax_error.desc
@@ -1,10 +1,10 @@
-KNOWNBUG
+CORE
 syntax_error.c
 --json-ui
 activate-multi-line-match
 ^EXIT=6$
 ^SIGNAL=0$
-"messageText": "syntax error before .*",[\n ]*"messageType": "ERROR",[\n ]*"sourceLocation": {[\n ]*"file": "syntax_error.c",[\n ]*"function": "main",[\n ]*"line": "4",
+"messageText": "syntax error before .*",[\n ]*"messageType": "ERROR",[\n ]*"sourceLocation": \{[\n ]*"file": "syntax_error.c",[\n ]*"function": "main",[\n ]*"line": "4",
 --
 ^warning: ignoring
 ^VERIFICATION SUCCESSFUL$
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index b1407a5d71e..5c6dd02eeb6 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -71,9 +71,9 @@ 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),
+  : messaget(ui_message_handler),
+    parse_options_baset(CBMC_OPTIONS, argc, argv, *this),
     xml_interfacet(cmdline),
-    messaget(ui_message_handler),
     ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION)
 {
 }
@@ -82,9 +82,9 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
   int argc,
   const char **argv,
   const std::string &extra_options)
-  : parse_options_baset(CBMC_OPTIONS + extra_options, argc, argv),
+  : messaget(ui_message_handler),
+    parse_options_baset(CBMC_OPTIONS + extra_options, argc, argv, *this),
     xml_interfacet(cmdline),
-    messaget(ui_message_handler),
     ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION)
 {
 }
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 1b26e83ab7e..5ba0c3205bb 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -83,10 +83,9 @@ class optionst;
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 
-class cbmc_parse_optionst:
-  public parse_options_baset,
-  public xml_interfacet,
-  public messaget
+class cbmc_parse_optionst : public messaget,
+                            public parse_options_baset,
+                            public xml_interfacet
 {
 public:
   virtual int doit() override;
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index a54e6f8b0a5..28a61c75abc 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -67,8 +67,8 @@ 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),
-    messaget(ui_message_handler),
+  : messaget(ui_message_handler),
+    parse_options_baset(GOTO_ANALYSER_OPTIONS, argc, argv, *this),
     ui_message_handler(cmdline, std::string("GOTO-ANALYZER ") + CBMC_VERSION)
 {
 }
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index 02cbaa59ce6..9517a8be598 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -154,8 +154,8 @@ class optionst;
 // clang-format on
 
 class goto_analyzer_parse_optionst:
-  public parse_options_baset,
-  public messaget
+  public messaget,
+  public parse_options_baset
 {
 public:
   virtual int doit() override;
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 5342c761ce0..f0d88c54070 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -61,8 +61,8 @@ 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),
-    goto_diff_languagest(cmdline, ui_message_handler),
+  : goto_diff_languagest(cmdline, ui_message_handler),
+    parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv, *this),
     ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION),
     languages2(cmdline, ui_message_handler)
 {
@@ -72,8 +72,8 @@ ::goto_diff_parse_optionst::goto_diff_parse_optionst(
   int argc,
   const char **argv,
   const std::string &extra_options)
-  : parse_options_baset(GOTO_DIFF_OPTIONS + extra_options, argc, argv),
-    goto_diff_languagest(cmdline, ui_message_handler),
+  : goto_diff_languagest(cmdline, ui_message_handler),
+    parse_options_baset(GOTO_DIFF_OPTIONS + extra_options, argc, argv, *this),
     ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION),
     languages2(cmdline, ui_message_handler)
 {
diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h
index e7822385f8d..1fb0beca8ce 100644
--- a/src/goto-diff/goto_diff_parse_options.h
+++ b/src/goto-diff/goto_diff_parse_options.h
@@ -41,9 +41,8 @@ class optionst;
   "(compact-output)"
 // clang-format on
 
-class goto_diff_parse_optionst:
-  public parse_options_baset,
-  public goto_diff_languagest
+class goto_diff_parse_optionst : public goto_diff_languagest,
+                                 public parse_options_baset
 {
 public:
   virtual int doit();
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index 7e70a1ff1d7..c1dfee56281 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -111,21 +111,20 @@ Author: Daniel Kroening, kroening@kroening.com
 
 // clang-format on
 
-class goto_instrument_parse_optionst:
-  public parse_options_baset,
-  public messaget
+class goto_instrument_parse_optionst : public messaget,
+                                       public parse_options_baset
 {
 public:
   virtual int doit();
   virtual void help();
 
-  goto_instrument_parse_optionst(int argc, const char **argv):
-    parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv),
-    messaget(ui_message_handler),
-    ui_message_handler(cmdline, "goto-instrument"),
-    function_pointer_removal_done(false),
-    partial_inlining_done(false),
-    remove_returns_done(false)
+  goto_instrument_parse_optionst(int argc, const char **argv)
+    : messaget(ui_message_handler),
+      parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv, *this),
+      ui_message_handler(cmdline, "goto-instrument"),
+      function_pointer_removal_done(false),
+      partial_inlining_done(false),
+      remove_returns_done(false)
   {
   }
 
diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp
index 1b556f85c3f..041ac3e6426 100644
--- a/src/util/parse_options.cpp
+++ b/src/util/parse_options.cpp
@@ -22,13 +22,30 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "cmdline.h"
 #include "exception_utils.h"
 #include "exit_codes.h"
+#include "message.h"
 #include "signal_catcher.h"
 
 parse_options_baset::parse_options_baset(
-  const std::string &_optstring, int argc, const char **argv)
+  const std::string &_optstring,
+  int argc,
+  const char **argv,
+  messaget &l)
+  : log(l)
 {
   std::string optstring=std::string("?h(help)")+_optstring;
   parse_result=cmdline.parse(argc, argv, optstring.c_str());
+
+  // DO NOT USE l 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 messaget object has a reference to a
+  // an uninitialised object.  Using it here will likely cause a
+  // hard to debug failure somewhere in the messaget code.
 }
 
 void parse_options_baset::help()
@@ -37,7 +54,7 @@ void parse_options_baset::help()
 
 void parse_options_baset::usage_error()
 {
-  std::cerr << "Usage error!\n\n";
+  log.error() << "Usage error!\n" << messaget::eom;;
   help();
 }
 
@@ -46,7 +63,7 @@ void parse_options_baset::usage_error()
 void parse_options_baset::unknown_option_msg()
 {
   if(!cmdline.unknown_arg.empty())
-    std::cerr << "Unknown option: " << cmdline.unknown_arg << "\n";
+    log.error() << "Unknown option: " << cmdline.unknown_arg << messaget::eom;
 }
 
 int parse_options_baset::main()
@@ -77,43 +94,43 @@ int parse_options_baset::main()
   // CPROVER style exceptions in order of decreasing happiness
   catch(const invalid_command_line_argument_exceptiont &e)
   {
-    std::cerr << e.what() << '\n';
+    log.error() << e.what() << messaget::eom;
     return CPROVER_EXIT_USAGE_ERROR;
   }
   catch(const cprover_exception_baset &e)
   {
-    std::cerr << e.what() << '\n';
+    log.error() << e.what() << messaget::eom;
     return CPROVER_EXIT_EXCEPTION;
   }
   catch(const std::string &e)
   {
-    std::cerr << "C++ string exception : " << e << '\n';
+    log.error() << "C++ string exception : " << e << messaget::eom;
     return CPROVER_EXIT_EXCEPTION;
   }
   catch(const char *e)
   {
-    std::cerr << "C string exception : " << e << '\n';
+    log.error() << "C string exception : " << e << messaget::eom;
     return CPROVER_EXIT_EXCEPTION;
   }
   catch(int e)
   {
-    std::cerr << "Numeric exception : " << e << '\n';
+    log.error() << "Numeric exception : " << e << messaget::eom;
     return CPROVER_EXIT_EXCEPTION;
   }
   // C++ style exceptions
   catch(const std::bad_alloc &)
   {
-    std::cerr << "Out of memory" << '\n';
+    log.error() << "Out of memory" << messaget::eom;
     return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
   }
   catch(const std::exception &e)
   {
-    std::cerr << e.what() << '\n';
+    log.error() << e.what() << messaget::eom;
     return CPROVER_EXIT_EXCEPTION;
   }
   catch(...)
   {
-    std::cerr << "Unknown exception type!" << '\n';
+    log.error() << "Unknown exception type!" << messaget::eom;
     return CPROVER_EXIT_EXCEPTION;
   }
 }
diff --git a/src/util/parse_options.h b/src/util/parse_options.h
index 304657c6879..b1700a41890 100644
--- a/src/util/parse_options.h
+++ b/src/util/parse_options.h
@@ -14,11 +14,17 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "cmdline.h"
 
+// Forwards declare messaget so we can use references to it
+class messaget;
+
 class parse_options_baset
 {
 public:
   parse_options_baset(
-    const std::string &optstring, int argc, const char **argv);
+    const std::string &optstring,
+    int argc,
+    const char **argv,
+    messaget &l);
 
   cmdlinet cmdline;
 
@@ -30,6 +36,9 @@ class parse_options_baset
   virtual int main();
   virtual ~parse_options_baset() { }
 
+protected:
+  messaget &log;
+
 private:
   void unknown_option_msg();
   bool parse_result;