summaryrefslogtreecommitdiff
path: root/src/options/quantifiers_options
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/quantifiers_options')
-rw-r--r--src/options/quantifiers_options2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 856de103e..cf8fca2fa 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -165,6 +165,8 @@ option fmfBound fmf-bound --fmf-bound bool :default false :read-write
finite model finding on bounded quantification
option fmfBoundLazy --fmf-bound-lazy bool :default false :read-write
enforce bounds for bounded quantification lazily via use of proxy variables
+option fmfBoundMinMode --fmf-bound-min-mode=MODE CVC4::theory::quantifiers::FmfBoundMinMode :default CVC4::theory::quantifiers::FMF_BOUND_MIN_INT_RANGE :include "options/quantifiers_modes.h" :handler stringToFmfBoundMinMode
+ mode for which types of bounds to minimize via first decision heuristics
### conflict-based instantiation options
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback