printer change for string smtlib2

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 += "\\\\";
       }