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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8705bfb9bb8f48d13fa79a3f5599b6cd4c3c1814..d72b303a67e7a87c5038c8f9736808f7c852bf85 100644 (file)
--- 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."); 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d3f463afd3d6515be3529d55dfab27d7de3ae191..194dbd66305ca2978756ed5f9cf1ef2364ddc380 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -553,6 +553,7 @@ set(regress_0_tests
   regress0/nl/very-easy-sat.smt2
   regress0/nl/very-simple-unsat.smt2
   regress0/options/invalid_dump.smt2
+  regress0/options/invalid_option_inc_proofs.smt2
   regress0/opt-abd-no-use.smt2
   regress0/parallel-let.smt2
   regress0/parser/as.smt2

diff --git a/test/regress/regress0/options/invalid_option_inc_proofs.smt2 b/test/regress/regress0/options/invalid_option_inc_proofs.smt2
new file mode 100644 (file)
index 0000000..f63dbd2
--- /dev/null
+++ b/test/regress/regress0/options/invalid_option_inc_proofs.smt2
@@ -0,0 +1,6 @@
+; REQUIRES: proof
+; COMMAND-LINE: --incremental --proof
+; EXPECT: (error "Error in option parsing: --incremental is not supported with proofs")
+; EXIT: 1
+(set-logic QF_BV)
+(check-sat)