diff options
Diffstat (limited to 'test/unit/parser')
| -rw-r--r-- | test/unit/parser/parser_black.h | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index af9b7bd0f..dbc8e2281 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -2,10 +2,10 @@ /*! \file parser_black.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -206,7 +206,12 @@ public: tryGoodInput("a, b : BOOLEAN;"); tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;"); tryGoodInput("T, U : TYPE; f : T -> U; x : T; y : U; CHECKSAT f(x) = y;"); + tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;"); + tryGoodInput("a : ARRAY INT OF REAL; ASSERT (a WITH [1] := 0.0)[1] = a[0];"); + tryGoodInput("b : BITVECTOR(3); ASSERT b = 0bin101;"); + tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;"); tryGoodInput("T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;"); + tryGoodInput("CHECKSAT 0bin0000 /= 0hex7;"); tryGoodInput("%% nothing but a comment"); tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment"); } @@ -219,6 +224,7 @@ public: tryBadInput("a, b : boolean;"); // lowercase boolean isn't a type tryBadInput("0x : INT;"); // 0x isn't an identifier tryBadInput("a, b : BOOLEAN\nQUERY (a => b) AND a => b;"); // no semicolon after decl + tryBadInput("ASSERT 0bin012 /= 0hex0;"); // bad binary literal tryBadInput("a : BOOLEAN; a: BOOLEAN;"); // double decl tryBadInput("a, b: BOOLEAN; QUERY a(b);"); // non-function used as function } |