diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-06-18 23:42:59 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-18 23:42:59 -0700 |
| commit | f7036fc10ccdebfc1ca7fffe692cd26dd5eb50fe (patch) | |
| tree | 660b6877dd4aec0f2d60fe3a1558ded8e0db498b /test/regress/regress0/bv/bv-int-collapse1.smt2 | |
| parent | e8884b9b8ba86ce71807887cab87a5188cce4003 (diff) | |
Bv to int elimination bugfix (#4435)
fix 1:
------
The wrong flag was checked in the traversal, causing an assertion error [here](https://github.com/CVC4/CVC4/blob/8236d7f9bff3aef4f7b37a15d509b8a11551401f/src/preprocessing/passes/bv_to_int.cpp#L247)
This is fixed in this PR. A test was added as well.
fix 2:
------
It is desirable that bv-to-bool runs before bv-to-int, but this was not the case, and is fixed in this PR.
Do not merge until after competition release (label added).
Diffstat (limited to 'test/regress/regress0/bv/bv-int-collapse1.smt2')
0 files changed, 0 insertions, 0 deletions