minor fix for internal string print

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 20b13f7b1b83867bd8475dd6dc7138d3325b7a0a..061b1adb5904a22f2f5a89626376775ce419b95f 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -2082,7 +2082,8 @@ std::string RegExpOpr::mkString( Node r ) {
         break;
       }
       case kind::STRING_TO_REGEXP: {
-        retStr += niceChar( r[0] );
+        std::string tmp( niceChar( r[0] ) );
+        retStr += tmp.size()==1? tmp : "(" + tmp + ")";
         break;
       }
       case kind::REGEXP_CONCAT: {