1 files changed, 10 insertions, 1 deletions
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 2c20e06bb..4f214ddd1 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -73,7 +73,7 @@ benchmark\n\
   modes.\n\
 \n\
 declarations\n\
-+ Dump declarations.  Implied by all following modes.\n\
++ Dump user declarations.  Implied by all following modes.\n\
 \n\
 assertions\n\
 + Output the assertions after non-clausal simplification and static\n\
@@ -82,6 +82,11 @@ assertions\n\
   (--simplification=none --no-static-learning), the output\n\
   will closely resemble the input (with term-level ITEs removed).\n\
 \n\
+skolems\n\
++ Dump internally-created skolem variable declarations.  These can\n\
+  arise from preprocessing simplifications, existential elimination,\n\
+  and a number of other things.  Implied by all following modes.\n\
+\n\
 learned\n\
 + Output the assertions after non-clausal simplification, static\n\
   learning, and presolve-time T-lemmas.  This should include all eager\n\
@@ -172,6 +177,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
     if(!strcmp(optargPtr, "benchmark")) {
     } else if(!strcmp(optargPtr, "declarations")) {
     } else if(!strcmp(optargPtr, "assertions")) {
+    } else if(!strcmp(optargPtr, "skolems")) {
     } else if(!strcmp(optargPtr, "learned")) {
     } else if(!strcmp(optargPtr, "clauses")) {
     } else if(!strcmp(optargPtr, "t-conflicts") ||
@@ -219,6 +225,9 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
     Dump.on("benchmark");
     if(strcmp(optargPtr, "benchmark")) {
       Dump.on("declarations");
+      if(strcmp(optargPtr, "declarations") && strcmp(optargPtr, "assertions")) {
+        Dump.on("skolems");
+      }
     }
   }
   free(optargPtr);