Fix option handler for lazy/bv-sat-solver combinations. (#2225)

Further, unifies all *limitHandler and *limitPerHandler to limitHandler.

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()) {