diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-14 17:42:47 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-14 17:42:47 +0000 |
commit | 4c956f292906c59ba77c000084a08a4e7888e49b (patch) | |
tree | b068a48c9fc8579eb078432ad6335b48e9a820d6 /src/main | |
parent | 69693d7c8e5ca84b76fa807cb0797823058caa9a (diff) |
some changes to make CVC4 work nicely with trace executor for application track; (set-option :print-success true) supported, (exit) causes immediate exit regardless of EOF, etc.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/driver.cpp | 7 | ||||
-rw-r--r-- | src/main/driver_portfolio.cpp | 3 |
2 files changed, 10 insertions, 0 deletions
diff --git a/src/main/driver.cpp b/src/main/driver.cpp index 00072d6d9..5ecfed3a6 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -242,6 +242,9 @@ int runCvc4(int argc, char* argv[], Options& options) { *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1); } + // important even for muzzled builds (to get result output right) + *options.out << Expr::setlanguage(options.outputLanguage); + // Parse and execute commands until we are done Command* cmd; bool status = true; @@ -281,6 +284,10 @@ int runCvc4(int argc, char* argv[], Options& options) { replayParser->useDeclarationsFrom(parser); } while((cmd = parser->nextCommand())) { + if(dynamic_cast<QuitCommand*>(cmd) != NULL) { + delete cmd; + break; + } status = doCommand(smt, cmd, options) && status; delete cmd; } diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp index 1908d3e90..7972cd94d 100644 --- a/src/main/driver_portfolio.cpp +++ b/src/main/driver_portfolio.cpp @@ -301,6 +301,9 @@ int runCvc4(int argc, char *argv[], Options& options) { << Expr::printtypes(false); } + // important even for muzzled builds (to get result output right) + *options.out << Expr::setlanguage(options.outputLanguage); + vector<Options> threadOptions; for(int i = 0; i < numThreads; ++i) { threadOptions.push_back(options); |