diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
index afd8feab06c..1aa6b69ad69 100644
--- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp
+++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -51,7 +51,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/options.h>
-#include <util/string2int.h>
 #include <util/unicode.h>
 
 #include <cbmc/version.h>
@@ -74,21 +73,6 @@ void janalyzer_parse_optionst::register_languages()
   register_language(new_java_bytecode_language);
 }
 
-void janalyzer_parse_optionst::eval_verbosity()
-{
-  // this is our default verbosity
-  unsigned int v = messaget::M_STATISTICS;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v = unsafe_string2unsigned(cmdline.get_value("verbosity"));
-    if(v > 10)
-      v = 10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 void janalyzer_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -356,7 +340,8 @@ int janalyzer_parse_optionst::doit()
 
   optionst options;
   get_command_line_options(options);
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // Print a banner
diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.h b/jbmc/src/janalyzer/janalyzer_parse_options.h
index cfe867cd329..cd3ac664ae2 100644
--- a/jbmc/src/janalyzer/janalyzer_parse_options.h
+++ b/jbmc/src/janalyzer/janalyzer_parse_options.h
@@ -173,8 +173,6 @@ class janalyzer_parse_optionst : public parse_options_baset, public messaget
 
   ai_baset *build_analyzer(const optionst &, const namespacet &ns);
 
-  void eval_verbosity();
-
   ui_message_handlert::uit get_ui()
   {
     return ui_message_handler.get_ui();
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 328dc639156..630fc2a283a 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <memory>
 
 #include <util/exit_codes.h>
-#include <util/string2int.h>
 #include <util/config.h>
 #include <util/unicode.h>
 #include <util/invariant.h>
@@ -82,21 +81,6 @@ ::jbmc_parse_optionst::jbmc_parse_optionst(
 {
 }
 
-void jbmc_parse_optionst::eval_verbosity()
-{
-  // this is our default verbosity
-  unsigned int v=messaget::M_STATISTICS;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-    if(v>10)
-      v=10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 void jbmc_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -443,7 +427,8 @@ int jbmc_parse_optionst::doit()
     return 6; // should contemplate EX_SOFTWARE from sysexits.h
   }
 
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // Print a banner
diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
index f176a96bce5..6de84d59d97 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:
   object_factory_parameterst object_factory_params;
   bool stub_objects_are_not_null;
 
-  void eval_verbosity();
   void get_command_line_options(optionst &);
   int get_goto_program(
     std::unique_ptr<goto_modelt> &goto_model, const optionst &);
diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp
index 3773dd4dce0..5cf3135aba6 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.cpp
+++ b/jbmc/src/jdiff/jdiff_parse_options.cpp
@@ -20,7 +20,6 @@ Author: Peter Schrammel
 #include <util/exit_codes.h>
 #include <util/make_unique.h>
 #include <util/options.h>
-#include <util/string2int.h>
 
 #include <langapi/language.h>
 
@@ -82,21 +81,6 @@ ::jdiff_parse_optionst::jdiff_parse_optionst(
 {
 }
 
-void jdiff_parse_optionst::eval_verbosity()
-{
-  // this is our default verbosity
-  unsigned int v = messaget::M_STATISTICS;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v = unsafe_string2unsigned(cmdline.get_value("verbosity"));
-    if(v > 10)
-      v = 10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 void jdiff_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -211,7 +195,8 @@ int jdiff_parse_optionst::doit()
 
   optionst options;
   get_command_line_options(options);
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // Print a banner
diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h
index 9c306aa1f75..b23af102930 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.h
+++ b/jbmc/src/jdiff/jdiff_parse_options.h
@@ -66,8 +66,6 @@ class jdiff_parse_optionst : public parse_options_baset, public jdiff_languagest
   virtual bool
   process_goto_program(const optionst &options, goto_modelt &goto_model);
 
-  void eval_verbosity();
-
   void preprocessing();
 };
 
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 35069fc9665..ec6fe1ee02e 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 #include <memory>
 
-#include <util/string2int.h>
 #include <util/config.h>
 #include <util/unicode.h>
 #include <util/invariant.h>
@@ -100,21 +99,6 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("arrays-uf", "auto");
 }
 
-void cbmc_parse_optionst::eval_verbosity()
-{
-  // this is our default verbosity
-  unsigned int v=messaget::M_STATISTICS;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-    if(v>10)
-      v=10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 void cbmc_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -435,7 +419,8 @@ int cbmc_parse_optionst::doit()
     return CPROVER_EXIT_EXCEPTION;
   }
 
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // Print a banner
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 55da16b09d8..24204c061b4 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -112,7 +112,6 @@ class cbmc_parse_optionst:
   ui_message_handlert ui_message_handler;
   const path_strategy_choosert path_strategy_chooser;
 
-  void eval_verbosity();
   void register_languages();
   void get_command_line_options(optionst &);
   void preprocessing();
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index fa21fa905c2..0d0c637c75d 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <fstream>
 #include <cstdlib>
 
-#include <util/string2int.h>
 #include <util/config.h>
 #include <util/options.h>
 #include <util/memory_info.h>
@@ -45,23 +44,6 @@ clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv):
 {
 }
 
-void clobber_parse_optionst::eval_verbosity()
-{
-  // this is our default verbosity
-  int v=messaget::M_STATISTICS;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v=unsafe_string2int(cmdline.get_value("verbosity"));
-    if(v<0)
-      v=0;
-    else if(v>10)
-      v=10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 void clobber_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -115,7 +97,8 @@ int clobber_parse_optionst::doit()
   optionst options;
   get_command_line_options(options);
 
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   goto_modelt goto_model;
 
diff --git a/src/clobber/clobber_parse_options.h b/src/clobber/clobber_parse_options.h
index 5dd3fc12b84..fd35c90940d 100644
--- a/src/clobber/clobber_parse_options.h
+++ b/src/clobber/clobber_parse_options.h
@@ -66,8 +66,6 @@ class clobber_parse_optionst:
   void report_success();
   void report_failure();
   void show_counterexample(const class goto_tracet &);
-
-  void eval_verbosity();
 };
 
 #endif // CPROVER_CLOBBER_CLOBBER_PARSE_OPTIONS_H
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 5758a5e4523..7022fc3d771 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -47,7 +47,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/options.h>
 #include <util/config.h>
-#include <util/string2int.h>
 #include <util/unicode.h>
 #include <util/exit_codes.h>
 
@@ -76,21 +75,6 @@ void goto_analyzer_parse_optionst::register_languages()
   register_language(new_jsil_language);
 }
 
-void goto_analyzer_parse_optionst::eval_verbosity()
-{
-  // this is our default verbosity
-  unsigned int v=messaget::M_STATISTICS;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-    if(v>10)
-      v=10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -381,7 +365,8 @@ int goto_analyzer_parse_optionst::doit()
 
   optionst options;
   get_command_line_options(options);
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // Print a banner
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index 1ec346ffa36..9392ab2e7f8 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -175,8 +175,6 @@ class goto_analyzer_parse_optionst:
 
   ai_baset *build_analyzer(const optionst &, const namespacet &ns);
 
-  void eval_verbosity();
-
   ui_message_handlert::uit get_ui()
   {
     return ui_message_handler.get_ui();
diff --git a/src/goto-cc/armcc_mode.cpp b/src/goto-cc/armcc_mode.cpp
index b297ade1246..03a3a0e689a 100644
--- a/src/goto-cc/armcc_mode.cpp
+++ b/src/goto-cc/armcc_mode.cpp
@@ -21,7 +21,6 @@ Author: CM Wintersteiger, 2006
 
 #include <iostream>
 
-#include <util/string2int.h>
 #include <util/message.h>
 #include <util/prefix.h>
 #include <util/config.h>
@@ -37,8 +36,6 @@ int armcc_modet::doit()
     return EX_OK;
   }
 
-  unsigned int verbosity=1;
-
   compilet compiler(cmdline, message_handler, cmdline.isset("diag_error="));
 
   #if 0
@@ -49,11 +46,8 @@ int armcc_modet::doit()
     has_prefix(base_name, "goto-link");
   #endif
 
-  if(cmdline.isset("verbosity"))
-    verbosity=unsafe_string2int(cmdline.get_value("verbosity"));
-
-  compiler.set_message_handler(get_message_handler());
-  message_handler.set_verbosity(verbosity);
+  const auto verbosity = eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_ERROR, message_handler);
 
   debug() << "ARM mode" << eom;
 
@@ -136,7 +130,7 @@ int armcc_modet::doit()
     compiler.output_file_executable="a.out";
   }
 
