Fix usability issue with tear-down incremental mode.

1 files changed, 15 insertions, 3 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 8117dbc05..60b99132d 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -238,8 +238,14 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     Command* cmd;
     bool status = true;
     if(opts[options::interactive] && inputFromStdin) {
-      if( opts[options::tearDownIncremental] ) {
-        throw OptionException("--tear-down-incremental incompatible with --interactive");
+      if(opts[options::tearDownIncremental] && opts[options::incrementalSolving]) {
+        if(opts.wasSetByUser(options::incrementalSolving)) {
+          throw OptionException("--tear-down-incremental incompatible with --interactive");
+        }
+
+        cmd = new SetOptionCommand("incremental", false);
+        pExecutor->doCommand(cmd);
+        delete cmd;
       }
 #ifndef PORTFOLIO_BUILD
       if(!opts.wasSetByUser(options::incrementalSolving)) {
@@ -272,7 +278,13 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       }
     } else if(opts[options::tearDownIncremental]) {
       if(opts[options::incrementalSolving]) {
-        throw OptionException("--tear-down-incremental incompatible with --incremental");
+        if(opts.wasSetByUser(options::incrementalSolving)) {
+          throw OptionException("--tear-down-incremental incompatible with --interactive");
+        }
+
+        cmd = new SetOptionCommand("incremental", false);
+        pExecutor->doCommand(cmd);
+        delete cmd;
       }
 
       ParserBuilder parserBuilder(exprMgr, filename, opts);