1 files changed, 8 insertions, 0 deletions
diff --git a/src/util/options.h b/src/util/options.h
index 699895c47..1e392e87d 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -223,6 +223,14 @@ struct CVC4_PUBLIC Options {
    */
   static void printUsage(const std::string msg, std::ostream& out);
 
+  /**
+   * Print command-line option usage message for only the most-commonly
+   * used options.  The message is prefixed by "msg"---which could be
+   * an error message causing the usage output in the first place, e.g.
+   * "no such option --foo"
+   */
+  static void printShortUsage(const std::string msg, std::ostream& out);
+
   /** Print help for the --lang command line option */
   static void printLanguageHelp(std::ostream& out);