diff options
Diffstat (limited to 'src/main/usage.h')
-rw-r--r-- | src/main/usage.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/main/usage.h b/src/main/usage.h index 4da37749b..982dd240e 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -47,7 +47,9 @@ CVC4 options:\n\ --quiet | -q decrease verbosity (repeatable)\n\ --trace | -t tracing for something (e.g. --trace pushpop)\n\ --debug | -d debugging for something (e.g. --debug arith), implies -t\n\ - --stats give statistics on exit\n" + --stats give statistics on exit\n\ + --strict-parsing FIXME\n\ + --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n" #endif ; |