diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-10-08 17:24:49 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-08 17:24:49 -0700 |
commit | 8fa91361af7e891b82f9156e76b7d7e6bb70aa65 (patch) | |
tree | ff96cf082751900c84808bee7d4123c7b729ab01 /test | |
parent | 1b6784fe52f4fb745262842e0406d6dd34053cb2 (diff) |
New C++ API: Term: Add missing checks for null. (#3364)
Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com>
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/api/term_black.h | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index 945944467..c5300dbfe 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -168,6 +168,7 @@ void TermBlack::testNotTerm() Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); + TS_ASSERT_THROWS(Term().notTerm(), CVC4ApiException&); Term b = d_solver.mkTrue(); TS_ASSERT_THROWS_NOTHING(b.notTerm()); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); @@ -205,6 +206,8 @@ void TermBlack::testAndTerm() Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); + TS_ASSERT_THROWS(Term().andTerm(b), CVC4ApiException&); + TS_ASSERT_THROWS(b.andTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.andTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.andTerm(b), CVC4ApiException&); @@ -269,6 +272,8 @@ void TermBlack::testOrTerm() Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); + TS_ASSERT_THROWS(Term().orTerm(b), CVC4ApiException&); + TS_ASSERT_THROWS(b.orTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.orTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.orTerm(b), CVC4ApiException&); @@ -333,6 +338,8 @@ void TermBlack::testXorTerm() Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); + TS_ASSERT_THROWS(Term().xorTerm(b), CVC4ApiException&); + TS_ASSERT_THROWS(b.xorTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.xorTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.xorTerm(b), CVC4ApiException&); @@ -397,6 +404,8 @@ void TermBlack::testEqTerm() Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); + TS_ASSERT_THROWS(Term().eqTerm(b), CVC4ApiException&); + TS_ASSERT_THROWS(b.eqTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.eqTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.eqTerm(b), CVC4ApiException&); @@ -461,6 +470,8 @@ void TermBlack::testImpTerm() Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); + TS_ASSERT_THROWS(Term().impTerm(b), CVC4ApiException&); + TS_ASSERT_THROWS(b.impTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.impTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.impTerm(b), CVC4ApiException&); @@ -525,6 +536,9 @@ void TermBlack::testIteTerm() Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); + TS_ASSERT_THROWS(Term().iteTerm(b, b), CVC4ApiException&); + TS_ASSERT_THROWS(b.iteTerm(Term(), b), CVC4ApiException&); + TS_ASSERT_THROWS(b.iteTerm(b, Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x)); |