diff --git a/src/analyses/natural_loops.cpp b/src/analyses/natural_loops.cpp
index 00ece2cf213..2ac9bbc8ed7 100644
--- a/src/analyses/natural_loops.cpp
+++ b/src/analyses/natural_loops.cpp
@@ -11,18 +11,18 @@ Author: Georg Weissenbacher, georg@weissenbacher.name
 
 #include "natural_loops.h"
 
-#include <iostream>
-
-void show_natural_loops(const goto_modelt &goto_model)
+void show_natural_loops(
+  const goto_modelt &goto_model,
+  std::ostream &out)
 {
   forall_goto_functions(it, goto_model.goto_functions)
   {
-    std::cout << "*** " << it->first << '\n';
+    out << "*** " << it->first << '\n';
 
     natural_loopst natural_loops;
     natural_loops(it->second.body);
-    natural_loops.output(std::cout);
+    natural_loops.output(out);
 
-    std::cout << '\n';
+    out << '\n';
   }
 }
diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h
index 8fb41d7e1d2..710fd9d2c56 100644
--- a/src/analyses/natural_loops.h
+++ b/src/analyses/natural_loops.h
@@ -69,7 +69,9 @@ class natural_loopst:
 typedef natural_loops_templatet<goto_programt, goto_programt::targett>
     natural_loops_mutablet;
 
-void show_natural_loops(const goto_modelt &);
+void show_natural_loops(
+  const goto_modelt &,
+  std::ostream &out);
 
 /// Finds all back-edges and computes the natural loops
 #ifdef DEBUG
diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
index f91fd5c52c3..cce96904495 100644
--- a/src/cbmc/all_properties.cpp
+++ b/src/cbmc/all_properties.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "all_properties_class.h"
 
-#include <iostream>
-
 #include <util/time_stopping.h>
 #include <util/xml.h>
 #include <util/json.h>
@@ -163,10 +161,10 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
   {
   case ui_message_handlert::uit::PLAIN:
     {
-      status() << "\n** Results:" << eom;
+      result() << "\n** Results:" << eom;
 
       for(const auto &goal_pair : goal_map)
-        status() << "[" << goal_pair.first << "] "
+        result() << "[" << goal_pair.first << "] "
                  << goal_pair.second.description << ": "
                  << goal_pair.second.status_string()
                  << eom;
@@ -176,10 +174,11 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
         for(const auto &g : goal_map)
           if(g.second.status==goalt::statust::FAILURE)
           {
-            std::cout << "\n" << "Trace for " << g.first << ":" << "\n";
-            show_goto_trace(std::cout, bmc.ns, g.second.goto_trace);
+            result() << "\n" << "Trace for " << g.first << ":" << "\n";
+            show_goto_trace(result(), bmc.ns, g.second.goto_trace);
           }
       }
+      result() << eom;
 
       status() << "\n** " << cover_goals.number_covered()
                << " of " << cover_goals.size() << " failed ("
@@ -200,7 +199,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
         if(g.second.status==goalt::statust::FAILURE)
           convert(bmc.ns, g.second.goto_trace, xml_result.new_element());
 
-        std::cout << xml_result << "\n";
+        result() << xml_result;
       }
       break;
     }
@@ -224,7 +223,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
         }
       }
 
