Ignore error result when an error is squelched via command verbosity.

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 87836b116d018a396bf573f512f345b99d65cf3a..5dc10a4739a8ef088d24ce943e6276e3ebbcd95a 100644 (file)
--- 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();
 }