diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-04 22:22:41 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-04 22:22:41 +0000 |
commit | ce6c366450cc9cb30c254f26089696c1c7c913c0 (patch) | |
tree | a7ea29ec2f222c0e7ae4d9559a486905be10a923 /src/main | |
parent | 5d9670acc3c8eacdebdbb07302a8e35f837d0e52 (diff) |
Accepted some patches from the Multicore Programming Group at Imperial College London (via Peter Collingbourne):
cvc4-0001-Look-for-cxxtestgen-as-well-as-cxxtestgen.pl-and-cxx.patch
* better checking for cxxtest
cvc4-0002-Do-not-read-an-additional-command-after-failure.patch
* more correct failure behavior for interactive tools
cvc4-0003-Only-exit-when-encountering-a-CommandFailure.patch
* don't consider "unsupported" as a failure (accepted with modifications)
cvc4-0004-Produce-SMT-LIB-v2-conformant-output-for-get-info.patch
* better get-info responses (accepted with modifications)
These patches will help the group build Boogie support for CVC4.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/driver.cpp | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/main/driver.cpp b/src/main/driver.cpp index ca5dfad93..1e6f87d24 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -293,12 +293,12 @@ int runCvc4(int argc, char* argv[], Options& opts) { // have the replay parser use the file's declarations replayParser->useDeclarationsFrom(parser); } - while((cmd = parser->nextCommand()) && status) { + while(status && (cmd = parser->nextCommand())) { if(dynamic_cast<QuitCommand*>(cmd) != NULL) { delete cmd; break; } - status = doCommand(smt, cmd, opts) && status; + status = doCommand(smt, cmd, opts); delete cmd; } // Remove the parser @@ -352,16 +352,18 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& opts) { return true; } - // assume no error - bool status = true; - CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd); if(seq != NULL) { + // assume no error + bool status = true; + for(CommandSequence::iterator subcmd = seq->begin(); - subcmd != seq->end(); + status && subcmd != seq->end(); ++subcmd) { - status = doCommand(smt, *subcmd, opts) && status; + status = doCommand(smt, *subcmd, opts); } + + return status; } else { if(opts[options::verbosity] > 0) { *opts[options::out] << "Invoking: " << *cmd << endl; @@ -372,8 +374,6 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& opts) { } else { cmd->invoke(&smt); } - status = status && cmd->ok(); + return !cmd->fail(); } - - return status; } |