-      std::cout << ",\n" << json_result;
+      result() << json_result;
     }
     break;
   }
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index ab5d6883ab0..8a95b7cfafe 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -55,33 +55,33 @@ void bmct::error_trace()
   switch(ui)
   {
   case ui_message_handlert::uit::PLAIN:
-    status() << "Counterexample:" << eom;
-    show_goto_trace(status(), ns, goto_trace);
-    status() << eom;
+    result() << "Counterexample:" << eom;
+    show_goto_trace(result(), ns, goto_trace);
+    result() << eom;
     break;
 
   case ui_message_handlert::uit::XML_UI:
     {
       xmlt xml;
       convert(ns, goto_trace, xml);
-      status() << preformatted_output << xml << eom;
+      status() << xml;
     }
     break;
 
   case ui_message_handlert::uit::JSON_UI:
     {
-      json_objectt json_result;
-      json_arrayt &result_array=json_result["results"].make_array();
-      json_objectt &result=result_array.push_back().make_object();
+      json_objectt json;
+      json_arrayt &result_array=json["results"].make_array();
+      json_objectt &json_result=result_array.push_back().make_object();
       const goto_trace_stept &step=goto_trace.steps.back();
-      result["property"]=
+      json_result["property"]=
         json_stringt(id2string(step.pc->source_location.get_property_id()));
-      result["description"]=
+      json_result["description"]=
         json_stringt(id2string(step.pc->source_location.get_comment()));
-      result["status"]=json_stringt("failed");
-      jsont &json_trace=result["trace"];
+      json_result["status"]=json_stringt("failed");
+      jsont &json_trace=json_result["trace"];
       convert(ns, goto_trace, json_trace);
-      status() << preformatted_output << json_result << eom;
+      status() << json_result;
     }
     break;
   }
@@ -173,8 +173,7 @@ void bmct::report_success()
     {
       xmlt xml("cprover-status");
       xml.data="SUCCESS";
-      std::cout << xml;
-      std::cout << "\n";
+      result() << xml;
     }
     break;
 
@@ -182,7 +181,7 @@ void bmct::report_success()
     {
       json_objectt json_result;
       json_result["cProverStatus"]=json_stringt("success");
-      std::cout << ",\n" << json_result;
+      result() << json_result;
     }
     break;
   }
@@ -201,8 +200,7 @@ void bmct::report_failure()
     {
       xmlt xml("cprover-status");
       xml.data="FAILURE";
-      std::cout << xml;
-      std::cout << "\n";
+      result() << xml;
     }
     break;
 
@@ -210,7 +208,7 @@ void bmct::report_failure()
     {
       json_objectt json_result;
       json_result["cProverStatus"]=json_stringt("failure");
-      std::cout << ",\n" << json_result;
+      result() << json_result;
     }
     break;
   }
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
index c0ad5465c6a..5baf32cda49 100644
--- a/src/cbmc/bmc_cover.cpp
+++ b/src/cbmc/bmc_cover.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "bmc.h"
 
-#include <iostream>
-
 #include <util/time_stopping.h>
 #include <util/xml.h>
 #include <util/xml_expr.h>
@@ -185,10 +183,6 @@ void bmc_covert::satisfying_assignment()
       goto_trace.steps.erase(++s_it1, goto_trace.steps.end());
       break;
     }
-
-  #if 0
-  show_goto_trace(std::cout, bmc.ns, test.goto_trace);
-  #endif
 }
 
 bool bmc_covert::operator()()
@@ -223,8 +217,6 @@ bool bmc_covert::operator()()
 
   bmc.do_conversion();
 
-  // bmc.equation.output(std::cout);
-
   // get the conditions for these goals from formula
   // collect all 'instances' of the goals
   for(auto it = bmc.equation.SSA_steps.begin();
@@ -280,26 +272,25 @@ bool bmc_covert::operator()()
   {
     case ui_message_handlert::uit::PLAIN:
     {
-      status() << "\n** coverage results:" << eom;
+      result() << "\n** coverage results:" << eom;
 
       for(const auto &g : goal_map)
       {
         const goalt &goal=g.second;
 
-        status() << "[" << g.first << "]";
+        result() << "[" << g.first << "]";
 
         if(goal.source_location.is_not_nil())
-          status() << ' ' << goal.source_location;
+          result() << ' ' << goal.source_location;
 
         if(!goal.description.empty())
-          status() << ' ' << goal.description;
+          result() << ' ' << goal.description;
 
-        status() << ": " << (goal.satisfied?"SATISFIED":"FAILED")
-                 << eom;
+        result() << ": " << (goal.satisfied?"SATISFIED":"FAILED")
+                 << '\n';
       }
 
-      status() << '\n';
-
+      result() << eom;
       break;
     }
 
@@ -317,7 +308,7 @@ bool bmc_covert::operator()()
         if(goal.source_location.is_not_nil())
           xml_result.new_element()=xml(goal.source_location);
 
-        std::cout << xml_result << "\n";
+        result() << xml_result;
       }
 
       for(const auto &test : tests)
@@ -350,7 +341,7 @@ bool bmc_covert::operator()()
           xml_goal.set_attribute("id", id2string(goal_id));
         }
 
