From f588fa1e9263bd96642343340b0eefc006838a4c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 22 Aug 2024 14:57:40 +0000
Subject: [PATCH] Remove dynamic_cast from hardness collection code paths

Use a `shared_ptr` to retain co-ownership of the hardness collector in
`solver_factoryt::solvert` and adjust the `symex_target_equationt` API
to `consume a solver_hardnesst`.
---
 src/goto-checker/bmc_util.cpp                 | 10 ++-
 src/goto-checker/bmc_util.h                   |  6 --
 .../goto_symex_property_decider.cpp           | 12 ++-
 .../goto_symex_property_decider.h             |  4 +
 src/goto-checker/multi_path_symex_checker.cpp |  7 +-
 .../single_loop_incremental_symex_checker.cpp |  7 +-
 src/goto-checker/solver_factory.cpp           | 75 +++++++++++-----
 src/goto-checker/solver_factory.h             |  7 ++
 .../accelerate/scratch_program.cpp            |  2 +-
 src/goto-symex/solver_hardness.h              | 22 -----
 src/goto-symex/symex_target_equation.cpp      | 89 ++++++++++++-------
 src/goto-symex/symex_target_equation.h        | 64 ++++++++++---
 src/solvers/hardness_collector.h              |  2 +-
 src/solvers/prop/prop_conv_solver.h           | 12 +--
 14 files changed, 201 insertions(+), 118 deletions(-)

diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp
index 6e31d312d77..605ad17ae80 100644
--- a/src/goto-checker/bmc_util.cpp
+++ b/src/goto-checker/bmc_util.cpp
@@ -147,15 +147,16 @@ void output_graphml(
   }
 }
 
-void convert_symex_target_equation(
+static void convert_symex_target_equation(
   symex_target_equationt &equation,
   decision_proceduret &decision_procedure,
+  solver_hardnesst *hardness_collector,
   message_handlert &message_handler)
 {
   messaget msg(message_handler);
   msg.status() << "converting SSA" << messaget::eom;
 
-  equation.convert(decision_procedure);
+  equation.convert(decision_procedure, hardness_collector);
 }
 
 std::unique_ptr<memory_model_baset>
@@ -370,7 +371,10 @@ std::chrono::duration<double> prepare_property_decider(
     << messaget::eom;
 
   convert_symex_target_equation(
-    equation, property_decider.get_decision_procedure(), ui_message_handler);
+    equation,
+    property_decider.get_decision_procedure(),
+    property_decider.get_hardness_collector(),
+    ui_message_handler);
   property_decider.update_properties_goals_from_symex_target_equation(
     properties);
   property_decider.convert_goals();
diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h
index 92e0e3a82de..0af83f54d4d 100644
--- a/src/goto-checker/bmc_util.h
+++ b/src/goto-checker/bmc_util.h
@@ -25,7 +25,6 @@ class decision_proceduret;
 class goto_symex_property_decidert;
 class goto_tracet;
 class memory_model_baset;
-class message_handlert;
 class namespacet;
 class optionst;
 class symex_bmct;
@@ -33,11 +32,6 @@ class symex_target_equationt;
 struct trace_optionst;
 class ui_message_handlert;
 
-void convert_symex_target_equation(
-  symex_target_equationt &equation,
-  decision_proceduret &decision_procedure,
-  message_handlert &message_handler);
-
 /// Returns a function that checks whether an SSA step is an assertion
 /// with \p property_id. Usually used for `build_goto_trace`.
 ssa_step_predicatet
diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp
index 7dcc0fe1c40..96e3177c659 100644
--- a/src/goto-checker/goto_symex_property_decider.cpp
+++ b/src/goto-checker/goto_symex_property_decider.cpp
@@ -100,13 +100,14 @@ void goto_symex_property_decidert::add_constraint_from_goals(
   exprt goal_disjunction = disjunction(disjuncts);
   decision_procedure.set_to_true(goal_disjunction);
 
-  with_solver_hardness(decision_procedure, [](solver_hardnesst &hardness) {
+  if(auto hardness = solver->hardness_collector())
+  {
     // SSA expr and involved steps have already been collected
     // in symex_target_equationt::convert_assertions
     exprt ssa_expr_unused;
     std::vector<goto_programt::const_targett> involved_steps_unused;
-    hardness.register_assertion_ssas(ssa_expr_unused, involved_steps_unused);
-  });
+    hardness->register_assertion_ssas(ssa_expr_unused, involved_steps_unused);
+  };
 }
 
 decision_proceduret::resultt goto_symex_property_decidert::solve()
@@ -125,6 +126,11 @@ boolbvt &goto_symex_property_decidert::get_boolbv_decision_procedure() const
   return solver->boolbv_decision_procedure();
 }
 
+solver_hardnesst *goto_symex_property_decidert::get_hardness_collector() const
+{
+  return solver->hardness_collector();
+}
+
 symex_target_equationt &goto_symex_property_decidert::get_equation() const
 {
   return equation;
diff --git a/src/goto-checker/goto_symex_property_decider.h b/src/goto-checker/goto_symex_property_decider.h
index 21b4036b65d..63e7a6fc0a7 100644
--- a/src/goto-checker/goto_symex_property_decider.h
+++ b/src/goto-checker/goto_symex_property_decider.h
@@ -50,6 +50,10 @@ class goto_symex_property_decidert
   /// Returns the solver instance
   boolbvt &get_boolbv_decision_procedure() const;
 
+  /// Returns a pointer to the hardness collector or `nullptr` when hardness
+  /// collection is not set up.
+  solver_hardnesst *get_hardness_collector() const;
+
   /// Return the equation associated with this instance
   symex_target_equationt &get_equation() const;
 
diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp
index 40f60b6ed85..6576909e504 100644
--- a/src/goto-checker/multi_path_symex_checker.cpp
+++ b/src/goto-checker/multi_path_symex_checker.cpp
@@ -169,8 +169,9 @@ void multi_path_symex_checkert::report()
 {
   if(options.is_set("write-solver-stats-to"))
   {
-    with_solver_hardness(
-      property_decider.get_decision_procedure(),
-      [](solver_hardnesst &hardness) { hardness.produce_report(); });
+    if(auto hardness = property_decider.get_hardness_collector())
+    {
+      hardness->produce_report();
+    }
   }
 }
diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/src/goto-checker/single_loop_incremental_symex_checker.cpp
index 47a2194d55d..0f2cab6a85d 100644
--- a/src/goto-checker/single_loop_incremental_symex_checker.cpp
+++ b/src/goto-checker/single_loop_incremental_symex_checker.cpp
@@ -108,7 +108,8 @@ operator()(propertiest &properties)
 
         log.status() << "converting SSA" << messaget::eom;
         equation.convert_without_assertions(
-          property_decider.get_decision_procedure());
+          property_decider.get_decision_procedure(),
+          property_decider.get_hardness_collector());
 
         property_decider.update_properties_goals_from_symex_target_equation(
           properties);
@@ -116,7 +117,9 @@ operator()(propertiest &properties)
         // We convert the assertions in a new context.
         property_decider.get_decision_procedure().push();
         equation.convert_assertions(
-          property_decider.get_decision_procedure(), false);
+          property_decider.get_decision_procedure(),
+          property_decider.get_hardness_collector(),
+          false);
         property_decider.convert_goals();
 
         current_equation_converted = true;
diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
index 79d4c2a2d99..38d8a3b0e58 100644
--- a/src/goto-checker/solver_factory.cpp
+++ b/src/goto-checker/solver_factory.cpp
@@ -19,7 +19,6 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/unicode.h>
 #include <util/version.h>
 
-#include <goto-symex/solver_hardness.h>
 #include <solvers/flattening/bv_dimacs.h>
 #include <solvers/prop/prop.h>
 #include <solvers/prop/solver_resource_limits.h>