-  if(verbosity>8)
+  if(verbosity > messaget::M_STATISTICS)
   {
     std::list<std::string>::iterator it;
 
diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp
index bf69e209eda..2ad810a4c0f 100644
--- a/src/goto-cc/as_mode.cpp
+++ b/src/goto-cc/as_mode.cpp
@@ -24,7 +24,6 @@ Author: Michael Tautschnig
 #include <cstring>
 
 #include <util/run.h>
-#include <util/string2int.h>
 #include <util/tempdir.h>
 #include <util/config.h>
 #include <util/get_base_name.h>
@@ -76,8 +75,6 @@ int as_modet::doit()
     return EX_OK;
   }
 
-  unsigned int verbosity=1;
-
   bool act_as_as86=
     base_name=="as86" ||
     base_name.find("goto-as86")!=std::string::npos;
@@ -101,13 +98,10 @@ int as_modet::doit()
     return EX_OK; // Exit!
   }
 
-  if(cmdline.isset("w-") || cmdline.isset("warn"))
-    verbosity=2;
-
-  if(cmdline.isset("verbosity"))
-    verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-
-  message_handler.set_verbosity(verbosity);
+  auto default_verbosity = (cmdline.isset("w-") || cmdline.isset("warn")) ?
+    messaget::M_WARNING : messaget::M_ERROR;
+  eval_verbosity(
+    cmdline.get_value("verbosity"), default_verbosity, message_handler);
 
   if(act_as_as86)
   {
diff --git a/src/goto-cc/cw_mode.cpp b/src/goto-cc/cw_mode.cpp
index ee84c58959b..eed01de1d55 100644
--- a/src/goto-cc/cw_mode.cpp
+++ b/src/goto-cc/cw_mode.cpp
@@ -21,7 +21,6 @@ Author: CM Wintersteiger, 2006
 
 #include <iostream>
 
-#include <util/string2int.h>
 #include <util/message.h>
 #include <util/prefix.h>
 #include <util/config.h>
@@ -37,8 +36,6 @@ int cw_modet::doit()
     return EX_OK;
   }
 
