From: Andrew V. Jones <andrew.jones@vector.com>
Date: Fri, 21 Feb 2020 18:19:45 +0000 (+0000)
Subject: Adding checks to the validation of 'bv-sat-solver' to ensure that the selected SAT... 
X-Git-Tag: cvc5-1.0.0~3623
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=be7ed89f137f4d0d64cf66ec40880370fbff2d4d;p=cvc5.git

Adding checks to the validation of 'bv-sat-solver' to ensure that the selected SAT solver is compiled-in (#3771)
---

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index c99b0c7b5..3e6c4da3c 100644
--- 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