6 files changed, 60 insertions, 16 deletions
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 92db8d453..edda090ba 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -8,19 +8,19 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 
 # Regression tests for SMT inputs
-SMT_TESTS = 
+SMT_TESTS =
 
 # Regression tests for SMT2 inputs
-SMT2_TESTS = 
+SMT2_TESTS =
 
 # Regression tests for PL inputs
 CVC_TESTS = bvsimple.cvc
 
 # Regression tests derived from bug reports
-BUG_TESTS = 
+BUG_TESTS =
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) \
-	test00.smt
-
+	test00.smt \
+	bvcomp.smt
diff --git a/test/regress/regress0/bv/bvcomp.cvc b/test/regress/regress0/bv/bvcomp.cvc
new file mode 100644
index 000000000..c3397dfd7
--- /dev/null
+++ b/test/regress/regress0/bv/bvcomp.cvc
@@ -0,0 +1,6 @@
+% EXPECT: valid
+% EXIT: 20
+
+x : BITVECTOR(10);
+
+QUERY x /= ~x;
diff --git a/test/regress/regress0/bv/bvsimple.cvc b/test/regress/regress0/bv/bvsimple.cvc
index f1cb8ff01..59fe57386 100644
--- a/test/regress/regress0/bv/bvsimple.cvc
+++ b/test/regress/regress0/bv/bvsimple.cvc
@@ -4,18 +4,47 @@
 % Some tests from the CVC3 user manual.
 % http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html
 
+x : BITVECTOR(5);
+y : BITVECTOR(4);
+yy : BITVECTOR(3);
+
+bv : BITVECTOR(10);
+a : BOOLEAN;
+
+xx : BITVECTOR(8);
+zz : BITVECTOR(12);
+
+x4, y4 : BITVECTOR(4);
+
 QUERY
+( 0bin0000111101010000 = 0hex0f50 ) AND
 ( 0bin01@0bin0 = 0bin010 ) AND
 ( 0bin1000 >> 3 = 0bin0001 ) AND
 ( 0bin0011 << 3 = 0bin0011000 ) AND
 ( 0bin1000 >> 3 = 0bin0001 ) AND
 
-TRUE
-
 % these not working yet..
-%( BVZEROEXTEND(0bin100, 5) = 0bin00100 ) AND
+%
+%( BVZEROEXTEND(0bin100, 2) = 0bin00100 ) AND
 %( SX(0bin100, 5) = 0bin11100 ) AND
 %
-%( BVZEROEXTEND(0bin100, 3) = 0bin100 ) AND
-%( SX(0bin100, 3) = 0bin100 )
-;
+%( BVZEROEXTEND(0bin100, 0) = 0bin100 ) AND
+%( SX(0bin100, 3) = 0bin100 ) AND
+%
+%( (BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11)))[8:4] = BVPLUS(5, x, ~(y[3:2])) ) AND
+%
+%( x4 = 0hex5 AND y4 = 0bin0101 ) =>
+%( ( BVMULT(8,x4,y4)=BVMULT(8,y4,x4) ) AND
+%  ( NOT(BVLT(x4,y4)) ) AND
+%  ( BVLE(BVSUB(8,x4,y4), BVPLUS(8, x4, BVUMINUS(x4))) ) AND
+%  ( x4 = BVSUB(4, BVUMINUS(x4), BVPLUS(4, x4,0hex1)) ) ) AND
+
+
+( 0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2] ) AND
+( 0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF) = (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0] ) AND
+
+( xx = 0hexff AND zz = 0hexff0 =>
+  ( zz = xx << 4 ) AND
+  ( (zz >> 4)[7:0] = xx ) ) AND
+
+TRUE;
diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc
index 982731b34..6d1641092 100644
--- a/test/regress/regress0/error.cvc
+++ b/test/regress/regress0/error.cvc
@@ -1,4 +1,4 @@
 % EXPECT-ERROR: CVC4 Error:
-% EXPECT-ERROR: Parse Error: error.cvc:3.9: Symbol BOOL not declared
+% EXPECT-ERROR: Parse Error: error.cvc:3.8: Symbol BOOL not declared as a type
 p : BOOL;
 % EXIT: 1
diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp
index 497f11c08..821b43a2f 100644
--- a/test/system/ouroborous.cpp
+++ b/test/system/ouroborous.cpp
@@ -88,11 +88,15 @@ int runTest() {
   AlwaysAssert(parser->done(), "parser should be done");
 
   string instr = "(= (f (f y)) x)";
+  cout << "starting with: " << instr << endl;
   string smt2 = translate(parser, instr, input::LANG_SMTLIB_V2, output::LANG_SMTLIB_V2);
+  cout << "in SMT2      : " << smt2 << endl;
   string smt1 = translate(parser, smt2, input::LANG_SMTLIB_V2, output::LANG_SMTLIB);
-  //string cvc = translate(parser, smt1, input::LANG_SMTLIB, output::LANG_CVC4);
-  //string out = translate(parser, cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2);
-  string out = smt1;
+  cout << "in SMT1      : " << smt1 << endl;
+  string cvc = translate(parser, smt1, input::LANG_SMTLIB, output::LANG_CVC4);
+  cout << "in CVC       : " << cvc << endl;
+  string out = translate(parser, cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2);
+  cout << "back to SMT2 : " << out << endl;
 
   AlwaysAssert(out == smt2, "differences in output");
 
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() {