diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
index cd11f7c58b2..fbb86fb83e0 100644
--- a/src/goto-checker/solver_factory.cpp
+++ b/src/goto-checker/solver_factory.cpp
@@ -149,15 +149,14 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
     !options.get_bool_option("sat-preprocessor")) // no simplifier
   {
     // simplifier won't work with beautification
-    solver->set_prop(util_make_unique<satcheck_no_simplifiert>());
+    solver->set_prop(
+      util_make_unique<satcheck_no_simplifiert>(message_handler));
   }
   else // with simplifier
   {
-    solver->set_prop(util_make_unique<satcheckt>());
+    solver->set_prop(util_make_unique<satcheckt>(message_handler));
   }
 
-  solver->prop().set_message_handler(message_handler);
-
   auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());
 
   if(options.get_option("arrays-uf") == "never")
@@ -176,8 +175,7 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
   no_beautification();
   no_incremental_check();
 
-  auto prop = util_make_unique<dimacs_cnft>();
-  prop->set_message_handler(message_handler);
+  auto prop = util_make_unique<dimacs_cnft>(message_handler);
 
   std::string filename = options.get_option("outfile");
 
@@ -192,13 +190,11 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
     if(options.get_bool_option("sat-preprocessor"))
     {
       no_beautification();
-      return util_make_unique<satcheckt>();
+      return util_make_unique<satcheckt>(message_handler);
     }
-    return util_make_unique<satcheck_no_simplifiert>();
+    return util_make_unique<satcheck_no_simplifiert>(message_handler);
   }();
 
-  prop->set_message_handler(message_handler);
-
   bv_refinementt::infot info;
   info.ns = &ns;
   info.prop = prop.get();
@@ -225,8 +221,7 @@ solver_factoryt::get_string_refinement()
 {
   string_refinementt::infot info;
   info.ns = &ns;
-  auto prop = util_make_unique<satcheck_no_simplifiert>();
-  prop->set_message_handler(message_handler);
+  auto prop = util_make_unique<satcheck_no_simplifiert>(message_handler);
   info.prop = prop.get();
   info.refinement_bound = DEFAULT_MAX_NB_REFINEMENT;
   info.output_xml = output_xml_in_refinement;
diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index 4e30b813eba..712b349e490 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -48,7 +48,7 @@ literalt arrayst::record_array_equality(
   // check types
   if(!base_type_eq(op0.type(), op1.type(), ns))
   {
-    prop.error() << equality.pretty() << messaget::eom;
+    error() << equality.pretty() << messaget::eom;
     DATA_INVARIANT(
       false,
       "record_array_equality got equality without matching types");
@@ -116,7 +116,7 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, with_expr.old().type(), ns))
     {
-      prop.error() << a.pretty() << messaget::eom;
+      error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got 'with' without matching types");
     }
 
@@ -134,7 +134,7 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, update_expr.old().type(), ns))
     {
-      prop.error() << a.pretty() << messaget::eom;
+      error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(
         false,
         "collect_arrays got 'update' without matching types");
@@ -156,14 +156,14 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, if_expr.true_case().type(), ns))
     {
-      prop.error() << a.pretty() << messaget::eom;
+      error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got if without matching types");
     }
 
     // check types
     if(!base_type_eq(array_type, if_expr.false_case().type(), ns))
     {
-      prop.error() << a.pretty() << messaget::eom;
+      error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got if without matching types");
     }
 
