1 files changed, 10 insertions, 0 deletions
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 540db38ec..7395a9a30 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -163,6 +163,16 @@ enum MacrosQuantMode {
   MACROS_QUANT_MODE_GROUND_UF,
 };
 
+enum QuantDSplitMode {
+  /** never do quantifiers splitting */
+  QUANT_DSPLIT_MODE_NONE,
+  /** default */
+  QUANT_DSPLIT_MODE_DEFAULT,
+  /** do quantifiers splitting aggressively */
+  QUANT_DSPLIT_MODE_AGG,
+};
+
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */