diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-01-05 14:24:49 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-01-05 14:24:49 -0800 |
| commit | f836073852cf8b2d4904620a6eb153599314dc46 (patch) | |
| tree | 2068003bfd5f0f3c6b91039821c89488164f9886 /test/unit/theory | |
| parent | 57b81ebe6eda45fa2a6d02c0fd071caf0fcd091a (diff) | |
Add UGT/SGT side conditions for AND/OR + other fixes. (#1481)
Diffstat (limited to 'test/unit/theory')
| -rw-r--r-- | test/unit/theory/theory_quantifiers_bv_inverter_white.h | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h index 291e2252d..ba8dd1668 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h @@ -104,15 +104,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite || k == BITVECTOR_SHL); Node sc = getsc(pol, litk, k, idx, d_sk, d_s, d_t); - // TODO amend / remove the following six lines as soon as inequality - // handling is implemented in getScBv* - TS_ASSERT (litk != EQUAL || sc != Node::null()); - if (sc.isNull()) - { - TS_ASSERT (litk == BITVECTOR_ULT || litk == BITVECTOR_SLT - || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); - return; - } + TS_ASSERT(!sc.isNull()); Kind ksc = sc.getKind(); TS_ASSERT((k == BITVECTOR_UDIV_TOTAL && idx == 1 && pol == false) || (k == BITVECTOR_ASHR && idx == 0 && pol == false) |