-  unsigned int verbosity=1;
-
   compilet compiler(cmdline, message_handler, cmdline.isset("Werror"));
 
   #if 0
@@ -49,11 +46,8 @@ int cw_modet::doit()
     has_prefix(base_name, "goto-link");
   #endif
 
-  if(cmdline.isset("verbosity"))
-    verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-
-  compiler.set_message_handler(get_message_handler());
-  message_handler.set_verbosity(verbosity);
+  const auto verbosity = eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_ERROR, message_handler);
 
   debug() << "CodeWarrior mode" << eom;
 
@@ -125,7 +119,7 @@ int cw_modet::doit()
       config.ansi_c.preprocessor_options.push_back("-isystem "+*it);
   }
 
-  if(verbosity>8)
+  if(verbosity > messaget::M_STATISTICS)
   {
     std::list<std::string>::iterator it;
 
diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp
index fade9d0307b..e989c886307 100644
--- a/src/goto-cc/gcc_mode.cpp
+++ b/src/goto-cc/gcc_mode.cpp
@@ -34,7 +34,6 @@ Author: CM Wintersteiger, 2006
 #include <util/expr.h>
 #include <util/c_types.h>
 #include <util/arith_tools.h>
-#include <util/string2int.h>
 #include <util/invariant.h>
 #include <util/tempdir.h>
 #include <util/tempfile.h>
@@ -331,15 +330,10 @@ int gcc_modet::doit()
     linker_name(cmdline, base_name) :
     compiler_name(cmdline, base_name);
 
-  unsigned int verbosity=1;
-
-  if(cmdline.isset("Wall") || cmdline.isset("Wextra"))
-    verbosity=2;
-
-  if(cmdline.isset("verbosity"))
-    verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-
-  gcc_message_handler.set_verbosity(verbosity);
+  auto default_verbosity = (cmdline.isset("Wall") || cmdline.isset("Wextra")) ?
+    messaget::M_WARNING : messaget::M_ERROR;
+  eval_verbosity(
+    cmdline.get_value("verbosity"), default_verbosity, gcc_message_handler);
 
   bool act_as_bcc=
     base_name=="bcc" ||
diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
index d89900d11f3..94e6cfb4a3d 100644
--- a/src/goto-cc/linker_script_merge.cpp
+++ b/src/goto-cc/linker_script_merge.cpp
@@ -685,9 +685,9 @@ int linker_script_merget::get_linker_script_data(
     "--out-file", def_out_file
   };
 
-  if(get_message_handler().get_verbosity()>9)
+  if(get_message_handler().get_verbosity() >= messaget::M_DEBUG)
     argv.push_back("--very-verbose");
-  else if(get_message_handler().get_verbosity()>4)
+  else if(get_message_handler().get_verbosity() > messaget::M_RESULT)
     argv.push_back("--verbose");
 
   debug() << "RUN:";
diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp
index 946a6454710..4e9c3789c19 100644
--- a/src/goto-cc/ms_cl_mode.cpp
+++ b/src/goto-cc/ms_cl_mode.cpp
@@ -21,7 +21,6 @@ Author: CM Wintersteiger, 2006
 
 #include <iostream>
 
-#include <util/string2int.h>
 #include <util/message.h>
 #include <util/prefix.h>
 #include <util/config.h>
@@ -50,8 +49,6 @@ int ms_cl_modet::doit()
     return EX_OK;
   }
 
-  unsigned int verbosity=1;
-
   compilet compiler(cmdline, message_handler, cmdline.isset("WX"));
 
   #if 0
@@ -60,11 +57,8 @@ int ms_cl_modet::doit()
     has_prefix(base_name, "goto-link");
   #endif
 
