From a33002181a581f28da66cbc2c93626996a1fb1aa Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.stanford.edu>
Date: Wed, 14 Dec 2016 11:12:58 -0800
Subject: [PATCH] Made tear-down-incremental more like it used to be: when
 tear-down value is 1, it does not automatically enable incremental mode.

---
 src/main/driver_unified.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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);
-- 
2.30.2