diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-04 22:27:40 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-04 22:27:40 +0000 |
commit | fec2b5751108088ff651ce6eed09bf3aa65f281e (patch) | |
tree | 8585e7a1b0225512e509f2ede6717d64a5aec900 | |
parent | 65d24277bfb9f76b612fa51770d5d63e1d34b528 (diff) |
Adding simple SMT2 parser tests
-rw-r--r-- | test/unit/parser/parser_black.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 0389a75ef..b8060086f 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -149,8 +149,10 @@ const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); const string goodSmt2Inputs[] = { "", // empty string is OK "(set-logic QF_UF)", + "(set-info :notes |This is a note, take note!|)", "(assert true)", "(check-sat)", + "(exit)", "(assert false) (check-sat)", "(declare-fun a () Bool) (declare-fun b () Bool)", "(declare-fun a () Bool) (declare-fun b () Bool) (assert (=> (and (=> a b) a) b))", @@ -179,6 +181,7 @@ const int numGoodSmt2Exprs = sizeof(goodSmt2Exprs) / sizeof(string); const string badSmt2Inputs[] = { "(assert)", // no args + "(set-info :notes |Symbols can't contain the | character|)", "(check-sat true)", // shouldn't have an arg "(declare-sort a)", // no arg "(declare-sort a 0) (declare-sort a 0)", // double decl |