diff options
| author | makaimann <makaim@stanford.edu> | 2019-10-18 11:42:15 -0700 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-10-18 11:42:15 -0700 |
| commit | ba175a951064250907494b7b5112f3882889df5e (patch) | |
| tree | 2d60d81e0696a6774014ee83b7ea7bdde4dede84 /test | |
| parent | 5396f014b66cbfd7cc16380c05c1539b1efe583c (diff) | |
Update overflow check to handle negative numbers (#3396)
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/api/solver_black.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 9dd913ea2..41c4a86dd 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -286,12 +286,14 @@ void SolverBlack::testMkBitVector() 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_NOTHING(d_solver->mkBitVector(8, "-127", 10)); 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(d_solver->mkBitVector(8, "101010101", 2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkBitVector(8, "-256", 10), CVC4ApiException&); TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2), d_solver->mkBitVector("10", 10)); TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2), @@ -300,6 +302,8 @@ void SolverBlack::testMkBitVector() "0bin01010101"); TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "F", 16).toString(), "0bin00001111"); + TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "-1", 10), + d_solver->mkBitVector(8, "FF", 16)); } void SolverBlack::testMkVar() |