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_options4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 85355c037..cb4f292c1 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -301,6 +301,10 @@ option cbqiMidpoint --cbqi-midpoint bool :default false
choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation
option cbqiNopt --cbqi-nopt bool :default true
non-optimal bounds for counterexample-based quantifier instantiation
+option cbqiLitDepend --cbqi-lit-dep bool :default false
+ dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation
+option cbqiInnermost --cbqi-innermost bool :default false
+ only process innermost quantified formulas in counterexample-based quantifier instantiation
### local theory extensions options
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback