1 files changed, 15 insertions, 4 deletions
diff --git a/src/options/ufss_mode.h b/src/options/ufss_mode.h
index d6a106ecf..452317b8f 100644
--- a/src/options/ufss_mode.h
+++ b/src/options/ufss_mode.h
@@ -23,12 +23,23 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
-enum UfssMode{
-  /** default, use uf strong solver to find minimal models for uninterpreted sorts */
+/**
+ * These modes determine the role of UF with cardinality when using finite model
+ * finding (--finite-model-find).
+ */
+enum UfssMode
+{
+  /**
+   * Default, use UF with cardinality to find minimal models for uninterpreted
+   * sorts.
+   */
   UF_SS_FULL,
-  /** use uf strong solver to shrink model sizes, but do no enforce minimality */
+  /**
+   * Use UF with cardinality to shrink model sizes, but do no enforce
+   * minimality.
+   */
   UF_SS_NO_MINIMAL,
-  /** do not use uf strong solver */
+  /** do not use UF with cardinality */
   UF_SS_NONE,
 };