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 e43c8a6ee2d328d93967c20937dda024048bab3c..1da4446a6895aa7019701effe33984382d9483d0 100644 (file)
--- 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);