From 5e08a8137ac8836e1dcdea842f45effe518d2e8c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 7 Aug 2024 11:04:50 +0000
Subject: [PATCH] Solver factory: make_satcheck_prop does not require
 dynamic_cast

We can determine at compile time whether a particular solver has harness
support for any given call site.
---
 src/goto-checker/solver_factory.cpp | 40 +++++++++++++++++------------
 1 file changed, 24 insertions(+), 16 deletions(-)

diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
index c44842474a8..49de6a2d7a4 100644
--- a/src/goto-checker/solver_factory.cpp
+++ b/src/goto-checker/solver_factory.cpp
@@ -188,27 +188,35 @@ static void emit_solver_warning(
 }
 
 template <typename SatcheckT>
-static std::unique_ptr<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)
 {
   auto satcheck = std::make_unique<SatcheckT>(message_handler);
   if(options.is_set("write-solver-stats-to"))
   {
-    if(
-      auto hardness_collector = dynamic_cast<hardness_collectort *>(&*satcheck))
-    {
-      std::unique_ptr<solver_hardnesst> solver_hardness =
-        std::make_unique<solver_hardnesst>();
-      solver_hardness->set_outfile(options.get_option("write-solver-stats-to"));
-      hardness_collector->solver_hardness = std::move(solver_hardness);
-    }
-    else
-    {
-      messaget log(message_handler);
-      log.warning()
-        << "Configured solver does not support --write-solver-stats-to. "
-        << "Solver stats will not be written." << messaget::eom;
-    }
+    messaget log(message_handler);
+    log.warning()
+      << "Configured solver does not support --write-solver-stats-to. "
+      << "Solver stats will not be written." << messaget::eom;
+  }
+  return satcheck;
+}
+
+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)
+{
+  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;
 }