* more complete support for --dump assertions:{pre,post}-PREPROCESSING-PASS

* more minor cleanup/doc

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 5 insertions, 1 deletions

diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 43d53ee4c..60b3b48c2 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -83,7 +83,8 @@ skolems\n\
 assertions\n\
 + Output the assertions after preprocessing and before clausification.\n\
   Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
-  where PASS is one of the preprocessing passes: skolem-quant simplify\n\
+  where PASS is one of the preprocessing passes: definition-expansion\n\
+  constrain-subtypes substitution skolem-quant simplify\n\
   static-learning ite-removal repeat-simplify theory-preprocessing.\n\
   PASS can also be the special value \"everything\", in which case the\n\
   assertions are printed before any preprocessing (with\n\
@@ -176,6 +177,9 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
                               optargPtr + "'.  Please consult --dump help.");
       }
       if(!strcmp(p, "everything")) {
+      } else if(!strcmp(p, "definition-expansion")) {
+      } else if(!strcmp(p, "constrain-subtypes")) {
+      } else if(!strcmp(p, "substitution")) {
       } else if(!strcmp(p, "skolem-quant")) {
       } else if(!strcmp(p, "simplify")) {
       } else if(!strcmp(p, "static-learning")) {