From c5970b88e4334146fe142fa1644a2a36049a6448 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 26 Jun 2014 00:41:48 -0400
Subject: Ignore error result when an error is squelched via command verbosity.

---
 src/main/command_executor.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src')

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();
 }
 
-- 
cgit v1.2.3