Limit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL (#2868)

Fixes #1715. We do not support the `--solve-int-as-bv=X` preprocessing
pass with logics other than pure QF_NIA/QF_LIA/QF_IDL. This commit adds
a corresponding check and throws an option exception if an incompatible
logic has been set.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9914992efef3ef3d2fbd9ee2d1b2c1b7dee94219..8427599a9807b101c3a74aed618fa05eae6df7a8 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1209,6 +1209,12 @@ void SmtEngine::setDefaults() {
   if(options::forceLogicString.wasSetByUser()) {
     d_logic = LogicInfo(options::forceLogicString());
   }else if (options::solveIntAsBV() > 0) {
+    if (!(d_logic <= LogicInfo("QF_NIA")))
+    {
+      throw OptionException(
+          "--solve-int-as-bv=X only supported for pure integer logics (QF_NIA, "
+          "QF_LIA, QF_IDL)");
+    }
     d_logic = LogicInfo("QF_BV");
   }else if (d_logic.getLogicString() == "QF_NRA" && options::solveRealAsInt()) {
     d_logic = LogicInfo("QF_NIA");