diff --git a/regression/ansi-c/message_handling1/main.c b/regression/ansi-c/message_handling1/main.c
new file mode 100644
index 00000000000..00193b44b77
--- /dev/null
+++ b/regression/ansi-c/message_handling1/main.c
@@ -0,0 +1,9 @@
+int main()
+{
+  goto bla;
+
+  for(int i=0; i<5; ++i)
+  {
+bla: i=10;
+  }
+}
diff --git a/regression/ansi-c/message_handling1/test.desc b/regression/ansi-c/message_handling1/test.desc
new file mode 100644
index 00000000000..277edf65161
--- /dev/null
+++ b/regression/ansi-c/message_handling1/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--verbosity 2
+^EXIT=0$
+^SIGNAL=0$
+--
+encountered goto `bla' that enters one or more lexical blocks
diff --git a/src/ansi-c/ansi_c_typecheck.cpp b/src/ansi-c/ansi_c_typecheck.cpp
index 08da6bbae01..79efef1b183 100644
--- a/src/ansi-c/ansi_c_typecheck.cpp
+++ b/src/ansi-c/ansi_c_typecheck.cpp
@@ -72,6 +72,9 @@ bool ansi_c_typecheck(
   message_handlert &message_handler,
   const namespacet &ns)
 {
+  const unsigned errors_before=
+    message_handler.get_message_count(messaget::M_ERROR);
+
   symbol_tablet symbol_table;
   ansi_c_parse_treet ansi_c_parse_tree;
 
@@ -99,5 +102,5 @@ bool ansi_c_typecheck(
     ansi_c_typecheck.error() << e << messaget::eom;
   }
 
-  return ansi_c_typecheck.get_error_found();
+  return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
 }
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index f20d666179b..b356658542a 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -655,7 +655,7 @@ int cbmc_parse_optionst::get_goto_program(
 
       language->set_message_handler(get_message_handler());
 
-      status("Parsing", filename);
+      status() << "Parsing " << filename << eom;
 
       if(language->parse(infile, filename))
       {
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index 7fda29931f0..4c70f7fa22f 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -326,7 +326,7 @@ bool clobber_parse_optionst::get_goto_program(
 
       language->set_message_handler(get_message_handler());
 
-      status("Parsing", filename);
+      status() << "Parsing " << filename << eom;
 
       if(language->parse(infile, filename))
       {
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
index fe8a9f063d7..f9c2e8fd4b3 100644
--- a/src/cpp/cpp_typecheck.cpp
+++ b/src/cpp/cpp_typecheck.cpp
@@ -178,6 +178,9 @@ bool cpp_typecheck(
   message_handlert &message_handler,
   const namespacet &ns)
 {
+  const unsigned errors_before=
+    message_handler.get_message_count(messaget::M_ERROR);
+
   symbol_tablet symbol_table;
   cpp_parse_treet cpp_parse_tree;
 
@@ -204,7 +207,7 @@ bool cpp_typecheck(
     cpp_typecheck.error() << e << messaget::eom;
   }
 
-  return cpp_typecheck.get_error_found();
+  return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
 }
 
 /*******************************************************************\
diff --git a/src/goto-cc/armcc_mode.cpp b/src/goto-cc/armcc_mode.cpp
index b6b801059c8..df5e2001237 100644
--- a/src/goto-cc/armcc_mode.cpp
+++ b/src/goto-cc/armcc_mode.cpp
@@ -46,7 +46,7 @@ int armcc_modet::doit()
 
   unsigned int verbosity=1;
 
-  compilet compiler(cmdline);
+  compilet compiler(cmdline, message_handler, cmdline.isset("diag_error="));
 
   #if 0
   bool act_as_ld=
diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp
index f2dd4be23d3..0f4fbf72fae 100644
--- a/src/goto-cc/as_mode.cpp
+++ b/src/goto-cc/as_mode.cpp
@@ -159,8 +159,7 @@ int as_modet::doit()
   config.set(cmdline);
 
   // determine actions to be undertaken
-  compilet compiler(cmdline);
-  compiler.ui_message_handler.set_verbosity(verbosity);
+  compilet compiler(cmdline, message_handler, cmdline.isset("fatal-warnings"));
 
   if(cmdline.isset('b')) // as86 only
   {
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index 58f74669c32..5b91efdeb47 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -121,6 +121,9 @@ bool compilet::doit()
     return true;
   }
 
+  const unsigned warnings_before=
+    get_message_handler().get_message_count(messaget::M_WARNING);
+
   if(source_files.size()>0)
     if(compile())
       return true;
@@ -133,7 +136,10 @@ bool compilet::doit()
       return true;
   }
 
-  return false;
+  return
+    warning_is_fatal &&
+    get_message_handler().get_message_count(messaget::M_WARNING)!=
+    warnings_before;
 }
 
 /*******************************************************************\
@@ -156,8 +162,8 @@ bool compilet::add_input_file(const std::string &file_name)
     std::ifstream in(file_name);
     if(!in)
     {
-      error() << "failed to open file `" << file_name << "'" << eom;
-      return false; // generously ignore
+      warning() << "failed to open file `" << file_name << "'" << eom;
+      return warning_is_fatal; // generously ignore unless -Werror
     }
   }
 
