summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-03-26 17:58:33 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-03-26 17:58:33 -0400
commita9912269ab2b47b783a66f381b14148c0ac73e93 (patch)
treef9804cc0b06369ac80b0771da405a6dd2227a484
parent70d1a0171840cd62b5c1d89b875ffb50da216793 (diff)
Make --incremental the default when running interactively
-rw-r--r--src/main/driver_unified.cpp9
1 files changed, 8 insertions, 1 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9fa40d3ab..bdce5639b 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -235,7 +235,14 @@ int runCvc4(int argc, char* argv[], Options& opts) {
// Parse and execute commands until we are done
Command* cmd;
bool status = true;
- if( opts[options::interactive] ) {
+ if(opts[options::interactive]) {
+#ifndef PORTFOLIO_BUILD
+ if(!opts.wasSetByUser(options::incrementalSolving)) {
+ cmd = new SetOptionCommand("incremental", true);
+ pExecutor->doCommand(cmd);
+ delete cmd;
+ }
+#endif /* PORTFOLIO_BUILD */
InteractiveShell shell(*exprMgr, opts);
Message() << Configuration::getPackageName()
<< " " << Configuration::getVersionString();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback