summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/driver_unified.cpp10
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 ) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback