diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-04 15:22:38 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-04 15:22:38 -0400 |
commit | 1fc1ce023da9b9596d19965b50d20b37fa6bb571 (patch) | |
tree | 325a68dea04afceeba0f5c52612622804500af40 | |
parent | 468f1afc7546ad47dc8aac097aa738c374acdc82 (diff) |
Fix usability issue with tear-down incremental mode.
-rw-r--r-- | src/main/driver_unified.cpp | 18 |
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); |