1 files changed, 7 insertions, 0 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index e4c0276ea..565f28334 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -538,6 +538,9 @@ enum  \n\
 var-agnostic \n\
 + Use sygus solver to enumerate terms that are agnostic to variables. \n\
 \n\
+auto (default) \n\
++ Internally decide the best policy for each enumerator. \n\
+\n\
 ";
 
 const std::string OptionsHandler::s_macrosQuantHelp = "\
@@ -987,6 +990,10 @@ OptionsHandler::stringToSygusActiveGenMode(std::string option,
   {
     return theory::quantifiers::SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
   }
+  else if (optarg == "auto")
+  {
+    return theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO;
+  }
   else if (optarg == "help")
   {
     puts(s_sygusActiveGenHelp.c_str());