@@ -168,7 +174,7 @@ bool compilet::add_input_file(const std::string &file_name)
     // a file without extension; will ignore
     warning() << "input file `" << file_name
               << "' has no extension, not considered" << eom;
-    return false;
+    return warning_is_fatal;
   }
 
   std::string ext = file_name.substr(r+1, file_name.length());
@@ -329,7 +335,7 @@ bool compilet::find_library(const std::string &name)
       else if(is_elf_file(libname))
       {
         warning() << "Warning: Cannot read ELF library " << libname << eom;
-        return false;
+        return warning_is_fatal;
       }
     }
   }
@@ -383,7 +389,7 @@ Function: compilet::link
 bool compilet::link()
 {
   // "compile" hitherto uncompiled functions
-  print(8, "Compiling functions");
+  statistics() << "Compiling functions" << eom;
   convert_symbols(compiled_functions);
 
   // parse object files
@@ -409,7 +415,7 @@ bool compilet::link()
     symbol_table.remove(goto_functionst::entry_point());
     compiled_functions.function_map.erase(goto_functionst::entry_point());
 
-    if(ansi_c_entry_point(symbol_table, "main", ui_message_handler))
+    if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
       return true;
 
     // entry_point may (should) add some more functions.
@@ -554,7 +560,7 @@ bool compilet::parse(const std::string &file_name)
 
   if(mode==PREPROCESS_ONLY)
   {
-    print(8, "Preprocessing: "+file_name);
+    statistics() << "Preprocessing: " << file_name << eom;
 
     std::ostream *os = &std::cout;
     std::ofstream ofs;
@@ -576,7 +582,7 @@ bool compilet::parse(const std::string &file_name)
   }
   else
   {
-    print(8, "Parsing: "+file_name);
+    statistics() << "Parsing: " << file_name << eom;
 
     if(language.parse(infile, file_name))
     {
@@ -608,7 +614,7 @@ bool compilet::parse_stdin()
 
   language.set_message_handler(get_message_handler());
 
-  print(8, "Parsing: (stdin)");
+  statistics() << "Parsing: (stdin)" << eom;
 
   if(mode==PREPROCESS_ONLY)
   {
@@ -752,11 +758,11 @@ Function: compilet::compilet
 
 \*******************************************************************/
 
-compilet::compilet(cmdlinet &_cmdline):
-  language_uit(_cmdline, ui_message_handler),
-  ui_message_handler(_cmdline, "goto-cc " CBMC_VERSION),
+compilet::compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror):
+  language_uit(_cmdline, mh),
   ns(symbol_table),
-  cmdline(_cmdline)
+  cmdline(_cmdline),
+  warning_is_fatal(Werror)
 {
   mode=COMPILE_LINK_EXECUTABLE;
   echo_file_name=false;
@@ -842,7 +848,7 @@ Function: compilet::convert_symbols
 
 void compilet::convert_symbols(goto_functionst &dest)
 {
-  goto_convert_functionst converter(symbol_table, dest, ui_message_handler);
+  goto_convert_functionst converter(symbol_table, dest, get_message_handler());
 
   // the compilation may add symbols!
 
@@ -872,7 +878,7 @@ void compilet::convert_symbols(goto_functionst &dest)
           s_it->second.value.id()!="compiled" &&
           s_it->second.value.is_not_nil())
       {
-        print(9, "Compiling "+id2string(s_it->first));
+        debug() << "Compiling " << s_it->first << eom;
         converter.convert_function(s_it->first);
         s_it->second.value=exprt("compiled");
       }
diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h
index 936f4cd21d5..37344935b33 100644
--- a/src/goto-cc/compile.h
+++ b/src/goto-cc/compile.h
@@ -20,7 +20,6 @@ Date: June 2006
 class compilet:public language_uit
 {
 public:
-  ui_message_handlert ui_message_handler;
   namespacet ns;
   goto_functionst compiled_functions;
   bool echo_file_name;
@@ -45,7 +44,7 @@ class compilet:public language_uit
   std::string object_file_extension;
   std::string output_file_object, output_file_executable;
 
-  explicit compilet(cmdlinet &_cmdline);
+  compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror);
 
   ~compilet();
 
@@ -72,6 +71,7 @@ class compilet:public language_uit
 
 protected:
   cmdlinet &cmdline;
+  bool warning_is_fatal;
 
   unsigned function_body_count(const goto_functionst &);
 
diff --git a/src/goto-cc/cw_mode.cpp b/src/goto-cc/cw_mode.cpp
index ce4b65e4645..9ee04df633a 100644
--- a/src/goto-cc/cw_mode.cpp
+++ b/src/goto-cc/cw_mode.cpp
@@ -46,7 +46,7 @@ int cw_modet::doit()
 
   unsigned int verbosity=1;
 
-  compilet compiler(cmdline);
+  compilet compiler(cmdline, message_handler, cmdline.isset("Werror"));
 
   #if 0
   bool act_as_ld=
diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp
index 81c75d5c3bf..bbae0bcf009 100644
--- a/src/goto-cc/gcc_mode.cpp
+++ b/src/goto-cc/gcc_mode.cpp
@@ -218,7 +218,7 @@ int gcc_modet::doit()
     return EX_OK;
   }
 
-  if(cmdline.isset("Wall"))
+  if(cmdline.isset("Wall") || cmdline.isset("Wextra"))
     verbosity=2;
 
   if(cmdline.isset("verbosity"))
@@ -303,8 +303,11 @@ int gcc_modet::doit()
     config.ansi_c.double_width=config.ansi_c.single_width;
 
   // determine actions to be undertaken
-  compilet compiler(cmdline);
-  compiler.set_message_handler(get_message_handler());
+  compilet compiler(cmdline,
+                    gcc_message_handler,
+                    cmdline.isset("Werror") &&
+                    cmdline.isset("Wextra") &&
+                    !cmdline.isset("Wno-error"));
 
   if(act_as_ld)
     compiler.mode=compilet::LINK_LIBRARY;
diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp
index c452c374be6..20f4be66e28 100644
--- a/src/goto-cc/ms_cl_mode.cpp
+++ b/src/goto-cc/ms_cl_mode.cpp
@@ -59,7 +59,7 @@ int ms_cl_modet::doit()
 
   unsigned int verbosity=1;
 
-  compilet compiler(cmdline);
+  compilet compiler(cmdline, message_handler, cmdline.isset("WX"));
 
   #if 0
   bool act_as_ld=
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index 25118d0b223..031ba5f142a 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -2866,6 +2866,9 @@ void goto_convert(
   goto_programt &dest,
   message_handlert &message_handler)
 {
+  const unsigned errors_before=
+    message_handler.get_message_count(messaget::M_ERROR);
+
   goto_convertt goto_convert(symbol_table, message_handler);
 
   try
@@ -2876,20 +2879,20 @@ void goto_convert(
   catch(int)
   {
     goto_convert.error();
-    throw 0;
   }
 
   catch(const char *e)
   {
     goto_convert.error() << e << messaget::eom;
-    throw 0;
   }
 
   catch(const std::string &e)
   {
     goto_convert.error() << e << messaget::eom;
-    throw 0;
   }
+
+  if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
+    throw 0;
 }
 
 /*******************************************************************\
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index b25d8870f09..c287338b9c9 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -330,6 +330,9 @@ void goto_convert(
   goto_functionst &functions,
   message_handlert &message_handler)
 {
+  const unsigned errors_before=
+    message_handler.get_message_count(messaget::M_ERROR);
+
   goto_convert_functionst goto_convert_functions(
     symbol_table, functions, message_handler);
 
@@ -341,20 +344,20 @@ void goto_convert(
   catch(int)
   {
     goto_convert_functions.error();
-    throw 0;
   }
 
   catch(const char *e)
   {
     goto_convert_functions.error() << e << messaget::eom;
-    throw 0;
   }
 
   catch(const std::string &e)
   {
     goto_convert_functions.error() << e << messaget::eom;
-    throw 0;
   }
+
+  if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
+    throw 0;
 }
 
 /*******************************************************************\
@@ -375,6 +378,9 @@ void goto_convert(
   goto_functionst &functions,
   message_handlert &message_handler)
 {
+  const unsigned errors_before=
+    message_handler.get_message_count(messaget::M_ERROR);
+
   goto_convert_functionst goto_convert_functions(
     symbol_table, functions, message_handler);
 
@@ -386,18 +392,18 @@ void goto_convert(
   catch(int)
   {
     goto_convert_functions.error();
-    throw 0;
   }
 
   catch(const char *e)
   {
     goto_convert_functions.error() << e << messaget::eom;
-    throw 0;
   }
 
   catch(const std::string &e)
   {
     goto_convert_functions.error() << e << messaget::eom;
-    throw 0;
   }
+
+  if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
+    throw 0;
 }
diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp
index 52a6caeeba2..779593a245b 100644
--- a/src/goto-programs/initialize_goto_model.cpp
+++ b/src/goto-programs/initialize_goto_model.cpp
@@ -91,7 +91,10 @@ bool initialize_goto_model(
 
         if(lf.language==NULL)
         {
-          msg.error("failed to figure out type of file", filename);
+          source_locationt location;
+          location.set_file(filename);
+          msg.error().source_location=location;
+          msg.error() << "failed to figure out type of file" << messaget::eom;
           return true;
         }
 
diff --git a/src/goto-symex/memory_model_pso.cpp b/src/goto-symex/memory_model_pso.cpp
index 629451fc80b..d21a7f1bb2c 100644
--- a/src/goto-symex/memory_model_pso.cpp
+++ b/src/goto-symex/memory_model_pso.cpp
@@ -22,7 +22,7 @@ Function: memory_model_psot::operator()
 
 void memory_model_psot::operator()(symex_target_equationt &equation)
 {
-  print(8, "Adding PSO constraints");
+  statistics() << "Adding PSO constraints" << eom;
 
   build_event_lists(equation);
   build_clock_type(equation);
diff --git a/src/goto-symex/memory_model_sc.cpp b/src/goto-symex/memory_model_sc.cpp
index 7c131269802..59de4870300 100644
--- a/src/goto-symex/memory_model_sc.cpp
+++ b/src/goto-symex/memory_model_sc.cpp
@@ -24,7 +24,7 @@ Function: memory_model_sct::operator()
 
 void memory_model_sct::operator()(symex_target_equationt &equation)
 {
-  print(8, "Adding SC constraints");
+  statistics() << "Adding SC constraints" << eom;
 
   build_event_lists(equation);
   build_clock_type(equation);
diff --git a/src/goto-symex/memory_model_tso.cpp b/src/goto-symex/memory_model_tso.cpp
index 1fec15c9bdd..22fd6a1b238 100644
--- a/src/goto-symex/memory_model_tso.cpp
+++ b/src/goto-symex/memory_model_tso.cpp
@@ -25,7 +25,7 @@ Function: memory_model_tsot::operator()
 
 void memory_model_tsot::operator()(symex_target_equationt &equation)
 {
-  print(8, "Adding TSO constraints");
+  statistics() << "Adding TSO constraints" << eom;
 
   build_event_lists(equation);
   build_clock_type(equation);
diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
index a644f1acf99..0e8168b7fbf 100644
--- a/src/jsil/jsil_typecheck.cpp
+++ b/src/jsil/jsil_typecheck.cpp
@@ -1398,6 +1398,9 @@ bool jsil_typecheck(
   message_handlert &message_handler,
   const namespacet &ns)
 {
+  const unsigned errors_before=
+    message_handler.get_message_count(messaget::M_ERROR);
+
   symbol_tablet symbol_table;
 
   jsil_typecheckt jsil_typecheck(
@@ -1424,5 +1427,5 @@ bool jsil_typecheck(
     jsil_typecheck.error() << e << messaget::eom;
   }
 
-  return jsil_typecheck.get_error_found();
+  return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
 }
diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
index 502bb932c60..70853be9e6b 100644
--- a/src/langapi/language_ui.cpp
+++ b/src/langapi/language_ui.cpp
@@ -33,8 +33,8 @@ Function: language_uit::language_uit
 language_uit::language_uit(
   const cmdlinet &cmdline,
   ui_message_handlert &_ui_message_handler):
-  ui_message_handler(_ui_message_handler),
-  _cmdline(cmdline)
+  _cmdline(cmdline),
+  ui_message_handler(_ui_message_handler)
 {
   set_message_handler(ui_message_handler);
 }
@@ -115,7 +115,10 @@ bool language_uit::parse(const std::string &filename)
 
   if(lf.language==NULL)
   {
-    error("failed to figure out type of file", filename);
+    source_locationt location;
+    location.set_file(filename);
+    error().source_location=location;
+    error() << "failed to figure out type of file" << eom;
     return true;
   }
 
diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h
index b82507f4c75..50c8311b714 100644
--- a/src/langapi/language_ui.h
+++ b/src/langapi/language_ui.h
@@ -48,10 +48,9 @@ class language_uit:public messaget
     return ui_message_handler.get_ui();
   }
 
-  ui_message_handlert &ui_message_handler;
-
 protected:
   const cmdlinet &_cmdline;
+  ui_message_handlert &ui_message_handler;
 };
 
 #endif // CPROVER_LANGAPI_LANGUAGE_UI_H
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp
index 7e8207f4d09..e2958953c42 100644
--- a/src/solvers/prop/prop_conv.cpp
+++ b/src/solvers/prop/prop_conv.cpp
@@ -624,9 +624,7 @@ void prop_conv_solvert::ignoring(const exprt &expr)
 {
   // fall through
 
-  std::string msg="warning: ignoring "+expr.pretty();
-
-  print(2, msg);
+  warning() << "warning: ignoring " << expr.pretty() << eom;
 }
 
 /*******************************************************************\
@@ -662,12 +660,12 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
   // post-processing isn't incremental yet
   if(!post_processing_done)
   {
-    print(8, "Post-processing");
+    statistics() << "Post-processing" << eom;
     post_process();
     post_processing_done=true;
   }
 
-  print(7, "Solving with "+prop.solver_text());
+  statistics() << "Solving with " << prop.solver_text() << eom;
 
   propt::resultt result=prop.prop_solve();
 
diff --git a/src/solvers/sat/pbs_dimacs_cnf.cpp b/src/solvers/sat/pbs_dimacs_cnf.cpp
index 5c45f8e0a09..cd2f04039bb 100644
--- a/src/solvers/sat/pbs_dimacs_cnf.cpp
+++ b/src/solvers/sat/pbs_dimacs_cnf.cpp
@@ -190,7 +190,8 @@ bool pbs_dimacs_cnft::pbs_solve()
           // print(line);
           if(strstr(line.c_str(), "time out")!=NULL)
             {
-              print(6, "WARNING:  TIMED OUT.  SOLUTION MAY BE INCORRECT.\n");
+              status() << "WARNING:  TIMED OUT.  SOLUTION MAY BE INCORRECT."
+                       << eom;
               return satisfied;
             }
           sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp
index 393ec62432f..c709999c662 100644
--- a/src/util/cout_message.cpp
+++ b/src/util/cout_message.cpp
@@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 /*******************************************************************\
 
-Function: cout_message_handlert::print
+Function: cout_message_handlert::cout_message_handlert
 
   Inputs:
 
@@ -30,23 +30,14 @@ Function: cout_message_handlert::print
 
 \*******************************************************************/
 
-void cout_message_handlert::print(
-  unsigned level,
-  const std::string &message)
+cout_message_handlert::cout_message_handlert():
+  stream_message_handlert(std::cout)
 {
-  if(verbosity>=level)
-  {
-    std::cout << message << '\n';
-
-    // We flush for level 6 or below.
-    if(level<=6)
-      std::cout << std::flush;
-  }
 }
 
 /*******************************************************************\
 
-Function: cerr_message_handlert::print
+Function: cerr_message_handlert::cerr_message_handlert
 
   Inputs:
 
@@ -56,12 +47,9 @@ Function: cerr_message_handlert::print
 
 \*******************************************************************/
 
-void cerr_message_handlert::print(
-  unsigned level,
-  const std::string &message)
+cerr_message_handlert::cerr_message_handlert():
+  stream_message_handlert(std::cerr)
 {
-  if(verbosity>=level)
-    std::cerr << message << '\n' << std::flush;
 }
 
 /*******************************************************************\
@@ -80,6 +68,8 @@ void console_message_handlert::print(
   unsigned level,
   const std::string &message)
 {
+  message_handlert::print(level, message);
+
   if(verbosity<level)
     return;
 
@@ -111,30 +101,47 @@ void console_message_handlert::print(
     if(level>=4)
     {
       std::cout << message << '\n';
-
-      if(level<=6)
-        std::cout << std::flush;
     }
     else
-      std::cerr << message << '\n' << std::flush;
+      std::cerr << message << '\n';
   }
   #else
-  // We flush after messages of level 6 or lower.
-  // We don't for messages of level 7 or higher to improve performance,
-  // in particular when writing to NFS.
   // Messages level 3 or lower go to cerr, messages level 4 or
   // above go to cout.
 
   if(level>=4)
   {
     std::cout << message << '\n';
+  }
+  else
+    std::cerr << message << '\n';
+  #endif
+}
+
+/*******************************************************************\
+
+Function: console_message_handlert::flush
+
+  Inputs:
 
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void console_message_handlert::flush(unsigned level)
+{
+  // We flush after messages of level 6 or lower.
+  // We don't for messages of level 7 or higher to improve performance,
+  // in particular when writing to NFS.
+  if(level>=4)
+  {
     if(level<=6)
       std::cout << std::flush;
   }
   else
-    std::cerr << message << '\n' << std::flush;
-  #endif
+    std::cerr << std::flush;
 }
 
 /*******************************************************************\
@@ -183,9 +190,9 @@ void gcc_message_handlert::print(
     else
       dest+=id2string(column)+": ";
 
-    if(level==message_clientt::M_ERROR)
+    if(level==messaget::M_ERROR)
       dest+="error: ";
-    else if(level==message_clientt::M_WARNING)
+    else if(level==messaget::M_WARNING)
       dest+="warning: ";
   }
 
@@ -210,6 +217,8 @@ void gcc_message_handlert::print(
   unsigned level,
   const std::string &message)
 {
+  message_handlert::print(level, message);
+
   // gcc appears to send everything to cerr
   if(verbosity>=level)
     std::cerr << message << '\n' << std::flush;
diff --git a/src/util/cout_message.h b/src/util/cout_message.h
index ab78148c6d6..1f22e5c009c 100644
--- a/src/util/cout_message.h
+++ b/src/util/cout_message.h
@@ -9,36 +9,34 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_COUT_MESSAGE_H
 #define CPROVER_UTIL_COUT_MESSAGE_H
 
-#include "message.h"
+#include "ui_message.h"
 
-class cout_message_handlert:public message_handlert
+class cout_message_handlert:public stream_message_handlert
 {
 public:
-  // all messages go to cout
-  virtual void print(
-    unsigned level,
-    const std::string &message) override;
+  // all messages go to stdout
+  cout_message_handlert();
 };
 
-class cerr_message_handlert:public message_handlert
+class cerr_message_handlert:public stream_message_handlert
 {
 public:
-  // all messages go to cerr
-  virtual void print(
-    unsigned level,
-    const std::string &message) override;
+  // all messages go to stderr
+  cerr_message_handlert();
 };
 
-class console_message_handlert:public message_handlert
+class console_message_handlert:public ui_message_handlert
 {
 public:
   // level 4 and upwards go to cout, level 1-3 to cerr
   virtual void print(
     unsigned level,
     const std::string &message) override;
+
+  virtual void flush(unsigned level) override;
 };
 
-class gcc_message_handlert:public message_handlert
+class gcc_message_handlert:public ui_message_handlert
 {
 public:
   // aims to imitate the messages gcc prints
diff --git a/src/util/message.cpp b/src/util/message.cpp
index 21a67433609..0033395cc9e 100644
--- a/src/util/message.cpp
+++ b/src/util/message.cpp
@@ -67,25 +67,7 @@ void message_handlert::print(
 
 /*******************************************************************\
 
-Function: messaget::print
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void messaget::print(unsigned level, const std::string &message)
-{
-  if(message_handler!=NULL)
-    message_handler->print(level, message);
-}
-
-/*******************************************************************\
-
-Function: messaget::print
+Function: message_handlert::print
 
   Inputs:
 
@@ -95,36 +77,18 @@ Function: messaget::print
 
 \*******************************************************************/
 
-void messaget::print(
+void message_handlert::print(
   unsigned level,
-  const std::string &message,
-  int sequence_number,
-  const source_locationt &location)
-{
-  if(message_handler!=NULL)
-    message_handler->print(level, message, sequence_number,
-                           location);
-}
-
-/*******************************************************************\
-
-Function: message_clientt::~message_clientt
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-message_clientt::~message_clientt()
+  const std::string &message)
 {
+  if(level>=message_count.size())
+    message_count.resize(level+1, 0);
+  ++message_count[level];
 }
 
 /*******************************************************************\
 
-Function: message_clientt::set_message_handler
+Function: messaget::~messaget
 
   Inputs:
 
@@ -134,8 +98,6 @@ Function: message_clientt::set_message_handler
 
 \*******************************************************************/
 
-void message_clientt::set_message_handler(
-  message_handlert &_message_handler)
+messaget::~messaget()
 {
-  message_handler=&_message_handler;
 }
diff --git a/src/util/message.h b/src/util/message.h
index b92fb8f3dfd..8497c206d83 100644
--- a/src/util/message.h
+++ b/src/util/message.h
@@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 class message_handlert
 {
 public:
-  message_handlert():verbosity(10)
+  message_handlert():verbosity(10), message_count(10, 0)
   {
   }
 
@@ -30,6 +30,11 @@ class message_handlert
     int sequence_number,
     const source_locationt &location);
 
+  virtual void flush(unsigned level)
+  {
+    // no-op by default
+  }
+
   virtual ~message_handlert()
   {
   }
@@ -37,8 +42,17 @@ class message_handlert
   void set_verbosity(unsigned _verbosity) { verbosity=_verbosity; }
   unsigned get_verbosity() const { return verbosity; }
 
+  unsigned get_message_count(unsigned level) const
+  {
+    if(level>=message_count.size())
+      return 0;
+
+    return message_count[level];
+  }
+
 protected:
   unsigned verbosity;
+  std::vector<unsigned> message_count;
 };
 
 class null_message_handlert:public message_handlert
@@ -46,6 +60,7 @@ class null_message_handlert:public message_handlert
 public:
   virtual void print(unsigned level, const std::string &message)
   {
+    message_handlert::print(level, message);
   }
 
   virtual void print(
@@ -54,6 +69,7 @@ class null_message_handlert:public message_handlert
     int sequence_number,
     const source_locationt &location)
   {
+    print(level, message);
   }
 };
 
@@ -65,13 +81,23 @@ class stream_message_handlert:public message_handlert
   }
 
   virtual void print(unsigned level, const std::string &message)
-  { out << message << '\n'; }
+  {
+    message_handlert::print(level, message);
+
+    if(verbosity>=level)
+      out << message << '\n';
+  }
+
+  virtual void flush(unsigned level)
+  {
+    out << std::flush;
+  }
 
 protected:
   std::ostream &out;
 };
 
-class message_clientt
+class messaget
 {
 public:
   // Standard message levels:
@@ -91,17 +117,9 @@ class message_clientt
     M_STATISTICS=8, M_PROGRESS=9, M_DEBUG=10
   };
 
-  virtual ~message_clientt();
-
-  virtual void set_message_handler(message_handlert &_message_handler);
-
-  message_clientt():message_handler(NULL)
-  {
-  }
-
-  explicit message_clientt(message_handlert &_message_handler):
-    message_handler(&_message_handler)
+  virtual void set_message_handler(message_handlert &_message_handler)
   {
+    message_handler=&_message_handler;
   }
 
   message_handlert &get_message_handler()
@@ -109,62 +127,27 @@ class message_clientt
     return *message_handler;
   }
 
