diff options
Diffstat (limited to 'test/unit/api/term_black.cpp')
-rw-r--r-- | test/unit/api/term_black.cpp | 496 |
1 files changed, 248 insertions, 248 deletions
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index d894f9720..9dd803c93 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -43,7 +43,7 @@ TEST_F(TestApiBlackTerm, eq) TEST_F(TestApiBlackTerm, getId) { Term n; - ASSERT_THROW(n.getId(), CVC4ApiException); + ASSERT_THROW(n.getId(), CVC5ApiException); Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x"); ASSERT_NO_THROW(x.getId()); Term y = x; @@ -62,7 +62,7 @@ TEST_F(TestApiBlackTerm, getKind) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term n; - ASSERT_THROW(n.getKind(), CVC4ApiException); + ASSERT_THROW(n.getKind(), CVC5ApiException); Term x = d_solver.mkVar(uSort, "x"); ASSERT_NO_THROW(x.getKind()); Term y = d_solver.mkVar(uSort, "y"); @@ -104,7 +104,7 @@ TEST_F(TestApiBlackTerm, getSort) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term n; - ASSERT_THROW(n.getSort(), CVC4ApiException); + ASSERT_THROW(n.getSort(), CVC5ApiException); Term x = d_solver.mkVar(bvSort, "x"); ASSERT_NO_THROW(x.getSort()); ASSERT_EQ(x.getSort(), bvSort); @@ -152,7 +152,7 @@ TEST_F(TestApiBlackTerm, getOp) Term b = d_solver.mkConst(bvsort, "b"); ASSERT_FALSE(x.hasOp()); - ASSERT_THROW(x.getOp(), CVC4ApiException); + ASSERT_THROW(x.getOp(), CVC5ApiException); Term ab = d_solver.mkTerm(SELECT, a, b); Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); @@ -169,7 +169,7 @@ TEST_F(TestApiBlackTerm, getOp) Term fx = d_solver.mkTerm(APPLY_UF, f, x); ASSERT_FALSE(f.hasOp()); - ASSERT_THROW(f.getOp(), CVC4ApiException); + ASSERT_THROW(f.getOp(), CVC5ApiException); ASSERT_TRUE(fx.hasOp()); std::vector<Term> children(fx.begin(), fx.end()); // testing rebuild from op and children @@ -228,21 +228,21 @@ TEST_F(TestApiBlackTerm, notTerm) Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); - ASSERT_THROW(Term().notTerm(), CVC4ApiException); + ASSERT_THROW(Term().notTerm(), CVC5ApiException); Term b = d_solver.mkTrue(); ASSERT_NO_THROW(b.notTerm()); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); - ASSERT_THROW(x.notTerm(), CVC4ApiException); + ASSERT_THROW(x.notTerm(), CVC5ApiException); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.notTerm(), CVC4ApiException); + ASSERT_THROW(f.notTerm(), CVC5ApiException); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.notTerm(), CVC4ApiException); + ASSERT_THROW(p.notTerm(), CVC5ApiException); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.notTerm(), CVC4ApiException); + ASSERT_THROW(zero.notTerm(), CVC5ApiException); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.notTerm(), CVC4ApiException); + ASSERT_THROW(f_x.notTerm(), CVC5ApiException); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.notTerm(), CVC4ApiException); + ASSERT_THROW(sum.notTerm(), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.notTerm()); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); @@ -258,59 +258,59 @@ TEST_F(TestApiBlackTerm, andTerm) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); - ASSERT_THROW(Term().andTerm(b), CVC4ApiException); - ASSERT_THROW(b.andTerm(Term()), CVC4ApiException); + ASSERT_THROW(Term().andTerm(b), CVC5ApiException); + ASSERT_THROW(b.andTerm(Term()), CVC5ApiException); ASSERT_NO_THROW(b.andTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); - ASSERT_THROW(x.andTerm(b), CVC4ApiException); - ASSERT_THROW(x.andTerm(x), CVC4ApiException); + ASSERT_THROW(x.andTerm(b), CVC5ApiException); + ASSERT_THROW(x.andTerm(x), CVC5ApiException); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.andTerm(b), CVC4ApiException); - ASSERT_THROW(f.andTerm(x), CVC4ApiException); - ASSERT_THROW(f.andTerm(f), CVC4ApiException); + ASSERT_THROW(f.andTerm(b), CVC5ApiException); + ASSERT_THROW(f.andTerm(x), CVC5ApiException); + ASSERT_THROW(f.andTerm(f), CVC5ApiException); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.andTerm(b), CVC4ApiException); - ASSERT_THROW(p.andTerm(x), CVC4ApiException); - ASSERT_THROW(p.andTerm(f), CVC4ApiException); - ASSERT_THROW(p.andTerm(p), CVC4ApiException); + ASSERT_THROW(p.andTerm(b), CVC5ApiException); + ASSERT_THROW(p.andTerm(x), CVC5ApiException); + ASSERT_THROW(p.andTerm(f), CVC5ApiException); + ASSERT_THROW(p.andTerm(p), CVC5ApiException); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.andTerm(b), CVC4ApiException); - ASSERT_THROW(zero.andTerm(x), CVC4ApiException); - ASSERT_THROW(zero.andTerm(f), CVC4ApiException); - ASSERT_THROW(zero.andTerm(p), CVC4ApiException); - ASSERT_THROW(zero.andTerm(zero), CVC4ApiException); + ASSERT_THROW(zero.andTerm(b), CVC5ApiException); + ASSERT_THROW(zero.andTerm(x), CVC5ApiException); + ASSERT_THROW(zero.andTerm(f), CVC5ApiException); + ASSERT_THROW(zero.andTerm(p), CVC5ApiException); + ASSERT_THROW(zero.andTerm(zero), CVC5ApiException); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.andTerm(b), CVC4ApiException); - ASSERT_THROW(f_x.andTerm(x), CVC4ApiException); - ASSERT_THROW(f_x.andTerm(f), CVC4ApiException); - ASSERT_THROW(f_x.andTerm(p), CVC4ApiException); - ASSERT_THROW(f_x.andTerm(zero), CVC4ApiException); - ASSERT_THROW(f_x.andTerm(f_x), CVC4ApiException); + ASSERT_THROW(f_x.andTerm(b), CVC5ApiException); + ASSERT_THROW(f_x.andTerm(x), CVC5ApiException); + ASSERT_THROW(f_x.andTerm(f), CVC5ApiException); + ASSERT_THROW(f_x.andTerm(p), CVC5ApiException); + ASSERT_THROW(f_x.andTerm(zero), CVC5ApiException); + ASSERT_THROW(f_x.andTerm(f_x), CVC5ApiException); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.andTerm(b), CVC4ApiException); - ASSERT_THROW(sum.andTerm(x), CVC4ApiException); - ASSERT_THROW(sum.andTerm(f), CVC4ApiException); - ASSERT_THROW(sum.andTerm(p), CVC4ApiException); - ASSERT_THROW(sum.andTerm(zero), CVC4ApiException); - ASSERT_THROW(sum.andTerm(f_x), CVC4ApiException); - ASSERT_THROW(sum.andTerm(sum), CVC4ApiException); + ASSERT_THROW(sum.andTerm(b), CVC5ApiException); + ASSERT_THROW(sum.andTerm(x), CVC5ApiException); + ASSERT_THROW(sum.andTerm(f), CVC5ApiException); + ASSERT_THROW(sum.andTerm(p), CVC5ApiException); + ASSERT_THROW(sum.andTerm(zero), CVC5ApiException); + ASSERT_THROW(sum.andTerm(f_x), CVC5ApiException); + ASSERT_THROW(sum.andTerm(sum), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.andTerm(b)); - ASSERT_THROW(p_0.andTerm(x), CVC4ApiException); - ASSERT_THROW(p_0.andTerm(f), CVC4ApiException); - ASSERT_THROW(p_0.andTerm(p), CVC4ApiException); - ASSERT_THROW(p_0.andTerm(zero), CVC4ApiException); - ASSERT_THROW(p_0.andTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_0.andTerm(sum), CVC4ApiException); + ASSERT_THROW(p_0.andTerm(x), CVC5ApiException); + ASSERT_THROW(p_0.andTerm(f), CVC5ApiException); + ASSERT_THROW(p_0.andTerm(p), CVC5ApiException); + ASSERT_THROW(p_0.andTerm(zero), CVC5ApiException); + ASSERT_THROW(p_0.andTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_0.andTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.andTerm(p_0)); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); ASSERT_NO_THROW(p_f_x.andTerm(b)); - ASSERT_THROW(p_f_x.andTerm(x), CVC4ApiException); - ASSERT_THROW(p_f_x.andTerm(f), CVC4ApiException); - ASSERT_THROW(p_f_x.andTerm(p), CVC4ApiException); - ASSERT_THROW(p_f_x.andTerm(zero), CVC4ApiException); - ASSERT_THROW(p_f_x.andTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_f_x.andTerm(sum), CVC4ApiException); + ASSERT_THROW(p_f_x.andTerm(x), CVC5ApiException); + ASSERT_THROW(p_f_x.andTerm(f), CVC5ApiException); + ASSERT_THROW(p_f_x.andTerm(p), CVC5ApiException); + ASSERT_THROW(p_f_x.andTerm(zero), CVC5ApiException); + ASSERT_THROW(p_f_x.andTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_f_x.andTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_f_x.andTerm(p_0)); ASSERT_NO_THROW(p_f_x.andTerm(p_f_x)); } @@ -324,59 +324,59 @@ TEST_F(TestApiBlackTerm, orTerm) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); - ASSERT_THROW(Term().orTerm(b), CVC4ApiException); - ASSERT_THROW(b.orTerm(Term()), CVC4ApiException); + ASSERT_THROW(Term().orTerm(b), CVC5ApiException); + ASSERT_THROW(b.orTerm(Term()), CVC5ApiException); ASSERT_NO_THROW(b.orTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); - ASSERT_THROW(x.orTerm(b), CVC4ApiException); - ASSERT_THROW(x.orTerm(x), CVC4ApiException); + ASSERT_THROW(x.orTerm(b), CVC5ApiException); + ASSERT_THROW(x.orTerm(x), CVC5ApiException); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.orTerm(b), CVC4ApiException); - ASSERT_THROW(f.orTerm(x), CVC4ApiException); - ASSERT_THROW(f.orTerm(f), CVC4ApiException); + ASSERT_THROW(f.orTerm(b), CVC5ApiException); + ASSERT_THROW(f.orTerm(x), CVC5ApiException); + ASSERT_THROW(f.orTerm(f), CVC5ApiException); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.orTerm(b), CVC4ApiException); - ASSERT_THROW(p.orTerm(x), CVC4ApiException); - ASSERT_THROW(p.orTerm(f), CVC4ApiException); - ASSERT_THROW(p.orTerm(p), CVC4ApiException); + ASSERT_THROW(p.orTerm(b), CVC5ApiException); + ASSERT_THROW(p.orTerm(x), CVC5ApiException); + ASSERT_THROW(p.orTerm(f), CVC5ApiException); + ASSERT_THROW(p.orTerm(p), CVC5ApiException); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.orTerm(b), CVC4ApiException); - ASSERT_THROW(zero.orTerm(x), CVC4ApiException); - ASSERT_THROW(zero.orTerm(f), CVC4ApiException); - ASSERT_THROW(zero.orTerm(p), CVC4ApiException); - ASSERT_THROW(zero.orTerm(zero), CVC4ApiException); + ASSERT_THROW(zero.orTerm(b), CVC5ApiException); + ASSERT_THROW(zero.orTerm(x), CVC5ApiException); + ASSERT_THROW(zero.orTerm(f), CVC5ApiException); + ASSERT_THROW(zero.orTerm(p), CVC5ApiException); + ASSERT_THROW(zero.orTerm(zero), CVC5ApiException); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.orTerm(b), CVC4ApiException); - ASSERT_THROW(f_x.orTerm(x), CVC4ApiException); - ASSERT_THROW(f_x.orTerm(f), CVC4ApiException); - ASSERT_THROW(f_x.orTerm(p), CVC4ApiException); - ASSERT_THROW(f_x.orTerm(zero), CVC4ApiException); - ASSERT_THROW(f_x.orTerm(f_x), CVC4ApiException); + ASSERT_THROW(f_x.orTerm(b), CVC5ApiException); + ASSERT_THROW(f_x.orTerm(x), CVC5ApiException); + ASSERT_THROW(f_x.orTerm(f), CVC5ApiException); + ASSERT_THROW(f_x.orTerm(p), CVC5ApiException); + ASSERT_THROW(f_x.orTerm(zero), CVC5ApiException); + ASSERT_THROW(f_x.orTerm(f_x), CVC5ApiException); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.orTerm(b), CVC4ApiException); - ASSERT_THROW(sum.orTerm(x), CVC4ApiException); - ASSERT_THROW(sum.orTerm(f), CVC4ApiException); - ASSERT_THROW(sum.orTerm(p), CVC4ApiException); - ASSERT_THROW(sum.orTerm(zero), CVC4ApiException); - ASSERT_THROW(sum.orTerm(f_x), CVC4ApiException); - ASSERT_THROW(sum.orTerm(sum), CVC4ApiException); + ASSERT_THROW(sum.orTerm(b), CVC5ApiException); + ASSERT_THROW(sum.orTerm(x), CVC5ApiException); + ASSERT_THROW(sum.orTerm(f), CVC5ApiException); + ASSERT_THROW(sum.orTerm(p), CVC5ApiException); + ASSERT_THROW(sum.orTerm(zero), CVC5ApiException); + ASSERT_THROW(sum.orTerm(f_x), CVC5ApiException); + ASSERT_THROW(sum.orTerm(sum), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.orTerm(b)); - ASSERT_THROW(p_0.orTerm(x), CVC4ApiException); - ASSERT_THROW(p_0.orTerm(f), CVC4ApiException); - ASSERT_THROW(p_0.orTerm(p), CVC4ApiException); - ASSERT_THROW(p_0.orTerm(zero), CVC4ApiException); - ASSERT_THROW(p_0.orTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_0.orTerm(sum), CVC4ApiException); + ASSERT_THROW(p_0.orTerm(x), CVC5ApiException); + ASSERT_THROW(p_0.orTerm(f), CVC5ApiException); + ASSERT_THROW(p_0.orTerm(p), CVC5ApiException); + ASSERT_THROW(p_0.orTerm(zero), CVC5ApiException); + ASSERT_THROW(p_0.orTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_0.orTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.orTerm(p_0)); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); ASSERT_NO_THROW(p_f_x.orTerm(b)); - ASSERT_THROW(p_f_x.orTerm(x), CVC4ApiException); - ASSERT_THROW(p_f_x.orTerm(f), CVC4ApiException); - ASSERT_THROW(p_f_x.orTerm(p), CVC4ApiException); - ASSERT_THROW(p_f_x.orTerm(zero), CVC4ApiException); - ASSERT_THROW(p_f_x.orTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_f_x.orTerm(sum), CVC4ApiException); + ASSERT_THROW(p_f_x.orTerm(x), CVC5ApiException); + ASSERT_THROW(p_f_x.orTerm(f), CVC5ApiException); + ASSERT_THROW(p_f_x.orTerm(p), CVC5ApiException); + ASSERT_THROW(p_f_x.orTerm(zero), CVC5ApiException); + ASSERT_THROW(p_f_x.orTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_f_x.orTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_f_x.orTerm(p_0)); ASSERT_NO_THROW(p_f_x.orTerm(p_f_x)); } @@ -390,59 +390,59 @@ TEST_F(TestApiBlackTerm, xorTerm) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); - ASSERT_THROW(Term().xorTerm(b), CVC4ApiException); - ASSERT_THROW(b.xorTerm(Term()), CVC4ApiException); + ASSERT_THROW(Term().xorTerm(b), CVC5ApiException); + ASSERT_THROW(b.xorTerm(Term()), CVC5ApiException); ASSERT_NO_THROW(b.xorTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); - ASSERT_THROW(x.xorTerm(b), CVC4ApiException); - ASSERT_THROW(x.xorTerm(x), CVC4ApiException); + ASSERT_THROW(x.xorTerm(b), CVC5ApiException); + ASSERT_THROW(x.xorTerm(x), CVC5ApiException); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.xorTerm(b), CVC4ApiException); - ASSERT_THROW(f.xorTerm(x), CVC4ApiException); - ASSERT_THROW(f.xorTerm(f), CVC4ApiException); + ASSERT_THROW(f.xorTerm(b), CVC5ApiException); + ASSERT_THROW(f.xorTerm(x), CVC5ApiException); + ASSERT_THROW(f.xorTerm(f), CVC5ApiException); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.xorTerm(b), CVC4ApiException); - ASSERT_THROW(p.xorTerm(x), CVC4ApiException); - ASSERT_THROW(p.xorTerm(f), CVC4ApiException); - ASSERT_THROW(p.xorTerm(p), CVC4ApiException); + ASSERT_THROW(p.xorTerm(b), CVC5ApiException); + ASSERT_THROW(p.xorTerm(x), CVC5ApiException); + ASSERT_THROW(p.xorTerm(f), CVC5ApiException); + ASSERT_THROW(p.xorTerm(p), CVC5ApiException); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.xorTerm(b), CVC4ApiException); - ASSERT_THROW(zero.xorTerm(x), CVC4ApiException); - ASSERT_THROW(zero.xorTerm(f), CVC4ApiException); - ASSERT_THROW(zero.xorTerm(p), CVC4ApiException); - ASSERT_THROW(zero.xorTerm(zero), CVC4ApiException); + ASSERT_THROW(zero.xorTerm(b), CVC5ApiException); + ASSERT_THROW(zero.xorTerm(x), CVC5ApiException); + ASSERT_THROW(zero.xorTerm(f), CVC5ApiException); + ASSERT_THROW(zero.xorTerm(p), CVC5ApiException); + ASSERT_THROW(zero.xorTerm(zero), CVC5ApiException); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.xorTerm(b), CVC4ApiException); - ASSERT_THROW(f_x.xorTerm(x), CVC4ApiException); - ASSERT_THROW(f_x.xorTerm(f), CVC4ApiException); - ASSERT_THROW(f_x.xorTerm(p), CVC4ApiException); - ASSERT_THROW(f_x.xorTerm(zero), CVC4ApiException); - ASSERT_THROW(f_x.xorTerm(f_x), CVC4ApiException); + ASSERT_THROW(f_x.xorTerm(b), CVC5ApiException); + ASSERT_THROW(f_x.xorTerm(x), CVC5ApiException); + ASSERT_THROW(f_x.xorTerm(f), CVC5ApiException); + ASSERT_THROW(f_x.xorTerm(p), CVC5ApiException); + ASSERT_THROW(f_x.xorTerm(zero), CVC5ApiException); + ASSERT_THROW(f_x.xorTerm(f_x), CVC5ApiException); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.xorTerm(b), CVC4ApiException); - ASSERT_THROW(sum.xorTerm(x), CVC4ApiException); - ASSERT_THROW(sum.xorTerm(f), CVC4ApiException); - ASSERT_THROW(sum.xorTerm(p), CVC4ApiException); - ASSERT_THROW(sum.xorTerm(zero), CVC4ApiException); - ASSERT_THROW(sum.xorTerm(f_x), CVC4ApiException); - ASSERT_THROW(sum.xorTerm(sum), CVC4ApiException); + ASSERT_THROW(sum.xorTerm(b), CVC5ApiException); + ASSERT_THROW(sum.xorTerm(x), CVC5ApiException); + ASSERT_THROW(sum.xorTerm(f), CVC5ApiException); + ASSERT_THROW(sum.xorTerm(p), CVC5ApiException); + ASSERT_THROW(sum.xorTerm(zero), CVC5ApiException); + ASSERT_THROW(sum.xorTerm(f_x), CVC5ApiException); + ASSERT_THROW(sum.xorTerm(sum), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.xorTerm(b)); - ASSERT_THROW(p_0.xorTerm(x), CVC4ApiException); - ASSERT_THROW(p_0.xorTerm(f), CVC4ApiException); - ASSERT_THROW(p_0.xorTerm(p), CVC4ApiException); - ASSERT_THROW(p_0.xorTerm(zero), CVC4ApiException); - ASSERT_THROW(p_0.xorTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_0.xorTerm(sum), CVC4ApiException); + ASSERT_THROW(p_0.xorTerm(x), CVC5ApiException); + ASSERT_THROW(p_0.xorTerm(f), CVC5ApiException); + ASSERT_THROW(p_0.xorTerm(p), CVC5ApiException); + ASSERT_THROW(p_0.xorTerm(zero), CVC5ApiException); + ASSERT_THROW(p_0.xorTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_0.xorTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.xorTerm(p_0)); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); ASSERT_NO_THROW(p_f_x.xorTerm(b)); - ASSERT_THROW(p_f_x.xorTerm(x), CVC4ApiException); - ASSERT_THROW(p_f_x.xorTerm(f), CVC4ApiException); - ASSERT_THROW(p_f_x.xorTerm(p), CVC4ApiException); - ASSERT_THROW(p_f_x.xorTerm(zero), CVC4ApiException); - ASSERT_THROW(p_f_x.xorTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_f_x.xorTerm(sum), CVC4ApiException); + ASSERT_THROW(p_f_x.xorTerm(x), CVC5ApiException); + ASSERT_THROW(p_f_x.xorTerm(f), CVC5ApiException); + ASSERT_THROW(p_f_x.xorTerm(p), CVC5ApiException); + ASSERT_THROW(p_f_x.xorTerm(zero), CVC5ApiException); + ASSERT_THROW(p_f_x.xorTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_f_x.xorTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_f_x.xorTerm(p_0)); ASSERT_NO_THROW(p_f_x.xorTerm(p_f_x)); } @@ -456,59 +456,59 @@ TEST_F(TestApiBlackTerm, eqTerm) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); - ASSERT_THROW(Term().eqTerm(b), CVC4ApiException); - ASSERT_THROW(b.eqTerm(Term()), CVC4ApiException); + ASSERT_THROW(Term().eqTerm(b), CVC5ApiException); + ASSERT_THROW(b.eqTerm(Term()), CVC5ApiException); ASSERT_NO_THROW(b.eqTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); - ASSERT_THROW(x.eqTerm(b), CVC4ApiException); + ASSERT_THROW(x.eqTerm(b), CVC5ApiException); ASSERT_NO_THROW(x.eqTerm(x)); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.eqTerm(b), CVC4ApiException); - ASSERT_THROW(f.eqTerm(x), CVC4ApiException); + ASSERT_THROW(f.eqTerm(b), CVC5ApiException); + ASSERT_THROW(f.eqTerm(x), CVC5ApiException); ASSERT_NO_THROW(f.eqTerm(f)); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.eqTerm(b), CVC4ApiException); - ASSERT_THROW(p.eqTerm(x), CVC4ApiException); - ASSERT_THROW(p.eqTerm(f), CVC4ApiException); + ASSERT_THROW(p.eqTerm(b), CVC5ApiException); + ASSERT_THROW(p.eqTerm(x), CVC5ApiException); + ASSERT_THROW(p.eqTerm(f), CVC5ApiException); ASSERT_NO_THROW(p.eqTerm(p)); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.eqTerm(b), CVC4ApiException); - ASSERT_THROW(zero.eqTerm(x), CVC4ApiException); - ASSERT_THROW(zero.eqTerm(f), CVC4ApiException); - ASSERT_THROW(zero.eqTerm(p), CVC4ApiException); + ASSERT_THROW(zero.eqTerm(b), CVC5ApiException); + ASSERT_THROW(zero.eqTerm(x), CVC5ApiException); + ASSERT_THROW(zero.eqTerm(f), CVC5ApiException); + ASSERT_THROW(zero.eqTerm(p), CVC5ApiException); ASSERT_NO_THROW(zero.eqTerm(zero)); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.eqTerm(b), CVC4ApiException); - ASSERT_THROW(f_x.eqTerm(x), CVC4ApiException); - ASSERT_THROW(f_x.eqTerm(f), CVC4ApiException); - ASSERT_THROW(f_x.eqTerm(p), CVC4ApiException); + ASSERT_THROW(f_x.eqTerm(b), CVC5ApiException); + ASSERT_THROW(f_x.eqTerm(x), CVC5ApiException); + ASSERT_THROW(f_x.eqTerm(f), CVC5ApiException); + ASSERT_THROW(f_x.eqTerm(p), CVC5ApiException); ASSERT_NO_THROW(f_x.eqTerm(zero)); ASSERT_NO_THROW(f_x.eqTerm(f_x)); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.eqTerm(b), CVC4ApiException); - ASSERT_THROW(sum.eqTerm(x), CVC4ApiException); - ASSERT_THROW(sum.eqTerm(f), CVC4ApiException); - ASSERT_THROW(sum.eqTerm(p), CVC4ApiException); + ASSERT_THROW(sum.eqTerm(b), CVC5ApiException); + ASSERT_THROW(sum.eqTerm(x), CVC5ApiException); + ASSERT_THROW(sum.eqTerm(f), CVC5ApiException); + ASSERT_THROW(sum.eqTerm(p), CVC5ApiException); ASSERT_NO_THROW(sum.eqTerm(zero)); ASSERT_NO_THROW(sum.eqTerm(f_x)); ASSERT_NO_THROW(sum.eqTerm(sum)); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.eqTerm(b)); - ASSERT_THROW(p_0.eqTerm(x), CVC4ApiException); - ASSERT_THROW(p_0.eqTerm(f), CVC4ApiException); - ASSERT_THROW(p_0.eqTerm(p), CVC4ApiException); - ASSERT_THROW(p_0.eqTerm(zero), CVC4ApiException); - ASSERT_THROW(p_0.eqTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_0.eqTerm(sum), CVC4ApiException); + ASSERT_THROW(p_0.eqTerm(x), CVC5ApiException); + ASSERT_THROW(p_0.eqTerm(f), CVC5ApiException); + ASSERT_THROW(p_0.eqTerm(p), CVC5ApiException); + ASSERT_THROW(p_0.eqTerm(zero), CVC5ApiException); + ASSERT_THROW(p_0.eqTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_0.eqTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.eqTerm(p_0)); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); ASSERT_NO_THROW(p_f_x.eqTerm(b)); - ASSERT_THROW(p_f_x.eqTerm(x), CVC4ApiException); - ASSERT_THROW(p_f_x.eqTerm(f), CVC4ApiException); - ASSERT_THROW(p_f_x.eqTerm(p), CVC4ApiException); - ASSERT_THROW(p_f_x.eqTerm(zero), CVC4ApiException); - ASSERT_THROW(p_f_x.eqTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_f_x.eqTerm(sum), CVC4ApiException); + ASSERT_THROW(p_f_x.eqTerm(x), CVC5ApiException); + ASSERT_THROW(p_f_x.eqTerm(f), CVC5ApiException); + ASSERT_THROW(p_f_x.eqTerm(p), CVC5ApiException); + ASSERT_THROW(p_f_x.eqTerm(zero), CVC5ApiException); + ASSERT_THROW(p_f_x.eqTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_f_x.eqTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_f_x.eqTerm(p_0)); ASSERT_NO_THROW(p_f_x.eqTerm(p_f_x)); } @@ -522,59 +522,59 @@ TEST_F(TestApiBlackTerm, impTerm) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); - ASSERT_THROW(Term().impTerm(b), CVC4ApiException); - ASSERT_THROW(b.impTerm(Term()), CVC4ApiException); + ASSERT_THROW(Term().impTerm(b), CVC5ApiException); + ASSERT_THROW(b.impTerm(Term()), CVC5ApiException); ASSERT_NO_THROW(b.impTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); - ASSERT_THROW(x.impTerm(b), CVC4ApiException); - ASSERT_THROW(x.impTerm(x), CVC4ApiException); + ASSERT_THROW(x.impTerm(b), CVC5ApiException); + ASSERT_THROW(x.impTerm(x), CVC5ApiException); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.impTerm(b), CVC4ApiException); - ASSERT_THROW(f.impTerm(x), CVC4ApiException); - ASSERT_THROW(f.impTerm(f), CVC4ApiException); + ASSERT_THROW(f.impTerm(b), CVC5ApiException); + ASSERT_THROW(f.impTerm(x), CVC5ApiException); + ASSERT_THROW(f.impTerm(f), CVC5ApiException); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.impTerm(b), CVC4ApiException); - ASSERT_THROW(p.impTerm(x), CVC4ApiException); - ASSERT_THROW(p.impTerm(f), CVC4ApiException); - ASSERT_THROW(p.impTerm(p), CVC4ApiException); + ASSERT_THROW(p.impTerm(b), CVC5ApiException); + ASSERT_THROW(p.impTerm(x), CVC5ApiException); + ASSERT_THROW(p.impTerm(f), CVC5ApiException); + ASSERT_THROW(p.impTerm(p), CVC5ApiException); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.impTerm(b), CVC4ApiException); - ASSERT_THROW(zero.impTerm(x), CVC4ApiException); - ASSERT_THROW(zero.impTerm(f), CVC4ApiException); - ASSERT_THROW(zero.impTerm(p), CVC4ApiException); - ASSERT_THROW(zero.impTerm(zero), CVC4ApiException); + ASSERT_THROW(zero.impTerm(b), CVC5ApiException); + ASSERT_THROW(zero.impTerm(x), CVC5ApiException); + ASSERT_THROW(zero.impTerm(f), CVC5ApiException); + ASSERT_THROW(zero.impTerm(p), CVC5ApiException); + ASSERT_THROW(zero.impTerm(zero), CVC5ApiException); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.impTerm(b), CVC4ApiException); - ASSERT_THROW(f_x.impTerm(x), CVC4ApiException); - ASSERT_THROW(f_x.impTerm(f), CVC4ApiException); - ASSERT_THROW(f_x.impTerm(p), CVC4ApiException); - ASSERT_THROW(f_x.impTerm(zero), CVC4ApiException); - ASSERT_THROW(f_x.impTerm(f_x), CVC4ApiException); + ASSERT_THROW(f_x.impTerm(b), CVC5ApiException); + ASSERT_THROW(f_x.impTerm(x), CVC5ApiException); + ASSERT_THROW(f_x.impTerm(f), CVC5ApiException); + ASSERT_THROW(f_x.impTerm(p), CVC5ApiException); + ASSERT_THROW(f_x.impTerm(zero), CVC5ApiException); + ASSERT_THROW(f_x.impTerm(f_x), CVC5ApiException); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.impTerm(b), CVC4ApiException); - ASSERT_THROW(sum.impTerm(x), CVC4ApiException); - ASSERT_THROW(sum.impTerm(f), CVC4ApiException); - ASSERT_THROW(sum.impTerm(p), CVC4ApiException); - ASSERT_THROW(sum.impTerm(zero), CVC4ApiException); - ASSERT_THROW(sum.impTerm(f_x), CVC4ApiException); - ASSERT_THROW(sum.impTerm(sum), CVC4ApiException); + ASSERT_THROW(sum.impTerm(b), CVC5ApiException); + ASSERT_THROW(sum.impTerm(x), CVC5ApiException); + ASSERT_THROW(sum.impTerm(f), CVC5ApiException); + ASSERT_THROW(sum.impTerm(p), CVC5ApiException); + ASSERT_THROW(sum.impTerm(zero), CVC5ApiException); + ASSERT_THROW(sum.impTerm(f_x), CVC5ApiException); + ASSERT_THROW(sum.impTerm(sum), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.impTerm(b)); - ASSERT_THROW(p_0.impTerm(x), CVC4ApiException); - ASSERT_THROW(p_0.impTerm(f), CVC4ApiException); - ASSERT_THROW(p_0.impTerm(p), CVC4ApiException); - ASSERT_THROW(p_0.impTerm(zero), CVC4ApiException); - ASSERT_THROW(p_0.impTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_0.impTerm(sum), CVC4ApiException); + ASSERT_THROW(p_0.impTerm(x), CVC5ApiException); + ASSERT_THROW(p_0.impTerm(f), CVC5ApiException); + ASSERT_THROW(p_0.impTerm(p), CVC5ApiException); + ASSERT_THROW(p_0.impTerm(zero), CVC5ApiException); + ASSERT_THROW(p_0.impTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_0.impTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.impTerm(p_0)); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); ASSERT_NO_THROW(p_f_x.impTerm(b)); - ASSERT_THROW(p_f_x.impTerm(x), CVC4ApiException); - ASSERT_THROW(p_f_x.impTerm(f), CVC4ApiException); - ASSERT_THROW(p_f_x.impTerm(p), CVC4ApiException); - ASSERT_THROW(p_f_x.impTerm(zero), CVC4ApiException); - ASSERT_THROW(p_f_x.impTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_f_x.impTerm(sum), CVC4ApiException); + ASSERT_THROW(p_f_x.impTerm(x), CVC5ApiException); + ASSERT_THROW(p_f_x.impTerm(f), CVC5ApiException); + ASSERT_THROW(p_f_x.impTerm(p), CVC5ApiException); + ASSERT_THROW(p_f_x.impTerm(zero), CVC5ApiException); + ASSERT_THROW(p_f_x.impTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_f_x.impTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_f_x.impTerm(p_0)); ASSERT_NO_THROW(p_f_x.impTerm(p_f_x)); } @@ -588,39 +588,39 @@ TEST_F(TestApiBlackTerm, iteTerm) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); - ASSERT_THROW(Term().iteTerm(b, b), CVC4ApiException); - ASSERT_THROW(b.iteTerm(Term(), b), CVC4ApiException); - ASSERT_THROW(b.iteTerm(b, Term()), CVC4ApiException); + ASSERT_THROW(Term().iteTerm(b, b), CVC5ApiException); + ASSERT_THROW(b.iteTerm(Term(), b), CVC5ApiException); + ASSERT_THROW(b.iteTerm(b, Term()), CVC5ApiException); ASSERT_NO_THROW(b.iteTerm(b, b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); ASSERT_NO_THROW(b.iteTerm(x, x)); ASSERT_NO_THROW(b.iteTerm(b, b)); - ASSERT_THROW(b.iteTerm(x, b), CVC4ApiException); - ASSERT_THROW(x.iteTerm(x, x), CVC4ApiException); - ASSERT_THROW(x.iteTerm(x, b), CVC4ApiException); + ASSERT_THROW(b.iteTerm(x, b), CVC5ApiException); + ASSERT_THROW(x.iteTerm(x, x), CVC5ApiException); + ASSERT_THROW(x.iteTerm(x, b), CVC5ApiException); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.iteTerm(b, b), CVC4ApiException); - ASSERT_THROW(x.iteTerm(b, x), CVC4ApiException); + ASSERT_THROW(f.iteTerm(b, b), CVC5ApiException); + ASSERT_THROW(x.iteTerm(b, x), CVC5ApiException); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.iteTerm(b, b), CVC4ApiException); - ASSERT_THROW(p.iteTerm(x, b), CVC4ApiException); + ASSERT_THROW(p.iteTerm(b, b), CVC5ApiException); + ASSERT_THROW(p.iteTerm(x, b), CVC5ApiException); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.iteTerm(x, x), CVC4ApiException); - ASSERT_THROW(zero.iteTerm(x, b), CVC4ApiException); + ASSERT_THROW(zero.iteTerm(x, x), CVC5ApiException); + ASSERT_THROW(zero.iteTerm(x, b), CVC5ApiException); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.iteTerm(b, b), CVC4ApiException); - ASSERT_THROW(f_x.iteTerm(b, x), CVC4ApiException); + ASSERT_THROW(f_x.iteTerm(b, b), CVC5ApiException); + ASSERT_THROW(f_x.iteTerm(b, x), CVC5ApiException); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.iteTerm(x, x), CVC4ApiException); - ASSERT_THROW(sum.iteTerm(b, x), CVC4ApiException); + ASSERT_THROW(sum.iteTerm(x, x), CVC5ApiException); + ASSERT_THROW(sum.iteTerm(b, x), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.iteTerm(b, b)); ASSERT_NO_THROW(p_0.iteTerm(x, x)); - ASSERT_THROW(p_0.iteTerm(x, b), CVC4ApiException); + ASSERT_THROW(p_0.iteTerm(x, b), CVC5ApiException); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); ASSERT_NO_THROW(p_f_x.iteTerm(b, b)); ASSERT_NO_THROW(p_f_x.iteTerm(x, x)); - ASSERT_THROW(p_f_x.iteTerm(x, b), CVC4ApiException); + ASSERT_THROW(p_f_x.iteTerm(x, b), CVC5ApiException); } TEST_F(TestApiBlackTerm, termAssignment) @@ -650,7 +650,7 @@ TEST_F(TestApiBlackTerm, termChildren) ASSERT_EQ(t1[0], two); ASSERT_EQ(t1.getNumChildren(), 2); Term tnull; - ASSERT_THROW(tnull.getNumChildren(), CVC4ApiException); + ASSERT_THROW(tnull.getNumChildren(), CVC5ApiException); // apply term f(2) Sort intSort = d_solver.getIntegerSort(); @@ -661,7 +661,7 @@ TEST_F(TestApiBlackTerm, termChildren) ASSERT_EQ(t2.getNumChildren(), 2); ASSERT_EQ(t2[0], f); ASSERT_EQ(t2[1], two); - ASSERT_THROW(tnull[0], CVC4ApiException); + ASSERT_THROW(tnull[0], CVC5ApiException); } TEST_F(TestApiBlackTerm, getInteger) @@ -679,15 +679,15 @@ TEST_F(TestApiBlackTerm, getInteger) Term int11 = d_solver.mkInteger("18446744073709551616"); Term int12 = d_solver.mkInteger("-0"); - ASSERT_THROW(d_solver.mkInteger(""), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("-"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("-1-"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("0.0"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("-0.1"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("012"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("0000"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("-01"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("-00"), CVC4ApiException); + ASSERT_THROW(d_solver.mkInteger(""), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("-"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("-1-"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("0.0"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("-0.1"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("012"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("0000"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("-01"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("-00"), CVC5ApiException); ASSERT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64() && !int1.isUInt64() && int1.isInteger()); @@ -760,7 +760,7 @@ TEST_F(TestApiBlackTerm, substitute) ASSERT_EQ(xpx.substitute(x, one), onepone); ASSERT_EQ(onepone.substitute(one, x), xpx); // incorrect due to type - ASSERT_THROW(xpx.substitute(one, ttrue), CVC4ApiException); + ASSERT_THROW(xpx.substitute(one, ttrue), CVC5ApiException); // simultaneous substitution Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y"); @@ -776,28 +776,28 @@ TEST_F(TestApiBlackTerm, substitute) // incorrect substitution due to arity rs.pop_back(); - ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException); + ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException); // incorrect substitution due to types rs.push_back(ttrue); - ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException); + ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException); // null cannot substitute Term tnull; - ASSERT_THROW(tnull.substitute(one, x), CVC4ApiException); - ASSERT_THROW(xpx.substitute(tnull, x), CVC4ApiException); - ASSERT_THROW(xpx.substitute(x, tnull), CVC4ApiException); + ASSERT_THROW(tnull.substitute(one, x), CVC5ApiException); + ASSERT_THROW(xpx.substitute(tnull, x), CVC5ApiException); + ASSERT_THROW(xpx.substitute(x, tnull), CVC5ApiException); rs.pop_back(); rs.push_back(tnull); - ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException); + ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException); es.clear(); rs.clear(); es.push_back(x); rs.push_back(y); - ASSERT_THROW(tnull.substitute(es, rs), CVC4ApiException); + ASSERT_THROW(tnull.substitute(es, rs), CVC5ApiException); es.push_back(tnull); rs.push_back(one); - ASSERT_THROW(xpx.substitute(es, rs), CVC4ApiException); + ASSERT_THROW(xpx.substitute(es, rs), CVC5ApiException); } TEST_F(TestApiBlackTerm, constArray) @@ -810,7 +810,7 @@ TEST_F(TestApiBlackTerm, constArray) ASSERT_EQ(constarr.getKind(), CONST_ARRAY); ASSERT_EQ(constarr.getConstArrayBase(), one); - ASSERT_THROW(a.getConstArrayBase(), CVC4ApiException); + ASSERT_THROW(a.getConstArrayBase(), CVC5ApiException); arrsort = d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort()); @@ -837,7 +837,7 @@ TEST_F(TestApiBlackTerm, constSequenceElements) // A seq.unit app is not a constant sequence (regardless of whether it is // applied to a constant). Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1)); - ASSERT_THROW(su.getConstSequenceElements(), CVC4ApiException); + ASSERT_THROW(su.getConstSequenceElements(), CVC5ApiException); } TEST_F(TestApiBlackTerm, termScopedToString) |