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, 7 insertions, 3 deletions

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");