diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-01-02 20:30:04 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-01-02 20:30:04 -0800 |
| commit | 54fa2b48723ace784f2fa5e710aef6c2a38a7bd2 (patch) | |
| tree | 8a1ed8319083521dda0c0e55ab369dbdd1988a4a /test/unit/theory | |
| parent | 06ca7e3709fefbbec5d20f9c99e4a630a391dc28 (diff) | |
Add side conditions for inequalities over BITVECTOR_UDIV for CBQI BV. (#1464)
We now can handle all cases of (in|dis)equality over BITVECTOR_UREM. This also simplifies some
of the side conditions for equality.
Diffstat (limited to 'test/unit/theory')
| -rw-r--r-- | test/unit/theory/theory_quantifiers_bv_inverter_white.h | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h index dc7164e54..291e2252d 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h @@ -101,7 +101,6 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite || k == BITVECTOR_OR || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR - || k == BITVECTOR_SHL); Node sc = getsc(pol, litk, k, idx, d_sk, d_s, d_t); |