diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-30 16:23:42 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-30 16:23:42 +0000 |
| commit | 206ceb28ca03fae452b420ad517a0b5bc82dab04 (patch) | |
| tree | 15c226ba991ac232ac15b35cd63c8fc627ef4efc /src | |
| parent | 4d2c7ccaa905534342fe99a23fc137c75a707d6a (diff) | |
Adding documentation for --strict-parsing (Closes: #166)
Diffstat (limited to 'src')
| -rw-r--r-- | src/main/usage.h | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/src/main/usage.h b/src/main/usage.h index 982dd240e..ef37b7650 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -30,25 +30,25 @@ 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" + --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" + --segv-nospin don't spin on segfault waiting for gdb\n" #endif #ifndef CVC4_MUZZLE "\ - --no-checking disable semantic checks in the parser\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\ - --strict-parsing FIXME\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" #endif ; |