From 1fc1ce023da9b9596d19965b50d20b37fa6bb571 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 4 Jun 2014 15:22:38 -0400 Subject: [PATCH] Fix usability issue with tear-down incremental mode. --- src/main/driver_unified.cpp | 18 +++++++++++++++--- 1 file 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); -- 2.30.2