printer change for string smtlib2

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 999dc870ff282772dd4034592488148028bd2eff..a98a106a1076e3145ae38e723ae18cb18c8dd8f9 100644 (file)
--- 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 90029495ba8449be7ee9b02399dfcb4edf055292..1869145007d90faa94a01aadcb54defcf2b343a6 100644 (file)
--- 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 6bbdcb36a154f2d6ae2bd5b9de609901ca584be8..05aacc06c5658b8c7aeb7c5bca196df564c3fb8e 100644 (file)
--- 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 += "\\\\";
       }