projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6e775c1) | patch
Enable regressions for CBQI BV and fix inverse for LSHR. (#1234)
authorAina Niemetz <aina.niemetz@gmail.com>
Thu, 12 Oct 2017 05:20:17 +0000 (22:20 -0700)
committerGitHub <noreply@github.com>
Thu, 12 Oct 2017 05:20:17 +0000 (22:20 -0700)
commit5dd102d4cb7fc8413d6e8f68b0c32c9ef06b1b17
treea2b969959d3682250b1949fa42ef0193aa80c237tree
parent6e775c15fa0754e9e376a57ae424275091558063commit | diff
Enable regressions for CBQI BV and fix inverse for LSHR. (#1234)

This fixes and enables previously added regression tests for CBQI BV. It further removes one of the tests that was obsolete (since it goes through even without --cbqi-bv).

This further fixes the inverse computation for BITVECTOR_LSHR, which was broken due to a mismatching bit-width when creating a shift node.
src/theory/quantifiers/bv_inverter.cpp diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 diff | blob | history
test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 diff | blob | history
test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 diff | blob | history
test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 [deleted file] blob | history
test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 diff | blob | history
test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 diff | blob | history