Merge pull request #5622 from tautschnig/messaget-smt2_dec

smt2_dect isn't a messaget

Author: tautschnig

src/goto-checker/solver_factory.cpp

@@ -343,14 +343,12 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
       "cbmc",
       std::string("Generated by CBMC ") + CBMC_VERSION,
       "QF_AUFBV",
-      solver);
-    smt2_dec->set_message_handler(message_handler);
+      solver,
+      message_handler);
 
     if(options.get_bool_option("fpa"))
       smt2_dec->use_FPA_theory = true;
 
-    smt2_dec->set_message_handler(message_handler);
-
     set_decision_procedure_time_limit(*smt2_dec);
     return util_make_unique<solvert>(std::move(smt2_dec));
   }

src/goto-instrument/accelerate/scratch_program.h

@@ -50,7 +50,7 @@ class scratch_programt:public goto_programt
       symex(mh, symbol_table, equation, options, path_storage, guard_manager),
       satcheck(util_make_unique<satcheckt>(mh)),
       satchecker(ns, *satcheck, mh),
-      z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
+      z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3, mh),
       checker(&z3) // checker(&satchecker)
   {
   }

src/solvers/smt2/smt2_dec.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
+#include <util/message.h>
 #include <util/run.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
@@ -122,7 +123,8 @@ decision_proceduret::resultt smt2_dect::dec_solve()
 
   if(res<0)
   {
-    error() << "error running SMT2 solver" << eom;
+    messaget log{message_handler};
+    log.error() << "error running SMT2 solver" << messaget::eom;
     return decision_proceduret::resultt::D_ERROR;
   }
 
@@ -143,7 +145,7 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
 
   while(in)
   {
-    auto parsed_opt = smt2irep(in, get_message_handler());
+    auto parsed_opt = smt2irep(in, message_handler);
 
     if(!parsed_opt.has_value())
       break;
@@ -177,8 +179,10 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
       // returns unsat will give an error.
       if(res!=resultt::D_UNSATISFIABLE)
       {
-        error() << "SMT2 solver returned error message:\n"
-                << "\t\"" << parsed.get_sub()[1].id() <<"\"" << eom;
+        messaget log{message_handler};
+        log.error() << "SMT2 solver returned error message:\n"
+                    << "\t\"" << parsed.get_sub()[1].id() << "\""
+                    << messaget::eom;
         return decision_proceduret::resultt::D_ERROR;
       }
     }

src/solvers/smt2/smt2_dec.h

@@ -12,10 +12,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "smt2_conv.h"
 
-#include <util/message.h>
-
 #include <fstream>
 
+class message_handlert;
+
 class smt2_stringstreamt
 {
 protected:
@@ -24,25 +24,27 @@ class smt2_stringstreamt
 
 /*! \brief Decision procedure interface for various SMT 2.x solvers
 */
-class smt2_dect : protected smt2_stringstreamt,
-                  public smt2_convt,
-                  public messaget
+class smt2_dect : protected smt2_stringstreamt, public smt2_convt
 {
 public:
   smt2_dect(
     const namespacet &_ns,
     const std::string &_benchmark,
     const std::string &_notes,
     const std::string &_logic,
-    solvert _solver):
-    smt2_convt(_ns, _benchmark, _notes, _logic, _solver, stringstream)
+    solvert _solver,
+    message_handlert &_message_handler)
+    : smt2_convt(_ns, _benchmark, _notes, _logic, _solver, stringstream),
+      message_handler(_message_handler)
   {
   }
 
   resultt dec_solve() override;
   std::string decision_procedure_text() const override;
 
 protected:
+  message_handlert &message_handler;
+
   resultt read_result(std::istream &in);
 };