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.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/main/usage.h b/src/main/usage.h
index 9fdc6a67b..2be5f092e 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -45,7 +45,8 @@ CVC4 options:\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"
+ --print-expr-types print types with variables when printing exprs\n\
+ --uf=morgan|tim select uninterpreted function theory implementation\n"
;
}/* CVC4::main namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback