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/option_exception.i | |
| 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/option_exception.i')
0 files changed, 0 insertions, 0 deletions