summaryrefslogtreecommitdiff
path: root/src/main/usage.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-02-04 03:31:38 +0000
committerMorgan Deters <mdeters@gmail.com>2010-02-04 03:31:38 +0000
commitfc14c009e8e9d2274368b54c12f3580a9ec8f718 (patch)
tree853fdc64b8f6f29dc106e581dfe8ed8e4c569778 /src/main/usage.h
parent33988bd64b92960f7bed5c68d1266adc4183454b (diff)
src/expr/kind.h is now automatically generated.
Build src/expr before src/util. Moved CVC4::Command to the expr package. Re-quieted the "result is sat/invalid" etc. from PropEngine (this is now done at the main driver level). Added file-level documentation to Antlr sources When built for debug, spin on SEGV instead of aborting. Really useful for debugging problems that crop up only on long runs. Added '--segv-nospin' to override this spinning so that "make check," nightly regressions, etc. don't hang when built with debug. Updated src/main/about.h for 2010.
Diffstat (limited to 'src/main/usage.h')
-rw-r--r--src/main/usage.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/main/usage.h b/src/main/usage.h
index f6c089f1d..6927f0f2f 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -27,8 +27,7 @@ usage: %s [options] [input-file]\n\
Without an input file, or with `-', CVC4 reads from standard input.\n\
\n\
CVC4 options:\n\
- --lang | -L set input language (--lang help gives a list;\n\
- `auto' is default)\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\
--verbose | -v increase verbosity (repeatable)\n\
@@ -36,6 +35,7 @@ CVC4 options:\n\
--debug | -d debugging for something (e.g. --debug arith)\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\
";
}/* CVC4::main namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback