diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 90aa52ea8c0..c72826326d9 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -433,22 +433,7 @@ int cbmc_parse_optionst::doit()
   //
 
   optionst options;
-  try
-  {
-    get_command_line_options(options);
-  }
-
-  catch(const char *error_msg)
-  {
-    error() << error_msg << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(const std::string &error_msg)
-  {
-    error() << error_msg << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
+  get_command_line_options(options);
 
   eval_verbosity(
     cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
@@ -575,32 +560,11 @@ int cbmc_parse_optionst::doit()
 
 bool cbmc_parse_optionst::set_properties()
 {
-  try
-  {
-    if(cmdline.isset("claim")) // will go away
-      ::set_properties(goto_model, cmdline.get_values("claim"));
+  if(cmdline.isset("claim")) // will go away
+    ::set_properties(goto_model, cmdline.get_values("claim"));
 
-    if(cmdline.isset("property")) // use this one
-      ::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 e)
-  {
-    error() << "Numeric exception : " << e << eom;
-    return true;
-  }
+  if(cmdline.isset("property")) // use this one
+    ::set_properties(goto_model, cmdline.get_values("property"));
 
   return false;
 }
@@ -618,7 +582,6 @@ int cbmc_parse_optionst::get_goto_program(
     return CPROVER_EXIT_INCORRECT_TASK;
   }
 
-  try
   {
     goto_model =
       initialize_goto_model(cmdline.args, ui_message_handler, options);
@@ -655,42 +618,11 @@ int cbmc_parse_optionst::get_goto_program(
     log.status() << config.object_bits_info() << log.eom;
   }
 
-  catch(incorrect_goto_program_exceptiont &e)
-  {
-    log.error() << e.what() << log.eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(const char *e)
-  {
-    log.error() << e << log.eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(const std::string &e)
-  {
-    log.error() << e << log.eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(int e)
-  {
-    log.error() << "Numeric exception : " << e << log.eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    log.error() << "Out of memory" << log.eom;
-    return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
-  }
-
   return -1; // no error, continue
 }
 
 void cbmc_parse_optionst::preprocessing(const optionst &options)
 {
-  try
   {
     if(cmdline.args.size()!=1)
     {
@@ -722,27 +654,6 @@ void cbmc_parse_optionst::preprocessing(const optionst &options)
     if(language->preprocess(infile, filename, std::cout))
       error() << "PREPROCESSING ERROR" << eom;
   }
-
-  catch(const char *e)
-  {
-    error() << e << eom;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-  }
-
-  catch(int e)
-  {
-    error() << "Numeric exception : " << e << eom;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
-  }
 }
 
 bool cbmc_parse_optionst::process_goto_program(
@@ -750,7 +661,6 @@ bool cbmc_parse_optionst::process_goto_program(
   const optionst &options,
   messaget &log)
 {
-  try
   {
     // Remove inline assembler; this needs to happen before
     // adding the library.
@@ -878,31 +788,6 @@ bool cbmc_parse_optionst::process_goto_program(
     remove_skip(goto_model);
   }
 
-  catch(const char *e)
-  {
-    log.error() << e << eom;
-    return true;
-  }
-
-  catch(const std::string &e)
-  {
-    log.error() << e << eom;
-    return true;
-  }
-
-  catch(int e)
-  {
-    log.error() << "Numeric exception : " << e << eom;
-    return true;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    log.error() << "Out of memory" << eom;
-    exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
-    return true;
-  }
-
   return false;
 }
 
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 9bc226c9a62..0487e82211c 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -396,29 +396,8 @@ int goto_analyzer_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;
@@ -448,34 +427,7 @@ int goto_analyzer_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);
 }
 
 
@@ -603,8 +555,8 @@ int goto_analyzer_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"))
   {
@@ -713,38 +665,9 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
   return CPROVER_EXIT_USAGE_ERROR;
 }
 
-bool goto_analyzer_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 goto_analyzer_parse_optionst::process_goto_program(
   const optionst &options)
 {
-  try
   {
     #if 0
     // Remove inline assembler; this needs to happen before
@@ -786,30 +709,6 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     // add loop ids
     goto_model.goto_functions.compute_loop_numbers();
   }
-
-  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/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index d0c8342d1e9..02cbaa59ce6 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -172,7 +172,6 @@ class goto_analyzer_parse_optionst:
   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/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 1fc55a1280b..db3b506cb12 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -386,7 +386,6 @@ bool goto_diff_parse_optionst::process_goto_program(
   const optionst &options,
   goto_modelt &goto_model)
 {
-  try
   {
     // Remove inline assembler; this needs to happen before
     // adding the library.
@@ -450,31 +449,6 @@ bool goto_diff_parse_optionst::process_goto_program(
     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 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/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 7e191181b58..ce2ca697688 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -121,7 +121,6 @@ int goto_instrument_parse_optionst::doit()
   eval_verbosity(
     cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
-  try
   {
     register_languages();
 
@@ -823,30 +822,6 @@ int goto_instrument_parse_optionst::doit()
     help();
     return CPROVER_EXIT_USAGE_ERROR;
   }
-
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT;
-  }
-
-  catch(int e)
-  {
-    error() << "Numeric exception : " << e << eom;
-    return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT;
-  }
 // NOLINTNEXTLINE(readability/fn_size)
 }
 
diff --git a/src/util/exit_codes.h b/src/util/exit_codes.h
index 3b5cdc8b007..3b1eafba4ed 100644
--- a/src/util/exit_codes.h
+++ b/src/util/exit_codes.h
@@ -40,7 +40,6 @@ Author: Martin Brain, martin.brain@diffblue.com
 /// An (unanticipated) exception was thrown during computation.
 #define CPROVER_EXIT_EXCEPTION 6
 // should contemplate EX_SOFTWARE from sysexits.h
-#define CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT 11
 
 /// An error has been encountered during processing the requested analysis.
 #define CPROVER_EXIT_INTERNAL_ERROR 6
diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp
index 03719c03094..5c1db010b2e 100644
--- a/src/util/parse_options.cpp
+++ b/src/util/parse_options.cpp
@@ -71,9 +71,11 @@ int parse_options_baset::main()
 
     return doit();
   }
+
+  // CPROVER style exceptions in order of decreasing happiness
   catch(const invalid_command_line_argument_exceptiont &e)
   {
-    std::cerr << e.what() << "\n";
+    std::cerr << e.what() << '\n';
     return CPROVER_EXIT_USAGE_ERROR;
   }
   catch(const cprover_exception_baset &e)
@@ -81,6 +83,37 @@ int parse_options_baset::main()
     std::cerr << e.what() << '\n';
     return CPROVER_EXIT_EXCEPTION;
   }
+  catch(const std::string &e)
+  {
+    std::cerr << "C++ string exception : " << e << '\n';
+    return CPROVER_EXIT_EXCEPTION;
+  }
+  catch(const char *e)
+  {
+    std::cerr << "C string exception : " << e << '\n';
+    return CPROVER_EXIT_EXCEPTION;
+  }
+  catch(int e)
+  {
+    std::cerr << "Numeric exception : " << e << '\n';
+    return CPROVER_EXIT_EXCEPTION;
+  }
+  // C++ style exceptions
+  catch(const std::bad_alloc &)
+  {
+    std::cerr << "Out of memory" << '\n';
+    return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
+  }
+  catch(const std::exception &e)
+  {
+    std::cerr << e.what() << '\n';
+    return CPROVER_EXIT_EXCEPTION;
+  }
+  catch(...)
+  {
+    std::cerr << "Unknown exception type!" << '\n';
+    return CPROVER_EXIT_EXCEPTION;
+  }
 }
 
 std::string