diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-01-21 20:41:39 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-01-21 20:41:39 -0800 |
| commit | 6c9a210e2ca3e6dc56217f186cb632beb82ae0fa (patch) | |
| tree | e0f7f4bf3d86cb7f6f7ddaa6f336315c026b9acd /src/options/quantifiers_options | |
| parent | be9484dc7f7db5e4301142ccfe493871d9f7eac8 (diff) | |
Refactor and fix solveBvLit for CBQI BV. (#1526)
This refactors and simplifies solveBvLit() and fixes the following:
- generate side conditions for BITVECTOR_NEG, BITVECTOR_NOT, BITVECTOR_PLUS,
BITVECTOR_XOR over inequalities and disequality
- fix CONCAT handling (generate side conditions rather then computing an inverse which was incorrect)
- fix SIGN_EXTEND handling (same as with CONCATs)
Diffstat (limited to 'src/options/quantifiers_options')
| -rw-r--r-- | src/options/quantifiers_options | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 2166f0add..2376409e0 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -345,7 +345,7 @@ option quantEprMatching --quant-epr-match bool :default true use matching heuristics for EPR instantiation # CEGQI for BV -option cbqiBv --cbqi-bv bool :read-write :default true +option cbqiBv cbqi-bv --cbqi-bv bool :read-write :default true 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 |