1 files changed, 34 insertions, 6 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 04690f500..a3d15f822 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -173,6 +173,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       toStream(out, n[1], depth, types, true);
       out << " ELSE ";
       toStream(out, n[2], depth, types, true);
+      out << " ENDIF";
       return;
       break;
     case kind::TUPLE_TYPE:
@@ -237,18 +238,18 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
         if (n.getNumChildren() > 2) {
           out << '(';
         }
-        for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
-          if (i > 0) {
+        for (unsigned i = 1; i < n.getNumChildren(); ++i) {
+          if (i > 1) {
             out << ", ";
           }
-          toStream(out, n[i], depth, types, false);
+          toStream(out, n[i - 1], depth, types, false);
         }
         if (n.getNumChildren() > 2) {
           out << ')';
         }
       }
       out << " -> ";
-      toStream(out, n[n.getNumChildren()-1], depth, types, false);
+      toStream(out, n[n.getNumChildren() - 1], depth, types, false);
       return;
       break;
 
@@ -630,6 +631,29 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
 }/* CvcPrinter::toStream(CommandStatus*) */
 
+static void toStream(std::ostream& out, const SExpr& sexpr) throw() {
+  if(sexpr.isInteger()) {
+    out << sexpr.getIntegerValue();
+  } else if(sexpr.isRational()) {
+    out << sexpr.getRationalValue();
+  } else if(sexpr.isString()) {
+    string s = sexpr.getValue();
+    // escape backslash and quote
+    for(string::iterator i = s.begin(); i != s.end(); ++i) {
+      if(*i == '"') {
+        s.replace(i, i + 1, "\\\"");
+        ++i;
+      } else if(*i == '\\') {
+        s.replace(i, i + 1, "\\\\");
+        ++i;
+      }
+    }
+    out << "\"" << s << "\"";
+  } else {
+    out << sexpr;
+  }
+}
+
 static void toStream(std::ostream& out, const AssertCommand* c) throw() {
   out << "ASSERT " << c->getExpr() << ";";
 }
@@ -756,7 +780,9 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw
 }
 
 static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
-  out << "% (set-info " << c->getFlag() << " " << c->getSExpr() << ")";
+  out << "% (set-info " << c->getFlag() << " ";
+  toStream(out, c->getSExpr());
+  out << ")";
 }
 
 static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
@@ -764,7 +790,9 @@ static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
 }
 
 static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
-  out << "% (set-option " << c->getFlag() << " " << c->getSExpr() << ")";
+  out << "% (set-option " << c->getFlag() << " ";
+  toStream(out, c->getSExpr());
+  out << ")";
 }
 
 static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {