diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-16 06:23:06 +0000 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-16 06:23:06 +0000 |
| commit | 192aa1b5d98ca1a0a2c5e5c8ec603ebb9d14d261 (patch) | |
| tree | 02d53553529fcfe5cb43bca77abcbaf906309072 | |
| parent | 5d0a5a729680a1db3f44e31037955390e86440ce (diff) | |
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.
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
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"); |