SMT-LIBv2 compliance updates:

* chainability of =, <, <=, >, >= via the new CHAINABLE kind and
  TheoryBuiltin rewriter support (resolves bug #383)
* with --smtlib2, force interactive mode off by default

Also:

* fix a few bugs causing crashes
* better "alias" processing for options
* configure-time fixes to readline detection

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 5 insertions, 1 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 6dbf4ed03..b14f6a9c8 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -73,7 +73,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
   if (depth == 0) {
     out << "(...)";
   } else {
-    depth --;
+    --depth;
   }
 
   // null
@@ -221,6 +221,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     case kind::APPLY:
       toStream(op, n.getOperator(), depth, types, true);
       break;
+    case kind::CHAIN:
+    case kind::DISTINCT: // chain and distinct not supported directly in CVC4, blast them away with the rewriter
+      toStream(out, theory::Rewriter::rewrite(n), depth, types, true);
+      return;
     case kind::SORT_TYPE:
     {
       string name;