diff options
Diffstat (limited to 'src')
-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(); } |