diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
| commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
| tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /test/unit/theory | |
| parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) | |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'test/unit/theory')
| -rw-r--r-- | test/unit/theory/theory_engine_white.h | 2 | ||||
| -rw-r--r-- | test/unit/theory/theory_quantifiers_bv_inverter_white.h | 18 |
2 files changed, 10 insertions, 10 deletions
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index d357b200e..88f8ed6dd 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -25,7 +25,7 @@ #include <memory> #include <string> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "context/context.h" #include "expr/kind.h" #include "expr/node.h" diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h index 5be92b19e..03fcaab69 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h @@ -47,9 +47,9 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite Node x, Node (*getsc)(bool, Kind, Node, Node)) { - Assert(k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == EQUAL - || k == BITVECTOR_UGT || k == BITVECTOR_SGT); - Assert(k != EQUAL || pol == false); + TS_ASSERT(k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == EQUAL + || k == BITVECTOR_UGT || k == BITVECTOR_SGT); + TS_ASSERT(k != EQUAL || pol == false); Node sc = getsc(pol, k, d_sk, d_t); Kind ksc = sc.getKind(); @@ -78,7 +78,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite } else { - Assert(k == EQUAL); + TS_ASSERT(k == EQUAL); k = DISTINCT; } } @@ -95,10 +95,10 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite unsigned idx, Node (*getsc)(bool, Kind, Kind, unsigned, Node, Node, Node)) { - Assert(k == BITVECTOR_MULT || k == BITVECTOR_UREM_TOTAL - || k == BITVECTOR_UDIV_TOTAL || k == BITVECTOR_AND - || k == BITVECTOR_OR || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR - || k == BITVECTOR_SHL); + TS_ASSERT(k == BITVECTOR_MULT || k == BITVECTOR_UREM_TOTAL + || k == BITVECTOR_UDIV_TOTAL || k == BITVECTOR_AND + || 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); TS_ASSERT(!sc.isNull()); @@ -148,7 +148,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite } else { - Assert(idx == 2); + TS_ASSERT(idx == 2); s1 = d_nm->mkVar("s1", d_nm->mkBitVectorType(4)); s2 = d_nm->mkVar("s2", d_nm->mkBitVectorType(4)); x = d_nm->mkBoundVar(s2.getType()); |