diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-10-11 22:20:17 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-11 22:20:17 -0700 |
| commit | 5dd102d4cb7fc8413d6e8f68b0c32c9ef06b1b17 (patch) | |
| tree | a2b969959d3682250b1949fa42ef0193aa80c237 /src/theory | |
| parent | 6e775c15fa0754e9e376a57ae424275091558063 (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.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 9b84c8ecf..0795c3068 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -384,9 +384,10 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk, * with w = getSize(t) = getSize(s) and z = 0 with getSize(z) = w */ unsigned w = bv::utils::getSize(s); Node z = bv::utils::mkZero(w); - Node z_o_t = nm->mkNode(BITVECTOR_CONCAT, z, t); - Node zot_shl_s = nm->mkNode(BITVECTOR_SHL, z_o_t, s); - Node ext = bv::utils::mkExtract(zot_shl_s, 2*w-1, w); + Node z_o_t = nm->mkNode(BITVECTOR_CONCAT, z, t); + Node z_o_s = nm->mkNode(BITVECTOR_CONCAT, z, s); + Node zot_shl_zos = nm->mkNode(BITVECTOR_SHL, z_o_t, z_o_s); + Node ext = bv::utils::mkExtract(zot_shl_zos, 2*w-1, w); scl = nm->mkNode(OR, nm->mkNode(EQUAL, s, z), nm->mkNode(EQUAL, ext, z)); |