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.h6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/main/usage.h b/src/main/usage.h
index 7affc254c..5ad96aea6 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -37,8 +37,10 @@ CVC4 options:\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\
- --no-type-checking disable type checking [default in non-debug builds]\n\
+ --lazy-type-checking type check expressions only when necessary (default)\n\
+ --eager-type-checking type check expressions immediately on creation\n\
+ --no-type-checking never type check expressions\n\
+ --no-checking disable ALL semantic checks, including type checks \n\
--strict-parsing fail on non-conformant inputs (SMT2 only)\n\
--verbose | -v increase verbosity (repeatable)\n\
--quiet | -q decrease verbosity (repeatable)\n\
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback