summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-02-04 16:24:33 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2013-02-04 16:37:04 -0500
commit2c460aacc9b3d52e4c6423fa54a8437b5be5c04b (patch)
treea0d91d70a2c075fdfe054299c7d0a583f52b44e2
parentcc9733246f9f50625d049ee9aa6b12aff49cacc4 (diff)
Printing commands as they're executed now requires verbosity 3+
-rw-r--r--NEWS5
-rw-r--r--src/main/command_executor.cpp2
2 files changed, 5 insertions, 2 deletions
diff --git a/NEWS b/NEWS
index c25f09f5a..445ba9ecf 100644
--- a/NEWS
+++ b/NEWS
@@ -7,5 +7,8 @@ Changes since 1.0
* user patterns are now supported in the SMT-LIBv1.2 parser
* SMT-LIB get-model output now is easier to machine-parse: contains (model...)
* Win32 support via mingw
+* 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.
--- Morgan Deters <mdeters@cs.nyu.edu> Mon, 28 Jan 2013 15:26:24 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu> Mon, 04 Feb 2013 16:24:20 -0500
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 14625f1d8..010d4a6f4 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -48,7 +48,7 @@ bool CommandExecutor::doCommand(Command* cmd)
return status;
} else {
- if(d_options[options::verbosity] > 0) {
+ if(d_options[options::verbosity] > 2) {
*d_options[options::out] << "Invoking: " << *cmd << std::endl;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback