diff options
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index d7b66d52d..cdefcf8e9 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -257,6 +257,10 @@ option cbqiSymLia --cbqi-sym-lia bool :default false use symbolic integer division in substitutions for counterexample-based quantifier instantiation option cbqiRoundUpLowerLia --cbqi-round-up-lia bool :default false round up integer lower bounds in substitutions for counterexample-based quantifier instantiation +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 ### local theory extensions options |