Fix for bug 555; SMT-LIBv2 symbols now output with proper quoting.

2 files changed, 20 insertions, 0 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 849d5c0a5..6485670b5 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -697,6 +697,25 @@ static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
   Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
 }
 
+void Smt2Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
+  if(sexpr.isKeyword()) {
+    std::string s = sexpr.getValue();
+    if(s.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789~!@%^&*_-+=<>.?/") == std::string::npos) {
+      // simple unquoted symbol
+      out << s;
+    } else {
+      // must quote the symbol, but it cannot contain | or \, we turn those into _
+      size_t p;
+      while((p = s.find_first_of("\\|")) != std::string::npos) {
+        s = s.replace(p, 1, "_");
+      }
+      out << "|" << s << "|";
+    }
+  } else {
+    this->Printer::toStream(out, sexpr);
+  }
+}
+
 template <class T>
 static bool tryToStream(std::ostream& out, const CommandStatus* s) throw();
 
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index c70bb78c3..c3f8deb9c 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -45,6 +45,7 @@ public:
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   void toStream(std::ostream& out, const Result& r) const throw();
+  void toStream(std::ostream& out, const SExpr& sexpr) const throw();
 };/* class Smt2Printer */
 
 }/* CVC4::printer::smt2 namespace */