From: Clark Barrett <barrett@cs.stanford.edu>
Date: Wed, 14 Dec 2016 19:12:58 +0000 (-0800)
Subject: Made tear-down-incremental more like it used to be: when tear-down value
X-Git-Tag: cvc5-1.0.0~5939
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a33002181a581f28da66cbc2c93626996a1fb1aa;p=cvc5.git

Made tear-down-incremental more like it used to be: when tear-down value
is 1, it does not automatically enable incremental mode.
---

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index e43c8a6ee..1da4446a6 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -320,7 +320,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         delete cmd;
       }
     } else if( opts.getTearDownIncremental() > 0) {
-      if(!opts.getIncrementalSolving()) {
+      if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) {
+        // For tear-down-incremental values greater than 1, need incremental
+        // on too.
         cmd = new SetOptionCommand("incremental", SExpr(true));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);