From 09af96d09c4cb90c976fee700daba8af34bed1e4 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 8 Oct 2019 09:05:50 -0700
Subject: [PATCH] Disallow --proof and --incremental (#3332)

---
 src/smt/smt_engine.cpp                          | 17 ++++++++++++-----
 test/regress/CMakeLists.txt                     |  1 +
 .../options/invalid_option_inc_proofs.smt2      |  6 ++++++
 3 files changed, 19 insertions(+), 5 deletions(-)
 create mode 100644 test/regress/regress0/options/invalid_option_inc_proofs.smt2

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."); 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d3f463afd..194dbd663 100644
--- 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
index 000000000..f63dbd27f
--- /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)
-- 
2.30.2