diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-12-29 20:02:38 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-29 20:02:38 -0800 |
| commit | dc2f9914f49076d56cdb18e14971df67fbe567bb (patch) | |
| tree | a82f640d60e27525a3094efaaae110b542ffccc9 /test/unit/theory | |
| parent | 2d147b72e1339f4c281caf7786dfa9b4d79ed21c (diff) | |
Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)
We now can handle all cases of (in|dis)equality over UREM. Previously, we could not handle equality
for index=0 and had to rewrite x % s = t to x - x / s * s. Since we can now handle this case, we do not
apply this rewriting anymore.
Diffstat (limited to 'test/unit/theory')
| -rw-r--r-- | test/unit/theory/theory_quantifiers_bv_inverter_white.h | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h index e1d950050..6f078d2e3 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h @@ -85,8 +85,6 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite || k == BITVECTOR_ASHR || k == BITVECTOR_SHL); - Assert(litk != EQUAL - || k != BITVECTOR_UREM_TOTAL || pol == false || idx == 1); Node sc = getsc(pol, litk, k, idx, d_sk, d_s, d_t); // TODO amend / remove the following six lines as soon as inequality @@ -219,8 +217,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite void testGetScBvUremEqTrue0() { - TS_ASSERT_THROWS(runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 0, getScBvUrem), - AssertionException); + runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 0, getScBvUrem); } void testGetScBvUremEqTrue1() |