diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-03-30 06:33:33 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-30 13:33:33 +0000 |
| commit | e5bf082fde4c8b3c10448cbf3cb962739df9cf66 (patch) | |
| tree | 1f5690a300a3558355915411b61ec617f8e1a54e /test/unit/api/grammar_black.cpp | |
| parent | c7a8c32825af7dceb6cee631523a480a5b2cc6ba (diff) | |
Give a better error when sygus grammar rules contain free variables. (#6199)
Diffstat (limited to 'test/unit/api/grammar_black.cpp')
| -rw-r--r-- | test/unit/api/grammar_black.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp index cabc3e249..c816fa5a3 100644 --- a/test/unit/api/grammar_black.cpp +++ b/test/unit/api/grammar_black.cpp @@ -44,6 +44,7 @@ TEST_F(TestApiBlackGrammar, addRule) 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); d_solver.synthFun("f", {}, boolean, g); @@ -68,6 +69,7 @@ TEST_F(TestApiBlackGrammar, addRules) 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); d_solver.synthFun("f", {}, boolean, g); |