From 9ced0e7a1119c625923ccbecb6a942c750319e56 Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 26 Feb 2014 14:19:49 -0600
Subject: [PATCH] bug fix (caused by merge), move cardinality option to expert
 option

---
 src/theory/strings/options                     |  2 +-
 src/theory/strings/regexp_operation.cpp        |  2 +-
 src/util/regexp.cpp                            | 10 +++++-----
 test/regress/regress0/strings/Makefile.am      |  1 +
 test/regress/regress0/strings/cardinality.smt2 |  2 +-
 5 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/theory/strings/options b/src/theory/strings/options
index 5ac86dcae..139eca6ac 100644
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -5,7 +5,7 @@
 
 module STRINGS "theory/strings/options.h" Strings theory
 
-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 256 :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
+expert-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 256 :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  the cardinality of the characters used by the theory of strings, default 256
 
 option stringRegExpUnrollDepth strings-regexp-depth --strings-regexp-depth=N int16_t :default 10 :read-write
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 1f4e86846..e608a0533 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -702,7 +702,7 @@ void RegExpOpr::simplifyRegExp( Node s, Node r, std::vector< Node > &new_nodes )
 				for(unsigned i=0; i<r.getNumChildren(); ++i) {
 					if(r[i].getKind() == kind::STRING_TO_REGEXP) {
 						cc.push_back( r[i][0] );
-					} if(r[i].getKind() == kind::STRING_TO_REGEXP) {
+					} else if(r[i].getKind() == kind::REGEXP_EMPTY) {
 						emptyflag = true;
 						break;
 					} else {
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 246f16243..684a480fb 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -17,6 +17,7 @@
 
 #include "util/regexp.h"
 #include <iostream>
+#include <iomanip>
 
 using namespace std;
 
@@ -46,11 +47,10 @@ std::string String::toString() const {
 			case '\n': s = "\\n"; break;
 			case '\e': s = "\\e"; break;
 			default  : {
-				std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();
-				if(s2.size() == 1) {
-					s2 = "0" + s2;
-				}
-				s = "\\x" + s2;
+				std::stringstream ss;
+				ss << std::setfill ('0') << std::setw(2) << std::hex << ((int)c);
+				s = "\\x" + ss.str();
+				//std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();
 			}
 		  }
 		  str += s;
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 254df183e..f11ada1a1 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -21,6 +21,7 @@ MAKEFLAGS = -k
 TESTS =	\
   at001.smt2 \
   cardinality.smt2 \
+  escchar.smt2 \
   str001.smt2 \
   str002.smt2 \
   str003.smt2 \
diff --git a/test/regress/regress0/strings/cardinality.smt2 b/test/regress/regress0/strings/cardinality.smt2
index d64bc240e..921991f74 100644
--- a/test/regress/regress0/strings/cardinality.smt2
+++ b/test/regress/regress0/strings/cardinality.smt2
@@ -1,6 +1,6 @@
 (set-logic QF_S)
 (set-info :status unsat)
-
+;this option for experts only
 (set-option :strings-alphabet-card 2)
 
 (declare-fun x () String)
-- 
2.30.2