@@ -71,6 +70,16 @@ solver_factoryt::solvert::solvert(
 {
 }
 
+solver_factoryt::solvert::solvert(
+  std::unique_ptr<boolbvt> p1,
+  std::unique_ptr<propt> p2,
+  std::shared_ptr<solver_hardnesst> p3)
+  : hardness_ptr(std::move(p3)),
+    prop_ptr(std::move(p2)),
+    decision_procedure_is_boolbvt_ptr(std::move(p1))
+{
+}
+
 stack_decision_proceduret &solver_factoryt::solvert::decision_procedure() const
 {
   PRECONDITION(
@@ -88,6 +97,11 @@ boolbvt &solver_factoryt::solvert::boolbv_decision_procedure() const
   return *decision_procedure_is_boolbvt_ptr;
 }
 
+solver_hardnesst *solver_factoryt::solvert::hardness_collector() const
+{
+  return hardness_ptr.get();
+}
+
 void solver_factoryt::set_decision_procedure_time_limit(
   solver_resource_limitst &decision_procedure)
 {
@@ -168,8 +182,9 @@ static void emit_solver_warning(
 template <typename SatcheckT>
 static typename std::enable_if<
   !std::is_base_of<hardness_collectort, SatcheckT>::value,
-  std::unique_ptr<SatcheckT>>::type
-make_satcheck_prop(message_handlert &message_handler, const optionst &options)
+  std::pair<std::unique_ptr<SatcheckT>, std::shared_ptr<solver_hardnesst>>>::
+  type
+  make_satcheck_prop(message_handlert &message_handler, const optionst &options)
 {
   auto satcheck = std::make_unique<SatcheckT>(message_handler);
   if(options.is_set("write-solver-stats-to"))
@@ -179,27 +194,29 @@ make_satcheck_prop(message_handlert &message_handler, const optionst &options)
       << "Configured solver does not support --write-solver-stats-to. "
       << "Solver stats will not be written." << messaget::eom;
   }
-  return satcheck;
+  return {std::move(satcheck), nullptr};
 }
 
 template <typename SatcheckT>
 static typename std::enable_if<
   std::is_base_of<hardness_collectort, SatcheckT>::value,
-  std::unique_ptr<SatcheckT>>::type
-make_satcheck_prop(message_handlert &message_handler, const optionst &options)
+  std::pair<std::unique_ptr<SatcheckT>, std::shared_ptr<solver_hardnesst>>>::
+  type
+  make_satcheck_prop(message_handlert &message_handler, const optionst &options)
 {
   auto satcheck = std::make_unique<SatcheckT>(message_handler);
-  if(options.is_set("write-solver-stats-to"))
-  {
-    std::unique_ptr<solver_hardnesst> solver_hardness =
-      std::make_unique<solver_hardnesst>();
-    solver_hardness->set_outfile(options.get_option("write-solver-stats-to"));
-    satcheck->solver_hardness = std::move(solver_hardness);
-  }
-  return satcheck;
+  if(!options.is_set("write-solver-stats-to"))
+    return {std::move(satcheck), nullptr};
+
+  std::shared_ptr<solver_hardnesst> solver_hardness =
+    std::make_shared<solver_hardnesst>();
+  solver_hardness->set_outfile(options.get_option("write-solver-stats-to"));
+  satcheck->solver_hardness = solver_hardness;
+
+  return {std::move(satcheck), std::move(solver_hardness)};
 }
 
-static std::unique_ptr<propt>
+static std::pair<std::unique_ptr<propt>, std::shared_ptr<solver_hardnesst>>
 get_sat_solver(message_handlert &message_handler, const optionst &options)
 {
   const bool no_simplifier = options.get_bool_option("beautify") ||
@@ -326,12 +343,15 @@ get_sat_solver(message_handlert &message_handler, const optionst &options)
 
 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
 {
-  auto sat_solver = get_sat_solver(message_handler, options);
+  auto sat_solver_and_hardness_opt = get_sat_solver(message_handler, options);
 
   bool get_array_constraints =
     options.get_bool_option("show-array-constraints");
   auto bv_pointers = std::make_unique<bv_pointerst>(
-    ns, *sat_solver, message_handler, get_array_constraints);
+    ns,
+    *sat_solver_and_hardness_opt.first,
+    message_handler,
+    get_array_constraints);
 
   if(options.get_option("arrays-uf") == "never")
     bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
@@ -341,7 +361,10 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
   set_decision_procedure_time_limit(*bv_pointers);
 
   std::unique_ptr<boolbvt> boolbv = std::move(bv_pointers);
-  return std::make_unique<solvert>(std::move(boolbv), std::move(sat_solver));
+  return std::make_unique<solvert>(
+    std::move(boolbv),
+    std::move(sat_solver_and_hardness_opt.first),
+    std::move(sat_solver_and_hardness_opt.second));
 }
 
 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
@@ -376,11 +399,11 @@ 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 = get_sat_solver(message_handler, options);
+  auto prop_and_hardness_opt = get_sat_solver(message_handler, options);
 
   bv_refinementt::infot info;
   info.ns = &ns;
-  info.prop = prop.get();
+  info.prop = prop_and_hardness_opt.first.get();
   info.output_xml = output_xml_in_refinement;
 
   // we allow setting some parameters
@@ -396,7 +419,9 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
     std::make_unique<bv_refinementt>(info);
   set_decision_procedure_time_limit(*decision_procedure);
   return std::make_unique<solvert>(
-    std::move(decision_procedure), std::move(prop));
+    std::move(decision_procedure),
+    std::move(prop_and_hardness_opt.first),
+    std::move(prop_and_hardness_opt.second));
 }
 
 /// the string refinement adds to the bit vector refinement specifications for
@@ -407,8 +432,8 @@ solver_factoryt::get_string_refinement()
 {
   string_refinementt::infot info;
   info.ns = &ns;
-  auto prop = get_sat_solver(message_handler, options);
-  info.prop = prop.get();
+  auto prop_and_hardness_opt = get_sat_solver(message_handler, options);
+  info.prop = prop_and_hardness_opt.first.get();
   info.refinement_bound = DEFAULT_MAX_NB_REFINEMENT;
   info.output_xml = output_xml_in_refinement;
   if(options.get_bool_option("max-node-refinement"))
@@ -422,7 +447,9 @@ solver_factoryt::get_string_refinement()
     std::make_unique<string_refinementt>(info);
   set_decision_procedure_time_limit(*decision_procedure);
   return std::make_unique<solvert>(
-    std::move(decision_procedure), std::move(prop));
+    std::move(decision_procedure),
+    std::move(prop_and_hardness_opt.first),
+    std::move(prop_and_hardness_opt.second));
 }
 
 std::unique_ptr<std::ofstream> open_outfile_and_check(
diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h
index 98784c45ba2..c44576943ca 100644
--- a/src/goto-checker/solver_factory.h
+++ b/src/goto-checker/solver_factory.h
@@ -12,6 +12,7 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
 #define CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
 
+#include <goto-symex/solver_hardness.h>
 #include <solvers/flattening/boolbv.h>
 #include <solvers/smt2/smt2_dec.h>
 
@@ -46,11 +47,17 @@ class solver_factoryt final
       std::unique_ptr<stack_decision_proceduret> p1,
       std::unique_ptr<std::ofstream> p2);
     solvert(std::unique_ptr<boolbvt> p1, std::unique_ptr<propt> p2);
