Adding checks to the validation of 'bv-sat-solver' to ensure that the selected SAT...

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index c99b0c7b52f07cd6cff7e0e38b6414120f3bf1ed..3e6c4da3ca4b072b51f5779ef2e8cedf8cfaaf68 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -147,6 +147,25 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
 
 void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
 {
+  if (m == SatSolverMode::CRYPTOMINISAT
+      && !Configuration::isBuiltWithCryptominisat())
+  {
+    std::stringstream ss;
+    ss << "option `" << option
+       << "' requires a CryptoMiniSat build of CVC4; this binary was not built "
+          "with CryptoMiniSat support";
+    throw OptionException(ss.str());
+  }
+
+  if (m == SatSolverMode::CADICAL && !Configuration::isBuiltWithCadical())
+  {
+    std::stringstream ss;
+    ss << "option `" << option
+       << "' requires a CaDiCaL build of CVC4; this binary was not built with "
+          "CaDiCaL support";
+    throw OptionException(ss.str());
+  }
+
   if (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL)
   {
     if (options::bitblastMode() == options::BitblastMode::LAZY