diff options
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.cpp | 2 | ||||
-rw-r--r-- | src/util/regexp.cpp | 2 |
3 files changed, 3 insertions, 5 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 999dc870f..a98a106a1 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -226,13 +226,11 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, //char c = String::convertUnsignedIntToChar(s[i]); char c = s[i]; if(c == '"') { - if(d_variant == z3str_variant || d_variant == smt2_0_variant) { + if(d_variant == smt2_0_variant) { out << "\\\""; } else { out << "\"\""; } - } else if(c == '\\' && (d_variant == z3str_variant || d_variant == smt2_0_variant)) { - out << "\\\\"; } else { out << c; } diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 90029495b..186914500 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -34,7 +34,7 @@ ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDa d_constraintDatabase(cd), d_setupLiteral(setup), d_avariables(avars), - d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", false) + d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true) {} ArithCongruenceManager::Statistics::Statistics(): diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index 6bbdcb36a..05aacc06c 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -114,7 +114,7 @@ std::string String::toString() const { std::string str; for(unsigned int i=0; i<d_str.size(); ++i) { unsigned char c = convertUnsignedIntToChar( d_str[i] ); - if(isprint( c )) { + if(isprint( c )) { if(c == '\\') { str += "\\\\"; } |