+    solvert(
+      std::unique_ptr<boolbvt> p1,
+      std::unique_ptr<propt> p2,
+      std::shared_ptr<solver_hardnesst> p3);
 
     stack_decision_proceduret &decision_procedure() const;
     boolbvt &boolbv_decision_procedure() const;
+    solver_hardnesst *hardness_collector() const;
 
   private:
+    std::shared_ptr<solver_hardnesst> hardness_ptr;
     // the objects are deleted in the opposite order they appear below
     std::unique_ptr<std::ofstream> ofstream_ptr;
     std::unique_ptr<propt> prop_ptr;
diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp
index daae044e9cd..e48811c035c 100644
--- a/src/goto-instrument/accelerate/scratch_program.cpp
+++ b/src/goto-instrument/accelerate/scratch_program.cpp
@@ -63,7 +63,7 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
     return false;
   }
 
-  equation.convert(*checker);
+  equation.convert(*checker, nullptr);
 
 #ifdef DEBUG
   std::cout << "Finished symex, invoking decision procedure.\n";
diff --git a/src/goto-symex/solver_hardness.h b/src/goto-symex/solver_hardness.h
index 97c466fcc2a..d655e2682d0 100644
--- a/src/goto-symex/solver_hardness.h
+++ b/src/goto-symex/solver_hardness.h
@@ -158,26 +158,4 @@ struct hash<solver_hardnesst::hardness_ssa_keyt>
 };
 } // namespace std
 
-static inline void with_solver_hardness(
-  decision_proceduret &maybe_hardness_collector,
-  std::function<void(solver_hardnesst &hardness)> handler)
-{
-  // FIXME I am wondering if there is a way to do this that is a bit less
-  // dynamically typed.
-  if(
-    auto prop_conv_solver =
-      dynamic_cast<prop_conv_solvert *>(&maybe_hardness_collector))
-  {
-    if(auto hardness_collector = prop_conv_solver->get_hardness_collector())
-    {
-      if(hardness_collector->solver_hardness)
-      {
-        auto &solver_hardness = static_cast<solver_hardnesst &>(
-          *(hardness_collector->solver_hardness));
-        handler(solver_hardness);
-      }
-    }
-  }
-}
-
 #endif // CPROVER_SOLVERS_SOLVER_HARDNESS_H
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index b785acc6b07..7152c8915a5 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -19,6 +19,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <chrono> // IWYU pragma: keep
 
+static void with_solver_hardness(
+  solver_hardnesst *maybe_hardness_collector,
+  std::function<void(solver_hardnesst &hardness)> handler)
+{
+  if(maybe_hardness_collector)
+    handler(*maybe_hardness_collector);
+}
+
 static std::function<void(solver_hardnesst &)>
 hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
 {
@@ -328,28 +336,31 @@ void symex_target_equationt::constraint(
 }
 
 void symex_target_equationt::convert_without_assertions(
-  decision_proceduret &decision_procedure)
+  decision_proceduret &decision_procedure,
+  solver_hardnesst *hardness_collector)
 {
-  with_solver_hardness(decision_procedure, [&](solver_hardnesst &hardness) {
+  with_solver_hardness(hardness_collector, [&](solver_hardnesst &hardness) {
     hardness.register_ssa_size(SSA_steps.size());
   });
 
-  convert_guards(decision_procedure);
-  convert_assignments(decision_procedure);
-  convert_decls(decision_procedure);
-  convert_assumptions(decision_procedure);
-  convert_goto_instructions(decision_procedure);
-  convert_function_calls(decision_procedure);
-  convert_io(decision_procedure);
-  convert_constraints(decision_procedure);
+  convert_guards(decision_procedure, hardness_collector);
+  convert_assignments(decision_procedure, hardness_collector);
+  convert_decls(decision_procedure, hardness_collector);
+  convert_assumptions(decision_procedure, hardness_collector);
+  convert_goto_instructions(decision_procedure, hardness_collector);
+  convert_function_calls(decision_procedure, hardness_collector);
+  convert_io(decision_procedure, hardness_collector);
+  convert_constraints(decision_procedure, hardness_collector);
 }
 
-void symex_target_equationt::convert(decision_proceduret &decision_procedure)
+void symex_target_equationt::convert(
+  decision_proceduret &decision_procedure,
+  solver_hardnesst *hardness_collector)
 {
   const auto convert_SSA_start = std::chrono::steady_clock::now();
 
-  convert_without_assertions(decision_procedure);
-  convert_assertions(decision_procedure, true);
+  convert_without_assertions(decision_procedure, hardness_collector);
+  convert_assertions(decision_procedure, hardness_collector, true);
 
   const auto convert_SSA_stop = std::chrono::steady_clock::now();
   std::chrono::duration<double> convert_SSA_runtime =
@@ -359,7 +370,8 @@ void symex_target_equationt::convert(decision_proceduret &decision_procedure)
 }
 
 void symex_target_equationt::convert_assignments(
-  decision_proceduret &decision_procedure)
+  decision_proceduret &decision_procedure,
+  solver_hardnesst *hardness_collector)
 {
   std::size_t step_index = 0;
   for(auto &step : SSA_steps)
@@ -374,14 +386,15 @@ void symex_target_equationt::convert_assignments(
       decision_procedure.set_to_true(step.cond_expr);
       step.converted = true;
       with_solver_hardness(
-        decision_procedure, hardness_register_ssa(step_index, step));
+        hardness_collector, hardness_register_ssa(step_index, step));
     }
     ++step_index;
   }
 }
 
 void symex_target_equationt::convert_decls(
-  decision_proceduret &decision_procedure)
+  decision_proceduret &decision_procedure,
+  solver_hardnesst *hardness_collector)
 {
   std::size_t step_index = 0;
   for(auto &step : SSA_steps)
@@ -395,14 +408,15 @@ void symex_target_equationt::convert_decls(
         equal_exprt{step.ssa_full_lhs, step.ssa_full_lhs});
       step.converted = true;
       with_solver_hardness(
-        decision_procedure, hardness_register_ssa(step_index, step));
+        hardness_collector, hardness_register_ssa(step_index, step));
     }
     ++step_index;
   }
 }
 
 void symex_target_equationt::convert_guards(
-  decision_proceduret &decision_procedure)
+  decision_proceduret &decision_procedure,
+  solver_hardnesst *hardness_collector)
 {
   std::size_t step_index = 0;
   for(auto &step : SSA_steps)
@@ -418,7 +432,7 @@ void symex_target_equationt::convert_guards(
 
       step.guard_handle = decision_procedure.handle(step.guard);
       with_solver_hardness(
-        decision_procedure, [step_index, &step](solver_hardnesst &hardness) {
+        hardness_collector, [step_index, &step](solver_hardnesst &hardness) {
           hardness.register_ssa(step_index, step.guard, step.source.pc);
         });
     }
@@ -427,7 +441,8 @@ void symex_target_equationt::convert_guards(
 }
 
 void symex_target_equationt::convert_assumptions(
-  decision_proceduret &decision_procedure)
+  decision_proceduret &decision_procedure,
+  solver_hardnesst *hardness_collector)
 {
   std::size_t step_index = 0;
   for(auto &step : SSA_steps)
@@ -447,7 +462,7 @@ void symex_target_equationt::convert_assumptions(
         step.cond_handle = decision_procedure.handle(step.cond_expr);
 
         with_solver_hardness(
-          decision_procedure, hardness_register_ssa(step_index, step));
+          hardness_collector, hardness_register_ssa(step_index, step));
       }
     }
     ++step_index;
