From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Sat, 28 Mar 2015 17:04:33 +0000 (-0500)
Subject: printer change for string smtlib2
X-Git-Tag: cvc5-1.0.0~6370
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8b79e00ea9baf7fec7a2ce390827065ba7e60fcf;p=cvc5.git

printer change for string smtlib2
---

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