diff options
Diffstat (limited to 'test/unit/api/grammar_black.cpp')
| -rw-r--r-- | test/unit/api/grammar_black.cpp | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp index ccab121db..7b7556539 100644 --- a/test/unit/api/grammar_black.cpp +++ b/test/unit/api/grammar_black.cpp @@ -39,15 +39,15 @@ TEST_F(TestApiBlackGrammar, addRule) ASSERT_NO_THROW(g.addRule(start, d_solver.mkBoolean(false))); ASSERT_THROW(g.addRule(nullTerm, d_solver.mkBoolean(false)), - CVC4ApiException); - ASSERT_THROW(g.addRule(start, nullTerm), CVC4ApiException); - ASSERT_THROW(g.addRule(nts, d_solver.mkBoolean(false)), CVC4ApiException); - ASSERT_THROW(g.addRule(start, d_solver.mkInteger(0)), CVC4ApiException); - ASSERT_THROW(g.addRule(start, nts), CVC4ApiException); + CVC5ApiException); + ASSERT_THROW(g.addRule(start, nullTerm), CVC5ApiException); + ASSERT_THROW(g.addRule(nts, d_solver.mkBoolean(false)), CVC5ApiException); + ASSERT_THROW(g.addRule(start, d_solver.mkInteger(0)), CVC5ApiException); + ASSERT_THROW(g.addRule(start, nts), CVC5ApiException); d_solver.synthFun("f", {}, boolean, g); - ASSERT_THROW(g.addRule(start, d_solver.mkBoolean(false)), CVC4ApiException); + ASSERT_THROW(g.addRule(start, d_solver.mkBoolean(false)), CVC5ApiException); } TEST_F(TestApiBlackGrammar, addRules) @@ -64,16 +64,16 @@ TEST_F(TestApiBlackGrammar, addRules) ASSERT_NO_THROW(g.addRules(start, {d_solver.mkBoolean(false)})); ASSERT_THROW(g.addRules(nullTerm, {d_solver.mkBoolean(false)}), - CVC4ApiException); - ASSERT_THROW(g.addRules(start, {nullTerm}), CVC4ApiException); - ASSERT_THROW(g.addRules(nts, {d_solver.mkBoolean(false)}), CVC4ApiException); - ASSERT_THROW(g.addRules(start, {d_solver.mkInteger(0)}), CVC4ApiException); - ASSERT_THROW(g.addRules(start, {nts}), CVC4ApiException); + CVC5ApiException); + ASSERT_THROW(g.addRules(start, {nullTerm}), CVC5ApiException); + ASSERT_THROW(g.addRules(nts, {d_solver.mkBoolean(false)}), CVC5ApiException); + ASSERT_THROW(g.addRules(start, {d_solver.mkInteger(0)}), CVC5ApiException); + ASSERT_THROW(g.addRules(start, {nts}), CVC5ApiException); d_solver.synthFun("f", {}, boolean, g); ASSERT_THROW(g.addRules(start, {d_solver.mkBoolean(false)}), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackGrammar, addAnyConstant) @@ -89,12 +89,12 @@ TEST_F(TestApiBlackGrammar, addAnyConstant) ASSERT_NO_THROW(g.addAnyConstant(start)); ASSERT_NO_THROW(g.addAnyConstant(start)); - ASSERT_THROW(g.addAnyConstant(nullTerm), CVC4ApiException); - ASSERT_THROW(g.addAnyConstant(nts), CVC4ApiException); + ASSERT_THROW(g.addAnyConstant(nullTerm), CVC5ApiException); + ASSERT_THROW(g.addAnyConstant(nts), CVC5ApiException); d_solver.synthFun("f", {}, boolean, g); - ASSERT_THROW(g.addAnyConstant(start), CVC4ApiException); + ASSERT_THROW(g.addAnyConstant(start), CVC5ApiException); } TEST_F(TestApiBlackGrammar, addAnyVariable) @@ -113,12 +113,12 @@ TEST_F(TestApiBlackGrammar, addAnyVariable) ASSERT_NO_THROW(g1.addAnyVariable(start)); ASSERT_NO_THROW(g2.addAnyVariable(start)); - ASSERT_THROW(g1.addAnyVariable(nullTerm), CVC4ApiException); - ASSERT_THROW(g1.addAnyVariable(nts), CVC4ApiException); + ASSERT_THROW(g1.addAnyVariable(nullTerm), CVC5ApiException); + ASSERT_THROW(g1.addAnyVariable(nts), CVC5ApiException); d_solver.synthFun("f", {}, boolean, g1); - ASSERT_THROW(g1.addAnyVariable(start), CVC4ApiException); + ASSERT_THROW(g1.addAnyVariable(start), CVC5ApiException); } } // namespace test } // namespace cvc5 |