@@ -455,7 +470,8 @@ void symex_target_equationt::convert_assumptions(
 }
 
 void symex_target_equationt::convert_goto_instructions(
-  decision_proceduret &decision_procedure)
+  decision_proceduret &decision_procedure,
+  solver_hardnesst *hardness_collector)
 {
   std::size_t step_index = 0;
   for(auto &step : SSA_steps)
@@ -474,7 +490,7 @@ void symex_target_equationt::convert_goto_instructions(
 
         step.cond_handle = decision_procedure.handle(step.cond_expr);
         with_solver_hardness(
-          decision_procedure, hardness_register_ssa(step_index, step));
+          hardness_collector, hardness_register_ssa(step_index, step));
       }
     }
     ++step_index;
@@ -482,7 +498,8 @@ void symex_target_equationt::convert_goto_instructions(
 }
 
 void symex_target_equationt::convert_constraints(
-  decision_proceduret &decision_procedure)
+  decision_proceduret &decision_procedure,
+  solver_hardnesst *hardness_collector)
 {
   std::size_t step_index = 0;
   for(auto &step : SSA_steps)
@@ -498,7 +515,7 @@ void symex_target_equationt::convert_constraints(
       step.converted = true;
 
       with_solver_hardness(
-        decision_procedure, hardness_register_ssa(step_index, step));
+        hardness_collector, hardness_register_ssa(step_index, step));
     }
     ++step_index;
   }
@@ -506,6 +523,7 @@ void symex_target_equationt::convert_constraints(
 
 void symex_target_equationt::convert_assertions(
   decision_proceduret &decision_procedure,
+  solver_hardnesst *hardness_collector,
   bool optimized_for_single_assertions)
 {
   // we find out if there is only _one_ assertion,
@@ -532,7 +550,7 @@ void symex_target_equationt::convert_assertions(
         step.cond_handle = false_exprt();
 
         with_solver_hardness(
-          decision_procedure, hardness_register_ssa(step_index, step));
+          hardness_collector, hardness_register_ssa(step_index, step));
         return; // prevent further assumptions!
       }
       else if(step.is_assume())
@@ -540,7 +558,7 @@ void symex_target_equationt::convert_assertions(
         decision_procedure.set_to_true(step.cond_expr);
 
         with_solver_hardness(
-          decision_procedure, hardness_register_ssa(step_index, step));
+          hardness_collector, hardness_register_ssa(step_index, step));
       }
       ++step_index;
     }
