Tuesday end-of-day commit.

Expected performance impact outside of datatypes/CVC parser is
negligible.

* CVC language LAMBDA, functional LET, type LET, precedence fixes,
  bitvectors, and arrays, with partial parsing support also for
  quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
    tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
  these are complicated because they have to be left unresolved
  at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
  (not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items

1 files changed, 6 insertions, 1 deletions

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index dbc8e2281..f288f6b1a 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -214,6 +214,8 @@ public:
     tryGoodInput("CHECKSAT 0bin0000 /= 0hex7;");
     tryGoodInput("%% nothing but a comment");
     tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment");
+    tryGoodInput("a : BOOLEAN; a: BOOLEAN;"); // double decl, but compatible
+    tryGoodInput("a : INT = 5; a: INT;"); // decl after define, compatible
   }
 
   void testBadCvc4Inputs() {
@@ -225,8 +227,11 @@ public:
     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
+    tryBadInput("a : BOOLEAN; a: INT;"); // double decl, incompatible
+    tryBadInput("A : TYPE; A: TYPE;"); // types can't be double-declared
+    tryBadInput("a : INT; a: INT = 5;"); // can't define after decl
+    tryBadInput("a : INT = 5; a: BOOLEAN;"); // decl w/ incompatible type
   }
 
   void testGoodCvc4Exprs() {