Remove ui from bv_refinementt::configt

Author: tautschnig

src/cbmc/cbmc_solvers.cpp

@@ -115,7 +115,6 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
   bv_refinementt::infot info;
   info.ns=&ns;
   info.prop=prop.get();
-  info.ui=ui;
 
   // we allow setting some parameters
   if(options.get_bool_option("max-node-refinement"))
@@ -141,7 +140,6 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
   prop->set_message_handler(get_message_handler());
   info.prop=prop.get();
   info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
-  info.ui=ui;
   if(options.get_bool_option("max-node-refinement"))
     info.max_node_refinement=
       options.get_unsigned_int_option("max-node-refinement");

src/solvers/refinement/bv_refinement.h

@@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
 #define CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
 
-#include <util/ui_message.h>
-
 #include <solvers/flattening/bv_pointers.h>
 
 #define MAX_STATE 10000
@@ -23,7 +21,6 @@ class bv_refinementt:public bv_pointerst
 private:
   struct configt
   {
-    ui_message_handlert::uit ui=ui_message_handlert::uit::PLAIN;
     /// Max number of times we refine a formula node
     unsigned max_node_refinement=5;
     /// Enable array refinement