@@ -511,7 +511,7 @@ void arrayst::add_array_constraints_with(
 
     if(index_expr.type()!=value.type())
     {
-      prop.error() << expr.pretty() << messaget::eom;
+      error() << expr.pretty() << messaget::eom;
       DATA_INVARIANT(
         false,
         "with-expression operand should match array element type");
@@ -580,7 +580,7 @@ void arrayst::add_array_constraints_update(
 
     if(index_expr.type()!=value.type())
     {
-      prop.error() << expr.pretty() << messaget::eom;
+      prop.message.error() << expr.pretty() << messaget::eom;
       DATA_INVARIANT(
         false,
         "update operand should match array element type");
diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h
index bf9820c6f3e..79fec011d64 100644
--- a/src/solvers/prop/prop.h
+++ b/src/solvers/prop/prop.h
@@ -21,10 +21,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 /*! \brief TO_BE_DOCUMENTED
 */
-class propt:public messaget
+class propt
 {
 public:
   propt() { }
+
   virtual ~propt() { }
 
   // boolean operators
@@ -113,12 +114,14 @@ class propt:public messaget
   // Resource limits:
   virtual void set_time_limit_seconds(uint32_t)
   {
-    warning() << "CPU limit ignored (not implemented)" << eom;
+    log.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
   }
 
 protected:
   // to avoid a temporary for lcnf(...)
   bvt lcnf_bv;
+
+  messaget log;
 };
 
 #endif // CPROVER_SOLVERS_PROP_PROP_H
diff --git a/src/solvers/qbf/qbf_quantor.cpp b/src/solvers/qbf/qbf_quantor.cpp
index b592eac7940..17c872b9180 100644
--- a/src/solvers/qbf/qbf_quantor.cpp
+++ b/src/solvers/qbf/qbf_quantor.cpp
@@ -34,10 +34,8 @@ const std::string qbf_quantort::solver_text()
 propt::resultt qbf_quantort::prop_solve()
 {
   {
-    messaget::status() <<
-      "Quantor: " <<
-      no_variables() << " variables, " <<
-      no_clauses() << " clauses" << eom;
+    log.status() << "Quantor: " << no_variables() << " variables, "
+                 << no_clauses() << " clauses" << messaget::eom;
   }
 
   std::string qbf_tmp_file="quantor.qdimacs";
@@ -87,19 +85,19 @@ propt::resultt qbf_quantort::prop_solve()
 
     if(!result_found)
     {
-      messaget::error() << "Quantor failed: unknown result" << eom;
+      log.error() << "Quantor failed: unknown result" << messaget::eom;
       return resultt::P_ERROR;
     }
   }
 
   if(result)
   {
-    messaget::status() << "Quantor: TRUE" << eom;
+    log.status() << "Quantor: TRUE" << messaget::eom;
     return resultt::P_SATISFIABLE;
   }
   else
   {
-    messaget::status() << "Quantor: FALSE" << eom;
+    log.status() << "Quantor: FALSE" << messaget::eom;
     return resultt::P_UNSATISFIABLE;
   }
 
diff --git a/src/solvers/qbf/qbf_qube.cpp b/src/solvers/qbf/qbf_qube.cpp
index 28921d4fadb..905c42e08c8 100644
--- a/src/solvers/qbf/qbf_qube.cpp
+++ b/src/solvers/qbf/qbf_qube.cpp
@@ -40,10 +40,8 @@ propt::resultt qbf_qubet::prop_solve()
     return resultt::P_SATISFIABLE;
 
   {
-    messaget::status() <<
-      "QuBE: " <<
-      no_variables() << " variables, " <<
-      no_clauses() << " clauses" << eom;
+    log.status() << "QuBE: " << no_variables() << " variables, " << no_clauses()
+                 << " clauses" << messaget::eom;
   }
 
   std::string qbf_tmp_file="qube.qdimacs";
@@ -95,19 +93,19 @@ propt::resultt qbf_qubet::prop_solve()
 
     if(!result_found)
     {
-      messaget::error() << "QuBE failed: unknown result" << eom;
+      log.error() << "QuBE failed: unknown result" << messaget::eom;
       return resultt::P_ERROR;
     }
   }
 
   if(result)
   {
-    messaget::status() << "QuBE: TRUE" << eom;
+    log.status() << "QuBE: TRUE" << messaget::eom;
     return resultt::P_SATISFIABLE;
   }
   else
   {
-    messaget::status() << "QuBE: FALSE" << eom;
+    log.status() << "QuBE: FALSE" << messaget::eom;
     return resultt::P_UNSATISFIABLE;
   }
 
diff --git a/src/solvers/qbf/qbf_qube_core.cpp b/src/solvers/qbf/qbf_qube_core.cpp
index 6f176fba9ab..cfd9e126c35 100644
--- a/src/solvers/qbf/qbf_qube_core.cpp
+++ b/src/solvers/qbf/qbf_qube_core.cpp
@@ -36,9 +36,8 @@ propt::resultt qbf_qube_coret::prop_solve()
     return resultt::P_SATISFIABLE;
 
   {
-    messaget::status() << "QuBE: "
-      << no_variables() << " variables, "
-      << no_clauses() << " clauses" << eom;
+    log.status() << "QuBE: " << no_variables() << " variables, " << no_clauses()
+                 << " clauses" << messaget::eom;
   }
 
   std::string result_tmp_file="qube.out";
@@ -98,7 +97,7 @@ propt::resultt qbf_qube_coret::prop_solve()
 
     if(!result_found)
     {
-      messaget::error() << "QuBE failed: unknown result" << eom;
+      log.error() << "QuBE failed: unknown result" << messaget::eom;
       return resultt::P_ERROR;
     }
   }
@@ -106,25 +105,25 @@ propt::resultt qbf_qube_coret::prop_solve()
   int remove_result=remove(result_tmp_file.c_str());
   if(remove_result!=0)
   {
-    messaget::error() << "Remove failed: " << std::strerror(errno) << eom;
+    log.error() << "Remove failed: " << std::strerror(errno) << messaget::eom;
     return resultt::P_ERROR;
   }
 
   remove_result=remove(qbf_tmp_file.c_str());
   if(remove_result!=0)
   {
-    messaget::error() << "Remove failed: " << std::strerror(errno) << eom;
+    log.error() << "Remove failed: " << std::strerror(errno) << messaget::eom;
     return resultt::P_ERROR;
   }
 
   if(result)
   {
-    messaget::status() << "QuBE: TRUE" << eom;
+    log.status() << "QuBE: TRUE" << messaget::eom;
     return resultt::P_SATISFIABLE;
   }
   else
   {
-    messaget::status() << "QuBE: FALSE" << eom;
+    log.status() << "QuBE: FALSE" << messaget::eom;
     return resultt::P_UNSATISFIABLE;
   }
 }
diff --git a/src/solvers/qbf/qbf_skizzo.cpp b/src/solvers/qbf/qbf_skizzo.cpp
index cb7f7dc8750..64f64c694cd 100644
--- a/src/solvers/qbf/qbf_skizzo.cpp
+++ b/src/solvers/qbf/qbf_skizzo.cpp
@@ -40,10 +40,8 @@ propt::resultt qbf_skizzot::prop_solve()
     return resultt::P_SATISFIABLE;
 
   {
-    messaget::status() <<
-      "Skizzo: " <<
-      no_variables() << " variables, " <<
-      no_clauses() << " clauses" << eom;
+    log.status() << "Skizzo: " << no_variables() << " variables, "
+                 << no_clauses() << " clauses" << messaget::eom;
   }
 
   std::string qbf_tmp_file="sKizzo.qdimacs";
@@ -95,19 +93,19 @@ propt::resultt qbf_skizzot::prop_solve()
 
     if(!result_found)
     {
-      messaget::error() << "Skizzo failed: unknown result" << eom;
+      log.error() << "Skizzo failed: unknown result" << messaget::eom;
       return resultt::P_ERROR;
     }
   }
 
   if(result)
   {
-    messaget::status() << "Skizzo: TRUE" << eom;
+    log.status() << "Skizzo: TRUE" << messaget::eom;
     return resultt::P_SATISFIABLE;
   }
   else
   {
-    messaget::status() << "Skizzo: FALSE" << eom;
+    log.status() << "Skizzo: FALSE" << messaget::eom;
     return resultt::P_UNSATISFIABLE;
   }
 
diff --git a/src/solvers/sat/dimacs_cnf.cpp b/src/solvers/sat/dimacs_cnf.cpp
index ee3e08c809a..cb384f89bf3 100644
--- a/src/solvers/sat/dimacs_cnf.cpp
+++ b/src/solvers/sat/dimacs_cnf.cpp
@@ -19,6 +19,11 @@ dimacs_cnft::dimacs_cnft():break_lines(false)
 {
 }
 
+dimacs_cnft::dimacs_cnft(message_handlert &message_handler) : dimacs_cnft()
+{
+  log.set_message_handler(message_handler);
+}
+
 void dimacs_cnft::set_assignment(literalt, bool)
 {
   UNIMPLEMENTED;
diff --git a/src/solvers/sat/dimacs_cnf.h b/src/solvers/sat/dimacs_cnf.h
index 4b9e22a69ea..eaa3b41e70a 100644
--- a/src/solvers/sat/dimacs_cnf.h
+++ b/src/solvers/sat/dimacs_cnf.h
@@ -18,6 +18,7 @@ class dimacs_cnft:public cnf_clause_listt
 {
 public:
   dimacs_cnft();
+  explicit dimacs_cnft(message_handlert &);
   virtual ~dimacs_cnft() { }
 
   virtual void write_dimacs_cnf(std::ostream &out);
diff --git a/src/solvers/sat/pbs_dimacs_cnf.cpp b/src/solvers/sat/pbs_dimacs_cnf.cpp
index c2a3721c419..0cb7829c9b1 100644
--- a/src/solvers/sat/pbs_dimacs_cnf.cpp
+++ b/src/solvers/sat/pbs_dimacs_cnf.cpp
@@ -128,7 +128,7 @@ bool pbs_dimacs_cnft::pbs_solve()
 
   if(file.fail())
   {
-    error() << "Unable to read SAT results!" << eom;
+    log.error() << "Unable to read SAT results!" << messaget::eom;
     return false;
   }
 
@@ -194,7 +194,8 @@ bool pbs_dimacs_cnft::pbs_solve()
 #endif
       if(strstr(line.c_str(), "time out") != nullptr)
       {
-        status() << "WARNING:  TIMED OUT.  SOLUTION MAY BE INCORRECT." << eom;
+        log.status() << "WARNING:  TIMED OUT.  SOLUTION MAY BE INCORRECT."
+                     << messaget::eom;
         return satisfied;
       }
       sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
@@ -218,21 +219,21 @@ propt::resultt pbs_dimacs_cnft::prop_solve()
   pbfile.close();
 
   // We start counting at 1, thus there is one variable fewer.
-  messaget::statistics() << (no_variables() - 1) << " variables, "
-                         << clauses.size() << " clauses" << eom;
+  log.statistics() << (no_variables() - 1) << " variables, " << clauses.size()
+                   << " clauses" << messaget::eom;
 
   const bool result = pbs_solve();
 
   if(!result)
   {
-    messaget::status() << "PBS checker: system is UNSATISFIABLE" << eom;
+    log.status() << "PBS checker: system is UNSATISFIABLE" << messaget::eom;
   }
   else
   {
-    messaget::status() << "PBS checker: system is SATISFIABLE";
+    log.status() << "PBS checker: system is SATISFIABLE";
     if(optimize)
-      messaget::status() << " (distance " << opt_sum << ")";
-    messaget::status() << eom;
+      log.status() << " (distance " << opt_sum << ")";
+    log.status() << messaget::eom;
   }
 
   if(result)
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
index 6f8365ded6a..1246ced7ac4 100644
--- a/src/solvers/sat/satcheck_minisat2.cpp
+++ b/src/solvers/sat/satcheck_minisat2.cpp
@@ -78,7 +78,7 @@ void satcheck_minisat2_baset<T>::set_polarity(literalt a, bool value)
   }
   catch(Minisat::OutOfMemoryException)
   {
-    messaget::error() << "SAT checker ran out of memory" << eom;
+    log.error() << "SAT checker ran out of memory" << messaget::eom;
     status = statust::ERROR;
     throw std::bad_alloc();
   }
@@ -144,7 +144,7 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
   }
   catch(const Minisat::OutOfMemoryException &)
   {
-    messaget::error() << "SAT checker ran out of memory" << eom;
+    log.error() << "SAT checker ran out of memory" << messaget::eom;
     status = statust::ERROR;
     throw std::bad_alloc();
   }
