diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-07-31 11:25:27 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-31 11:25:27 -0700 |
commit | 0b2eb659087dd3643e57fe39ee84f6cb42721e94 (patch) | |
tree | d273e0b2d7207f1fb5c1e49ebdfcb77d00eb0992 /src/smt | |
parent | cf97bbba5725abcb7a4085271719de8b1a832628 (diff) |
Fix option handler for lazy/bv-sat-solver combinations. (#2225)
Further, unifies all *limitHandler and *limitPerHandler to limitHandler.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index de4537807..801711a13 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1334,6 +1334,13 @@ void SmtEngine::setDefaults() { << "generation" << endl; setOption("bitblastMode", SExpr("lazy")); } + + if (options::incrementalSolving() && !d_logic.isPure(THEORY_BV)) + { + throw OptionException( + "Incremental eager bit-blasting is currently " + "only supported for QF_BV. Try --bitblast=lazy."); + } } if(options::forceLogicString.wasSetByUser()) { |