Disallow --proof and --incremental (#3332)

1 files changed, 12 insertions, 5 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8705bfb9b..d72b303a6 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2269,13 +2269,20 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  if(options::incrementalSolving() && options::proof()) {
-    Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof, try --tear-down-incremental instead)" << endl;
-    setOption("incremental", SExpr("false"));
-  }
-
   if (options::proof())
   {
+    if (options::incrementalSolving())
+    {
+      if (options::incrementalSolving.wasSetByUser())
+      {
+        throw OptionException("--incremental is not supported with proofs");
+      }
+      Warning()
+          << "SmtEngine: turning off incremental solving mode (not yet "
+             "supported with --proof, try --tear-down-incremental instead)"
+          << endl;
+      setOption("incremental", SExpr("false"));
+    }
     if (d_logic > LogicInfo("QF_AUFBVLRA")) {
         throw OptionException(
             "Proofs are only supported for sub-logics of QF_AUFBVLIA.");