From 1d8ed81bcb817139a50404646b753192de787576 Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Sun, 11 Jan 2015 12:00:10 -0600
Subject: [PATCH] adjusted to both v2.0 and v2.5 string literals

---
 src/printer/smt2/smt2_printer.cpp        | 6 +++---
 src/util/regexp.cpp                      | 8 +++++---
 test/regress/regress0/parser/Makefile.am | 5 ++---
 3 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index e72de92fd..72a64ab78 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -223,13 +223,13 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
         char c = s[i];
         if(c == '"') {
           if(d_variant == z3str_variant || d_variant == smt2_0_variant) {
-            out << c; //out << "\\\"";
+            out << "\\\"";
           } else {
             out << "\"\"";
           }
-        } /*else if(c == '\\' && (d_variant == z3str_variant || d_variant == smt2_0_variant)) {
+        } else if(c == '\\' && (d_variant == z3str_variant || d_variant == smt2_0_variant)) {
           out << "\\\\";
-        }*/ else {
+        } else {
           out << c;
         }
       }
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 24e894678..6bbdcb36a 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -117,9 +117,11 @@ std::string String::toString() const {
       if(isprint( c )) {
       if(c == '\\') {
         str += "\\\\";
-      } else if(c == '\"') {
-        str += "\\\"";
-      } else {
+      } 
+      //else if(c == '\"') {
+      //  str += "\\\"";
+      //} 
+      else {
         str += c;
       }
     } else {
diff --git a/test/regress/regress0/parser/Makefile.am b/test/regress/regress0/parser/Makefile.am
index 3808bd54d..eb27e797b 100644
--- a/test/regress/regress0/parser/Makefile.am
+++ b/test/regress/regress0/parser/Makefile.am
@@ -20,9 +20,8 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 TESTS =	\
 	declarefun-emptyset-uf.smt2 \
-	strings20.smt2
-
-#	strings25.smt2
+	strings20.smt2 \
+	strings25.smt2
 
 EXTRA_DIST = $(TESTS)
 
-- 
2.30.2