From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 16 Feb 2013 20:35:16 +0000 (-0500)
Subject: Single -q quiets messages/warnings.  Double -qq silences sat/unsat output too.
X-Git-Tag: cvc5-1.0.0~7403
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=deb304550fbb6e19346319ec24d83e0650c64e91;p=cvc5.git

Single -q quiets messages/warnings.  Double -qq silences sat/unsat output too.
---

diff --git a/NEWS b/NEWS
index 445ba9ecf..ba396ad0c 100644
--- a/NEWS
+++ b/NEWS
@@ -10,5 +10,9 @@ Changes since 1.0
 * for printing commands as they're invoked from the driver, you now need
   verbosity of 3 or higher (e.g. -vvv) instead of verbosity 1 or higher (-v).
   This allows tracing the solver's activities without having too much output.
+* To make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
+  use -q.  Previously, this would silence all output (including "sat" or
+  "unsat") as well.  Now, single -q silences messages and warnings, and
+  double -qq silences all output (except on exception or signal).
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Mon, 04 Feb 2013 16:24:20 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 20 Feb 2013 18:31:50 -0500
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 010d4a6f4..6a4e18b5b 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -59,7 +59,7 @@ bool CommandExecutor::doCommand(Command* cmd)
 bool CommandExecutor::doCommandSingleton(Command *cmd)
 {
   bool status = true;
-  if(d_options[options::verbosity] >= 0) {
+  if(d_options[options::verbosity] >= -1) {
     status = smtEngineInvoke(&d_smtEngine, cmd, d_options[options::out]);
   } else {
     status = smtEngineInvoke(&d_smtEngine, cmd, NULL);