projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e8884b9) | patch
Bv to int elimination bugfix (#4435)
authoryoni206 <yoni206@users.noreply.github.com>
Fri, 19 Jun 2020 06:42:59 +0000 (23:42 -0700)
committerGitHub <noreply@github.com>
Fri, 19 Jun 2020 06:42:59 +0000 (23:42 -0700)
commitf7036fc10ccdebfc1ca7fffe692cd26dd5eb50fe
tree660b6877dd4aec0f2d60fe3a1558ded8e0db498btree
parente8884b9b8ba86ce71807887cab87a5188cce4003commit | 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).
src/preprocessing/passes/bv_to_int.cpp diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/bv_to_int_elim_err.smt2 [new file with mode: 0644] blob