From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 26 Jun 2014 04:41:48 +0000 (-0400)
Subject: Ignore error result when an error is squelched via command verbosity.
X-Git-Tag: cvc5-1.0.0~6721
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c5970b88e4334146fe142fa1644a2a36049a6448;p=cvc5.git

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 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();
 }