-protected:
-  message_handlert *message_handler;
-};
-
-class messaget:public message_clientt
-{
-public:
   // constructors, destructor
 
   messaget():
+    message_handler(NULL),
     mstream(M_DEBUG, *this)
   {
   }
 
   messaget(const messaget &other):
-    message_clientt(other),
-    mstream(M_DEBUG, *this)
+    message_handler(other.message_handler),
+    mstream(other.mstream)
   {
   }
 
   explicit messaget(message_handlert &_message_handler):
-    message_clientt(_message_handler),
+    message_handler(&_message_handler),
     mstream(M_DEBUG, *this)
   {
   }
 
-  virtual ~messaget() { }
-
-  // old interface, will go away
-  void status(
-    const std::string &message,
-    const std::string &file)
-  {
-    source_locationt location;
-    location.set_file(file);
-    print(6, message, -1, location);
-  }
-
-  void error(
-    const std::string &message,
-    const std::string &file)
-  {
-    source_locationt location;
-    location.set_file(file);
-    print(1, message, -1, location);
-  }
-
-  virtual void print(unsigned level, const std::string &message);
-
-  virtual void print(
-    unsigned level,
-    const std::string &message,
-    int sequence_number, // -1: no sequence information
-    const source_locationt &location);
-
-  // New interface
+  virtual ~messaget();
 
   class mstreamt:public std::ostringstream
   {
@@ -177,6 +160,13 @@ class messaget:public message_clientt
     {
     }
 
+    mstreamt(const mstreamt &other):
+      message_level(other.message_level),
+      message(other.message),
+      source_location(other.source_location)
+    {
+    }
+
     unsigned message_level;
     messaget &message;
     source_locationt source_location;
@@ -197,9 +187,17 @@ class messaget:public message_clientt
 
   // Feeding 'eom' into the stream triggers
   // the printing of the message
-  static inline mstreamt &eom(mstreamt &m)
+  static mstreamt &eom(mstreamt &m)
   {
-    m.message.print(m.message_level, m.str(), -1, m.source_location);
+    if(m.message.message_handler)
+    {
+      m.message.message_handler->print(
+        m.message_level,
+        m.str(),
+        -1,
+        m.source_location);
+      m.message.message_handler->flush(m.message_level);
+    }
     m.clear(); // clears error bits
     m.str(std::string()); // clears the string
     m.source_location.clear();
@@ -207,61 +205,55 @@ class messaget:public message_clientt
   }
 
   // in lieu of std::endl
-  static inline mstreamt &endl(mstreamt &m)
+  static mstreamt &endl(mstreamt &m)
   {
     static_cast<std::ostream &>(m) << std::endl;
     return m;
   }
 
-  mstreamt &error()
+  mstreamt &get_mstream(unsigned message_level)
   {
-    mstream.message_level=M_ERROR;
+    mstream.message_level=message_level;
     return mstream;
   }
 
+  mstreamt &error()
+  {
+    return get_mstream(M_ERROR);
+  }
+
   mstreamt &warning()
   {
-    mstream.message_level=M_WARNING;
-    return mstream;
+    return get_mstream(M_WARNING);
   }
 
   mstreamt &result()
   {
-    mstream.message_level=M_RESULT;
-    return mstream;
+    return get_mstream(M_RESULT);
   }
 
   mstreamt &status()
   {
-    mstream.message_level=M_STATUS;
-    return mstream;
+    return get_mstream(M_STATUS);
   }
 
   mstreamt &statistics()
   {
-    mstream.message_level=M_STATISTICS;
-    return mstream;
+    return get_mstream(M_STATISTICS);
   }
 
   mstreamt &progress()
   {
-    mstream.message_level=M_PROGRESS;
-    return mstream;
+    return get_mstream(M_PROGRESS);
   }
 
   mstreamt &debug()
   {
-    mstream.message_level=M_DEBUG;
-    return mstream;
-  }
-
-  mstreamt &get_mstream(unsigned message_level)
-  {
-    mstream.message_level=message_level;
-    return mstream;
+    return get_mstream(M_DEBUG);
   }
 
 protected:
+  message_handlert *message_handler;
   mstreamt mstream;
 };
 
diff --git a/src/util/parser.cpp b/src/util/parser.cpp
index 539ed1f0e63..579dea6fd27 100644
--- a/src/util/parser.cpp
+++ b/src/util/parser.cpp
@@ -63,6 +63,7 @@ void parsert::parse_error(
   tmp_source_location.set_column(column-before.size());
   print(1, tmp, -1, tmp_source_location);
   #else
-  print(1, tmp, -1, source_location);
+  error().source_location=source_location;
+  error() << tmp << eom;
   #endif
 }
diff --git a/src/util/typecheck.cpp b/src/util/typecheck.cpp
index 67b695e53fa..020c202015d 100644
--- a/src/util/typecheck.cpp
+++ b/src/util/typecheck.cpp
@@ -22,6 +22,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bool typecheckt::typecheck_main()
 {
+  assert(message_handler);
+
+  const unsigned errors_before=
+    message_handler->get_message_count(messaget::M_ERROR);
+
   try
   {
     typecheck();
@@ -29,7 +34,7 @@ bool typecheckt::typecheck_main()
 
   catch(int)
   {
-    error_found=true;
+    error();
   }
 
   catch(const char *e)
@@ -42,5 +47,5 @@ bool typecheckt::typecheck_main()
     error() << e << eom;
   }
 
-  return error_found;
+  return message_handler->get_message_count(messaget::M_ERROR)!=errors_before;
 }
diff --git a/src/util/typecheck.h b/src/util/typecheck.h
index ee80f6e42f0..1d5cd51decc 100644
--- a/src/util/typecheck.h
+++ b/src/util/typecheck.h
@@ -16,30 +16,27 @@ class typecheckt:public messaget
 {
 public:
   explicit typecheckt(message_handlert &_message_handler):
-    messaget(_message_handler),
-    error_found(false)
+    messaget(_message_handler)
   {
   }
 
   virtual ~typecheckt() { }
 
-  mstreamt &error()
+  // not pretty, but makes transition easier
+  void err_location(const source_locationt &loc)
   {
-    error_found=true;
-    return messaget::error();
+    messaget::error().source_location=loc;
   }
 
   // not pretty, but makes transition easier
   void err_location(const exprt &src)
   {
-    error().source_location=src.find_source_location();
+    err_location(src.find_source_location());
   }
 
-  bool error_found;
-
-  bool get_error_found() const
+  void err_location(const typet &src)
   {
-    return error_found;
+    err_location(src.source_location());
   }
 
 protected:
diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp
index 1cc32ecf356..43f284fb444 100644
--- a/src/util/ui_message.cpp
+++ b/src/util/ui_message.cpp
@@ -191,6 +191,8 @@ void ui_message_handlert::print(
   int sequence_number,
   const source_locationt &location)
 {
+  message_handlert::print(level, message);
+
   if(verbosity>=level)
   {
     switch(get_ui())
@@ -319,3 +321,35 @@ void ui_message_handlert::json_ui_msg(
   //  a trailing comma.
   std::cout << ",\n" << result;
 }
+
+/*******************************************************************\
+
+Function: ui_message_handlert::flush
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void ui_message_handlert::flush(unsigned level)
+{
+  switch(get_ui())
+  {
+  case uit::PLAIN:
+  {
+    console_message_handlert console_message_handler;
+    console_message_handler.flush(level);
+  }
+  break;
+
+  case uit::XML_UI:
+  case uit::JSON_UI:
+  {
+    std::cout << std::flush;
+  }
+  break;
+  }
+}
diff --git a/src/util/ui_message.h b/src/util/ui_message.h
index 59cc5c21009..ea0c2dbc6e4 100644
--- a/src/util/ui_message.h
+++ b/src/util/ui_message.h
@@ -18,6 +18,10 @@ class ui_message_handlert:public message_handlert
 
   ui_message_handlert(uit, const std::string &program);
   ui_message_handlert(const class cmdlinet &, const std::string &program);
+  ui_message_handlert():
+    _ui(uit::PLAIN)
+  {
+  }
 
   virtual ~ui_message_handlert();
 
@@ -31,6 +35,8 @@ class ui_message_handlert:public message_handlert
     _ui=__ui;
   }
 
+  virtual void flush(unsigned level);
+
 protected:
   uit _ui;