From 48142c912d7571ee204b373eadf835c5b676af2c Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Tue, 16 Feb 2010 18:07:41 +0000 Subject: Converting semantic predicates in parser to AlwaysAssertions --- test/unit/parser/parser_black.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'test/unit/parser') diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 5d6326166..dbf434ed2 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -66,6 +66,7 @@ const string badCvc4Inputs[] = { "0x : INT;", // 0x isn't an identifier "a, b : BOOLEAN\nQUERY (a => b) AND a => b;", // no semicolon after decl "a : BOOLEAN; a: BOOLEAN;" // double decl + "a, b: BOOLEAN; QUERY a(b);" // non-function used as function }; const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string); @@ -142,7 +143,8 @@ const string badSmtExprs[] = { "(a IMPLIES b)", // infix AND wrong case "(not a b)", // wrong arity "not a", // needs parens - "(ite a x)" // wrong arity + "(ite a x)", // wrong arity + "(a b)" // using non-function as function }; const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); -- cgit v1.2.3