summaryrefslogtreecommitdiff
path: root/src/main/usage.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/usage.h')
-rw-r--r--src/main/usage.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/main/usage.h b/src/main/usage.h
index 3a609d2ec..c8ca6a179 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -32,7 +32,8 @@ CVC4 options:\n\
--help | -h this command line reference\n\
--verbose | -v increase verbosity (repeatable)\n\
--quiet | -q decrease verbosity (repeatable)\n\
- --debug | -d debugging for something (e.g. --debug arith)\n\
+ --trace | -t tracing for something (e.g. --trace pushpop)\n\
+ --debug | -d debugging for something (e.g. --debug arith), implies -t\n\
--smtcomp competition mode (very quiet)\n\
--stats give statistics on exit\n\
--segv-nospin (debug builds only) don't spin on segfault waiting for gdb\n\
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback