From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 12 Feb 2014 00:08:53 +0000 (-0600)
Subject: minor fix for recognizing the tail backslash, still have smt-lib compliance issue.
X-Git-Tag: cvc5-1.0.0~7093
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cbf8dffcd17e70d4d4c7d8d1e57bcb16317d246f;p=cvc5.git

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 4942c2652..10c8ba2b9 100644
--- 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) {