type checking for define-fun in production builds; related to (and might resolve) bug 212

1 files changed, 6 insertions, 2 deletions

diff --git a/src/main/usage.h b/src/main/usage.h
index 2be5f092e..15a30a426 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -46,8 +46,12 @@ CVC4 options:\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\
-   --uf=morgan|tim        select uninterpreted function theory implementation\n"
-;
+   --uf=morgan|tim        select uninterpreted function theory implementation\n\
+   --interactive          run interactively\n\
+   --no-interactive       do not run interactively\n\
+   --produce-models       support the get-value command\n\
+   --produce-assignments  support the get-assignment command\n\
+   --lazy-definition-expansion expand define-fun lazily\n";
 
 }/* CVC4::main namespace */
 }/* CVC4 namespace */