From ab1c041c8fb93ccd7923945d52e14cc741dfe63e Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sat, 18 Apr 2020 16:28:38 +0100
Subject: [PATCH] Satcheck need not implement hardness_collectort

Otherwise compilation fails for SAT solvers that
don't implement hardness_collectort yet, e.g. Glucose.
---
 src/goto-checker/solver_factory.cpp | 20 ++++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
index 926aa3897f6..1c162b3fd6b 100644
--- a/src/goto-checker/solver_factory.cpp
+++ b/src/goto-checker/solver_factory.cpp
@@ -183,10 +183,22 @@ make_satcheck_prop(message_handlert &message_handler, const optionst &options)
   auto satcheck = util_make_unique<SatcheckT>(message_handler);
   if(options.is_set("write-solver-stats-to"))
   {
-    satcheck->enable_hardness_collection();
-    satcheck->with_solver_hardness([&options](solver_hardnesst &hardness) {
-      hardness.set_outfile(options.get_option("write-solver-stats-to"));
-    });
+    if(
+      auto hardness_collector = dynamic_cast<hardness_collectort *>(&*satcheck))
+    {
+      hardness_collector->enable_hardness_collection();
+      hardness_collector->with_solver_hardness(
+        [&options](solver_hardnesst &hardness) {
+          hardness.set_outfile(options.get_option("write-solver-stats-to"));
+        });
+    }
+    else
+    {
+      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;
 }