Incremental is now on by default when using from API, off for command-line driver except in interactive mode.

1 files changed, 9 insertions, 1 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index e9d071918..3f5e5424e 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -194,7 +194,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   pExecutor = new CommandExecutor(*exprMgr, opts);
 # else
   vector<Options> threadOpts = parseThreadSpecificOptions(opts);
-  if(opts[options::incrementalSolving] && !opts[options::incrementalParallel]) {
+  if(opts.wasSetByUser[options::incrementalSolving] &&
+     opts[options::incrementalSolving] &&
+     !opts[options::incrementalParallel]) {
     Notice() << "Notice: In --incremental mode, using the sequential solver unless forced by...\n"
              << "Notice: ...the experimental --incremental-parallel option.\n";
     exprMgr = new ExprManager(opts);
@@ -264,6 +266,12 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         delete cmd;
       }
     } else {
+      if(!opts.wasSetByUser(options::incrementalSolving)) {
+        cmd = new SetOptionCommand("incremental", false);
+        pExecutor->doCommand(cmd);
+        delete cmd;
+      }
+
       ParserBuilder parserBuilder(exprMgr, filename, opts);
 
       if( inputFromStdin ) {