From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 4 Jun 2014 19:22:38 +0000 (-0400)
Subject: Fix usability issue with tear-down incremental mode.
X-Git-Tag: cvc5-1.0.0~6861
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1fc1ce023da9b9596d19965b50d20b37fa6bb571;p=cvc5.git

Fix usability issue with tear-down incremental mode.
---

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