diff options
Diffstat (limited to 'test/unit')
| -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) |