-  if(cmdline.isset("verbosity"))
-    verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-
-  compiler.set_message_handler(get_message_handler());
-  message_handler.set_verbosity(verbosity);
+  const auto verbosity = eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_ERROR, message_handler);
 
   debug() << "Visual Studio mode" << eom;
 
@@ -118,7 +112,7 @@ int ms_cl_modet::doit()
   if(cmdline.isset('J'))
     config.ansi_c.char_is_unsigned=true;
 
-  if(verbosity>8)
+  if(verbosity > messaget::M_STATISTICS)
   {
     std::list<std::string>::iterator it;
 
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index e181d1f72b3..73cc9655594 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -16,7 +16,6 @@ Author: Peter Schrammel
 #include <iostream>
 #include <memory>
 
-#include <util/string2int.h>
 #include <util/config.h>
 #include <util/options.h>
 #include <util/make_unique.h>
@@ -79,21 +78,6 @@ ::goto_diff_parse_optionst::goto_diff_parse_optionst(
 {
 }
 
-void goto_diff_parse_optionst::eval_verbosity()
-{
-  // this is our default verbosity
-  unsigned int v=messaget::M_STATISTICS;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-    if(v>10)
-      v=10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 void goto_diff_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -251,7 +235,8 @@ int goto_diff_parse_optionst::doit()
 
   optionst options;
   get_command_line_options(options);
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // Print a banner
diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h
index 2992b1ab615..e7822385f8d 100644
--- a/src/goto-diff/goto_diff_parse_options.h
+++ b/src/goto-diff/goto_diff_parse_options.h
@@ -70,8 +70,6 @@ class goto_diff_parse_optionst:
     const optionst &options,
     goto_modelt &goto_model);
 
-  void eval_verbosity();
-
   void preprocessing();
 };
 
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index c8ddbf16a50..66feb778817 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -99,20 +99,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "remove_function.h"
 #include "splice_call.h"
 
-void goto_instrument_parse_optionst::eval_verbosity()
-{
-  unsigned int v=8;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-    if(v>10)
-      v=10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 /// invoke main modules
 int goto_instrument_parse_optionst::doit()
 {
@@ -128,7 +114,8 @@ int goto_instrument_parse_optionst::doit()
     return CPROVER_EXIT_USAGE_ERROR;
   }
 
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   try
   {
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index 62f538db9a3..185b793a3a1 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -119,8 +119,6 @@ class goto_instrument_parse_optionst:
   void get_goto_program();
   void instrument_goto_program();
 
-  void eval_verbosity();
-
   void do_indirect_call_and_rtti_removal(bool force=false);
   void do_remove_const_function_pointers_only();
   void do_partial_inlining();
diff --git a/src/util/message.cpp b/src/util/message.cpp
index ad0448adf28..dece45a2d9b 100644
--- a/src/util/message.cpp
+++ b/src/util/message.cpp
@@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "message.h"
 
+#include "string2int.h"
+
 void message_handlert::print(
   unsigned level,
   const std::string &message,
@@ -66,3 +68,38 @@ void message_handlert::print(
 messaget::~messaget()
 {
 }
+
+/// Parse a (user-)provided string as a verbosity level and set it as the
+/// verbosity of dest.
+/// \param user_input  Input string; if empty, the default verbosity is used.
+/// \param default_verbosity  Verbosity to use if no value is provided.
+/// \param dest  message handler the verbosity of which is to be set.
+/// \return Computed verbosity
+unsigned messaget::eval_verbosity(
+  const std::string &user_input,
+  const message_levelt default_verbosity,
+  message_handlert &dest)
+{
+  unsigned v = default_verbosity;
+
+  if(!user_input.empty())
+  {
+    v = unsafe_string2unsigned(user_input);
+
+    if(v > messaget::M_DEBUG)
+    {
+      dest.print(
+        messaget::M_WARNING,
+        "verbosity value " + user_input + " out of range, using debug-level (" +
+          std::to_string(messaget::M_DEBUG) + ") verbosity",
+        -1,
+        source_locationt());
+
+      v = messaget::M_DEBUG;
+    }
+  }
+
+  dest.set_verbosity(v);
+
+  return v;
+}
diff --git a/src/util/message.h b/src/util/message.h
index 3f637ba837a..a20b4cc3041 100644
--- a/src/util/message.h
+++ b/src/util/message.h
@@ -139,6 +139,11 @@ class messaget
     M_STATISTICS=8, M_PROGRESS=9, M_DEBUG=10
   };
 
+  static unsigned eval_verbosity(
+    const std::string &user_input,
+    const message_levelt default_verbosity,
+    message_handlert &dest);
+
   virtual void set_message_handler(message_handlert &_message_handler)
   {
     message_handler=&_message_handler;