diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index ce7177ec9..eece67a32 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -305,14 +305,45 @@ format * smt2_pp_environment::mk_float(rational const & val) const {
 }
 
 format * smt2_pp_environment::pp_str_literal(app * t) {
-    TRACE("parse_string", tout << "pp_str_literal\n";);
-    str_util & u = get_strutil();
-    SASSERT(u.is_string(t));
-    const char * val;
-    u.is_string(t, &val);
     ast_manager & m = get_manager();
+    str_util & u = get_strutil();
+    TRACE("parse_string", tout << "pp_str_literal\n";);
+
+    SASSERT(u.is_string(t));
+    std::string strVal = u.get_string_constant_value(t);
     string_buffer<> buf;
-    buf << "\"" << val << "\"";
+    buf << "\"";
+
+    // we want to scan strVal and escape every non-printable character
+    for (unsigned int i = 0; i < strVal.length(); ++i) {
+        char c = strVal.at(i);
+        if (isprint(c)) {
+            buf << c;
+        } else if (c == '\a') {
+            buf << "\\a";
+        } else if (c == '\b') {
+            buf << "\\b";
+        } else if (c == '\e') {
+            buf << "\\e";
+        } else if (c == '\f') {
+            buf << "\\f";
+        } else if (c == '\n') {
+            buf << "\\n";
+        } else if (c == '\r') {
+            buf << "\\r";
+        } else if (c == '\t') {
+            buf << "\\t";
+        } else if (c == '\v') {
+            buf << "\\v";
+        } else if (c == '\\') {
+            buf << "\\" << "\\";
+        } else {
+            // TODO general hex escape
+            NOT_IMPLEMENTED_YET();
+        }
+    }
+
+    buf << "\"";
     return mk_string(m, buf.c_str());
 }
 
diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp
index f17551b94..8ac1f722f 100644
--- a/src/ast/str_decl_plugin.cpp
+++ b/src/ast/str_decl_plugin.cpp
@@ -344,7 +344,7 @@ str_util::str_util(ast_manager &m) :
  * as a possible escape sequence. Emit all other characters as-is.
  * This exists because the SMT-LIB 2.5 standard does not recognize escape sequences other than "" -> " .
  * The escape sequences recognized are as follows:
- *   \a \b \e \f \n \r \t \v : as specified by the C++ standard
+ *   \a \b \e \f \n \r \t \v \\ : as specified by the C++ standard
  *   \ooo : produces the ASCII character corresponding to the octal value "ooo", where each "o" is a
  *          single octal digit and between 1 and 3 valid digits are given
  *   \xhh : produces the ASCII character corresponding to the hexadecimal value "hh", where each "h" is a
@@ -381,6 +381,8 @@ app * str_util::mk_string_with_escape_characters(std::string & val) {
                 parsedStr.push_back('\t');
             } else if (escapeChar1 == 'v') {
                 parsedStr.push_back('\v');
+            } else if (escapeChar1 == '\\') {
+                parsedStr.push_back('\\');
             } else if (escapeChar1 == 'x') {
                 // TODO hex escape
                 NOT_IMPLEMENTED_YET();