minor fix for recognizing the tail backslash, still have smt-lib compliance issue.

diff --git a/src/util/regexp.h b/src/util/regexp.h
index 4942c2652f5f2f60106256df6c556e510b91c3e8..10c8ba2b958b416bb1663b0b9f1e96504aec22ea 100644 (file)
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -124,7 +124,8 @@ private:
                                          }
                                  }
                          } else {
-                                 throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
+                                 //throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
+                                 d_str.push_back( convertCharToUnsignedInt('\\') );
                          }
                  } else {
                          d_str.push_back( convertCharToUnsignedInt(s[i]) );
@@ -138,19 +139,11 @@ public:
 
   String(const std::string &s) {
        toInternal(s);
-       /*
-    for(unsigned int i=0; i<s.size(); ++i) {
-        d_str.push_back( convertCharToUnsignedInt(s[i]) );
-    }*/
   }
 
   String(const char* s) {
        std::string stmp(s);
        toInternal(stmp);
-       /*
-    for(unsigned int i=0,len=strlen(s); i<len; ++i) {
-        d_str.push_back( convertCharToUnsignedInt(s[i]) );
-    }*/
   }
 
   String(const char c) {