From be7ed89f137f4d0d64cf66ec40880370fbff2d4d Mon Sep 17 00:00:00 2001 From: "Andrew V. Jones" Date: Fri, 21 Feb 2020 18:19:45 +0000 Subject: [PATCH] Adding checks to the validation of 'bv-sat-solver' to ensure that the selected SAT solver is compiled-in (#3771) --- src/options/options_handler.cpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) 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 -- 2.30.2