@@ -167,8 +167,8 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
 {
   PRECONDITION(status != statust::ERROR);
 
-  messaget::statistics() << (no_variables() - 1) << " variables, "
-                         << solver->nClauses() << " clauses" << eom;
+  log.statistics() << (no_variables() - 1) << " variables, "
+                   << solver->nClauses() << " clauses" << messaget::eom;
 
   try
   {
@@ -176,8 +176,8 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
 
     if(!solver->okay())
     {
-      messaget::status() <<
-        "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
+      log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
+                   << messaget::eom;
     }
     else
     {
@@ -190,8 +190,8 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
 
       if(has_false)
       {
-        messaget::status() <<
-          "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
+        log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
+                     << messaget::eom;
       }
       else
       {
@@ -209,7 +209,7 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
           solver_to_interrupt=solver;
           old_handler=signal(SIGALRM, interrupt_solver);
           if(old_handler==SIG_ERR)
-            warning() << "Failed to set solver time limit" << eom;
+            log.warning() << "Failed to set solver time limit" << messaget::eom;
           else
             alarm(time_limit_seconds);
         }
@@ -227,8 +227,8 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
 
         if(time_limit_seconds!=0)
         {
-          messaget::warning() <<
-            "Time limit ignored (not supported on Win32 yet)" << messaget::eom;
+          log.warning() << "Time limit ignored (not supported on Win32 yet)"
+                        << messaget::eom;
         }
 
         lbool solver_result=
@@ -238,21 +238,21 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
 
         if(solver_result==l_True)
         {
-          messaget::status() <<
-            "SAT checker: instance is SATISFIABLE" << eom;
+          log.status() << "SAT checker: instance is SATISFIABLE"
+                       << messaget::eom;
           CHECK_RETURN(solver->model.size()>0);
           status=statust::SAT;
           return resultt::P_SATISFIABLE;
         }
         else if(solver_result==l_False)
         {
-          messaget::status() <<
-            "SAT checker: instance is UNSATISFIABLE" << eom;
+          log.status() << "SAT checker: instance is UNSATISFIABLE"
+                       << messaget::eom;
         }
         else
         {
-          messaget::status() <<
-            "SAT checker: timed out or other error" << eom;
+          log.status() << "SAT checker: timed out or other error"
+                       << messaget::eom;
           status=statust::ERROR;
           return resultt::P_ERROR;
         }
@@ -264,8 +264,7 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
   }
   catch(const Minisat::OutOfMemoryException &)
   {
-    messaget::error() <<
-      "SAT checker ran out of memory" << eom;
+    log.error() << "SAT checker ran out of memory" << messaget::eom;
     status=statust::ERROR;
     return resultt::P_ERROR;
   }
@@ -288,7 +287,7 @@ void satcheck_minisat2_baset<T>::set_assignment(literalt a, bool value)
   }
   catch(const Minisat::OutOfMemoryException &)
   {
-    messaget::error() << "SAT checker ran out of memory" << eom;
+    log.error() << "SAT checker ran out of memory" << messaget::eom;
     status = statust::ERROR;
     throw std::bad_alloc();
   }
@@ -342,11 +341,25 @@ satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert():
 {
 }
 
+satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert(
+  message_handlert &message_handler)
+  : satcheck_minisat_no_simplifiert()
+{
+  log.set_message_handler(message_handler);
+}
+
 satcheck_minisat_simplifiert::satcheck_minisat_simplifiert():
   satcheck_minisat2_baset<Minisat::SimpSolver>(new Minisat::SimpSolver)
 {
 }
 
+satcheck_minisat_simplifiert::satcheck_minisat_simplifiert(
+  message_handlert &message_handler)
+  : satcheck_minisat_simplifiert()
+{
+  log.set_message_handler(message_handler);
+}
+
 void satcheck_minisat_simplifiert::set_frozen(literalt a)
 {
   try
@@ -359,7 +372,7 @@ void satcheck_minisat_simplifiert::set_frozen(literalt a)
   }
   catch(const Minisat::OutOfMemoryException &)
   {
-    messaget::error() << "SAT checker ran out of memory" << eom;
+    log.error() << "SAT checker ran out of memory" << messaget::eom;
     status = statust::ERROR;
     throw std::bad_alloc();
   }
diff --git a/src/solvers/sat/satcheck_minisat2.h b/src/solvers/sat/satcheck_minisat2.h
index 9834cdb11f8..340bc955220 100644
--- a/src/solvers/sat/satcheck_minisat2.h
+++ b/src/solvers/sat/satcheck_minisat2.h
@@ -70,6 +70,7 @@ class satcheck_minisat_no_simplifiert:
 {
 public:
   satcheck_minisat_no_simplifiert();
+  explicit satcheck_minisat_no_simplifiert(message_handlert &message_handler);
   virtual const std::string solver_text();
 };
 
@@ -78,6 +79,7 @@ class satcheck_minisat_simplifiert:
 {
 public:
   satcheck_minisat_simplifiert();
+  explicit satcheck_minisat_simplifiert(message_handlert &message_handler);
   virtual const std::string solver_text() final;
   virtual void set_frozen(literalt a) final;
   bool is_eliminated(literalt a) const;
diff --git a/src/solvers/smt2/smt2_solver.cpp b/src/solvers/smt2/smt2_solver.cpp
index 840f467757f..ce283d0b884 100644
--- a/src/solvers/smt2/smt2_solver.cpp
+++ b/src/solvers/smt2/smt2_solver.cpp
@@ -373,9 +373,8 @@ int solver(std::istream &in)
   // this is our default verbosity
   message_handler.set_verbosity(messaget::M_STATISTICS);
 
-  satcheckt satcheck;
+  satcheckt satcheck(message_handler);
   boolbvt boolbv(ns, satcheck);
-  satcheck.set_message_handler(message_handler);
   boolbv.set_message_handler(message_handler);
 
   smt2_solvert smt2_solver(in, boolbv);