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.h37
1 files changed, 16 insertions, 21 deletions
diff --git a/src/main/usage.h b/src/main/usage.h
index ef37b7650..b56f083a5 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -30,27 +30,22 @@ usage: %s [options] [input-file]\n\
Without an input file, or with `-', CVC4 reads from standard input.\n\
\n\
CVC4 options:\n\
- --lang | -L force input language (default is `auto'; see --lang help)\n\
- --version | -V identify this CVC4 binary\n\
- --help | -h this command line reference\n\
- --parse-only exit after parsing input\n\
- --mmap memory map file input\n\
- --show-config show CVC4 static configuration\n"
-#ifdef CVC4_DEBUG
-"\
- --segv-nospin don't spin on segfault waiting for gdb\n"
-#endif
-#ifndef CVC4_MUZZLE
-"\
- --no-checking disable semantic checks in the parser\n\
- --strict-parsing fail on inputs that are not strictly conformant (SMT2 only)\n\
- --verbose | -v increase verbosity (repeatable)\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\
- --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n"
-#endif
+ --lang | -L force input language (default is `auto'; see --lang help)\n\
+ --version | -V identify this CVC4 binary\n\
+ --help | -h this command line reference\n\
+ --parse-only exit after parsing input\n\
+ --mmap memory map file input\n\
+ --show-config show CVC4 static configuration\n\
+ --segv-nospin don't spin on segfault waiting for gdb\n\
+ --no-checking disable semantic checks in the parser\n\
+ --strict-parsing fail on inputs that are not strictly conformant (SMT2 only)\n\
+ --verbose | -v increase verbosity (repeatable)\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\
+ --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
+ --print-expr-types print types with variables when printing exprs\n"
;
}/* CVC4::main namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback