Honour --sat-solver with refinement

Refinement should not unconditionally use the default solver despite the
user specifying `--sat-solver <solver>` on the command line.

Author: tautschnig

src/goto-checker/solver_factory.cpp

@@ -396,16 +396,7 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
 
 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
 {
-  std::unique_ptr<propt> prop = [this]() -> std::unique_ptr<propt> {
-    // We offer the option to disable the SAT preprocessor
-    if(options.get_bool_option("sat-preprocessor"))
-    {
-      no_beautification();
-      return make_satcheck_prop<satcheckt>(message_handler, options);
-    }
-    return make_satcheck_prop<satcheck_no_simplifiert>(
-      message_handler, options);
-  }();
+  std::unique_ptr<propt> prop = get_sat_solver(message_handler, options);
 
   bv_refinementt::infot info;
   info.ns = &ns;
@@ -435,8 +426,7 @@ solver_factoryt::get_string_refinement()
 {
   string_refinementt::infot info;
   info.ns = &ns;
-  auto prop =
-    make_satcheck_prop<satcheck_no_simplifiert>(message_handler, options);
+  auto prop = get_sat_solver(message_handler, options);
   info.prop = prop.get();
   info.refinement_bound = DEFAULT_MAX_NB_REFINEMENT;
   info.output_xml = output_xml_in_refinement;