diff options
Diffstat (limited to 'src/options/quantifiers_options')
| -rw-r--r-- | src/options/quantifiers_options | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 05c2512cd..0262012f6 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -337,10 +337,8 @@ option cbqiBv --cbqi-bv bool :read-write :default false 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 -option cbqiBvInvInDisEq --cbqi-bv-inv-in-dis-eq bool :read-write :default false - let bv inverter handle (un)signed less than nodes +option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqMode :read-write :default CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_SLACK :include "options/quantifiers_modes.h" :handler stringToCbqiBvIneqMode + choose mode for handling bit-vector inequalities with counterexample-guided instantiation ### local theory extensions options |