summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2015-01-11 12:00:10 -0600
committerTianyi Liang <tianyi-liang@uiowa.edu>2015-01-11 12:00:10 -0600
commit1d8ed81bcb817139a50404646b753192de787576 (patch)
tree0f7cee0f34afedb221dd1d26e5c25b6e56a43b66 /src
parent2d0ba1036e35a6ce6cb8d5cd9e68d311ae8cde80 (diff)
adjusted to both v2.0 and v2.5 string literals
Diffstat (limited to 'src')
-rw-r--r--src/printer/smt2/smt2_printer.cpp6
-rw-r--r--src/util/regexp.cpp8
2 files changed, 8 insertions, 6 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 {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback