Do not artificially separate message handler and uit

tautschnig · tautschnig · commit 4e9e13550a11 · 2018-06-21T20:23:33.000+01:00
They were passed around independently, even though they originated from the very
same object.
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -560,8 +560,7 @@ int jbmc_parse_optionst::doit()
       path_strategy_chooser,
       options,
       goto_model,
-      ui_message_handler.get_ui(),
-      *this,
+      ui_message_handler,
       configure_bmc);
   }
   else
@@ -605,8 +604,7 @@ int jbmc_parse_optionst::doit()
         path_strategy_chooser,
         options,
         lazy_goto_model,
-        ui_message_handler.get_ui(),
-        *this,
+        ui_message_handler,
         configure_bmc,
         callback_after_symex);
   }
@@ -661,8 +659,7 @@ int jbmc_parse_optionst::get_goto_program(
     {
       class_hierarchyt hierarchy;
       hierarchy(lazy_goto_model.symbol_table);
-      show_class_hierarchy(
-        hierarchy, get_message_handler(), ui_message_handler.get_ui());
+      show_class_hierarchy(hierarchy, ui_message_handler);
       return CPROVER_EXIT_SUCCESS;
     }
 
diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
@@ -157,7 +157,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 
 void bmc_all_propertiest::report(const cover_goalst &cover_goals)
 {
-  switch(bmc.ui)
+  switch(bmc.ui_message_handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     {
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
@@ -51,7 +51,7 @@ void bmct::error_trace()
   goto_tracet &goto_trace=safety_checkert::error_trace;
   build_goto_trace(equation, prop_conv, ns, goto_trace);
 
-  switch(ui)
+  switch(ui_message_handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     result() << "Counterexample:" << eom;
@@ -150,7 +150,7 @@ void bmct::report_success()
 {
   result() << "VERIFICATION SUCCESSFUL" << eom;
 
-  switch(ui)
+  switch(ui_message_handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     break;
@@ -177,7 +177,7 @@ void bmct::report_failure()
 {
   result() << "VERIFICATION FAILED" << eom;
 
-  switch(ui)
+  switch(ui_message_handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     break;
@@ -562,15 +562,14 @@ int bmct::do_language_agnostic_bmc(
   const path_strategy_choosert &path_strategy_chooser,
   const optionst &opts,
   abstract_goto_modelt &model,
-  const ui_message_handlert::uit &ui,
-  messaget &message,
+  ui_message_handlert &ui,
   std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc,
   std::function<bool(void)> callback_after_symex)
 {
   safety_checkert::resultt final_result = safety_checkert::resultt::UNKNOWN;
   safety_checkert::resultt tmp_result = safety_checkert::resultt::UNKNOWN;
   const symbol_tablet &symbol_table = model.get_symbol_table();
-  message_handlert &mh = message.get_message_handler();
+  messaget message(ui);
   std::unique_ptr<path_storaget> worklist;
   std::string strategy = opts.get_option("exploration-strategy");
   INVARIANT(
@@ -580,13 +579,11 @@ int bmct::do_language_agnostic_bmc(
   try
   {
     {
-      cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
-      solvers.set_ui(ui);
+      cbmc_solverst solvers(opts, symbol_table, ui);
       std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
       cbmc_solver = solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();
-      bmct bmc(opts, symbol_table, mh, pc, *worklist, callback_after_symex);
-      bmc.set_ui(ui);
+      bmct bmc(opts, symbol_table, ui, pc, *worklist, callback_after_symex);
       if(driver_configure_bmc)
         driver_configure_bmc(bmc, symbol_table);
       tmp_result = bmc.run(model);
@@ -621,16 +618,15 @@ int bmct::do_language_agnostic_bmc(
                          << "Starting new path (" << worklist->size()
                          << " to go)\n"
                          << message.eom;
-      cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
-      solvers.set_ui(ui);
+      cbmc_solverst solvers(opts, symbol_table, ui);
       std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
       cbmc_solver = solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();
       path_storaget::patht &resume = worklist->peek();
       path_explorert pe(
         opts,
         symbol_table,
-        mh,
+        ui,
         pc,
         resume.equation,
         resume.state,
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
@@ -66,7 +66,7 @@ class bmct:public safety_checkert
   bmct(
     const optionst &_options,
     const symbol_tablet &outer_symbol_table,
-    message_handlert &_message_handler,
+    ui_message_handlert &_message_handler,
     prop_convt &_prop_conv,
     path_storaget &_path_storage,
     std::function<bool(void)> callback_after_symex)
@@ -83,7 +83,7 @@ class bmct:public safety_checkert
         options,
         path_storage),
       prop_conv(_prop_conv),
-      ui(ui_message_handlert::uit::PLAIN),
+      ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
   {
     symex.constant_propagation=options.get_bool_option("propagation");
@@ -103,8 +103,6 @@ class bmct:public safety_checkert
   safety_checkert::resultt execute(abstract_goto_modelt &);
   virtual ~bmct() { }
 
-  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
-
   // the safety_checkert interface
   virtual resultt operator()(
     const goto_functionst &goto_functions)
@@ -127,8 +125,7 @@ class bmct:public safety_checkert
     const path_strategy_choosert &path_strategy_chooser,
     const optionst &opts,
     abstract_goto_modelt &goto_model,
-    const ui_message_handlert::uit &ui,
-    messaget &message,
+    ui_message_handlert &ui,
     std::function<void(bmct &, const symbol_tablet &)>
       driver_configure_bmc = nullptr,
     std::function<bool(void)> callback_after_symex = nullptr);
@@ -144,7 +141,7 @@ class bmct:public safety_checkert
   bmct(
     const optionst &_options,
     const symbol_tablet &outer_symbol_table,
-    message_handlert &_message_handler,
+    ui_message_handlert &_message_handler,
     prop_convt &_prop_conv,
     symex_target_equationt &_equation,
     path_storaget &_path_storage,
@@ -162,7 +159,7 @@ class bmct:public safety_checkert
         options,
         path_storage),
       prop_conv(_prop_conv),
-      ui(ui_message_handlert::uit::PLAIN),
+      ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
   {
     symex.constant_propagation = options.get_bool_option("propagation");
@@ -186,7 +183,7 @@ class bmct:public safety_checkert
   prop_convt &prop_conv;
   std::unique_ptr<memory_model_baset> memory_model;
   // use gui format
-  ui_message_handlert::uit ui;
+  ui_message_handlert &ui_message_handler;
 
   virtual decision_proceduret::resultt
     run_decision_procedure(prop_convt &prop_conv);
@@ -266,7 +263,7 @@ class path_explorert : public bmct
   path_explorert(
     const optionst &_options,
     const symbol_tablet &outer_symbol_table,
-    message_handlert &_message_handler,
+    ui_message_handlert &_message_handler,
     prop_convt &_prop_conv,
     symex_target_equationt &saved_equation,
     const goto_symex_statet &saved_state,
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
@@ -267,7 +267,7 @@ bool bmc_covert::operator()()
     if(g.second.satisfied)
       goals_covered++;
 
-  switch(bmc.ui)
+  switch(bmc.ui_message_handler.get_ui())
   {
     case ui_message_handlert::uit::PLAIN:
     {
@@ -412,7 +412,7 @@ bool bmc_covert::operator()()
                << (cover_goals.iterations()==1?"":"s")
                << eom;
 
-  if(bmc.ui==ui_message_handlert::uit::PLAIN)
+  if(bmc.ui_message_handler.get_ui() == ui_message_handlert::uit::PLAIN)
   {
     result() << "Test suite:" << '\n';
 
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -532,8 +532,7 @@ int cbmc_parse_optionst::doit()
     path_strategy_chooser,
     options,
     goto_model,
-    ui_message_handler.get_ui(),
-    *this);
+    ui_message_handler);
 }
 
 bool cbmc_parse_optionst::set_properties()
diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
@@ -70,7 +70,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
     solver->set_prop(util_make_unique<satcheckt>());
   }
 
-  solver->prop().set_message_handler(get_message_handler());
+  solver->prop().set_message_handler(ui);
 
   auto bv_cbmc=util_make_unique<bv_cbmct>(ns, solver->prop());
 
@@ -90,7 +90,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
   no_incremental_check();
 
   auto prop=util_make_unique<dimacs_cnft>();
-  prop->set_message_handler(get_message_handler());
+  prop->set_message_handler(ui);
 
   std::string filename=options.get_option("outfile");
 
@@ -111,12 +111,12 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
     return util_make_unique<satcheck_no_simplifiert>();
   }();
 
-  prop->set_message_handler(get_message_handler());
+  prop->set_message_handler(ui);
 
   bv_refinementt::infot info;
   info.ns=&ns;
   info.prop=prop.get();
-  info.ui=ui;
+  info.ui=ui.get_ui();
 
   // we allow setting some parameters
   if(options.get_bool_option("max-node-refinement"))
@@ -139,10 +139,10 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
   string_refinementt::infot info;
   info.ns=&ns;
   auto prop=util_make_unique<satcheck_no_simplifiert>();
-  prop->set_message_handler(get_message_handler());
+  prop->set_message_handler(ui);
   info.prop=prop.get();
   info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
-  info.ui=ui;
+  info.ui=ui.get_ui();
   if(options.get_bool_option("string-max-length"))
     info.max_string_length = options.get_signed_int_option("string-max-length");
   info.trace=options.get_bool_option("trace");
@@ -159,6 +159,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
 std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
   smt2_dect::solvert solver)
 {
+  messaget msg(ui);
   no_beautification();
 
   const std::string &filename=options.get_option("outfile");
@@ -167,7 +168,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
   {
     if(solver==smt2_dect::solvert::GENERIC)
     {
-      error() << "please use --outfile" << eom;
+      msg.error() << "please use --outfile" << messaget::eom;
       throw 0;
     }
 
@@ -198,7 +199,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
     if(options.get_bool_option("fpa"))
       smt2_conv->use_FPA_theory=true;
 
-    smt2_conv->set_message_handler(get_message_handler());
+    smt2_conv->set_message_handler(ui);
 
     return util_make_unique<solvert>(std::move(smt2_conv));
   }
@@ -212,7 +213,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
 
     if(!*out)
     {
-      error() << "failed to open " << filename << eom;
+      msg.error() << "failed to open " << filename << messaget::eom;
       throw 0;
     }
 
@@ -228,7 +229,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
     if(options.get_bool_option("fpa"))
       smt2_conv->use_FPA_theory=true;
 
-    smt2_conv->set_message_handler(get_message_handler());
+    smt2_conv->set_message_handler(ui);
 
     return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
   }
@@ -238,7 +239,8 @@ void cbmc_solverst::no_beautification()
 {
   if(options.get_bool_option("beautify"))
   {
-    error() << "sorry, this solver does not support beautification" << eom;
+    messaget(ui).error() << "sorry, this solver does not support beautification"
+                         << messaget::eom;
     throw 0;
   }
 }
@@ -249,7 +251,8 @@ void cbmc_solverst::no_incremental_check()
      options.get_option("cover")!="" ||
      options.get_option("incremental-check")!="")
   {
-    error() << "sorry, this solver does not support incremental solving" << eom;
+    messaget(ui).error() << "sorry, this solver does not support incremental "
+                         << "solving" << messaget::eom;
     throw 0;
   }
 }
diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h
@@ -29,18 +29,17 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "bv_cbmc.h"
 
-class cbmc_solverst:public messaget
+class cbmc_solverst
 {
 public:
   cbmc_solverst(
     const optionst &_options,
     const symbol_tablet &_symbol_table,
-    message_handlert &_message_handler):
-    messaget(_message_handler),
+    ui_message_handlert &_message_handler):
     options(_options),
     symbol_table(_symbol_table),
     ns(_symbol_table),
-    ui(ui_message_handlert::uit::PLAIN)
+    ui(_message_handler)
   {
   }
 
@@ -120,15 +119,11 @@ class cbmc_solverst:public messaget
   {
   }
 
-  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
-
 protected:
   const optionst &options;
   const symbol_tablet &symbol_table;
   namespacet ns;
-
-  // use gui format
-  ui_message_handlert::uit ui;
+  ui_message_handlert &ui;
 
   std::unique_ptr<solvert> get_default();
   std::unique_ptr<solvert> get_dimacs();
diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
@@ -289,7 +289,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()
     // localize faults
     run(ID_nil);
 
-    switch(bmc.ui)
+    switch(bmc.ui_message_handler.get_ui())
     {
     case ui_message_handlert::uit::PLAIN:
     {
@@ -356,7 +356,7 @@ void fault_localizationt::report(
 {
   bmc_all_propertiest::report(cover_goals);
 
-  switch(bmc.ui)
+  switch(bmc.ui_message_handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     if(cover_goals.number_covered()>0)
diff --git a/src/cbmc/show_vcc.cpp b/src/cbmc/show_vcc.cpp
@@ -148,7 +148,7 @@ void bmct::show_vcc()
 
   std::ostream &out=have_file?of:std::cout;
 
-  switch(ui)
+  switch(ui_message_handler.get_ui())
   {
   case ui_message_handlert::uit::XML_UI:
     error() << "XML UI not supported" << eom;
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp
diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h

Original file line number	Diff line number	Diff line change
`@@ -157,7 +157,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()`
`157`	`157`
`158`	`158`	`void bmc_all_propertiest::report(const cover_goalst &cover_goals)`
`159`	`159`	`{`
`160`		`- switch(bmc.ui)`
	`160`	`+ switch(bmc.ui_message_handler.get_ui())`
`161`	`161`	`{`
`162`	`162`	`case ui_message_handlert::uit::PLAIN:`
`163`	`163`	`{`
Original file line number	Diff line number	Diff line change
`@@ -267,7 +267,7 @@ bool bmc_covert::operator()()`
`267`	`267`	`if(g.second.satisfied)`
`268`	`268`	`goals_covered++;`
`269`	`269`
`270`		`- switch(bmc.ui)`
	`270`	`+ switch(bmc.ui_message_handler.get_ui())`
`271`	`271`	`{`
`272`	`272`	`case ui_message_handlert::uit::PLAIN:`
`273`	`273`	`{`
`@@ -412,7 +412,7 @@ bool bmc_covert::operator()()`
`412`	`412`	`<< (cover_goals.iterations()==1?"":"s")`
`413`	`413`	`<< eom;`
`414`	`414`
`415`		`- if(bmc.ui==ui_message_handlert::uit::PLAIN)`
	`415`	`+ if(bmc.ui_message_handler.get_ui() == ui_message_handlert::uit::PLAIN)`
`416`	`416`	`{`
`417`	`417`	`result() << "Test suite:" << '\n';`
`418`	`418`
Original file line number	Diff line number	Diff line change
`@@ -532,8 +532,7 @@ int cbmc_parse_optionst::doit()`
`532`	`532`	`path_strategy_chooser,`
`533`	`533`	`options,`
`534`	`534`	`goto_model,`
`535`		`- ui_message_handler.get_ui(),`
`536`		`- *this);`
	`535`	`+ ui_message_handler);`
`537`	`536`	`}`
`538`	`537`
`539`	`538`	`bool cbmc_parse_optionst::set_properties()`
Original file line number	Diff line number	Diff line change
`@@ -70,7 +70,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()`
`70`	`70`	`solver->set_prop(util_make_unique<satcheckt>());`
`71`	`71`	`}`
`72`	`72`
`73`		`- solver->prop().set_message_handler(get_message_handler());`
	`73`	`+ solver->prop().set_message_handler(ui);`
`74`	`74`
`75`	`75`	`auto bv_cbmc=util_make_unique<bv_cbmct>(ns, solver->prop());`
`76`	`76`
`@@ -90,7 +90,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()`
`90`	`90`	`no_incremental_check();`
`91`	`91`
`92`	`92`	`auto prop=util_make_unique<dimacs_cnft>();`
`93`		`- prop->set_message_handler(get_message_handler());`
	`93`	`+ prop->set_message_handler(ui);`
`94`	`94`
`95`	`95`	`std::string filename=options.get_option("outfile");`
`96`	`96`
`@@ -111,12 +111,12 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()`
`111`	`111`	`return util_make_unique<satcheck_no_simplifiert>();`
`112`	`112`	`}();`
`113`	`113`
`114`		`- prop->set_message_handler(get_message_handler());`
	`114`	`+ prop->set_message_handler(ui);`
`115`	`115`
`116`	`116`	`bv_refinementt::infot info;`
`117`	`117`	`info.ns=&ns;`
`118`	`118`	`info.prop=prop.get();`
`119`		`- info.ui=ui;`
	`119`	`+ info.ui=ui.get_ui();`
`120`	`120`
`121`	`121`	`// we allow setting some parameters`
`122`	`122`	`if(options.get_bool_option("max-node-refinement"))`
`@@ -139,10 +139,10 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()`
`139`	`139`	`string_refinementt::infot info;`
`140`	`140`	`info.ns=&ns;`
`141`	`141`	`auto prop=util_make_unique<satcheck_no_simplifiert>();`
`142`		`- prop->set_message_handler(get_message_handler());`
	`142`	`+ prop->set_message_handler(ui);`
`143`	`143`	`info.prop=prop.get();`
`144`	`144`	`info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;`
`145`		`- info.ui=ui;`
	`145`	`+ info.ui=ui.get_ui();`
`146`	`146`	`if(options.get_bool_option("string-max-length"))`
`147`	`147`	`info.max_string_length = options.get_signed_int_option("string-max-length");`
`148`	`148`	`info.trace=options.get_bool_option("trace");`
`@@ -159,6 +159,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()`
`159`	`159`	`std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(`
`160`	`160`	`smt2_dect::solvert solver)`
`161`	`161`	`{`
	`162`	`+ messaget msg(ui);`
`162`	`163`	`no_beautification();`
`163`	`164`
`164`	`165`	`const std::string &filename=options.get_option("outfile");`
`@@ -167,7 +168,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(`
`167`	`168`	`{`
`168`	`169`	`if(solver==smt2_dect::solvert::GENERIC)`
`169`	`170`	`{`
`170`		`- error() << "please use --outfile" << eom;`
	`171`	`+ msg.error() << "please use --outfile" << messaget::eom;`
`171`	`172`	`throw 0;`
`172`	`173`	`}`
`173`	`174`
`@@ -198,7 +199,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(`
`198`	`199`	`if(options.get_bool_option("fpa"))`
`199`	`200`	`smt2_conv->use_FPA_theory=true;`
`200`	`201`
`201`		`- smt2_conv->set_message_handler(get_message_handler());`
	`202`	`+ smt2_conv->set_message_handler(ui);`
`202`	`203`
`203`	`204`	`return util_make_unique<solvert>(std::move(smt2_conv));`
`204`	`205`	`}`
`@@ -212,7 +213,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(`
`212`	`213`
`213`	`214`	`if(!*out)`
`214`	`215`	`{`
`215`		`- error() << "failed to open " << filename << eom;`
	`216`	`+ msg.error() << "failed to open " << filename << messaget::eom;`
`216`	`217`	`throw 0;`
`217`	`218`	`}`
`218`	`219`
`@@ -228,7 +229,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(`
`228`	`229`	`if(options.get_bool_option("fpa"))`
`229`	`230`	`smt2_conv->use_FPA_theory=true;`
`230`	`231`
`231`		`- smt2_conv->set_message_handler(get_message_handler());`
	`232`	`+ smt2_conv->set_message_handler(ui);`
`232`	`233`
`233`	`234`	`return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));`
`234`	`235`	`}`
`@@ -238,7 +239,8 @@ void cbmc_solverst::no_beautification()`
`238`	`239`	`{`
`239`	`240`	`if(options.get_bool_option("beautify"))`
`240`	`241`	`{`
`241`		`- error() << "sorry, this solver does not support beautification" << eom;`
	`242`	`+ messaget(ui).error() << "sorry, this solver does not support beautification"`
	`243`	`+ << messaget::eom;`
`242`	`244`	`throw 0;`
`243`	`245`	`}`
`244`	`246`	`}`
`@@ -249,7 +251,8 @@ void cbmc_solverst::no_incremental_check()`
`249`	`251`	`options.get_option("cover")!="" \|\|`
`250`	`252`	`options.get_option("incremental-check")!="")`
`251`	`253`	`{`
`252`		`- error() << "sorry, this solver does not support incremental solving" << eom;`
	`254`	`+ messaget(ui).error() << "sorry, this solver does not support incremental "`
	`255`	`+ << "solving" << messaget::eom;`
`253`	`256`	`throw 0;`
`254`	`257`	`}`
`255`	`258`	`}`
Original file line number	Diff line number	Diff line change
`@@ -289,7 +289,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()`
`289`	`289`	`// localize faults`
`290`	`290`	`run(ID_nil);`
`291`	`291`
`292`		`- switch(bmc.ui)`
	`292`	`+ switch(bmc.ui_message_handler.get_ui())`
`293`	`293`	`{`
`294`	`294`	`case ui_message_handlert::uit::PLAIN:`
`295`	`295`	`{`
`@@ -356,7 +356,7 @@ void fault_localizationt::report(`
`356`	`356`	`{`
`357`	`357`	`bmc_all_propertiest::report(cover_goals);`
`358`	`358`
`359`		`- switch(bmc.ui)`
	`359`	`+ switch(bmc.ui_message_handler.get_ui())`
`360`	`360`	`{`
`361`	`361`	`case ui_message_handlert::uit::PLAIN:`
`362`	`362`	`if(cover_goals.number_covered()>0)`
Original file line number	Diff line number	Diff line change
`@@ -148,7 +148,7 @@ void bmct::show_vcc()`
`148`	`148`
`149`	`149`	`std::ostream &out=have_file?of:std::cout;`
`150`	`150`
`151`		`- switch(ui)`
	`151`	`+ switch(ui_message_handler.get_ui())`
`152`	`152`	`{`
`153`	`153`	`case ui_message_handlert::uit::XML_UI:`
`154`	`154`	`error() << "XML UI not supported" << eom;`