diff options
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/bv_options.toml | 3 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 5 |
2 files changed, 6 insertions, 2 deletions
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 6a0ca913b..acb010a2e 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -236,6 +236,9 @@ header = "options/bv_options.h" default = "LAZY" help = "choose bit-vector solver, see --bv-solver=help" help_mode = "Bit-vector solvers." +[[option.mode.BITBLAST]] + name = "bitblast" + help = "Enables bitblasting solver." [[option.mode.LAZY]] name = "lazy" help = "Enables the lazy BV solver infrastructure." diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index fe37e9363..ac33d9c51 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -145,8 +145,9 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) throw OptionException(ss.str()); } - if (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL - || m == SatSolverMode::KISSAT) + if (options::bvSolver() != options::BVSolver::BITBLAST + && (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL + || m == SatSolverMode::KISSAT)) { if (options::bitblastMode() == options::BitblastMode::LAZY && options::bitblastMode.wasSetByUser()) |