@@ -580,7 +598,7 @@ void symex_target_equationt::convert_assertions(
       step.cond_handle = decision_procedure.handle(implication);
 
       with_solver_hardness(
-        decision_procedure,
+        hardness_collector,
         [&involved_steps, &step](solver_hardnesst &hardness) {
           involved_steps.push_back(step.source.pc);
         });
@@ -598,7 +616,7 @@ void symex_target_equationt::convert_assertions(
         assumption = and_exprt(assumption, step.cond_handle);
 
       with_solver_hardness(
-        decision_procedure,
+        hardness_collector,
         [&involved_steps, &step](solver_hardnesst &hardness) {
           involved_steps.push_back(step.source.pc);
         });
@@ -610,14 +628,15 @@ void symex_target_equationt::convert_assertions(
   decision_procedure.set_to_true(assertion_disjunction);
 
   with_solver_hardness(
-    decision_procedure,
+    hardness_collector,
     [&assertion_disjunction, &involved_steps](solver_hardnesst &hardness) {
       hardness.register_assertion_ssas(assertion_disjunction, involved_steps);
     });
 }
 
 void symex_target_equationt::convert_function_calls(
-  decision_proceduret &decision_procedure)
+  decision_proceduret &decision_procedure,
+  solver_hardnesst *hardness_collector)
 {
   std::size_t step_index = 0;
   for(auto &step : SSA_steps)
@@ -646,7 +665,7 @@ void symex_target_equationt::convert_function_calls(
         }
       }
       with_solver_hardness(
-        decision_procedure,
+        hardness_collector,
         [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
           hardness.register_ssa(
             step_index, conjunction(conjuncts), step.source.pc);
@@ -656,7 +675,9 @@ void symex_target_equationt::convert_function_calls(
   }
 }
 
-void symex_target_equationt::convert_io(decision_proceduret &decision_procedure)
+void symex_target_equationt::convert_io(
+  decision_proceduret &decision_procedure,
+  solver_hardnesst *hardness_collector)
 {
   std::size_t step_index = 0;
   for(auto &step : SSA_steps)
@@ -684,7 +705,7 @@ void symex_target_equationt::convert_io(decision_proceduret &decision_procedure)
         }
       }
       with_solver_hardness(
-        decision_procedure,
+        hardness_collector,
         [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
           hardness.register_ssa(
             step_index, conjunction(conjuncts), step.source.pc);
diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h
index 8d1ab192f7a..c766dfb4943 100644
--- a/src/goto-symex/symex_target_equation.h
+++ b/src/goto-symex/symex_target_equation.h
@@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class decision_proceduret;
 class namespacet;
+class solver_hardnesst;
 
 /// Inheriting the interface of symex_targett this class represents the SSA
 /// form of the input program as a list of \ref SSA_stept. It further extends
@@ -172,7 +173,11 @@ class symex_target_equationt:public symex_targett
   /// format. The method iterates over the equation, i.e. over the SSA steps and
   /// converts each type of step separately.
   /// \param decision_procedure: A handle to a decision procedure interface
-  void convert(decision_proceduret &decision_procedure);
+  /// \param hardness_collector: If non-null, a collector for hardness
+  ///   statistics
+  void convert(
+    decision_proceduret &decision_procedure,
+    solver_hardnesst *hardness_collector);
 
   /// Interface method to initiate the conversion into a decision procedure
   /// format. The method iterates over the equation, i.e. over the SSA steps and
@@ -181,14 +186,21 @@ class symex_target_equationt:public symex_targett
   /// e.g. for incremental solving.
   /// \param decision_procedure: A handle to a particular decision procedure
   ///   interface
-  void convert_without_assertions(decision_proceduret &decision_procedure);
+  /// \param hardness_collector: If non-null, a collector for hardness
+  ///   statistics
+  void convert_without_assertions(
+    decision_proceduret &decision_procedure,
+    solver_hardnesst *hardness_collector);
 
   /// Converts assertions: build a disjunction of negated assertions.
   /// \param decision_procedure: A handle to a decision procedure interface
+  /// \param hardness_collector: If non-null, a collector for hardness
+  ///   statistics
   /// \param optimized_for_single_assertions: Use an optimized encoding for
   ///   single assertions (unsound for incremental conversions)
   void convert_assertions(
     decision_proceduret &decision_procedure,
+    solver_hardnesst *hardness_collector,
     bool optimized_for_single_assertions);
 
   typedef std::list<SSA_stept> SSA_stepst;
@@ -230,40 +242,72 @@ class symex_target_equationt:public symex_targett
   /// Converts assignments: set the equality _lhs==rhs_ to _True_.
   /// \param decision_procedure: A handle to a decision procedure
   ///  interface
-  void convert_assignments(decision_proceduret &decision_procedure);
+  /// \param hardness_collector: If non-null, a collector for hardness
+  ///   statistics
+  void convert_assignments(
+    decision_proceduret &decision_procedure,
+    solver_hardnesst *hardness_collector);
 
   /// Converts declarations: these are effectively ignored by the decision
   /// procedure.
   /// \param decision_procedure: A handle to a decision procedure
   ///  interface
-  void convert_decls(decision_proceduret &decision_procedure);
+  /// \param hardness_collector: If non-null, a collector for hardness
+  ///   statistics
+  void convert_decls(
+    decision_proceduret &decision_procedure,
+    solver_hardnesst *hardness_collector);
 
   /// Converts assumptions: convert the expression the assumption represents.
   /// \param decision_procedure: A handle to a decision procedure interface
-  void convert_assumptions(decision_proceduret &decision_procedure);
+  /// \param hardness_collector: If non-null, a collector for hardness
+  ///   statistics
+  void convert_assumptions(
+    decision_proceduret &decision_procedure,
+    solver_hardnesst *hardness_collector);
 
   /// Converts constraints: set the represented condition to _True_.
   /// \param decision_procedure: A handle to a decision procedure interface
-  void convert_constraints(decision_proceduret &decision_procedure);
+  /// \param hardness_collector: If non-null, a collector for hardness
+  ///   statistics
+  void convert_constraints(
+    decision_proceduret &decision_procedure,
+    solver_hardnesst *hardness_collector);
 
   /// Converts goto instructions: convert the expression representing the
   /// condition of this goto.
   /// \param decision_procedure: A handle to a decision procedure interface
-  void convert_goto_instructions(decision_proceduret &decision_procedure);
+  /// \param hardness_collector: If non-null, a collector for hardness
+  ///   statistics
+  void convert_goto_instructions(
+    decision_proceduret &decision_procedure,
+    solver_hardnesst *hardness_collector);
 
   /// Converts guards: convert the expression the guard represents.
   /// \param decision_procedure: A handle to a decision procedure interface
-  void convert_guards(decision_proceduret &decision_procedure);
+  /// \param hardness_collector: If non-null, a collector for hardness
+  ///   statistics
+  void convert_guards(
+    decision_proceduret &decision_procedure,
+    solver_hardnesst *hardness_collector);
 
   /// Converts function calls: for each argument build an equality between its
   /// symbol and the argument itself.
   /// \param decision_procedure: A handle to a decision procedure interface
-  void convert_function_calls(decision_proceduret &decision_procedure);
+  /// \param hardness_collector: If non-null, a collector for hardness
+  ///   statistics
+  void convert_function_calls(
+    decision_proceduret &decision_procedure,
+    solver_hardnesst *hardness_collector);
 
   /// Converts I/O: for each argument build an equality between its
   /// symbol and the argument itself.
   /// \param decision_procedure: A handle to a decision procedure interface
-  void convert_io(decision_proceduret &decision_procedure);
+  /// \param hardness_collector: If non-null, a collector for hardness
+  ///   statistics
+  void convert_io(
+    decision_proceduret &decision_procedure,
+    solver_hardnesst *hardness_collector);
 
   messaget log;
 
diff --git a/src/solvers/hardness_collector.h b/src/solvers/hardness_collector.h
index 88a9e8e0087..b16c979c819 100644
--- a/src/solvers/hardness_collector.h
+++ b/src/solvers/hardness_collector.h
@@ -44,7 +44,7 @@ class clause_hardness_collectort
 class hardness_collectort
 {
 public:
-  std::unique_ptr<clause_hardness_collectort> solver_hardness;
+  std::shared_ptr<clause_hardness_collectort> solver_hardness;
 };
 
 #endif // CPROVER_SOLVERS_HARDNESS_COLLECTOR_H
diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h
index f8bcb40fda1..1a30dcbc029 100644
--- a/src/solvers/prop/prop_conv_solver.h
+++ b/src/solvers/prop/prop_conv_solver.h
@@ -9,19 +9,18 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_PROP_PROP_CONV_SOLVER_H
 #define CPROVER_SOLVERS_PROP_PROP_CONV_SOLVER_H
 
-#include <map>
-#include <string>
-
 #include <util/expr.h>
 #include <util/message.h>
 
 #include <solvers/conflict_provider.h>
-#include <solvers/hardness_collector.h>
 
 #include "prop.h"
 #include "prop_conv.h"
 #include "solver_resource_limits.h"
 
+#include <map>
+#include <string>
+
 class equal_exprt;
 
 class prop_conv_solvert : public conflict_providert,
@@ -99,11 +98,6 @@ class prop_conv_solvert : public conflict_providert,
 
   std::size_t get_number_of_solver_calls() const override;
 
-  hardness_collectort *get_hardness_collector()
-  {
-    return dynamic_cast<hardness_collectort *>(&prop);
-  }
-
 protected:
   bool post_processing_done = false;