projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0ddae47) | patch
bv2int: rewritings and unsat cores (#5263)
authoryoni206 <yoni206@users.noreply.github.com>
Wed, 14 Oct 2020 06:28:36 +0000 (23:28 -0700)
committerGitHub <noreply@github.com>
Wed, 14 Oct 2020 06:28:36 +0000 (23:28 -0700)
commit1cecdb3b4d8be47d446be5d33cc4d3063061d2b3
tree11416528c4ba2132b756d4a7b39ce99387a37a79tree
parent0ddae476216452696dbb809173afc2fb440a7c57commit | diff
bv2int: rewritings and unsat cores (#5263)

This commit fixes several issues with bv-to-int preprocessing pass, mostly raised by @ajreynol:

1. make sure to rewrite the processed node before and after processing it
2. use the new `mkAnd` function
3. remove `--no-check-unsat-cores` from tests whenever possible
4. add new tests from #5230 . These tests now pass, and so this PR closes #5230 if merged. This also makes #5253 redundant.
5. remove an unused test
src/preprocessing/passes/bv_to_int.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/bv_to_int1.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_5230_binary.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv_to_int_zext.smt2 diff | blob | history
test/regress/regress2/bv_to_int_ashr.smt2 diff | blob | history
test/regress/regress2/bv_to_int_mask_array_3.smt2 diff | blob | history
test/regress/regress2/bv_to_int_shifts.smt2 diff | blob | history
test/regress/regress3/bv_to_int_signed_sub_or.smt2 [deleted file] blob | history