diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-03-18 16:07:03 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-18 16:07:03 -0700 |
| commit | 7e3457b0e16cacef456287ae761c5293be1209d5 (patch) | |
| tree | 0be91c1ed36950cbb17e2ad3484e89636b518c45 /test/unit | |
| parent | 192aa1b5d98ca1a0a2c5e5c8ec603ebb9d14d261 (diff) | |
BitVector: Allow base 10 in constructor. (#2870)
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/api/solver_black.h | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index e3f9e0852..c42854fce 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -267,16 +267,23 @@ void SolverBlack::testMkBitVector() { uint32_t size0 = 0, size1 = 8, size2 = 32, val1 = 2; uint64_t val2 = 2; + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size1, val1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size2, val2)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 2)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 10)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1234", 10)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 16)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("a09f", 16)); TS_ASSERT_THROWS(d_solver->mkBitVector(size0, val1), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkBitVector(size0, val2), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkBitVector("", 2), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkBitVector("10", 3), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkBitVector("20", 2), CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size1, val1)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size2, val2)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 2)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 16)); TS_ASSERT_THROWS(d_solver->mkBitVector(8, "101010101", 2), CVC4ApiException&); + TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2), + d_solver->mkBitVector("10", 10)); + TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2), + d_solver->mkBitVector("a", 16)); TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "01010101", 2).toString(), "0bin01010101"); TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "F", 16).toString(), |