From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 29 Nov 2013 16:32:29 +0000 (-0500)
Subject: Fix proofs build.
X-Git-Tag: cvc5-1.0.0~7229
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d542d80f1241341752ed1843b63799435642c6f2;p=cvc5.git

Fix proofs build.
---

diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index d97d11364..9c2d5aaa4 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -552,10 +552,6 @@ ${all_modules_option_handlers}
     }
   }
 
-  if((*this)[options::incrementalSolving] && (*this)[options::proof]) {
-    throw OptionException(std::string("The use of --incremental with --proof is not yet supported"));
-  }
-
   Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl;
 
   return nonOptions;
@@ -576,7 +572,7 @@ std::vector<std::string> Options::suggestCommandLineOptions(const std::string& o
 
 static const char* smtOptions[] = {
   ${all_modules_smt_options},
-#line 580 "${template}"
+#line 576 "${template}"
   NULL
 };/* smtOptions[] */
 
@@ -598,7 +594,7 @@ SExpr Options::getOptions() const throw() {
 
   ${all_modules_get_options}
 
-#line 602 "${template}"
+#line 598 "${template}"
 
   return SExpr(opts);
 }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2e1d5de3c..07b30a87e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1140,6 +1140,11 @@ void SmtEngine::setLogicInternal() throw() {
     }
   }
 
+  if (options::incrementalSolving() && options::proof()) {
+    Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof" << endl;
+    setOption("incremental", SExpr("false"));
+  }
+
   // datatypes theory should assign values to all datatypes terms if logic is quantified
   if (d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_DATATYPES)) {
     if( !options::dtForceAssignment.wasSetByUser() ){