diff options
Diffstat (limited to 'src/smt/set_defaults.cpp')
| -rw-r--r-- | src/smt/set_defaults.cpp | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index f98c9ee84..c887d1895 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -133,8 +133,19 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) if (options::solveIntAsBV() > 0) { + // not compatible with incremental + if (options::incrementalSolving()) + { + throw OptionException( + "solving integers as bitvectors is currently not supported " + "when solving incrementally."); + } + // Int to BV currently always eliminates arithmetic completely (or otherwise + // fails). Thus, it is safe to eliminate arithmetic. Also, bit-vectors + // are required. logic = logic.getUnlockedCopy(); logic.enableTheory(THEORY_BV); + logic.disableTheory(THEORY_ARITH); logic.lock(); } @@ -565,7 +576,11 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) || logic.isTheoryEnabled(THEORY_SETS) // Non-linear arithmetic requires UF to deal with division/mod because // their expansion introduces UFs for the division/mod-by-zero case. - || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()) + // If we are eliminating non-linear arithmetic via solve-int-as-bv, + // then this is not required, since non-linear arithmetic will be + // eliminated altogether (or otherwise fail at preprocessing). + || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() + && options::solveIntAsBV() == 0) // If division/mod-by-zero is not treated as a constant value in BV, we // need UF. || (logic.isTheoryEnabled(THEORY_BV) |