diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-27 18:34:44 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-27 18:34:44 +0000 |
commit | e56c41f47d43103a6e8bf744e12229ed6e5a8f19 (patch) | |
tree | 39be4124610edf8072206aa85b178b8fe3eab2e2 /src/main/usage.h | |
parent | 14c22833d05f632eb40eb68cc3c68345d891005c (diff) |
Adding --mmap option to use memory-mapped file input, which provides a marginal improvement (<5%) on big benchmarks.
Diffstat (limited to 'src/main/usage.h')
-rw-r--r-- | src/main/usage.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/main/usage.h b/src/main/usage.h index 6c44fef5a..3a609d2ec 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -37,6 +37,8 @@ CVC4 options:\n\ --stats give statistics on exit\n\ --segv-nospin (debug builds only) don't spin on segfault waiting for gdb\n\ --parse-only exit after parsing input\n\ + --no-checking disable semantic checks in the parser\n\ + --mmap memory map file input\n\ --show-config show CVC4 static configuration\n\ "; |