-        std::cout << xml_result << "\n";
+        result() << xml_result;
       }
       break;
     }
@@ -406,7 +397,8 @@ bool bmc_covert::operator()()
           goal_refs.push_back(json_stringt(id2string(goal_id)));
         }
       }
-      std::cout << ",\n" << json_result;
+
+      result() << json_result;
       break;
     }
   }
@@ -424,10 +416,12 @@ bool bmc_covert::operator()()
 
   if(bmc.ui==ui_message_handlert::uit::PLAIN)
   {
-    std::cout << "Test suite:" << '\n';
+    result() << "Test suite:" << '\n';
 
     for(const auto &test : tests)
-      std::cout << get_test(test.goto_trace) << '\n';
+      result() << get_test(test.goto_trace) << '\n';
+
+    result() << eom;
   }
 
   return false;
diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
index adcfd3dff20..31a1673f0ca 100644
--- a/src/cbmc/fault_localization.cpp
+++ b/src/cbmc/fault_localization.cpp
@@ -301,7 +301,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()
       xmlt dest("fault-localization");
       xmlt xml_diagnosis=report_xml(ID_nil);
       dest.new_element().swap(xml_diagnosis);
-      status() << preformatted_output << dest << eom;
+      status() << dest;
       break;
     }
     case ui_message_handlert::uit::JSON_UI:
@@ -379,7 +379,7 @@ void fault_localizationt::report(
         xmlt xml_diagnosis=report_xml(goal_pair.first);
         dest.new_element().swap(xml_diagnosis);
       }
-      status() << preformatted_output << dest << eom;
+      status() << dest;
     }
     break;
   case ui_message_handlert::uit::JSON_UI:
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 397dfc10536..8bf3451b8b4 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -564,7 +564,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-natural-loops"))
     {
-      show_natural_loops(goto_model);
+      show_natural_loops(goto_model, std::cout);
       return 0;
     }
 
diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp
index 3f84ea3e802..5221fda0f21 100644
--- a/src/util/cout_message.cpp
+++ b/src/util/cout_message.cpp
@@ -31,10 +31,9 @@ cerr_message_handlert::cerr_message_handlert():
 
 void console_message_handlert::print(
   unsigned level,
-  const std::string &message,
-  bool preformatted)
+  const std::string &message)
 {
-  message_handlert::print(level, message, preformatted);
+  message_handlert::print(level, message);
 
   if(verbosity<level)
     return;
@@ -102,8 +101,7 @@ void gcc_message_handlert::print(
   unsigned level,
   const std::string &message,
   int sequence_number,
-  const source_locationt &location,
-  bool preformatted)
+  const source_locationt &location)
 {
   const irep_idt file=location.get_file();
   const irep_idt line=location.get_line();
@@ -141,15 +139,14 @@ void gcc_message_handlert::print(
 
   dest+=message;
 
-  print(level, dest, preformatted);
+  print(level, dest);
 }
 
 void gcc_message_handlert::print(
   unsigned level,
-  const std::string &message,
-  bool preformatted)
+  const std::string &message)
 {
-  message_handlert::print(level, message, preformatted);
+  message_handlert::print(level, message);
 
   // gcc appears to send everything to cerr
   if(verbosity>=level)
diff --git a/src/util/cout_message.h b/src/util/cout_message.h
index df3fd535dd6..39d4bddd349 100644
--- a/src/util/cout_message.h
+++ b/src/util/cout_message.h
@@ -32,8 +32,7 @@ class console_message_handlert:public ui_message_handlert
   // level 4 and upwards go to cout, level 1-3 to cerr
   virtual void print(
     unsigned level,
-    const std::string &message,
-    bool preformatted) override;
+    const std::string &message) override;
 
   virtual void flush(unsigned level) override;
 };
