diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-26 00:41:48 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-26 00:48:18 -0400 |
commit | c5970b88e4334146fe142fa1644a2a36049a6448 (patch) | |
tree | 7a93a9b550e3149479dbe6ba00147f78c40d475d /src/main/command_executor.cpp | |
parent | 23e6498e2323bdc176a9fbf6a04cb3cfb672b058 (diff) |
Ignore error result when an error is squelched via command verbosity.
Diffstat (limited to 'src/main/command_executor.cpp')
-rw-r--r-- | src/main/command_executor.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 87836b116..5dc10a473 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -13,12 +13,14 @@ **/ #include <iostream> +#include <string> #include "main/command_executor.h" #include "expr/command.h" #include "main/main.h" +#include "main/options.h" #include "smt/options.h" #ifndef __WIN32__ @@ -151,6 +153,10 @@ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out) } else { cmd->invoke(smt, *out); } + // ignore the error if the command-verbosity is 0 for this command + if(smt->getOption(std::string("command-verbosity:") + cmd->getCommandName()).getIntegerValue() == 0) { + return true; + } return !cmd->fail(); } |