diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-10 16:20:42 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-10 16:20:42 -0400 |
| commit | c30a3426c7c2cbaff88b5183b8d8c368a393ac4d (patch) | |
| tree | bd621f3766d2ae330a6c11499fe0a49958afa95d /src/main/driver_unified.cpp | |
| parent | d4f76fdfaed04bf63bb609a5fd26b0d45a9e94f4 (diff) | |
| parent | e926fd162c6cee95d31044305e3b4df90b59f9fc (diff) | |
Merge remote-tracking branch 'origin/master' into segfaultfix
Diffstat (limited to 'src/main/driver_unified.cpp')
| -rw-r--r-- | src/main/driver_unified.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 2f75c8887..1202c7882 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -133,6 +133,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { # ifndef PORTFOLIO_BUILD if( opts.wasSetByUser(options::threads) || + opts.wasSetByUser(options::threadStackSize) || ! opts[options::threadArgv].empty() ) { throw OptionException("Thread options cannot be used with sequential CVC4. Please build and use the portfolio binary `pcvc4'."); } @@ -337,7 +338,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { replayParser->useDeclarationsFrom(parser); } bool needReset = false; - while(status && (cmd = parser->nextCommand())) { + while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) { if(dynamic_cast<PushCommand*>(cmd) != NULL) { if(needReset) { pExecutor->reset(); @@ -416,7 +417,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { // have the replay parser use the file's declarations replayParser->useDeclarationsFrom(parser); } - while(status && (cmd = parser->nextCommand())) { + while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) { status = pExecutor->doCommand(cmd); if(dynamic_cast<QuitCommand*>(cmd) != NULL) { delete cmd; |