@@ -44,15 +43,13 @@ class gcc_message_handlert:public ui_message_handlert
   // aims to imitate the messages gcc prints
   virtual void print(
     unsigned level,
-    const std::string &message,
-    bool preformatted) override;
+    const std::string &message) override;
 
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location,
-    bool preformatted) override;
+    const source_locationt &location) override;
 };
 
 #endif // CPROVER_UTIL_COUT_MESSAGE_H
diff --git a/src/util/message.cpp b/src/util/message.cpp
index 522c9cd7b25..ad0448adf28 100644
--- a/src/util/message.cpp
+++ b/src/util/message.cpp
@@ -13,8 +13,7 @@ void message_handlert::print(
   unsigned level,
   const std::string &message,
   int sequence_number,
-  const source_locationt &location,
-  bool preformatted)
+  const source_locationt &location)
 {
   std::string dest;
 
@@ -52,13 +51,12 @@ void message_handlert::print(
     dest+=": ";
   dest+=message;
 
-  print(level, dest, preformatted);
+  print(level, dest);
 }
 
 void message_handlert::print(
   unsigned level,
-  const std::string &message,
-  bool preformatted)
+  const std::string &message)
 {
   if(level>=message_count.size())
     message_count.resize(level+1, 0);
diff --git a/src/util/message.h b/src/util/message.h
index 758fdd06879..c9da55416dd 100644
--- a/src/util/message.h
+++ b/src/util/message.h
@@ -15,7 +15,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <sstream>
 
 #include "invariant.h"
+#include "json.h"
 #include "source_location.h"
+#include "xml.h"
 
 class message_handlert
 {
@@ -24,17 +26,23 @@ class message_handlert
   {
   }
 
-  virtual void print(
-    unsigned level,
-    const std::string &message,
-    bool preformatted) = 0;
+  virtual void print(unsigned level, const std::string &message)=0;
+
+  virtual void print(unsigned level, const xmlt &xml)
+  {
+    // no-op by default
+  }
+
+  virtual void print(unsigned level, const jsont &json)
+  {
+    // no-op by default
+  }
 
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location,
-    bool preformatted);
+    const source_locationt &location);
 
   virtual void flush(unsigned level)
   {
@@ -64,22 +72,18 @@ class message_handlert
 class null_message_handlert:public message_handlert
 {
 public:
-  virtual void print(
-    unsigned level,
-    const std::string &message,
-    bool preformatted)
+  virtual void print(unsigned level, const std::string &message)
   {
-    message_handlert::print(level, message, preformatted);
+    message_handlert::print(level, message);
   }
 
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location,
-    bool preformatted)
+    const source_locationt &location)
   {
-    print(level, message, preformatted);
+    print(level, message);
   }
 };
 
@@ -90,12 +94,9 @@ class stream_message_handlert:public message_handlert
   {
   }
 
-  virtual void print(
-    unsigned level,
-    const std::string &message,
-    bool preformatted)
+  virtual void print(unsigned level, const std::string &message)
   {
-    message_handlert::print(level, message, preformatted);
+    message_handlert::print(level, message);
 
     if(verbosity>=level)
       out << message << '\n';
@@ -172,23 +173,40 @@ class messaget
       unsigned _message_level,
       messaget &_message):
       message_level(_message_level),
-      message(_message),
-      preformatted(false)
+      message(_message)
     {
     }
 
     mstreamt(const mstreamt &other):
       message_level(other.message_level),
       message(other.message),
-      source_location(other.source_location),
-      preformatted(false)
+      source_location(other.source_location)
     {
     }
 
     unsigned message_level;
     messaget &message;
     source_locationt source_location;
-    bool preformatted;
+
+    mstreamt &operator << (const xmlt &data)
+    {
+      *this << eom; // force end of previous message
+      if(message.message_handler)
+      {
+        message.message_handler->print(message_level, data);
+      }
+      return *this;
+    }
+
+    mstreamt &operator << (const json_objectt &data)
+    {
+      *this << eom; // force end of previous message
+      if(message.message_handler)
+      {
+        message.message_handler->print(message_level, data);
+      }
+      return *this;
+    }
 
     template <class T>
     mstreamt &operator << (const T &x)
@@ -214,23 +232,15 @@ class messaget
         m.message_level,
         m.str(),
         -1,
-        m.source_location,
-        m.preformatted);
+        m.source_location);
       m.message.message_handler->flush(m.message_level);
     }
-    m.preformatted=false;
     m.clear(); // clears error bits
     m.str(std::string()); // clears the string
     m.source_location.clear();
     return m;
   }
 
-  static mstreamt &preformatted_output(mstreamt &m)
-  {
-    m.preformatted=true;
-    return m;
-  }
-
   // in lieu of std::endl
   static mstreamt &endl(mstreamt &m)
   {
diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp
index 5757fc36acd..9aa7a3749d3 100644
--- a/src/util/ui_message.cpp
+++ b/src/util/ui_message.cpp
@@ -90,8 +90,7 @@ const char *ui_message_handlert::level_string(unsigned level)
 
 void ui_message_handlert::print(
   unsigned level,
-  const std::string &message,
-  bool preformatted)
+  const std::string &message)
 {
   if(verbosity>=level)
   {
@@ -100,7 +99,7 @@ void ui_message_handlert::print(
     case uit::PLAIN:
     {
       console_message_handlert console_message_handler;
-      console_message_handler.print(level, message, preformatted);
+      console_message_handler.print(level, message);
     }
     break;
 
@@ -109,21 +108,64 @@ void ui_message_handlert::print(
     {
       source_locationt location;
       location.make_nil();
-      print(level, message, -1, location, preformatted);
+      print(level, message, -1, location);
     }
     break;
     }
   }
 }
 
+void ui_message_handlert::print(
+  unsigned level,
+  const xmlt &data)
+{
+  if(verbosity>=level)
+  {
+    switch(get_ui())
+    {
+    case uit::PLAIN:
+      INVARIANT(false, "Cannot print xml data on PLAIN UI");
+      break;
+    case uit::XML_UI:
+      std::cout << data << '\n';
+      flush(level);
+      break;
+    case uit::JSON_UI:
+      INVARIANT(false, "Cannot print xml data on JSON UI");
+      break;
+    }
+  }
+}
+
+void ui_message_handlert::print(
+  unsigned level,
+  const jsont &data)
+{
+  if(verbosity>=level)
+  {
+    switch(get_ui())
+    {
+    case uit::PLAIN:
+      INVARIANT(false, "Cannot print json data on PLAIN UI");
+      break;
+    case uit::XML_UI:
+      INVARIANT(false, "Cannot print json data on XML UI");
+      break;
+    case uit::JSON_UI:
+      std::cout << ',' << '\n' << data;
+      flush(level);
+      break;
+    }
+  }
+}
+
 void ui_message_handlert::print(
   unsigned level,
   const std::string &message,
   int sequence_number,
-  const source_locationt &location,
-  bool preformatted)
+  const source_locationt &location)
 {
-  message_handlert::print(level, message, preformatted);
+  message_handlert::print(level, message);
 
   if(verbosity>=level)
   {
@@ -131,7 +173,7 @@ void ui_message_handlert::print(
     {
     case uit::PLAIN:
       message_handlert::print(
-        level, message, sequence_number, location, preformatted);
+        level, message, sequence_number, location);
       break;
 
     case uit::XML_UI:
@@ -147,7 +189,7 @@ void ui_message_handlert::print(
       std::string sequence_number_str=
         sequence_number>=0?std::to_string(sequence_number):"";
 
-      ui_msg(type, tmp_message, sequence_number_str, location, preformatted);
+      ui_msg(type, tmp_message, sequence_number_str, location);
     }
     break;
     }
@@ -158,8 +200,7 @@ void ui_message_handlert::ui_msg(
   const std::string &type,
   const std::string &msg1,
   const std::string &msg2,
-  const source_locationt &location,
-  bool preformatted)
+  const source_locationt &location)
 {
   switch(get_ui())
   {
@@ -167,11 +208,11 @@ void ui_message_handlert::ui_msg(
     break;
 
   case uit::XML_UI:
-    xml_ui_msg(type, msg1, msg2, location, preformatted);
+    xml_ui_msg(type, msg1, msg2, location);
     break;
 
   case uit::JSON_UI:
-    json_ui_msg(type, msg1, msg2, location, preformatted);
+    json_ui_msg(type, msg1, msg2, location);
     break;
   }
 }
@@ -180,16 +221,8 @@ void ui_message_handlert::xml_ui_msg(
   const std::string &type,
   const std::string &msg1,
   const std::string &msg2,
-  const source_locationt &location,
-  bool preformatted)
+  const source_locationt &location)
 {
-  if(preformatted)
-  {
-    // Expect the message is already an XML fragment.
-    std::cout << msg1 << '\n';
-    return;
-  }
-
   xmlt result;
   result.name="message";
 
@@ -208,16 +241,8 @@ void ui_message_handlert::json_ui_msg(
   const std::string &type,
   const std::string &msg1,
   const std::string &msg2,
-  const source_locationt &location,
-  bool preformatted)
+  const source_locationt &location)
 {
-  if(preformatted)
-  {
-    // Expect the message is already a JSON fragment.
-    std::cout << ",\n" << msg1;
-    return;
-  }
-
   json_objectt result;
 
   if(location.is_not_nil() &&
diff --git a/src/util/ui_message.h b/src/util/ui_message.h
index 646c96d1ea4..422633e1f40 100644
--- a/src/util/ui_message.h
+++ b/src/util/ui_message.h
@@ -36,45 +36,46 @@ class ui_message_handlert:public message_handlert
     _ui=__ui;
   }
 
-  virtual void flush(unsigned level);
+  virtual void flush(unsigned level) override;
 
 protected:
   uit _ui;
 
-  // overloading
   virtual void print(
     unsigned level,
-    const std::string &message,
-    bool preformatted);
+    const std::string &message) override;
 
-  // overloading
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location,
-    bool preformatted);
+    const source_locationt &location) override;
+
+  virtual void print(
+    unsigned level,
+    const xmlt &data) override;
+
+  virtual void print(
+    unsigned level,
+    const jsont &data) override;
 
   virtual void xml_ui_msg(
     const std::string &type,
     const std::string &msg1,
     const std::string &msg2,
-    const source_locationt &location,
-    bool preformatted);
+    const source_locationt &location);
 
   virtual void json_ui_msg(
     const std::string &type,
     const std::string &msg1,
     const std::string &msg2,
-    const source_locationt &location,
-    bool preformatted);
+    const source_locationt &location);
 
   virtual void ui_msg(
     const std::string &type,
     const std::string &msg1,
     const std::string &msg2,
-    const source_locationt &location,
-    bool preformatted);
+    const source_locationt &location);
 
   const char *level_string(unsigned level);
 };