diff options
Diffstat (limited to 'src/options/quantifiers_options')
| -rw-r--r-- | src/options/quantifiers_options | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 2e765ce6b..d3f8c9f6a 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -334,7 +334,11 @@ option quantEprMatching --quant-epr-match bool :default true # CEGQI for BV option cbqiBv --cbqi-bv bool :read-write :default false - use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors + use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors +option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :default false + interleave model value instantiation with word-level inversion approach +option cbqiBvSlackIneq --cbqi-bv-slack-ineq bool :read-write :default true + use model slack values when solving inequalities with word-level inversion approach ### local theory extensions options |