From 1b916866274cc238c708f25fbb8c17add33d3376 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 10 Feb 2014 21:04:58 -0500
Subject: [PATCH] Fix quotes in string constants.

---
 src/util/regexp.h | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/util/regexp.h b/src/util/regexp.h
index 46417cdb6..0cd92810b 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -21,6 +21,7 @@
 #define __CVC4__REGEXP_H
 
 #include <iostream>
+#include <iomanip>
 #include <string>
 #include <sstream>
 #include "util/exception.h"
@@ -390,7 +391,18 @@ struct CVC4_PUBLIC StringHashFunction {
 
 inline std::ostream& operator <<(std::ostream& os, const String& s) CVC4_PUBLIC;
 inline std::ostream& operator <<(std::ostream& os, const String& s) {
-  return os << "\"" << s.toString() << "\"";
+  os << '"';
+  std::string str = s.toString();
+  for(std::string::iterator i = str.begin(); i != str.end(); ++i) {
+    if(*i == '\\' || *i == '"') {
+      os << '\\';
+    } else if(!isprint(*i)) {
+      os << "\\x" << std::ios::hex << std::setw(2) << (unsigned(*i) % 0x100);
+      continue;
+    }
+    os << *i;
+  }
+  return os << '"';
 }
 
 class CVC4_PUBLIC RegExp {
-- 
2.30.2