diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 15 |
1 files changed, 2 insertions, 13 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5296a3bca..de4537807 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1318,18 +1318,6 @@ void SmtEngine::setDefaults() { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - if (options::incrementalSolving()) - { - if (options::incrementalSolving.wasSetByUser()) - { - throw OptionException(std::string( - "Eager bit-blasting does not currently support incremental mode. " - "Try --bitblast=lazy")); - } - Notice() << "SmtEngine: turning off incremental to support eager " - << "bit-blasting" << endl; - setOption("incremental", SExpr("false")); - } if (options::produceModels() && (d_logic.isTheoryEnabled(THEORY_ARRAYS) || d_logic.isTheoryEnabled(THEORY_UF))) @@ -4160,7 +4148,8 @@ void SmtEnginePrivate::processAssertions() { "Try --bv-div-zero-const to interpret division by zero as a constant."); } - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER + && !options::incrementalSolving()) { d_preprocessingPassRegistry.getPass("bv-ackermann")->apply(&d_assertions); } |