Merge pull request #4249 from tautschnig/messaget-cover_goalst

cover_goalst isn't a messaget [blocks: #3800]

Author: tautschnig

src/cbmc/all_properties.cpp

@@ -97,7 +97,6 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 
   cover_goalst cover_goals(solver);
 
-  cover_goals.set_message_handler(get_message_handler());
   cover_goals.register_observer(*this);
 
   for(const auto &g : goal_map)
@@ -112,7 +111,8 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 
   bool error=false;
 
-  decision_proceduret::resultt result=cover_goals();
+  const decision_proceduret::resultt result =
+    cover_goals(get_message_handler());
 
   if(result==decision_proceduret::resultt::D_ERROR)
   {

src/cbmc/bmc_cover.cpp

@@ -250,7 +250,7 @@ bool bmc_covert::operator()()
 
   status() << "Running " << solver.decision_procedure_text() << eom;
 
-  cover_goals();
+  cover_goals(get_message_handler());
 
   {
     auto solver_stop=std::chrono::steady_clock::now();

src/solvers/prop/cover_goals.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "cover_goals.h"
 
+#include <util/message.h>
+
 #include "literal_expr.h"
 #include "prop_conv.h"
 
@@ -69,7 +71,8 @@ void cover_goalst::freeze_goal_variables()
 }
 
 /// Try to cover all goals
-decision_proceduret::resultt cover_goalst::operator()()
+decision_proceduret::resultt cover_goalst::
+operator()(message_handlert &message_handler)
 {
   _iterations=_number_covered=0;
 
@@ -98,9 +101,12 @@ decision_proceduret::resultt cover_goalst::operator()()
       break;
 
     default:
-      error() << "decision procedure has failed" << eom;
+    {
+      messaget log(message_handler);
+      log.error() << "decision procedure has failed" << messaget::eom;
       return dec_result;
     }
+    }
   }
   while(dec_result==decision_proceduret::resultt::D_SATISFIABLE &&
         number_covered()<size());

src/solvers/prop/cover_goals.h

@@ -15,15 +15,15 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <list>
 
 #include <util/decision_procedure.h>
-#include <util/message.h>
 
 #include "literal.h"
 
+class message_handlert;
 class prop_convt;
 
 /// Try to cover some given set of goals incrementally. This can be seen as a
 /// heuristic variant of SAT-based set-cover. No minimality guarantee.
-class cover_goalst:public messaget
+class cover_goalst
 {
 public:
   explicit cover_goalst(prop_convt &_prop_conv):
@@ -36,7 +36,7 @@ class cover_goalst:public messaget
   virtual ~cover_goalst();
 
   // returns result of last run on success
-  decision_proceduret::resultt operator()();
+  decision_proceduret::resultt operator()(message_handlert &);
 
   // the goals