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

diff --git a/NEWS b/NEWS
index 445ba9ecf5559071bb2348a24f4468391d78ce90..ba396ad0c5d442d8a04d7914e19e7a116eed15b4 100644 (file)
--- 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 010d4a6f42dd9e96efb644ca3f16dcc1aa9e5c1c..6a4e18b5b12e698e9bd0278d3a5477b72ae8e52c 100644 (file)
--- 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);