From 192aa1b5d98ca1a0a2c5e5c8ec603ebb9d14d261 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 16 Mar 2019 06:23:06 +0000 Subject: [PATCH] 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. --- src/smt/smt_engine.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9914992ef..8427599a9 100644 --- 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"); -- 2.30.2