Merge remote-tracking branch 'upstream/master' into sets

12 files changed, 1563 insertions, 1273 deletions

diff --git a/src/theory/strings/options b/src/theory/strings/options
index f6d765fc4..10f22b05a 100644
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -17,6 +17,12 @@ option stringFMF strings-fmf --strings-fmf bool :default false :read-write
 option stringEIT strings-eit --strings-eit bool :default false
  the eager intersection used by the theory of strings
 
+option stringOpt1 strings-opt1 --strings-opt1 bool :default true
+ internal option1 for strings: normal form
+
+option stringOpt2 strings-opt2 --strings-opt2 bool :default false
+ internal option2 for strings: constant regexp splitting
+
 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
 
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 16bb7e694..5c664ba34 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -33,14 +33,14 @@ namespace theory {
 namespace strings {

 

 RegExpOpr::RegExpOpr() {

-    d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );

-    d_true = NodeManager::currentNM()->mkConst( true );

-    d_false = NodeManager::currentNM()->mkConst( false );

+  d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );

+  d_true = NodeManager::currentNM()->mkConst( true );

+  d_false = NodeManager::currentNM()->mkConst( false );

 	d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );

 	d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );

 	d_emptySingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );

 	std::vector< Node > nvec;

-    d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );

+  d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );

 	d_sigma = NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA, nvec );

 	d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );

 	d_card = 256;

@@ -1315,6 +1315,119 @@ Node RegExpOpr::complement(Node r, int &ret) {
 	Trace("regexp-compl") << "COMPL( " << mkString(r) << " ) = " << mkString(rNode) << ", ret=" << ret << std::endl;

 	return rNode;

 }

+

+void RegExpOpr::splitRegExp(Node r, std::vector< PairNodes > &pset) {

+	Assert(checkConstRegExp(r));

+	if(d_split_cache.find(r) != d_split_cache.end()) {

+		pset = d_split_cache[r];

+	} else {

+		switch( r.getKind() ) {

+			case kind::REGEXP_EMPTY: {

+				break;

+			}

+			case kind::REGEXP_OPT: {

+				PairNodes tmp(d_emptySingleton, d_emptySingleton);

+				pset.push_back(tmp);

+			}

+			case kind::REGEXP_RANGE:

+			case kind::REGEXP_SIGMA: {

+				PairNodes tmp1(d_emptySingleton, r);

+				PairNodes tmp2(r, d_emptySingleton);

+				pset.push_back(tmp1);

+				pset.push_back(tmp2);

+				break;

+			}

+			case kind::STRING_TO_REGEXP: {

+				Assert(r[0].isConst());

+				CVC4::String s = r[0].getConst< CVC4::String >();

+				PairNodes tmp1(d_emptySingleton, r);

+				pset.push_back(tmp1);

+				for(unsigned i=1; i<s.size(); i++) {

+					CVC4::String s1 = s.substr(0, i);

+					CVC4::String s2 = s.substr(i);

+					Node n1 = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(s1));

+					Node n2 = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(s2));

+					PairNodes tmp3(n1, n2);

+					pset.push_back(tmp3);

+				}

+				PairNodes tmp2(r, d_emptySingleton);

+				pset.push_back(tmp2);

+				break;

+			}

+			case kind::REGEXP_CONCAT: {

+				for(unsigned i=0; i<r.getNumChildren(); i++) {

+					std::vector< PairNodes > tset;

+					splitRegExp(r[i], tset);

+					std::vector< Node > hvec;

+					std::vector< Node > tvec;

+					for(unsigned j=0; j<=i; j++) {

+						hvec.push_back(r[j]);

+					}

+					for(unsigned j=i; j<r.getNumChildren(); j++) {

+						tvec.push_back(r[j]);

+					}

+					for(unsigned j=0; j<tset.size(); j++) {

+						hvec[i] = tset[j].first;

+						tvec[0] = tset[j].second;

+						Node r1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, hvec) );

+						Node r2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tvec) );

+						PairNodes tmp2(r1, r2);

+						pset.push_back(tmp2);

+					}

+				}

+				break;

+			}

+			case kind::REGEXP_UNION: {

+				for(unsigned i=0; i<r.getNumChildren(); ++i) {

+					std::vector< PairNodes > tset;

+					splitRegExp(r[i], tset);

+					pset.insert(pset.end(), tset.begin(), tset.end());

+				}

+				break;

+			}

+			case kind::REGEXP_INTER: {

+				bool spflag = false;

+				Node tmp = r[0];

+				for(unsigned i=1; i<r.getNumChildren(); i++) {

+					tmp = intersect(tmp, r[i], spflag);

+				}

+				splitRegExp(tmp, pset);

+				break;

+			}

+			case kind::REGEXP_STAR: {

+				std::vector< PairNodes > tset;

+				splitRegExp(r[0], tset);

+				PairNodes tmp1(d_emptySingleton, d_emptySingleton);

+				pset.push_back(tmp1);

+				for(unsigned i=0; i<tset.size(); i++) {

+					Node r1 = tset[i].first==d_emptySingleton ? r : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, r, tset[i].first);

+					Node r2 = tset[i].second==d_emptySingleton ? r : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tset[i].second, r);

+					PairNodes tmp2(r1, r2);

+					pset.push_back(tmp2);

+				}

+				break;

+			}

+			case kind::REGEXP_PLUS: {

+				std::vector< PairNodes > tset;

+				splitRegExp(r[0], tset);

+				for(unsigned i=0; i<tset.size(); i++) {

+					Node r1 = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, r, tset[i].first);

+					Node r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tset[i].second, r);

+					PairNodes tmp2(r1, r2);

+					pset.push_back(tmp2);

+				}

+				break;

+			}

+			default: {

+				Trace("strings-error") << "Unsupported term: " << r << " in splitRegExp." << std::endl;

+				Assert( false );

+				//return Node::null();

+			}

+		}

+		d_split_cache[r] = pset;

+	}

+}

+

 //printing

 std::string RegExpOpr::niceChar( Node r ) {

 	if(r.isConst()) {

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 116868820..0513eeef4 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -39,9 +39,9 @@ class RegExpOpr {
 

 private:

 	unsigned d_card;

-    Node d_emptyString;

-    Node d_true;

-    Node d_false;

+  Node d_emptyString;

+  Node d_true;

+  Node d_false;

 	Node d_emptySingleton;

 	Node d_emptyRegexp;

 	Node d_zero;

@@ -62,6 +62,7 @@ private:
 	std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_cset_cache;

 	std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_fset_cache;

 	std::map< PairNodes, Node > d_inter_cache;

+	std::map< Node, std::vector< PairNodes > > d_split_cache;

 	//bool checkStarPlus( Node t );

 	void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes );

 	void simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes );

@@ -80,13 +81,14 @@ public:
 	RegExpOpr();

 

 	bool checkConstRegExp( Node r );

-    void simplify(Node t, std::vector< Node > &new_nodes, bool polarity);

+  void simplify(Node t, std::vector< Node > &new_nodes, bool polarity);

 	int delta( Node r, Node &exp );

 	int derivativeS( Node r, CVC4::String c, Node &retNode );

 	Node derivativeSingle( Node r, CVC4::String c );

 	bool guessLength( Node r, int &co );

 	Node intersect(Node r1, Node r2, bool &spflag);

 	Node complement(Node r, int &ret);

+	void splitRegExp(Node r, std::vector< PairNodes > &pset);

 

 	std::string mkString( Node r );

 };

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index d44f38bc3..61d60d4cd 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -34,13 +34,13 @@ namespace theory {
 namespace strings {
 
 TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
-    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
-    d_notify( *this ),
-    d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"),
-    d_conflict(c, false),
-    d_infer(c),
-    d_infer_exp(c),
-    d_nf_pairs(c),
+  : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
+  d_notify( *this ),
+  d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"),
+  d_conflict(c, false),
+  d_infer(c),
+  d_infer_exp(c),
+  d_nf_pairs(c),
 	d_loop_antec(u),
 	d_length_intro_vars(u),
 	d_prereg_cached(u),
@@ -64,28 +64,28 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
 	d_cardinality_lits(u),
 	d_curr_cardinality(c, 0)
 {
-    // The kinds we are treating as function application in congruence
-    d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
-    d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
-    d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
-    d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
-    d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
-    d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
-    d_equalityEngine.addFunctionKind(kind::STRING_STOI);
-    //d_equalityEngine.addFunctionKind(kind::STRING_U16TOS);
-    //d_equalityEngine.addFunctionKind(kind::STRING_STOU16);
-    //d_equalityEngine.addFunctionKind(kind::STRING_U32TOS);
-    //d_equalityEngine.addFunctionKind(kind::STRING_STOU32);
-
-    d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
-    d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
-    d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
-	std::vector< Node > nvec;
-	d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
-	d_true = NodeManager::currentNM()->mkConst( true );
-    d_false = NodeManager::currentNM()->mkConst( false );
-
-	//d_opt_regexp_gcd = true;
+  // The kinds we are treating as function application in congruence
+  d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
+  d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
+  d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
+  d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
+  d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
+  d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
+  d_equalityEngine.addFunctionKind(kind::STRING_STOI);
+  //d_equalityEngine.addFunctionKind(kind::STRING_U16TOS);
+  //d_equalityEngine.addFunctionKind(kind::STRING_STOU16);
+  //d_equalityEngine.addFunctionKind(kind::STRING_U32TOS);
+  //d_equalityEngine.addFunctionKind(kind::STRING_STOU32);
+
+  d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+  d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+  d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
+  std::vector< Node > nvec;
+  d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
+  d_true = NodeManager::currentNM()->mkConst( true );
+  d_false = NodeManager::currentNM()->mkConst( false );
+
+  //d_opt_regexp_gcd = true;
 }
 
 TheoryStrings::~TheoryStrings() {
@@ -221,13 +221,13 @@ void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions){
     d_equalityEngine.explainPredicate(atom, polarity, tassumptions);
   }
   for( unsigned i=0; i<tassumptions.size(); i++ ){
-	if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
-		assumptions.push_back( tassumptions[i] );
-	}
+    if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
+      assumptions.push_back( tassumptions[i] );
+    }
   }
   Debug("strings-explain-debug") << "Explanation for " << literal << " was " << std::endl;
   for( unsigned i=ps; i<assumptions.size(); i++ ){
-	Debug("strings-explain-debug") << "   " << assumptions[i] << std::endl;
+	  Debug("strings-explain-debug") << "   " << assumptions[i] << std::endl;
   }
 }
 
@@ -263,7 +263,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 	Trace("strings-model") << "TheoryStrings : Collect model info, fullModel = " << fullModel << std::endl;
 	Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl;
 	m->assertEqualityEngine( &d_equalityEngine );
-    // Generate model
+  // Generate model
 	std::vector< Node > nodes;
 	getEquivalenceClasses( nodes );
 	std::map< Node, Node > processed;
@@ -410,120 +410,119 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 
 void TheoryStrings::preRegisterTerm(TNode n) {
   if(d_prereg_cached.find(n) == d_prereg_cached.end()) {
-	Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl;
-	//collectTerms( n );
-	switch (n.getKind()) {
-	case kind::EQUAL:
-		d_equalityEngine.addTriggerEquality(n);
-		break;
-	case kind::STRING_IN_REGEXP:
-		//do not add trigger here
-		d_equalityEngine.addTriggerPredicate(n);
-		break;
-	case kind::STRING_SUBSTR_TOTAL: {
-		Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
-							NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
-							NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
-		Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
-		Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero);
-		Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-		Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" );
-		Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" );
-		d_statistics.d_new_skolems += 2;
-		Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, n, sk3 ) );
-		Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-		Node lenc = n[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n ) );
-		Node lemma = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, cond, 
-			NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ),
-			n.eqNode(d_emptyString)));
-		Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
-		d_out->lemma(lemma);
-		//d_equalityEngine.addTerm(n);
-	}
-	default: {
-		if(n.getType().isString() && n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) {
-		  if( d_length_intro_vars.find(n)==d_length_intro_vars.end() ) {
-			  Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
-			  Node n_len_eq_z = n_len.eqNode( d_zero );
-			  n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
-			  Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
-										NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
-			  Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
-			  d_out->lemma(n_len_geq_zero);
-			  d_out->requirePhase( n_len_eq_z, true );
-		  }
-		  // FMF
-		  if( n.getKind() == kind::VARIABLE && options::stringFMF() ) {
-			  d_input_vars.insert(n);
-		  }
-		}
-		if (n.getType().isBoolean()) {
-		  // Get triggered for both equal and dis-equal
-		  d_equalityEngine.addTriggerPredicate(n);
-		} else {
-		  // Function applications/predicates
-		  d_equalityEngine.addTerm(n);
-		}
-	}
-	}
-	d_prereg_cached.insert(n);
+    Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl;
+    //collectTerms( n );
+    switch (n.getKind()) {
+      case kind::EQUAL:
+        d_equalityEngine.addTriggerEquality(n);
+        break;
+      case kind::STRING_IN_REGEXP:
+        //do not add trigger here
+        d_equalityEngine.addTriggerPredicate(n);
+        break;
+      case kind::STRING_SUBSTR_TOTAL: {
+        Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
+                  NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
+                  NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
+        Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
+        Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero);
+        Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
+        Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+        Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+        d_statistics.d_new_skolems += 2;
+        Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, n, sk3 ) );
+        Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+        Node lenc = n[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n ) );
+        Node lemma = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, cond, 
+          NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ),
+          n.eqNode(d_emptyString)));
+        Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
+        d_out->lemma(lemma);
+        //d_equalityEngine.addTerm(n);
+      }
+      default: {
+        if(n.getType().isString() && n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) {
+          if( d_length_intro_vars.find(n)==d_length_intro_vars.end() ) {
+            Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
+            Node n_len_eq_z = n_len.eqNode( d_zero );
+            n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
+            Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
+                        NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
+            Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
+            d_out->lemma(n_len_geq_zero);
+            d_out->requirePhase( n_len_eq_z, true );
+          }
+          // FMF
+          if( n.getKind() == kind::VARIABLE && options::stringFMF() ) {
+            d_input_vars.insert(n);
+          }
+        }
+        if (n.getType().isBoolean()) {
+          // Get triggered for both equal and dis-equal
+          d_equalityEngine.addTriggerPredicate(n);
+        } else {
+          // Function applications/predicates
+          d_equalityEngine.addTerm(n);
+        }
+      }
+    }
+    d_prereg_cached.insert(n);
   }
 }
 
 Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) {
   switch (node.getKind()) {
-  case kind::STRING_CHARAT: {
-    if(d_ufSubstr.isNull()) {
-      std::vector< TypeNode > argTypes;
-      argTypes.push_back(NodeManager::currentNM()->stringType());
-      argTypes.push_back(NodeManager::currentNM()->integerType());
-      argTypes.push_back(NodeManager::currentNM()->integerType());
-      d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
-						      NodeManager::currentNM()->mkFunctionType(
-											       argTypes, NodeManager::currentNM()->stringType()),
-						      "uf substr",
-						      NodeManager::SKOLEM_EXACT_NAME);
+    case kind::STRING_CHARAT: {
+      if(d_ufSubstr.isNull()) {
+        std::vector< TypeNode > argTypes;
+        argTypes.push_back(NodeManager::currentNM()->stringType());
+        argTypes.push_back(NodeManager::currentNM()->integerType());
+        argTypes.push_back(NodeManager::currentNM()->integerType());
+        d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
+                    NodeManager::currentNM()->mkFunctionType(
+                               argTypes, NodeManager::currentNM()->stringType()),
+                    "uf substr",
+                    NodeManager::SKOLEM_EXACT_NAME);
+      }
+      Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
+                   NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ), node[1] );
+      Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+      Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, node[1], zero);
+      Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
+      Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+      Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], one);
+      Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], one);
+      return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
+      break;
     }
-    Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
-						     NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ), node[1] );
-    Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
-    Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, node[1], zero);
-    Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
-    Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
-    Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], one);
-    Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], one);
-    return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
-  }
-  break;
-
-  case kind::STRING_SUBSTR: {
-    if(d_ufSubstr.isNull()) {
-      std::vector< TypeNode > argTypes;
-      argTypes.push_back(NodeManager::currentNM()->stringType());
-      argTypes.push_back(NodeManager::currentNM()->integerType());
-      argTypes.push_back(NodeManager::currentNM()->integerType());
-      d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
-						      NodeManager::currentNM()->mkFunctionType(
-											       argTypes, NodeManager::currentNM()->stringType()),
-						      "uf substr",
-						      NodeManager::SKOLEM_EXACT_NAME);
+
+    case kind::STRING_SUBSTR: {
+      if(d_ufSubstr.isNull()) {
+        std::vector< TypeNode > argTypes;
+        argTypes.push_back(NodeManager::currentNM()->stringType());
+        argTypes.push_back(NodeManager::currentNM()->integerType());
+        argTypes.push_back(NodeManager::currentNM()->integerType());
+        d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
+                    NodeManager::currentNM()->mkFunctionType(
+                               argTypes, NodeManager::currentNM()->stringType()),
+                    "uf substr",
+                    NodeManager::SKOLEM_EXACT_NAME);
+      }
+      Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
+                   NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ),
+                   NodeManager::currentNM()->mkNode( kind::PLUS, node[1], node[2] ) );
+      Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+      Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[1], zero);
+      Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[2], zero);
+      Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
+      Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]);
+      Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], node[2]);
+      return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
+      break;
     }
-    Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
-						     NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ),
-						     NodeManager::currentNM()->mkNode( kind::PLUS, node[1], node[2] ) );
-    Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
-    Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[1], zero);
-    Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[2], zero);
-    Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-    Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]);
-    Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], node[2]);
-    return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
-  }
-  break;
 
-  default :
-    return node;
-    break;
+    default :
+      return node;
   }
 
   Unreachable();
@@ -543,7 +542,7 @@ void TheoryStrings::check(Effort e) {
   }*/
 
   if( !done() && !hasTerm( d_emptyString ) ) {
-	 preRegisterTerm( d_emptyString );
+	  preRegisterTerm( d_emptyString );
   }
 
  // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
@@ -635,9 +634,9 @@ void TheoryStrings::conflict(TNode a, TNode b){
 	  d_conflict = true;
 	  Node conflictNode;
 	  if (a.getKind() == kind::CONST_BOOLEAN) {
-		conflictNode = explain( a.iffNode(b) );
+		  conflictNode = explain( a.iffNode(b) );
 	  } else {
-		conflictNode = explain( a.eqNode(b) );
+		  conflictNode = explain( a.eqNode(b) );
 	  }
 	  Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
 	  d_out->conflict( conflictNode );
@@ -662,48 +661,48 @@ void TheoryStrings::eqNotifyNewClass(TNode t){
 void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){
     EqcInfo * e2 = getOrMakeEqcInfo(t2, false);
     if( e2 ){
-        EqcInfo * e1 = getOrMakeEqcInfo( t1 );
-        //add information from e2 to e1
-        if( !e2->d_const_term.get().isNull() ){
-            e1->d_const_term.set( e2->d_const_term );
-        }
-        if( !e2->d_length_term.get().isNull() ){
-            e1->d_length_term.set( e2->d_length_term );
-        }
-        if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) {
-            e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k );
-        }
-		if( !e2->d_normalized_length.get().isNull() ){
-			e1->d_normalized_length.set( e2->d_normalized_length );
-		}
+      EqcInfo * e1 = getOrMakeEqcInfo( t1 );
+      //add information from e2 to e1
+      if( !e2->d_const_term.get().isNull() ){
+        e1->d_const_term.set( e2->d_const_term );
+      }
+      if( !e2->d_length_term.get().isNull() ){
+        e1->d_length_term.set( e2->d_length_term );
+      }
+      if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) {
+        e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k );
+      }
+      if( !e2->d_normalized_length.get().isNull() ){
+        e1->d_normalized_length.set( e2->d_normalized_length );
+      }
     }
     if( hasTerm( d_zero ) ){
-        Node leqc;
-        if( areEqual(d_zero, t1) ){
-            leqc = t2;
-        }else if( areEqual(d_zero, t2) ){
-            leqc = t1;
-        }
-        if( !leqc.isNull() ){
-            //scan equivalence class to see if we apply
-            eq::EqClassIterator eqc_i = eq::EqClassIterator( leqc, &d_equalityEngine );
-            while( !eqc_i.isFinished() ){
-              Node n = (*eqc_i);
-              if( n.getKind()==kind::STRING_LENGTH ){
-                if( !hasTerm( d_emptyString ) || !areEqual(n[0], d_emptyString ) ){
-                    //apply the rule length(n[0])==0 => n[0] == ""
-                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n[0], d_emptyString );
-                    d_pending.push_back( eq );
-                    Node eq_exp = NodeManager::currentNM()->mkNode( kind::EQUAL, n, d_zero );
-                    d_pending_exp[eq] = eq_exp;
-                    Trace("strings-infer") << "Strings : Infer Empty : " << eq << " from " << eq_exp << std::endl;
-                    d_infer.push_back(eq);
-                    d_infer_exp.push_back(eq_exp);
-                }
-              }
-              ++eqc_i;
+      Node leqc;
+      if( areEqual(d_zero, t1) ){
+        leqc = t2;
+      }else if( areEqual(d_zero, t2) ){
+        leqc = t1;
+      }
+      if( !leqc.isNull() ){
+        //scan equivalence class to see if we apply
+        eq::EqClassIterator eqc_i = eq::EqClassIterator( leqc, &d_equalityEngine );
+        while( !eqc_i.isFinished() ){
+          Node n = (*eqc_i);
+          if( n.getKind()==kind::STRING_LENGTH ){
+            if( !hasTerm( d_emptyString ) || !areEqual(n[0], d_emptyString ) ){
+              //apply the rule length(n[0])==0 => n[0] == ""
+              Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n[0], d_emptyString );
+              d_pending.push_back( eq );
+              Node eq_exp = NodeManager::currentNM()->mkNode( kind::EQUAL, n, d_zero );
+              d_pending_exp[eq] = eq_exp;
+              Trace("strings-infer") << "Strings : Infer Empty : " << eq << " from " << eq_exp << std::endl;
+              d_infer.push_back(eq);
+              d_infer_exp.push_back(eq_exp);
             }
+          }
+          ++eqc_i;
         }
+      }
     }
 }
 
@@ -726,21 +725,21 @@ void TheoryStrings::doPendingFacts() {
   while( !d_conflict && i<(int)d_pending.size() ){
     Node fact = d_pending[i];
     Node exp = d_pending_exp[ fact ];
-      Trace("strings-pending") << "Process pending fact : " << fact << " from " << exp << std::endl;
-      bool polarity = fact.getKind() != kind::NOT;
-      TNode atom = polarity ? fact : fact[0];
-      if (atom.getKind() == kind::EQUAL) {
-		//Assert( d_equalityEngine.hasTerm( atom[0] ) );
-		//Assert( d_equalityEngine.hasTerm( atom[1] ) );
-		for( unsigned j=0; j<2; j++ ){
-			if( !d_equalityEngine.hasTerm( atom[j] ) ){
-				d_equalityEngine.addTerm( atom[j] );
-			}
-		}
-		d_equalityEngine.assertEquality( atom, polarity, exp );
-      }else{
-        d_equalityEngine.assertPredicate( atom, polarity, exp );
+    Trace("strings-pending") << "Process pending fact : " << fact << " from " << exp << std::endl;
+    bool polarity = fact.getKind() != kind::NOT;
+    TNode atom = polarity ? fact : fact[0];
+    if (atom.getKind() == kind::EQUAL) {
+      //Assert( d_equalityEngine.hasTerm( atom[0] ) );
+      //Assert( d_equalityEngine.hasTerm( atom[1] ) );
+      for( unsigned j=0; j<2; j++ ){
+        if( !d_equalityEngine.hasTerm( atom[j] ) ){
+          d_equalityEngine.addTerm( atom[j] );
+        }
       }
+      d_equalityEngine.assertEquality( atom, polarity, exp );
+    }else{
+      d_equalityEngine.assertPredicate( atom, polarity, exp );
+    }
     i++;
   }
   d_pending.clear();
@@ -753,8 +752,8 @@ void TheoryStrings::doPendingLemmas() {
 		  d_out->lemma( d_lemma_cache[i] );
 	  }
 	  for( std::map< Node, bool >::iterator it = d_pending_req_phase.begin(); it != d_pending_req_phase.end(); ++it ){
-		Trace("strings-pending") << "Require phase : " << it->first << ", polarity = " << it->second << std::endl;
-		d_out->requirePhase( it->first, it->second );
+      Trace("strings-pending") << "Require phase : " << it->first << ", polarity = " << it->second << std::endl;
+      d_out->requirePhase( it->first, it->second );
 	  }
   }
   d_lemma_cache.clear();
@@ -762,7 +761,7 @@ void TheoryStrings::doPendingLemmas() {
 }
 
 bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
-    std::vector< std::vector< Node > > &normal_forms,  std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) {
+  std::vector< std::vector< Node > > &normal_forms,  std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) {
 	Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
 	// EqcItr
 	eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
@@ -883,37 +882,37 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
 		++eqc_i;
 	}
 
-    // Test the result
-    if( !normal_forms.empty() ) {
-        Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl;
-        for( unsigned i=0; i<normal_forms.size(); i++ ) {
-            Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : ";
-			//mergeCstVec(normal_forms[i]);
-            for( unsigned j=0; j<normal_forms[i].size(); j++ ) {
-                if(j>0) Trace("strings-solve") << ", ";
-                Trace("strings-solve") << normal_forms[i][j];
-            }
-            Trace("strings-solve") << std::endl;
-            Trace("strings-solve") << "   Explanation is : ";
-            if(normal_forms_exp[i].size() == 0) {
-                Trace("strings-solve") << "NONE";
-            } else {
-                for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) {
-                    if(j>0) Trace("strings-solve") << " AND ";
-                    Trace("strings-solve") << normal_forms_exp[i][j];
-                }
-            }
-            Trace("strings-solve") << std::endl;
+  // Test the result
+  if( !normal_forms.empty() ) {
+    Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl;
+    for( unsigned i=0; i<normal_forms.size(); i++ ) {
+      Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : ";
+      //mergeCstVec(normal_forms[i]);
+      for( unsigned j=0; j<normal_forms[i].size(); j++ ) {
+        if(j>0) Trace("strings-solve") << ", ";
+        Trace("strings-solve") << normal_forms[i][j];
+      }
+      Trace("strings-solve") << std::endl;
+      Trace("strings-solve") << "   Explanation is : ";
+      if(normal_forms_exp[i].size() == 0) {
+        Trace("strings-solve") << "NONE";
+      } else {
+        for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) {
+          if(j>0) Trace("strings-solve") << " AND ";
+          Trace("strings-solve") << normal_forms_exp[i][j];
         }
-    }else{
-      //std::vector< Node > nf;
-      //nf.push_back( eqc );
-      //normal_forms.push_back(nf);
-      //std::vector< Node > nf_exp_def;
-      //normal_forms_exp.push_back(nf_exp_def);
-      //normal_form_src.push_back(eqc);
-      Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl;
+      }
+      Trace("strings-solve") << std::endl;
     }
+  } else {
+    //std::vector< Node > nf;
+    //nf.push_back( eqc );
+    //normal_forms.push_back(nf);
+    //std::vector< Node > nf_exp_def;
+    //normal_forms_exp.push_back(nf_exp_def);
+    //normal_form_src.push_back(eqc);
+    Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl;
+  }
 	return true;
 }
 
@@ -939,8 +938,8 @@ void TheoryStrings::mergeCstVec(std::vector< Node > &vec_strings) {
 }
 
 bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms,
-								int i, int j, int index_i, int index_j,
-								int &loop_in_i, int &loop_in_j) {
+  int i, int j, int index_i, int index_j,
+  int &loop_in_i, int &loop_in_j) {
 	int has_loop[2] = { -1, -1 };
 	if( options::stringLB() != 2 ) {
 		for( unsigned r=0; r<2; r++ ) {
@@ -968,10 +967,10 @@ bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms
 }
 //xs(zy)=t(yz)xr
 bool TheoryStrings::processLoop(std::vector< Node > &antec,
-								std::vector< std::vector< Node > > &normal_forms,
-								std::vector< Node > &normal_form_src,
-								int i, int j, int loop_n_index, int other_n_index,
-								int loop_index, int index, int other_index) {
+  std::vector< std::vector< Node > > &normal_forms,
+  std::vector< Node > &normal_form_src,
+  int i, int j, int loop_n_index, int other_n_index,
+  int loop_index, int index, int other_index) {
 	Node conc;
 	Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index] << std::endl;
 	Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl;
@@ -1135,8 +1134,8 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
 	return true;
 }
 bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms,
-								std::vector< std::vector< Node > > &normal_forms_exp,
-								std::vector< Node > &normal_form_src) {
+  std::vector< std::vector< Node > > &normal_forms_exp,
+  std::vector< Node > &normal_form_src) {
 	bool flag_lb = false;
 	std::vector< Node > c_lb_exp;
 	int c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index;
@@ -1316,7 +1315,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
 }
 
 bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &normal_forms,
-									   std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j ) {
+  std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j ) {
 	//reverse normal form of i, j
 	std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
 	std::reverse( normal_forms[j].begin(), normal_forms[j].end() );
@@ -1335,8 +1334,8 @@ bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &norma
 }
 
 bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal_forms,
-									  std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp,
-									  unsigned i, unsigned j, unsigned& index_i, unsigned& index_j, bool isRev ) {
+  std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp,
+  unsigned i, unsigned j, unsigned& index_i, unsigned& index_j, bool isRev ) {
 	bool success;
 	do {
 		success = false;
@@ -1463,79 +1462,79 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
 
 //nf_exp is conjunction
 bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) {
-    Trace("strings-process") << "Process equivalence class " << eqc << std::endl;
-    if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){
-		getConcatVec( eqc, nf );
-        Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
-		return false;
-    } else if( areEqual( eqc, d_emptyString ) ) {
-		eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-		while( !eqc_i.isFinished() ) {
-			Node n = (*eqc_i);
-			if( n.getKind()==kind::STRING_CONCAT ){
-				for( unsigned i=0; i<n.getNumChildren(); i++ ){
-					if( !areEqual( n[i], d_emptyString ) ){
-						sendLemma( n.eqNode( d_emptyString ), n[i].eqNode( d_emptyString ), "CYCLE" );
-					}
-				}
-			}
-			++eqc_i;
-		}
-        //do nothing
-        Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl;
-		d_normal_forms_base[eqc] = d_emptyString;
-		d_normal_forms[eqc].clear();
-		d_normal_forms_exp[eqc].clear();
-		return true;
-    } else {
-        visited.push_back( eqc );
-		bool result;
-        if(d_normal_forms.find(eqc)==d_normal_forms.end() ) {
-            //phi => t = s1 * ... * sn
-            // normal form for each non-variable term in this eqc (s1...sn)
-            std::vector< std::vector< Node > > normal_forms;
-            // explanation for each normal form (phi)
-            std::vector< std::vector< Node > > normal_forms_exp;
-            // record terms for each normal form (t)
-            std::vector< Node > normal_form_src;
-            //Get Normal Forms
-            result = getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src);
-            if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
-                return true;
-            } else if( result ) {
-				if(processNEqc(normal_forms, normal_forms_exp, normal_form_src)) {
-					return true;
-				}
-			}
-
-            //construct the normal form
-            if( normal_forms.empty() ){
-                Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
-				getConcatVec( eqc, nf );
-            } else {
-                Trace("strings-solve-debug2") << "just take the first normal form" << std::endl;
-                //just take the first normal form
-                nf.insert( nf.end(), normal_forms[0].begin(), normal_forms[0].end() );
-                nf_exp.insert( nf_exp.end(), normal_forms_exp[0].begin(), normal_forms_exp[0].end() );
-                if( eqc!=normal_form_src[0] ){
-                    nf_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, normal_form_src[0] ) );
-                }
-                Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl;
-            }
+  Trace("strings-process") << "Process equivalence class " << eqc << std::endl;
+  if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){
+    getConcatVec( eqc, nf );
+    Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
+    return false;
+  } else if( areEqual( eqc, d_emptyString ) ) {
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+    while( !eqc_i.isFinished() ) {
+      Node n = (*eqc_i);
+      if( n.getKind()==kind::STRING_CONCAT ){
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          if( !areEqual( n[i], d_emptyString ) ){
+            sendLemma( n.eqNode( d_emptyString ), n[i].eqNode( d_emptyString ), "CYCLE" );
+          }
+        }
+      }
+      ++eqc_i;
+    }
+    //do nothing
+    Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl;
+    d_normal_forms_base[eqc] = d_emptyString;
+    d_normal_forms[eqc].clear();
+    d_normal_forms_exp[eqc].clear();
+    return true;
+  } else {
+    visited.push_back( eqc );
+    bool result;
+    if(d_normal_forms.find(eqc)==d_normal_forms.end() ) {
+      //phi => t = s1 * ... * sn
+      // normal form for each non-variable term in this eqc (s1...sn)
+      std::vector< std::vector< Node > > normal_forms;
+      // explanation for each normal form (phi)
+      std::vector< std::vector< Node > > normal_forms_exp;
+      // record terms for each normal form (t)
+      std::vector< Node > normal_form_src;
+      //Get Normal Forms
+      result = getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src);
+      if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
+          return true;
+      } else if( result ) {
+        if(processNEqc(normal_forms, normal_forms_exp, normal_form_src)) {
+          return true;
+        }
+      }
 
-    	    d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0];
-            d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() );
-            d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() );
-            Trace("strings-process") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl;
-        }else{
-            Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl;
-            nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() );
-            nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() );
-			result = true;
+      //construct the normal form
+      if( normal_forms.empty() ){
+        Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
+        getConcatVec( eqc, nf );
+      } else {
+        Trace("strings-solve-debug2") << "just take the first normal form" << std::endl;
+        //just take the first normal form
+        nf.insert( nf.end(), normal_forms[0].begin(), normal_forms[0].end() );
+        nf_exp.insert( nf_exp.end(), normal_forms_exp[0].begin(), normal_forms_exp[0].end() );
+        if( eqc!=normal_form_src[0] ){
+          nf_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, normal_form_src[0] ) );
         }
-        visited.pop_back();
-		return result;
+        Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl;
+      }
+
+      d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0];
+      d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() );
+      d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() );
+      Trace("strings-process") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl;
+    } else {
+      Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl;
+      nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() );
+      nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() );
+      result = true;
     }
+    visited.pop_back();
+    return result;
+  }
 }
 
 //return true for lemma, false if we succeed
@@ -1560,9 +1559,9 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
 		unsigned index = 0;
 		while( index<nfi.size() || index<nfj.size() ){
 			int ret = processSimpleDeq( nfi, nfj, ni, nj, index, false );
-			if( ret!=0 ){
+			if( ret!=0 ) {
 				return ret==-1;
-			}else{
+			} else {
 				Assert( index<nfi.size() && index<nfj.size() );
 				Node i = nfi[index];
 				Node j = nfj[index];
@@ -1649,8 +1648,8 @@ int TheoryStrings::processReverseDeq( std::vector< Node >& nfi, std::vector< Nod
 }
 
 int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ) {
-	while( index<nfi.size() || index<nfj.size() ){
-		if( index>=nfi.size() || index>=nfj.size() ){
+	while( index<nfi.size() || index<nfj.size() ) {
+		if( index>=nfi.size() || index>=nfj.size() ) {
 			std::vector< Node > ant;
 			//we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
 			Node lni = getLength( ni );
@@ -1708,7 +1707,7 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
 						Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i << " " << j << std::endl;
 						//we are done: D-Remove
 						return 1;
-					}else{
+					} else {
 						return 0;
 					}
 				}
@@ -1722,54 +1721,53 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
 void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) {
   if( !isNormalFormPair( n1, n2 ) ){
 		//Assert( !isNormalFormPair( n1, n2 ) );
-        NodeList* lst;
-        NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
-        if( nf_i == d_nf_pairs.end() ){
-          if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){
-            addNormalFormPair( n2, n1 );
-            return;
-          }
-          lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
-                                                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
-          d_nf_pairs.insertDataFromContextMemory( n1, lst );
-		  Trace("strings-nf") << "Create cache for " << n1 << std::endl;
-        }else{
-          lst = (*nf_i).second;
-        }
+    NodeList* lst;
+    NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
+    if( nf_i == d_nf_pairs.end() ){
+      if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){
+        addNormalFormPair( n2, n1 );
+        return;
+      }
+      lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
+                                                           ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
+      d_nf_pairs.insertDataFromContextMemory( n1, lst );
+      Trace("strings-nf") << "Create cache for " << n1 << std::endl;
+    } else {
+      lst = (*nf_i).second;
+    }
 		Trace("strings-nf") << "Add normal form pair : " << n1 << " " << n2 << std::endl;
-        lst->push_back( n2 );
+    lst->push_back( n2 );
 		Assert( isNormalFormPair( n1, n2 ) );
-    }else{
+  } else {
 		Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl;
 	}
-
 }
 bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) {
-    //TODO: modulo equality?
-    return isNormalFormPair2( n1, n2 ) || isNormalFormPair2( n2, n1 );
+  //TODO: modulo equality?
+  return isNormalFormPair2( n1, n2 ) || isNormalFormPair2( n2, n1 );
 }
 bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
     //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
   NodeList* lst;
   NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
-  if( nf_i != d_nf_pairs.end() ){
+  if( nf_i != d_nf_pairs.end() ) {
     lst = (*nf_i).second;
     for( NodeList::const_iterator i = lst->begin(); i != lst->end(); ++i ) {
-        Node n = *i;
-        if( n==n2 ){
-            return true;
-        }
+      Node n = *i;
+      if( n==n2 ) {
+          return true;
+      }
     }
   }
   return false;
 }
 
 void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
-	if( conc.isNull() || conc == d_false ){
+	if( conc.isNull() || conc == d_false ) {
 		d_out->conflict(ant);
 		Trace("strings-conflict") << "Strings::Conflict : " << ant << std::endl;
 		d_conflict = true;
-	}else{
+	} else {
 		Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
 		if( ant == d_true ) {
 			lem = conc;
@@ -1781,9 +1779,9 @@ void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
 
 void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) {
 	eq = Rewriter::rewrite( eq );
-	if( eq==d_false ){
+	if( eq==d_false ) {
 		sendLemma( eq_exp, eq, c );
-	}else{
+	} else {
 		Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
 		d_pending.push_back( eq );
 		d_pending_exp[eq] = eq_exp;
@@ -1804,11 +1802,11 @@ void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) {
 }
 
 Node TheoryStrings::mkConcat( Node n1, Node n2 ) {
-	return NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 );
+	return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 ) );
 }
 
 Node TheoryStrings::mkConcat( std::vector< Node >& c ) {
-    Node cc = c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString );
+  Node cc = c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString );
 	return Rewriter::rewrite( cc );
 }
 
@@ -1818,51 +1816,51 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a ) {
 }
 
 Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) {
-    std::vector< TNode > antec_exp;
-    for( unsigned i=0; i<a.size(); i++ ){
-		if( std::find( a.begin(), a.begin() + i, a[i] )==a.begin() + i ){
-			bool exp = true;
-			Trace("strings-solve-debug") << "Ask for explanation of " << a[i] << std::endl;
-			//assert
-			if(a[i].getKind() == kind::EQUAL) {
-				//assert( hasTerm(a[i][0]) );
-				//assert( hasTerm(a[i][1]) );
-				Assert( areEqual(a[i][0], a[i][1]) );
-				if( a[i][0]==a[i][1] ){
-					exp = false;
-				}
-			} else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ){
-				Assert( hasTerm(a[i][0][0]) );
-				Assert( hasTerm(a[i][0][1]) );
-				AlwaysAssert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
-			}
-			if( exp ){
-				unsigned ps = antec_exp.size();
-				explain(a[i], antec_exp);
-				Trace("strings-solve-debug") << "Done, explanation was : " << std::endl;
-				for( unsigned j=ps; j<antec_exp.size(); j++ ){
-					Trace("strings-solve-debug") << "  " << antec_exp[j] << std::endl;
-				}
-				Trace("strings-solve-debug") << std::endl;
-			}
-		}
-    }
-    for( unsigned i=0; i<an.size(); i++ ){
-		if( std::find( an.begin(), an.begin() + i, an[i] )==an.begin() + i ){
-			Trace("strings-solve-debug") << "Add to explanation (new literal) " << an[i] << std::endl;
-			antec_exp.push_back(an[i]);
-		}
+  std::vector< TNode > antec_exp;
+  for( unsigned i=0; i<a.size(); i++ ) {
+    if( std::find( a.begin(), a.begin() + i, a[i] )==a.begin() + i ) {
+      bool exp = true;
+      Trace("strings-solve-debug") << "Ask for explanation of " << a[i] << std::endl;
+      //assert
+      if(a[i].getKind() == kind::EQUAL) {
+        //assert( hasTerm(a[i][0]) );
+        //assert( hasTerm(a[i][1]) );
+        Assert( areEqual(a[i][0], a[i][1]) );
+        if( a[i][0]==a[i][1] ){
+          exp = false;
+        }
+      } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ) {
+        Assert( hasTerm(a[i][0][0]) );
+        Assert( hasTerm(a[i][0][1]) );
+        AlwaysAssert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
+      }
+      if( exp ) {
+        unsigned ps = antec_exp.size();
+        explain(a[i], antec_exp);
+        Trace("strings-solve-debug") << "Done, explanation was : " << std::endl;
+        for( unsigned j=ps; j<antec_exp.size(); j++ ) {
+          Trace("strings-solve-debug") << "  " << antec_exp[j] << std::endl;
+        }
+        Trace("strings-solve-debug") << std::endl;
+      }
     }
-    Node ant;
-    if( antec_exp.empty() ) {
-        ant = d_true;
-    } else if( antec_exp.size()==1 ) {
-        ant = antec_exp[0];
-    } else {
-        ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
+  }
+  for( unsigned i=0; i<an.size(); i++ ) {
+    if( std::find( an.begin(), an.begin() + i, an[i] )==an.begin() + i ){
+      Trace("strings-solve-debug") << "Add to explanation (new literal) " << an[i] << std::endl;
+      antec_exp.push_back(an[i]);
     }
+  }
+  Node ant;
+  if( antec_exp.empty() ) {
+    ant = d_true;
+  } else if( antec_exp.size()==1 ) {
+    ant = antec_exp[0];
+  } else {
+    ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
+  }
 	ant = Rewriter::rewrite( ant );
-    return ant;
+  return ant;
 }
 
 Node TheoryStrings::mkAnd( std::vector< Node >& a ) {
@@ -1876,13 +1874,13 @@ Node TheoryStrings::mkAnd( std::vector< Node >& a ) {
 }
 
 void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) {
-	if( n.getKind()==kind::STRING_CONCAT ){
-		for( unsigned i=0; i<n.getNumChildren(); i++ ){
-			if( !areEqual( n[i], d_emptyString ) ){
+	if( n.getKind()==kind::STRING_CONCAT ) {
+		for( unsigned i=0; i<n.getNumChildren(); i++ ) {
+			if( !areEqual( n[i], d_emptyString ) ) {
 				c.push_back( n[i] );
 			}
 		}
-	}else{
+	} else {
 		c.push_back( n );
 	}
 }
@@ -1892,91 +1890,91 @@ bool TheoryStrings::checkSimple() {
 
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ) {
-	Node eqc = (*eqcs_i);
-	//if eqc.getType is string
-	if (eqc.getType().isString()) {
-		//EqcInfo* ei = getOrMakeEqcInfo( eqc, true );
-		//get the constant for the equivalence class
-		//int c_len = ...;
-		eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-		while( !eqc_i.isFinished() ){
-			Node n = (*eqc_i);
-			//if n is concat, and
-			//if n has not instantiatied the concat..length axiom
-			//then, add lemma
-			if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
-				if( d_length_nodes.find(n)==d_length_nodes.end() ) {
-					Trace("strings-debug") << "get n: " << n << endl;
-					Node sk;
-					//if( d_length_inst.find(n)==d_length_inst.end() ) {
-						//Node nr = d_equalityEngine.getRepresentative( n );
-						sk = NodeManager::currentNM()->mkSkolem( "lsym", n.getType(), "created for length" );
-						d_statistics.d_new_skolems += 1;
-						d_length_intro_vars.insert( sk );
-						Node eq = sk.eqNode(n);
-						eq = Rewriter::rewrite(eq);
-						Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
-						d_out->lemma(eq);
-					//} else {
-					//	sk = d_length_inst[n];
-					//}
-					Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-					Node lsum;
-					if( n.getKind() == kind::STRING_CONCAT ) {
-						//add lemma
-						std::vector<Node> node_vec;
-						for( unsigned i=0; i<n.getNumChildren(); i++ ) {
-							Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
-							node_vec.push_back(lni);
-						}
-						lsum = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ) );
-					} else if( n.getKind() == kind::CONST_STRING ) {
-						//add lemma
-						lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
-					}
-					Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
-					ceq = Rewriter::rewrite(ceq);
-					Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
-					d_out->lemma(ceq);
-					addedLemma = true;
+    Node eqc = (*eqcs_i);
+    //if eqc.getType is string
+    if (eqc.getType().isString()) {
+      //EqcInfo* ei = getOrMakeEqcInfo( eqc, true );
+      //get the constant for the equivalence class
+      //int c_len = ...;
+      eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+      while( !eqc_i.isFinished() ) {
+        Node n = (*eqc_i);
+        //if n is concat, and
+        //if n has not instantiatied the concat..length axiom
+        //then, add lemma
+        if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
+          if( d_length_nodes.find(n)==d_length_nodes.end() ) {
+            Trace("strings-debug") << "get n: " << n << endl;
+            Node sk;
+            //if( d_length_inst.find(n)==d_length_inst.end() ) {
+              //Node nr = d_equalityEngine.getRepresentative( n );
+              sk = NodeManager::currentNM()->mkSkolem( "lsym", n.getType(), "created for length" );
+              d_statistics.d_new_skolems += 1;
+              d_length_intro_vars.insert( sk );
+              Node eq = sk.eqNode(n);
+              eq = Rewriter::rewrite(eq);
+              Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
+              d_out->lemma(eq);
+            //} else {
+            //	sk = d_length_inst[n];
+            //}
+            Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
+            Node lsum;
+            if( n.getKind() == kind::STRING_CONCAT ) {
+              //add lemma
+              std::vector<Node> node_vec;
+              for( unsigned i=0; i<n.getNumChildren(); i++ ) {
+                Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
+                node_vec.push_back(lni);
+              }
+              lsum = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ) );
+            } else if( n.getKind() == kind::CONST_STRING ) {
+              //add lemma
+              lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
+            }
+            Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
+            ceq = Rewriter::rewrite(ceq);
+            Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
+            d_out->lemma(ceq);
+            addedLemma = true;
 
-					d_length_nodes.insert(n);
-				}
-			}
-			++eqc_i;
-		}
-	}
-	++eqcs_i;
+            d_length_nodes.insert(n);
+          }
+        }
+        ++eqc_i;
+      }
+    }
+    ++eqcs_i;
   }
   return addedLemma;
 }
 
 bool TheoryStrings::checkNormalForms() {
-    Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
+  Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
 	eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
-	for( unsigned t=0; t<2; t++ ){
+	for( unsigned t=0; t<2; t++ ) {
 		Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl;
 		while( !eqcs2_i.isFinished() ){
-		Node eqc = (*eqcs2_i);
-		bool print = (t==0 && eqc.getType().isString() ) || (t==1 && !eqc.getType().isString() );
-		if (print) {
-			eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-			Trace("strings-eqc") << "Eqc( " << eqc << " ) : { ";
-			while( !eqc2_i.isFinished() ) {
-				if( (*eqc2_i)!=eqc ){
-					Trace("strings-eqc") << (*eqc2_i) << " ";
-				}
-				++eqc2_i;
-			}
-			Trace("strings-eqc") << " } " << std::endl;
-			EqcInfo * ei = getOrMakeEqcInfo( eqc, false );
-			if( ei ){
-				Trace("strings-eqc-debug") << "* Length term : " << ei->d_length_term.get() << std::endl;
-				Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei->d_cardinality_lem_k.get() << std::endl;
-				Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei->d_normalized_length.get() << std::endl;
-			}
-		}
-		++eqcs2_i;
+      Node eqc = (*eqcs2_i);
+      bool print = (t==0 && eqc.getType().isString() ) || (t==1 && !eqc.getType().isString() );
+      if (print) {
+        eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+        Trace("strings-eqc") << "Eqc( " << eqc << " ) : { ";
+        while( !eqc2_i.isFinished() ) {
+          if( (*eqc2_i)!=eqc ){
+            Trace("strings-eqc") << (*eqc2_i) << " ";
+          }
+          ++eqc2_i;
+        }
+        Trace("strings-eqc") << " } " << std::endl;
+        EqcInfo * ei = getOrMakeEqcInfo( eqc, false );
+        if( ei ){
+          Trace("strings-eqc-debug") << "* Length term : " << ei->d_length_term.get() << std::endl;
+          Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei->d_cardinality_lem_k.get() << std::endl;
+          Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei->d_normalized_length.get() << std::endl;
+        }
+      }
+      ++eqcs2_i;
 		}
 		Trace("strings-eqc") << std::endl;
 	}
@@ -2012,56 +2010,56 @@ bool TheoryStrings::checkNormalForms() {
 
   bool addedFact;
   do {
-	Trace("strings-process") << "Check Normal Forms........next round" << std::endl;
+    Trace("strings-process") << "Check Normal Forms........next round" << std::endl;
     //calculate normal forms for each equivalence class, possibly adding splitting lemmas
     d_normal_forms.clear();
     d_normal_forms_exp.clear();
     std::map< Node, Node > nf_to_eqc;
     std::map< Node, Node > eqc_to_exp;
     d_lemma_cache.clear();
-	d_pending_req_phase.clear();
-	//get equivalence classes
-	std::vector< Node > eqcs;
-	getEquivalenceClasses( eqcs );
-	for( unsigned i=0; i<eqcs.size(); i++ ){
-		Node eqc = eqcs[i];
-		Trace("strings-process") << "- Verify normal forms are the same for " << eqc << std::endl;
-		std::vector< Node > visited;
-		std::vector< Node > nf;
-		std::vector< Node > nf_exp;
-		normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
-		Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
-		if( d_conflict ){
-			doPendingFacts();
-			doPendingLemmas();
-			return true;
-		}else if ( d_pending.empty() && d_lemma_cache.empty() ){
-			Node nf_term;
-			if( nf.size()==0 ){
-				nf_term = d_emptyString;
-			}else if( nf.size()==1 ) {
-				nf_term = nf[0];
-			} else {
-				nf_term = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, nf );
-			}
-			nf_term = Rewriter::rewrite( nf_term );
-			Trace("strings-debug") << "Make nf_term_exp..." << std::endl;
-			Node nf_term_exp = nf_exp.empty() ? d_true :
-								nf_exp.size()==1 ? nf_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, nf_exp );
-			if( nf_to_eqc.find(nf_term)!=nf_to_eqc.end() ){
-				//Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
-				//two equivalence classes have same normal form, merge
-				Node eq_exp = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ) );
-				Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] );
-				sendInfer( eq_exp, eq, "Normal_Form" );
-				//d_equalityEngine.assertEquality( eq, true, eq_exp );
-			}else{
-				nf_to_eqc[nf_term] = eqc;
-				eqc_to_exp[eqc] = nf_term_exp;
-			}
-		}
-		Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl;
-	}
+    d_pending_req_phase.clear();
+    //get equivalence classes
+    std::vector< Node > eqcs;
+    getEquivalenceClasses( eqcs );
+    for( unsigned i=0; i<eqcs.size(); i++ ){
+      Node eqc = eqcs[i];
+      Trace("strings-process") << "- Verify normal forms are the same for " << eqc << std::endl;
+      std::vector< Node > visited;
+      std::vector< Node > nf;
+      std::vector< Node > nf_exp;
+      normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
+      Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
+      if( d_conflict ) {
+        doPendingFacts();
+        doPendingLemmas();
+        return true;
+      } else if ( d_pending.empty() && d_lemma_cache.empty() ) {
+        Node nf_term;
+        if( nf.size()==0 ){
+          nf_term = d_emptyString;
+        }else if( nf.size()==1 ) {
+          nf_term = nf[0];
+        } else {
+          nf_term = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, nf );
+        }
+        nf_term = Rewriter::rewrite( nf_term );
+        Trace("strings-debug") << "Make nf_term_exp..." << std::endl;
+        Node nf_term_exp = nf_exp.empty() ? d_true :
+                  nf_exp.size()==1 ? nf_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, nf_exp );
+        if( nf_to_eqc.find(nf_term)!=nf_to_eqc.end() ) {
+          //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
+          //two equivalence classes have same normal form, merge
+          Node eq_exp = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ) );
+          Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] );
+          sendInfer( eq_exp, eq, "Normal_Form" );
+          //d_equalityEngine.assertEquality( eq, true, eq_exp );
+        } else {
+          nf_to_eqc[nf_term] = eqc;
+          eqc_to_exp[eqc] = nf_term_exp;
+        }
+      }
+      Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl;
+    }
 
 	  Trace("strings-nf-debug") << "**** Normal forms are : " << std::endl;
 	  for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){
@@ -2078,10 +2076,10 @@ bool TheoryStrings::checkNormalForms() {
   Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache.size() << ", conflict = " << d_conflict << std::endl;
   //flush pending lemmas
   if( !d_lemma_cache.empty() ){
-	doPendingLemmas();
-	return true;
+    doPendingLemmas();
+    return true;
   }else{
-	return false;
+    return false;
   }
 }
 
@@ -2148,7 +2146,7 @@ bool TheoryStrings::checkLengthsEqc() {
 					addedLemma = true;
 				}
 			}
-		}else{
+		} else {
 			Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
 		}
 	}
@@ -2169,111 +2167,111 @@ bool TheoryStrings::checkCardinality() {
   std::vector< Node > lts;
   separateByLength( eqcs, cols, lts );
 
-  for( unsigned i = 0; i<cols.size(); ++i ){
+  for( unsigned i = 0; i<cols.size(); ++i ) {
     Node lr = lts[i];
     Trace("strings-card") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl;
     if( cols[i].size() > 1 ) {
-		// size > c^k
-		double k = 1.0 + std::log((double) cols[i].size() - 1) / log((double) cardinality);
-		unsigned int int_k = (unsigned int) k;
-		//double c_k = pow ( (double)cardinality, (double)lr );
-
-        bool allDisequal = true;
-        for( std::vector< Node >::iterator itr1 = cols[i].begin();
-              itr1 != cols[i].end(); ++itr1) {
-            for( std::vector< Node >::iterator itr2 = itr1 + 1;
-                  itr2 != cols[i].end(); ++itr2) {
-				if(!areDisequal( *itr1, *itr2 )) {
-                    allDisequal = false;
-                    // add split lemma
-					sendSplit( *itr1, *itr2, "CARD-SP" );
-					doPendingLemmas();
-					return true;
-                }
-            }
+      // size > c^k
+      double k = 1.0 + std::log((double) cols[i].size() - 1) / log((double) cardinality);
+      unsigned int int_k = (unsigned int) k;
+      //double c_k = pow ( (double)cardinality, (double)lr );
+
+      bool allDisequal = true;
+      for( std::vector< Node >::iterator itr1 = cols[i].begin();
+           itr1 != cols[i].end(); ++itr1) {
+        for( std::vector< Node >::iterator itr2 = itr1 + 1;
+          itr2 != cols[i].end(); ++itr2) {
+          if(!areDisequal( *itr1, *itr2 )) {
+            allDisequal = false;
+            // add split lemma
+            sendSplit( *itr1, *itr2, "CARD-SP" );
+            doPendingLemmas();
+            return true;
+          }
         }
-        if(allDisequal) {
-            EqcInfo* ei = getOrMakeEqcInfo( lr, true );
-            Trace("strings-card") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl;
-            if( int_k+1 > ei->d_cardinality_lem_k.get() ){
-				Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) );
-				//add cardinality lemma
-                Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] );
-                std::vector< Node > vec_node;
-                vec_node.push_back( dist );
-                for( std::vector< Node >::iterator itr1 = cols[i].begin();
-                      itr1 != cols[i].end(); ++itr1) {
-                    Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 );
-                    if( len!=lr ){
-                      Node len_eq_lr = len.eqNode(lr);
-                      vec_node.push_back( len_eq_lr );
-                    }
-                }
-                Node antc = NodeManager::currentNM()->mkNode( kind::AND, vec_node );
-                Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] );
-                Node cons = NodeManager::currentNM()->mkNode( kind::GEQ, len, k_node );
-				/*
-				sendLemma( antc, cons, "Cardinality" );
-				ei->d_cardinality_lem_k.set( int_k+1 );
-				if( !d_lemma_cache.empty() ){
-					doPendingLemmas();
-					return true;
-				}
-				*/
-                Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, antc, cons );
-				lemma = Rewriter::rewrite( lemma );
-				ei->d_cardinality_lem_k.set( int_k+1 );
-				if( lemma!=d_true ){
-					Trace("strings-lemma") << "Strings::Lemma CARDINALITY : " << lemma << std::endl;
-					d_out->lemma(lemma);
-					return true;
-				}
+      }
+      if(allDisequal) {
+        EqcInfo* ei = getOrMakeEqcInfo( lr, true );
+        Trace("strings-card") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl;
+        if( int_k+1 > ei->d_cardinality_lem_k.get() ){
+          Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) );
+          //add cardinality lemma
+          Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] );
+          std::vector< Node > vec_node;
+          vec_node.push_back( dist );
+          for( std::vector< Node >::iterator itr1 = cols[i].begin();
+               itr1 != cols[i].end(); ++itr1) {
+            Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 );
+            if( len!=lr ) {
+              Node len_eq_lr = len.eqNode(lr);
+              vec_node.push_back( len_eq_lr );
             }
+          }
+          Node antc = NodeManager::currentNM()->mkNode( kind::AND, vec_node );
+          Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] );
+          Node cons = NodeManager::currentNM()->mkNode( kind::GEQ, len, k_node );
+          /*
+          sendLemma( antc, cons, "Cardinality" );
+          ei->d_cardinality_lem_k.set( int_k+1 );
+          if( !d_lemma_cache.empty() ){
+            doPendingLemmas();
+            return true;
+          }
+          */
+          Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, antc, cons );
+          lemma = Rewriter::rewrite( lemma );
+          ei->d_cardinality_lem_k.set( int_k+1 );
+          if( lemma!=d_true ){
+            Trace("strings-lemma") << "Strings::Lemma CARDINALITY : " << lemma << std::endl;
+            d_out->lemma(lemma);
+            return true;
+          }
         }
+      }
     }
   }
   return false;
 }
 
 void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) {
-    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-    while( !eqcs_i.isFinished() ) {
-        Node eqc = (*eqcs_i);
-        //if eqc.getType is string
-        if (eqc.getType().isString()) {
-			eqcs.push_back( eqc );
-        }
-        ++eqcs_i;
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+  while( !eqcs_i.isFinished() ) {
+    Node eqc = (*eqcs_i);
+    //if eqc.getType is string
+    if (eqc.getType().isString()) {
+      eqcs.push_back( eqc );
     }
+    ++eqcs_i;
+  }
 }
 
 void TheoryStrings::getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp ) {
-	if( n!=d_emptyString ){
-		if( n.getKind()==kind::STRING_CONCAT ){
-			for( unsigned i=0; i<n.getNumChildren(); i++ ){
+	if( n!=d_emptyString ) {
+		if( n.getKind()==kind::STRING_CONCAT ) {
+			for( unsigned i=0; i<n.getNumChildren(); i++ ) {
 				getFinalNormalForm( n[i], nf, exp );
 			}
-		}else{
+		} else {
 			Trace("strings-debug") << "Get final normal form " << n << std::endl;
 			Assert( d_equalityEngine.hasTerm( n ) );
 			Node nr = d_equalityEngine.getRepresentative( n );
 			EqcInfo *eqc_n = getOrMakeEqcInfo( nr, false );
 			Node nc = eqc_n ? eqc_n->d_const_term.get() : Node::null();
-			if( !nc.isNull() ){
+			if( !nc.isNull() ) {
 				nf.push_back( nc );
-				if( n!=nc ){
+				if( n!=nc ) {
 					exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n, nc ) );
 				}
-			}else{
+			} else {
 				Assert( d_normal_forms.find( nr )!=d_normal_forms.end() );
-				if( d_normal_forms[nr][0]==nr ){
+				if( d_normal_forms[nr][0]==nr ) {
 					Assert( d_normal_forms[nr].size()==1 );
 					nf.push_back( nr );
-					if( n!=nr ){
+					if( n!=nr ) {
 						exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr ) );
 					}
-				}else{
-					for( unsigned i=0; i<d_normal_forms[nr].size(); i++ ){
+				} else {
+					for( unsigned i=0; i<d_normal_forms[nr].size(); i++ ) {
 						Assert( d_normal_forms[nr][i]!=nr );
 						getFinalNormalForm( d_normal_forms[nr][i], nf, exp );
 					}
@@ -2285,36 +2283,37 @@ void TheoryStrings::getFinalNormalForm( Node n, std::vector< Node >& nf, std::ve
 	}
 }
 
-void TheoryStrings::separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& cols,
-											 std::vector< Node >& lts ) {
+void TheoryStrings::separateByLength(std::vector< Node >& n,
+  std::vector< std::vector< Node > >& cols,
+	std::vector< Node >& lts ) {
   unsigned leqc_counter = 0;
   std::map< Node, unsigned > eqc_to_leqc;
   std::map< unsigned, Node > leqc_to_eqc;
   std::map< unsigned, std::vector< Node > > eqc_to_strings;
-  for( unsigned i=0; i<n.size(); i++ ){
-	Node eqc = n[i];
-	Assert( d_equalityEngine.getRepresentative(eqc)==eqc );
-	EqcInfo* ei = getOrMakeEqcInfo( eqc, false );
-	Node lt = ei ? ei->d_length_term : Node::null();
-	if( !lt.isNull() ){
-	  lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
-	  Node r = d_equalityEngine.getRepresentative( lt );
-	  if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){
-		eqc_to_leqc[r] = leqc_counter;
-		leqc_to_eqc[leqc_counter] = r;
-		leqc_counter++;
-	  }
-	  eqc_to_strings[ eqc_to_leqc[r] ].push_back( eqc );
-	}else{
-	  eqc_to_strings[leqc_counter].push_back( eqc );
-	  leqc_counter++;
-	}
+  for( unsigned i=0; i<n.size(); i++ ) {
+    Node eqc = n[i];
+    Assert( d_equalityEngine.getRepresentative(eqc)==eqc );
+    EqcInfo* ei = getOrMakeEqcInfo( eqc, false );
+    Node lt = ei ? ei->d_length_term : Node::null();
+    if( !lt.isNull() ){
+      lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
+      Node r = d_equalityEngine.getRepresentative( lt );
+      if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){
+      eqc_to_leqc[r] = leqc_counter;
+      leqc_to_eqc[leqc_counter] = r;
+      leqc_counter++;
+      }
+      eqc_to_strings[ eqc_to_leqc[r] ].push_back( eqc );
+    }else{
+      eqc_to_strings[leqc_counter].push_back( eqc );
+      leqc_counter++;
+    }
   }
   for( std::map< unsigned, std::vector< Node > >::iterator it = eqc_to_strings.begin(); it != eqc_to_strings.end(); ++it ){
-	std::vector< Node > vec;
-	vec.insert( vec.end(), it->second.begin(), it->second.end() );
-	lts.push_back( leqc_to_eqc[it->first] );
-	cols.push_back( vec );
+    std::vector< Node > vec;
+    vec.insert( vec.end(), it->second.begin(), it->second.end() );
+    lts.push_back( leqc_to_eqc[it->first] );
+    cols.push_back( vec );
   }
 }
 
@@ -2350,10 +2349,12 @@ Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) {
 
 bool TheoryStrings::checkMemberships() {
 	bool addedLemma = false;
+	bool changed = false;
 	std::vector< Node > processed;
 	std::vector< Node > cprocessed;
 
 	//if(options::stringEIT()) {
+		//TODO: Opt for normal forms
 		for(NodeListMap::const_iterator itr_xr = d_str_re_map.begin();
 			itr_xr != d_str_re_map.end(); ++itr_xr ) {
 			bool spflag = false;
@@ -2415,175 +2416,248 @@ bool TheoryStrings::checkMemberships() {
 
 	if(!addedLemma) {
 	  for( unsigned i=0; i<d_regexp_memberships.size(); i++ ) {
-		//check regular expression membership
-		Node assertion = d_regexp_memberships[i];
-		if( d_regexp_ucached.find(assertion) == d_regexp_ucached.end() 
-			&& d_regexp_ccached.find(assertion) == d_regexp_ccached.end() ) {
-			Trace("strings-regexp") << "We have regular expression assertion : " << assertion << std::endl;
-			Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion;
-			bool polarity = assertion.getKind()!=kind::NOT;
-			bool flag = true;
-			Node x = atom[0];
-			Node r = atom[1];
-			if( polarity ) {
-				flag = checkPDerivative(x, r, atom, addedLemma, processed, cprocessed);
-			} else {
-				if(! options::stringExp()) {
-					throw LogicException("Strings Incomplete (due to Negative Membership) by default, try --strings-exp option.");
-				}
-			}
-			if(flag) {
-				//check if the term is atomic
-				Node xr = getRepresentative( x );
-				Trace("strings-regexp") << xr << " is rep of " << x << std::endl;
-				Assert( d_normal_forms.find( xr )!=d_normal_forms.end() );
-				//TODO
-				if( true || r.getKind()!=kind::REGEXP_STAR || ( d_normal_forms[xr].size()==1 && x.getKind()!=kind::STRING_CONCAT ) ){
-					Trace("strings-regexp") << "Unroll/simplify membership of atomic term " << xr << std::endl;
-					//if so, do simple unrolling
-					std::vector< Node > nvec;
-					d_regexp_opr.simplify(atom, nvec, polarity);
-					Node antec = assertion;
-					if(d_regexp_ant.find(assertion) != d_regexp_ant.end()) {
-						antec = d_regexp_ant[assertion];
-						for(std::vector< Node >::const_iterator itr=nvec.begin(); itr<nvec.end(); itr++) {
-							if(itr->getKind() == kind::STRING_IN_REGEXP) {
-								if(d_regexp_ant.find( *itr ) == d_regexp_ant.end()) {
-									d_regexp_ant[ *itr ] = antec;
-								}
-							}
-						}
-					}
-					Node conc = nvec.size()==1 ? nvec[0] :
-							NodeManager::currentNM()->mkNode(kind::AND, nvec);
-					conc = Rewriter::rewrite(conc);
-					sendLemma( antec, conc, "REGEXP" );
-					addedLemma = true;
-					processed.push_back( assertion );
-					//d_regexp_ucached[assertion] = true;
-				} else {
-					Trace("strings-regexp") << "Unroll/simplify membership of non-atomic term " << xr << " = ";
-					for( unsigned j=0; j<d_normal_forms[xr].size(); j++ ){
-						Trace("strings-regexp") << d_normal_forms[xr][j] << " ";
-					}
-					Trace("strings-regexp") << ", polarity = " << polarity << std::endl;
-					//otherwise, distribute unrolling over parts
-					Node p1;
-					Node p2;
-					if( d_normal_forms[xr].size()>1 ){
-						p1 = d_normal_forms[xr][0];
-						std::vector< Node > cc;
-						cc.insert( cc.begin(), d_normal_forms[xr].begin() + 1, d_normal_forms[xr].end() );
-						p2 = mkConcat( cc );
-					}
+      //check regular expression membership
+      Node assertion = d_regexp_memberships[i];
+      if( d_regexp_ucached.find(assertion) == d_regexp_ucached.end() 
+        && d_regexp_ccached.find(assertion) == d_regexp_ccached.end() ) {
+        Trace("strings-regexp") << "We have regular expression assertion : " << assertion << std::endl;
+        Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion;
+        bool polarity = assertion.getKind()!=kind::NOT;
+        bool flag = true;
+        Node x = atom[0];
+        Node r = atom[1];
+        std::vector< Node > rnfexp;
+
+        if(options::stringOpt1()) {
+          if(!x.isConst()) {
+            x = getNormalString(x, rnfexp);
+            changed = true;
+          }
+          if(!d_regexp_opr.checkConstRegExp(r)) {
+            r = getNormalSymRegExp(r, rnfexp);
+            changed = true;
+          }
+          Trace("strings-regexp-nf") << "Term " << atom << " is normalized to " << x << " IN " << r << std::endl;
+          if(changed) {
+            Node tmp = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r) );
+            if(!polarity) {
+              tmp = tmp.negate();
+            }
+            if(tmp == d_true) {
+              d_regexp_ccached.insert(assertion);
+              continue;
+            } else if(tmp == d_false) {
+              Node antec = mkRegExpAntec(assertion, mkExplain(rnfexp));
+              Node conc = Node::null();
+              sendLemma(antec, conc, "REGEXP NF Conflict");
+              addedLemma = true;
+              break;
+            }
+          }
+        }
 
-					Trace("strings-regexp-debug") << "Construct antecedant..." << std::endl;
-					std::vector< Node > antec;
-					std::vector< Node > antecn;
-					antec.insert( antec.begin(), d_normal_forms_exp[xr].begin(), d_normal_forms_exp[xr].end() );
-					if( x!=xr ){
-						antec.push_back( x.eqNode( xr ) );
-					}
-					antecn.push_back( assertion );
-					Node ant = mkExplain( antec, antecn );
-					Trace("strings-regexp-debug") << "Construct conclusion..." << std::endl;
-					Node conc;
-					if( polarity ){
-						if( d_normal_forms[xr].size()==0 ){
-							conc = d_true;
-						}else if( d_normal_forms[xr].size()==1 ){
-							Trace("strings-regexp-debug") << "Case 1\n";
-							conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r);
-						}else{
-							Trace("strings-regexp-debug") << "Case 2\n";
-							std::vector< Node > conc_c;
-							Node s11 = NodeManager::currentNM()->mkSkolem( "s11", NodeManager::currentNM()->stringType(), "created for re" );
-							Node s12 = NodeManager::currentNM()->mkSkolem( "s12", NodeManager::currentNM()->stringType(), "created for re" );
-							Node s21 = NodeManager::currentNM()->mkSkolem( "s21", NodeManager::currentNM()->stringType(), "created for re" );
-							Node s22 = NodeManager::currentNM()->mkSkolem( "s22", NodeManager::currentNM()->stringType(), "created for re" );
-							conc = p1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s11, s12));
-							conc_c.push_back(conc);
-							conc = p2.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s21, s22));
-							conc_c.push_back(conc);
-							conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r);
-							conc_c.push_back(conc);
-							conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s12, s21), r[0]);
-							conc_c.push_back(conc);
-							conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r);
-							conc_c.push_back(conc);
-							conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc_c));
-							Node eqz = Rewriter::rewrite(x.eqNode(d_emptyString));
-							conc = NodeManager::currentNM()->mkNode(kind::OR, eqz, conc);
-							d_pending_req_phase[eqz] = true;
-						}
-					}else{
-						if( d_normal_forms[xr].size()==0 ){
-							conc = d_false;
-						}else if( d_normal_forms[xr].size()==1 ){
-							Trace("strings-regexp-debug") << "Case 3\n";
-							conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r).negate();
-						}else{
-							Trace("strings-regexp-debug") << "Case 4\n";
-							Node len1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p1);
-							Node len2 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p2);
-							Node bi = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-							Node bj = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-							Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, bi, bj);
-							Node g1 = NodeManager::currentNM()->mkNode(kind::AND, 
-										NodeManager::currentNM()->mkNode(kind::GEQ, bi, d_zero),
-										NodeManager::currentNM()->mkNode(kind::GEQ, len1, bi),
-										NodeManager::currentNM()->mkNode(kind::GEQ, bj, d_zero),
-										NodeManager::currentNM()->mkNode(kind::GEQ, len2, bj));
-							Node s11 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, d_zero, bi);
-							Node s12 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, bi, NodeManager::currentNM()->mkNode(kind::MINUS, len1, bi));
-							Node s21 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, d_zero, bj);
-							Node s22 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, bj, NodeManager::currentNM()->mkNode(kind::MINUS, len2, bj));
-							Node cc1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r).negate();
-							Node cc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s12, s21), r[0]).negate();
-							Node cc3 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r).negate();
-							conc = NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2, cc3);
-							conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);
-							conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);
-							conc = NodeManager::currentNM()->mkNode(kind::AND, x.eqNode(d_emptyString).negate(), conc);
-						}
-					}
-					if( conc!=d_true ){
-						ant = mkRegExpAntec(assertion, ant);
-						sendLemma(ant, conc, "REGEXP CSTAR");
-						addedLemma = true;
-						if( conc==d_false ){
-							d_regexp_ccached.insert( assertion );
-						}else{
-							cprocessed.push_back( assertion );
-						}
-					}else{
-						d_regexp_ccached.insert(assertion);
-					}
-				}
-			}
-		}
-		if(d_conflict) {
-			break;
-		}
+        if( polarity ) {
+          flag = checkPDerivative(x, r, atom, addedLemma, processed, cprocessed, rnfexp);
+          if(options::stringOpt2() && flag) {
+            if(d_regexp_opr.checkConstRegExp(r) && x.getKind()==kind::STRING_CONCAT) {
+              std::vector< std::pair< Node, Node > > vec_can;
+              d_regexp_opr.splitRegExp(r, vec_can);
+              //TODO: lazy cache or eager?
+              std::vector< Node > vec_or;
+              std::vector< Node > vec_s2;
+              for(unsigned int s2i=1; s2i<x.getNumChildren(); s2i++) {
+                vec_s2.push_back(x[s2i]);
+              }
+              Node s1 = x[0];
+              Node s2 = vec_s2.size()==1? vec_s2[0]: NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, vec_s2);
+              for(unsigned int i=0; i<vec_can.size(); i++) {
+                Node m1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, vec_can[i].first);
+                Node m2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, vec_can[i].second);
+                Node c = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, m1, m2) );
+                vec_or.push_back( c );
+              }
+              Node conc = vec_or.size()==1 ? vec_or[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR, vec_or) );
+              //Trace("regexp-split") << "R " << r << " to " << conc << std::endl;
+              Node antec = mkRegExpAntec(atom, mkExplain(rnfexp));
+              if(conc == d_true) {
+                if(changed) {
+                  cprocessed.push_back( assertion );
+                } else {
+                  processed.push_back( assertion );
+                }
+              } else if(conc == d_false) {
+                conc = Node::null();
+                sendLemma(antec, conc, "RegExp CST-SP Conflict");
+              } else {
+                sendLemma(antec, conc, "RegExp-CST-SP");
+              }
+              addedLemma = true;
+              flag = false;
+            }
+          }
+        } else {
+          if(! options::stringExp()) {
+            throw LogicException("Strings Incomplete (due to Negative Membership) by default, try --strings-exp option.");
+          }
+        }
+        if(flag) {
+          //check if the term is atomic
+          Node xr = getRepresentative( x );
+          //Trace("strings-regexp") << xr << " is rep of " << x << std::endl;
+          //Assert( d_normal_forms.find( xr )!=d_normal_forms.end() );
+          //TODO
+          if( true || r.getKind()!=kind::REGEXP_STAR || ( d_normal_forms[xr].size()==1 && x.getKind()!=kind::STRING_CONCAT ) ){
+            Trace("strings-regexp") << "Unroll/simplify membership of atomic term " << xr << std::endl;
+            //if so, do simple unrolling
+            std::vector< Node > nvec;
+            d_regexp_opr.simplify(atom, nvec, polarity);
+            Node antec = assertion;
+            if(d_regexp_ant.find(assertion) != d_regexp_ant.end()) {
+              antec = d_regexp_ant[assertion];
+              for(std::vector< Node >::const_iterator itr=nvec.begin(); itr<nvec.end(); itr++) {
+                if(itr->getKind() == kind::STRING_IN_REGEXP) {
+                  if(d_regexp_ant.find( *itr ) == d_regexp_ant.end()) {
+                    d_regexp_ant[ *itr ] = antec;
+                  }
+                }
+              }
+            }
+            antec = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, antec, mkExplain(rnfexp)) );
+            Node conc = nvec.size()==1 ? nvec[0] :
+                NodeManager::currentNM()->mkNode(kind::AND, nvec);
+            conc = Rewriter::rewrite(conc);
+            sendLemma( antec, conc, "REGEXP" );
+            addedLemma = true;
+            if(changed) {
+              cprocessed.push_back( assertion );
+            } else {
+              processed.push_back( assertion );
+            }
+            //d_regexp_ucached[assertion] = true;
+          } else {
+            Trace("strings-regexp") << "Unroll/simplify membership of non-atomic term " << xr << " = ";
+            for( unsigned j=0; j<d_normal_forms[xr].size(); j++ ){
+              Trace("strings-regexp") << d_normal_forms[xr][j] << " ";
+            }
+            Trace("strings-regexp") << ", polarity = " << polarity << std::endl;
+            //otherwise, distribute unrolling over parts
+            Node p1;
+            Node p2;
+            if( d_normal_forms[xr].size()>1 ){
+              p1 = d_normal_forms[xr][0];
+              std::vector< Node > cc;
+              cc.insert( cc.begin(), d_normal_forms[xr].begin() + 1, d_normal_forms[xr].end() );
+              p2 = mkConcat( cc );
+            }
+
+            Trace("strings-regexp-debug") << "Construct antecedant..." << std::endl;
+            std::vector< Node > antec;
+            std::vector< Node > antecn;
+            antec.insert( antec.begin(), d_normal_forms_exp[xr].begin(), d_normal_forms_exp[xr].end() );
+            if( x!=xr ){
+              antec.push_back( x.eqNode( xr ) );
+            }
+            antecn.push_back( assertion );
+            Node ant = mkExplain( antec, antecn );
+            Trace("strings-regexp-debug") << "Construct conclusion..." << std::endl;
+            Node conc;
+            if( polarity ){
+              if( d_normal_forms[xr].size()==0 ){
+                conc = d_true;
+              }else if( d_normal_forms[xr].size()==1 ){
+                Trace("strings-regexp-debug") << "Case 1\n";
+                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r);
+              }else{
+                Trace("strings-regexp-debug") << "Case 2\n";
+                std::vector< Node > conc_c;
+                Node s11 = NodeManager::currentNM()->mkSkolem( "s11", NodeManager::currentNM()->stringType(), "created for re" );
+                Node s12 = NodeManager::currentNM()->mkSkolem( "s12", NodeManager::currentNM()->stringType(), "created for re" );
+                Node s21 = NodeManager::currentNM()->mkSkolem( "s21", NodeManager::currentNM()->stringType(), "created for re" );
+                Node s22 = NodeManager::currentNM()->mkSkolem( "s22", NodeManager::currentNM()->stringType(), "created for re" );
+                conc = p1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s11, s12));
+                conc_c.push_back(conc);
+                conc = p2.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s21, s22));
+                conc_c.push_back(conc);
+                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r);
+                conc_c.push_back(conc);
+                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s12, s21), r[0]);
+                conc_c.push_back(conc);
+                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r);
+                conc_c.push_back(conc);
+                conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc_c));
+                Node eqz = Rewriter::rewrite(x.eqNode(d_emptyString));
+                conc = NodeManager::currentNM()->mkNode(kind::OR, eqz, conc);
+                d_pending_req_phase[eqz] = true;
+              }
+            }else{
+              if( d_normal_forms[xr].size()==0 ){
+                conc = d_false;
+              }else if( d_normal_forms[xr].size()==1 ){
+                Trace("strings-regexp-debug") << "Case 3\n";
+                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r).negate();
+              }else{
+                Trace("strings-regexp-debug") << "Case 4\n";
+                Node len1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p1);
+                Node len2 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p2);
+                Node bi = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+                Node bj = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+                Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, bi, bj);
+                Node g1 = NodeManager::currentNM()->mkNode(kind::AND, 
+                      NodeManager::currentNM()->mkNode(kind::GEQ, bi, d_zero),
+                      NodeManager::currentNM()->mkNode(kind::GEQ, len1, bi),
+                      NodeManager::currentNM()->mkNode(kind::GEQ, bj, d_zero),
+                      NodeManager::currentNM()->mkNode(kind::GEQ, len2, bj));
+                Node s11 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, d_zero, bi);
+                Node s12 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, bi, NodeManager::currentNM()->mkNode(kind::MINUS, len1, bi));
+                Node s21 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, d_zero, bj);
+                Node s22 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, bj, NodeManager::currentNM()->mkNode(kind::MINUS, len2, bj));
+                Node cc1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r).negate();
+                Node cc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s12, s21), r[0]).negate();
+                Node cc3 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r).negate();
+                conc = NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2, cc3);
+                conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);
+                conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);
+                conc = NodeManager::currentNM()->mkNode(kind::AND, x.eqNode(d_emptyString).negate(), conc);
+              }
+            }
+            if( conc!=d_true ){
+              ant = mkRegExpAntec(assertion, ant);
+              sendLemma(ant, conc, "REGEXP CSTAR");
+              addedLemma = true;
+              if( conc==d_false ){
+                d_regexp_ccached.insert( assertion );
+              }else{
+                cprocessed.push_back( assertion );
+              }
+            }else{
+              d_regexp_ccached.insert(assertion);
+            }
+          }
+        }
+      }
+      if(d_conflict) {
+        break;
+      }
 	  }
 	}
-	if( addedLemma ){
+	if( addedLemma ) {
 		if( !d_conflict ){
-			for( unsigned i=0; i<processed.size(); i++ ){
+			for( unsigned i=0; i<processed.size(); i++ ) {
 				d_regexp_ucached.insert(processed[i]);
 			}
-			for( unsigned i=0; i<cprocessed.size(); i++ ){
+			for( unsigned i=0; i<cprocessed.size(); i++ ) {
 				d_regexp_ccached.insert(cprocessed[i]);
 			}
 		}
 		doPendingLemmas();
 		return true;
-	}else{
+	} else {
 		return false;
 	}
 }
 
-bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &processed, std::vector< Node > &cprocessed) {
+bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma,
+	std::vector< Node > &processed, std::vector< Node > &cprocessed, std::vector< Node > &nf_exp) {
 	/*if(d_opt_regexp_gcd) {
 		if(d_membership_length.find(atom) == d_membership_length.end()) {
 			addedLemma = addMembershipLength(atom);
@@ -2592,11 +2666,14 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma
 			Trace("strings-regexp") << "Membership length is already added." << std::endl;
 		}
 	}*/
+	Node antnf = mkExplain(nf_exp);
+
 	if(areEqual(x, d_emptyString)) {
 		Node exp;
 		switch(d_regexp_opr.delta(r, exp)) {
 			case 0: {
 				Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
+				antec = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, antec, antnf));
 				sendLemma(antec, exp, "RegExp Delta");
 				addedLemma = true;
 				d_regexp_ccached.insert(atom);
@@ -2608,6 +2685,7 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma
 			}
 			case 2: {
 				Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
+				antec = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, antec, antnf));
 				Node conc = Node::null();
 				sendLemma(antec, conc, "RegExp Delta CONFLICT");
 				addedLemma = true;
@@ -2619,7 +2697,7 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma
 				break;
 		}
 	} else {
-		Node xr = getRepresentative( x );
+		/*Node xr = getRepresentative( x );
 		if(x != xr) {
 			Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, xr, r);
 			Node nn = Rewriter::rewrite( n );
@@ -2634,9 +2712,10 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma
 				d_regexp_ccached.insert(atom);
 				return false;
 			}
-		}
+		}*/
 		Node sREant = mkRegExpAntec(atom, d_true);
-		if(splitRegExp( x, r, sREant )) {
+		sREant = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, sREant, antnf));
+		if(deriveRegExp( x, r, sREant )) {
 			addedLemma = true;
 			processed.push_back( atom );
 			return false;
@@ -2809,10 +2888,10 @@ bool TheoryStrings::addMembershipLength(Node atom) {
 	return false;
 }
 
-bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
+bool TheoryStrings::deriveRegExp( Node x, Node r, Node ant ) {
 	// TODO cstr in vre
 	Assert(x != d_emptyString);
-	Trace("regexp-split") << "TheoryStrings::splitRegExp: x=" << x << ", r= " << r << std::endl;
+	Trace("regexp-derive") << "TheoryStrings::deriveRegExp: x=" << x << ", r= " << r << std::endl;
 	//if(x.isConst()) {
 	//	Node n = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r );
 	//	Node r = Rewriter::rewrite( n );
@@ -2841,7 +2920,7 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
 		// send lemma
 		if(flag) {
 			if(x.isConst()) {
-				Assert(false, "Impossible: TheoryStrings::splitRegExp: const string in const regular expression.");
+				Assert(false, "Impossible: TheoryStrings::deriveRegExp: const string in const regular expression.");
 				return false;
 			} else {
 				Assert( x.getKind() == kind::STRING_CONCAT );
@@ -2862,7 +2941,7 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
 				}
 			}
 		}
-		sendLemma(ant, conc, "RegExp-CST-SP");
+		sendLemma(ant, conc, "RegExp-Derive");
 		return true;
 	} else {
 		return false;
@@ -2904,9 +2983,93 @@ void TheoryStrings::addMembership(Node assertion) {
 	d_regexp_memberships.push_back( assertion );
 }
 
-Node TheoryStrings::instantiateSymRegExp(Node r) {
-	//TODO:
-	return r;
+Node TheoryStrings::getNormalString(Node x, std::vector<Node> &nf_exp) {
+	Node ret = x;
+	if(x.getKind() == kind::STRING_CONCAT) {
+		std::vector< Node > vec_nodes;
+		for(unsigned i=0; i<x.getNumChildren(); i++) {
+			if(x[i].isConst()) {
+				vec_nodes.push_back(x[i]);
+			} else {
+				Node tmp = x[i];
+				if(d_normal_forms.find( tmp ) != d_normal_forms.end()) {
+					Trace("regexp-debug") << "Term: " << tmp << " has a normal form." << std::endl;
+					vec_nodes.insert(vec_nodes.end(), d_normal_forms[tmp].begin(), d_normal_forms[tmp].end());
+					nf_exp.insert(nf_exp.end(), d_normal_forms_exp[tmp].begin(), d_normal_forms_exp[tmp].end());
+				} else {
+					Trace("regexp-debug") << "Term: " << tmp << " has NO normal form." << std::endl;
+					vec_nodes.push_back(tmp);
+				}
+			}
+		}
+		ret = mkConcat(vec_nodes);
+	} else {
+		if(d_normal_forms.find( x ) != d_normal_forms.end()) {
+			ret = mkConcat( d_normal_forms[x] );
+			nf_exp.insert(nf_exp.end(), d_normal_forms_exp[x].begin(), d_normal_forms_exp[x].end());
+			Trace("regexp-debug") << "Term: " << x << " has a normal form " << ret << std::endl;
+		} else {
+			Trace("regexp-debug") << "Term: " << x << " has NO normal form." << std::endl;
+		}
+	}
+	return ret;
+}
+
+Node TheoryStrings::getNormalSymRegExp(Node r, std::vector<Node> &nf_exp) {
+	Node ret = r;
+	switch( r.getKind() ) {
+		case kind::REGEXP_EMPTY:
+		case kind::REGEXP_SIGMA:
+			break;
+		case kind::STRING_TO_REGEXP: {
+			if(!r[0].isConst()) {
+				Node tmp = getNormalString( r[0], nf_exp );
+				if(tmp != r[0]) {
+					ret = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, tmp);
+				}
+			}
+			break;
+		}
+		case kind::REGEXP_CONCAT: {
+			std::vector< Node > vec_nodes;
+			for(unsigned i=0; i<r.getNumChildren(); ++i) {
+				vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) );
+			}
+			ret = mkConcat(vec_nodes);
+			break;
+		}
+		case kind::REGEXP_UNION: {
+			std::vector< Node > vec_nodes;
+			for(unsigned i=0; i<r.getNumChildren(); ++i) {
+				vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) );
+			}
+			ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes) );
+			break;
+		}
+		case kind::REGEXP_INTER: {
+			std::vector< Node > vec_nodes;
+			for(unsigned i=0; i<r.getNumChildren(); ++i) {
+				vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) );
+			}
+			ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_INTER, vec_nodes) );
+			break;
+		}
+		case kind::REGEXP_STAR: {
+			ret = getNormalSymRegExp( r[0], nf_exp );
+			ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, ret) );
+			break;
+		}
+		//case kind::REGEXP_PLUS:
+		//case kind::REGEXP_OPT:
+		//case kind::REGEXP_RANGE:
+		default: {
+			Trace("strings-error") << "Unsupported term: " << r << " in normalization SymRegExp." << std::endl;
+			Assert( false );
+			//return Node::null();
+		}
+	}
+
+	return ret;
 }
 
 //// Finite Model Finding
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 33283d1cf..f4a17fa46 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -67,18 +67,18 @@ public:
 		bool eqNotifyTriggerEquality(TNode equality, bool value) {
 		  Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
 		  if (value) {
-			return d_str.propagate(equality);
+			  return d_str.propagate(equality);
 		  } else {
-			// We use only literal triggers so taking not is safe
-			return d_str.propagate(equality.notNode());
+        // We use only literal triggers so taking not is safe
+        return d_str.propagate(equality.notNode());
 		  }
 		}
 		bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
 		  Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
 		  if (value) {
-			return d_str.propagate(predicate);
+        return d_str.propagate(predicate);
 		  } else {
-		   return d_str.propagate(predicate.notNode());
+         return d_str.propagate(predicate.notNode());
 		  }
 		}
 		bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
@@ -119,11 +119,11 @@ private:
 	Node d_ufSubstr;
 
 	// Constants
-    Node d_emptyString;
+  Node d_emptyString;
 	Node d_emptyRegexp;
-    Node d_true;
-    Node d_false;
-    Node d_zero;
+  Node d_true;
+  Node d_false;
+  Node d_zero;
 	Node d_one;
 	// Options
 	bool d_opt_fmf;
@@ -137,12 +137,12 @@ private:
 	Node getLength( Node t );
 
 private:
-    /** The notify class */
-    NotifyClass d_notify;
-    /** Equaltity engine */
-    eq::EqualityEngine d_equalityEngine;
-    /** Are we in conflict */
-    context::CDO<bool> d_conflict;
+  /** The notify class */
+  NotifyClass d_notify;
+  /** Equaltity engine */
+  eq::EqualityEngine d_equalityEngine;
+  /** Are we in conflict */
+  context::CDO<bool> d_conflict;
 	//list of pairs of nodes to merge
 	std::map< Node, Node > d_pending_exp;
 	std::vector< Node > d_pending;
@@ -206,41 +206,43 @@ private:
 	NodeNodeMap d_length_inst;
 private:
 	void mergeCstVec(std::vector< Node > &vec_strings);
-    bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
-						std::vector< std::vector< Node > > &normal_forms,
-						std::vector< std::vector< Node > > &normal_forms_exp,
-						std::vector< Node > &normal_form_src);
+  bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
+        std::vector< std::vector< Node > > &normal_forms,
+        std::vector< std::vector< Node > > &normal_forms_exp,
+        std::vector< Node > &normal_form_src);
 	bool detectLoop(std::vector< std::vector< Node > > &normal_forms,
-					int i, int j, int index_i, int index_j, 
-					int &loop_in_i, int &loop_in_j);
+        int i, int j, int index_i, int index_j, 
+        int &loop_in_i, int &loop_in_j);
 	bool processLoop(std::vector< Node > &antec,
-					 std::vector< std::vector< Node > > &normal_forms,
-					 std::vector< Node > &normal_form_src,
-					 int i, int j, int loop_n_index, int other_n_index,
-					 int loop_index, int index, int other_index);
+        std::vector< std::vector< Node > > &normal_forms,
+        std::vector< Node > &normal_form_src,
+        int i, int j, int loop_n_index, int other_n_index,
+        int loop_index, int index, int other_index);
 	bool processNEqc(std::vector< std::vector< Node > > &normal_forms,
-					 std::vector< std::vector< Node > > &normal_forms_exp,
-					 std::vector< Node > &normal_form_src);
+        std::vector< std::vector< Node > > &normal_forms_exp,
+        std::vector< Node > &normal_form_src);
 	bool processReverseNEq(std::vector< std::vector< Node > > &normal_forms,
-						   std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j );
+        std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j );
 	bool processSimpleNEq( std::vector< std::vector< Node > > &normal_forms,
-						   std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j,
-						   unsigned& index_i, unsigned& index_j, bool isRev );
-    bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
-    bool processDeq( Node n1, Node n2 );
+        std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j,
+        unsigned& index_i, unsigned& index_j, bool isRev );
+  bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
+  bool processDeq( Node n1, Node n2 );
 	int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj );
 	int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
 	//bool unrollStar( Node atom );
 	Node mkRegExpAntec(Node atom, Node ant);
 
 	bool checkSimple();
-    bool checkNormalForms();
+  bool checkNormalForms();
 	void checkDeqNF();
 	bool checkLengthsEqc();
-    bool checkCardinality();
-    bool checkInductiveEquations();
+  bool checkCardinality();
+  bool checkInductiveEquations();
 	bool checkMemberships();
-	bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &processed, std::vector< Node > &cprocessed);
+	bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma,
+		std::vector< Node > &processed, std::vector< Node > &cprocessed,
+		std::vector< Node > &nf_exp);
 	bool checkContains();
 	bool checkPosContains();
 	bool checkNegContains();
@@ -320,10 +322,11 @@ private:
 	RegExpOpr d_regexp_opr;
 
 	CVC4::String getHeadConst( Node x );
-	bool splitRegExp( Node x, Node r, Node ant );
+	bool deriveRegExp( Node x, Node r, Node ant );
 	bool addMembershipLength(Node atom);
 	void addMembership(Node assertion);
-	Node instantiateSymRegExp(Node r);
+	Node getNormalString(Node x, std::vector<Node> &nf_exp);
+	Node getNormalSymRegExp(Node r, std::vector<Node> &nf_exp);
 
 
 	// Finite Model Finding
@@ -334,7 +337,7 @@ private:
 	context::CDO< int > d_curr_cardinality;
 public:
 	//for finite model finding
-    Node getNextDecisionRequest();
+  Node getNextDecisionRequest();
 	void assertNode( Node lit );
 
 public:
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 85ab73691..ef5da000f 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -137,10 +137,10 @@ int StringsPreprocess::checkFixLenVar( Node t ) {
 	return ret;
 }
 Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
-    std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
-    if(i != d_cache.end()) {
-      return (*i).second.isNull() ? t : (*i).second;
-    }
+  std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
+  if(i != d_cache.end()) {
+    return (*i).second.isNull() ? t : (*i).second;
+  }
 
 	Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl;
 	Node retNode = t;
@@ -179,8 +179,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 		retNode = n;
 	} else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ) {
 		Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
-							NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ),
-							NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
+          NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ),
+          NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
 		Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero);
 		Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[2], d_zero);
 		Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
@@ -554,10 +554,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 }
 
 Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
-    std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
-    if(i != d_cache.end()) {
-      return (*i).second.isNull() ? t : (*i).second;
-    }
+  std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
+  if(i != d_cache.end()) {
+    return (*i).second.isNull() ? t : (*i).second;
+  }
 
 	unsigned num = t.getNumChildren();
 	if(num == 0) {
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 69454db84..6d0af4d1b 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -40,8 +40,8 @@ private:
 	Node simplify( Node t, std::vector< Node > &new_nodes );
 	Node decompose( Node t, std::vector< Node > &new_nodes );
 public:
-    void simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes);
-    void simplify(std::vector< Node > &vec_node);
+  void simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes);
+  void simplify(std::vector< Node > &vec_node);
 	StringsPreprocess();
 };
 
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index f6de1b129..a47b4fbca 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -25,52 +25,52 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::strings;
 
 Node TheoryStringsRewriter::rewriteConcatString( TNode node ) {
-    Trace("strings-prerewrite") << "Strings::rewriteConcatString start " << node << std::endl;
-    Node retNode = node;
-    std::vector<Node> node_vec;
-    Node preNode = Node::null();
-    for(unsigned int i=0; i<node.getNumChildren(); ++i) {
-        Node tmpNode = node[i];
+  Trace("strings-prerewrite") << "Strings::rewriteConcatString start " << node << std::endl;
+  Node retNode = node;
+  std::vector<Node> node_vec;
+  Node preNode = Node::null();
+  for(unsigned int i=0; i<node.getNumChildren(); ++i) {
+    Node tmpNode = node[i];
 		if(node[i].getKind() == kind::STRING_CONCAT) {
-            tmpNode = rewriteConcatString(node[i]);
-            if(tmpNode.getKind() == kind::STRING_CONCAT) {
+      tmpNode = rewriteConcatString(node[i]);
+      if(tmpNode.getKind() == kind::STRING_CONCAT) {
 				unsigned j=0;
-                if(!preNode.isNull()) {
-                    if(tmpNode[0].isConst()) {
-                        preNode = NodeManager::currentNM()->mkConst( preNode.getConst<String>().concat( tmpNode[0].getConst<String>() ) );
-                        node_vec.push_back( preNode );
-                        preNode = Node::null();
-                    } else {
-                        node_vec.push_back( preNode );
-                        preNode = Node::null();
-                        node_vec.push_back( tmpNode[0] );
-                    }
-					++j;
-                }
-                for(; j<tmpNode.getNumChildren() - 1; ++j) {
-                    node_vec.push_back( tmpNode[j] );
-                }
-                tmpNode = tmpNode[j];
-            }
+        if(!preNode.isNull()) {
+          if(tmpNode[0].isConst()) {
+            preNode = NodeManager::currentNM()->mkConst( preNode.getConst<String>().concat( tmpNode[0].getConst<String>() ) );
+            node_vec.push_back( preNode );
+            preNode = Node::null();
+          } else {
+            node_vec.push_back( preNode );
+            preNode = Node::null();
+            node_vec.push_back( tmpNode[0] );
+          }
+          ++j;
         }
-        if(!tmpNode.isConst()) {
-            if(!preNode.isNull()) {
-                if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ) {
-                    preNode = Node::null();
-                } else {
-                    node_vec.push_back( preNode );
-                    preNode = Node::null();
-                }
-            }
-            node_vec.push_back( tmpNode );
+        for(; j<tmpNode.getNumChildren() - 1; ++j) {
+          node_vec.push_back( tmpNode[j] );
+        }
+        tmpNode = tmpNode[j];
+      }
+    }
+    if(!tmpNode.isConst()) {
+      if(!preNode.isNull()) {
+        if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ) {
+          preNode = Node::null();
         } else {
-            if(preNode.isNull()) {
-                preNode = tmpNode;
-            } else {
-                preNode = NodeManager::currentNM()->mkConst( preNode.getConst<String>().concat( tmpNode.getConst<String>() ) );
-            }
+          node_vec.push_back( preNode );
+          preNode = Node::null();
         }
+      }
+      node_vec.push_back( tmpNode );
+    } else {
+      if(preNode.isNull()) {
+        preNode = tmpNode;
+      } else {
+        preNode = NodeManager::currentNM()->mkConst( preNode.getConst<String>().concat( tmpNode.getConst<String>() ) );
+      }
     }
+  }
 	if(preNode != Node::null()) {
 		node_vec.push_back( preNode );
 	}
@@ -79,65 +79,65 @@ Node TheoryStringsRewriter::rewriteConcatString( TNode node ) {
 	} else {
 		retNode = node_vec[0];
 	}
-    Trace("strings-prerewrite") << "Strings::rewriteConcatString end " << retNode << std::endl;
-    return retNode;
+  Trace("strings-prerewrite") << "Strings::rewriteConcatString end " << retNode << std::endl;
+  return retNode;
 }
 
 Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) {
-	Assert( node.getKind() == kind::REGEXP_CONCAT );
-    Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp start " << node << std::endl;
-    Node retNode = node;
-    std::vector<Node> node_vec;
-    Node preNode = Node::null();
-	bool emptyflag = false;
-    for(unsigned int i=0; i<node.getNumChildren(); ++i) {
+  Assert( node.getKind() == kind::REGEXP_CONCAT );
+  Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp start " << node << std::endl;
+  Node retNode = node;
+  std::vector<Node> node_vec;
+  Node preNode = Node::null();
+  bool emptyflag = false;
+  for(unsigned int i=0; i<node.getNumChildren(); ++i) {
 		Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp preNode: " << preNode << std::endl;
-        Node tmpNode = node[i];
-        if(tmpNode.getKind() == kind::REGEXP_CONCAT) {
-            tmpNode = prerewriteConcatRegExp(node[i]);
-            if(tmpNode.getKind() == kind::REGEXP_CONCAT) {
-				unsigned j=0;
-                if(!preNode.isNull()) {
-                    if(tmpNode[0].getKind() == kind::STRING_TO_REGEXP) {
-                        preNode = rewriteConcatString(
-							NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) );
-                        node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
-                        preNode = Node::null();
-                    } else {
-                        node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
-                        preNode = Node::null();
-                        node_vec.push_back( tmpNode[0] );
-                    }
-					++j;
-                }
-                for(; j<tmpNode.getNumChildren() - 1; ++j) {
-                    node_vec.push_back( tmpNode[j] );
-                }
-                tmpNode = tmpNode[j];
-            }
+    Node tmpNode = node[i];
+    if(tmpNode.getKind() == kind::REGEXP_CONCAT) {
+      tmpNode = prerewriteConcatRegExp(node[i]);
+      if(tmpNode.getKind() == kind::REGEXP_CONCAT) {
+        unsigned j=0;
+        if(!preNode.isNull()) {
+          if(tmpNode[0].getKind() == kind::STRING_TO_REGEXP) {
+            preNode = rewriteConcatString(
+            NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) );
+            node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
+            preNode = Node::null();
+          } else {
+            node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
+            preNode = Node::null();
+            node_vec.push_back( tmpNode[0] );
+          }
+          ++j;
+        }
+        for(; j<tmpNode.getNumChildren() - 1; ++j) {
+          node_vec.push_back( tmpNode[j] );
         }
-        if( tmpNode.getKind() == kind::STRING_TO_REGEXP ) {
-            if(preNode.isNull()) {
-                preNode = tmpNode[0];
-            } else {
-				preNode = rewriteConcatString(
-							NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0] ) );
-            }
-        } else if( tmpNode.getKind() == kind::REGEXP_EMPTY ) {
-			emptyflag = true;
-			break;
+        tmpNode = tmpNode[j];
+      }
+    }
+    if( tmpNode.getKind() == kind::STRING_TO_REGEXP ) {
+      if(preNode.isNull()) {
+        preNode = tmpNode[0];
+      } else {
+        preNode = rewriteConcatString(
+        NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0] ) );
+      }
+    } else if( tmpNode.getKind() == kind::REGEXP_EMPTY ) {
+      emptyflag = true;
+      break;
 		} else {
-            if(!preNode.isNull()) {
-                if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ) {
-                    preNode = Node::null();
-                } else {
-                    node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
-                    preNode = Node::null();
-                }
-            }
-            node_vec.push_back( tmpNode );
+      if(!preNode.isNull()) {
+        if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ) {
+          preNode = Node::null();
+        } else {
+          node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
+          preNode = Node::null();
         }
+      }
+      node_vec.push_back( tmpNode );
     }
+  }
 	if(emptyflag) {
 		std::vector< Node > nvec;
 		retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
@@ -151,17 +151,17 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) {
 			retNode = node_vec[0];
 		}
 	}
-    Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp end " << retNode << std::endl;
-    return retNode;
+  Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp end " << retNode << std::endl;
+  return retNode;
 }
 
 Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) {
 	Assert( node.getKind() == kind::REGEXP_UNION );
-    Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl;
-    Node retNode = node;
-    std::vector<Node> node_vec;
+  Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl;
+  Node retNode = node;
+  std::vector<Node> node_vec;
 	bool flag = false;
-    for(unsigned i=0; i<node.getNumChildren(); ++i) {
+  for(unsigned i=0; i<node.getNumChildren(); ++i) {
 		if(node[i].getKind() == kind::REGEXP_UNION) {
 			Node tmpNode = prerewriteOrRegExp( node[i] );
 			for(unsigned int j=0; j<tmpNode.getNumChildren(); ++j) {
@@ -180,7 +180,7 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) {
 					node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, node_vec);
 	}
 	Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl;
-    return retNode;
+  return retNode;
 }
 
 bool TheoryStringsRewriter::checkConstRegExp( TNode t ) {
@@ -322,54 +322,54 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
 	Node retNode = node;
 	Node orig = retNode;
 
-    if(node.getKind() == kind::STRING_CONCAT) {
-        retNode = rewriteConcatString(node);
-    } else if(node.getKind() == kind::EQUAL) {
-        Node leftNode  = node[0];
-        if(node[0].getKind() == kind::STRING_CONCAT) {
-            leftNode = rewriteConcatString(node[0]);
-        }
-        Node rightNode = node[1];
-        if(node[1].getKind() == kind::STRING_CONCAT) {
-            rightNode = rewriteConcatString(node[1]);
-        }
+  if(node.getKind() == kind::STRING_CONCAT) {
+    retNode = rewriteConcatString(node);
+  } else if(node.getKind() == kind::EQUAL) {
+    Node leftNode  = node[0];
+    if(node[0].getKind() == kind::STRING_CONCAT) {
+      leftNode = rewriteConcatString(node[0]);
+    }
+    Node rightNode = node[1];
+    if(node[1].getKind() == kind::STRING_CONCAT) {
+      rightNode = rewriteConcatString(node[1]);
+    }
 
-        if(leftNode == rightNode) {
-            retNode = NodeManager::currentNM()->mkConst(true);
-        } else if(leftNode.isConst() && rightNode.isConst()) {
-            retNode = NodeManager::currentNM()->mkConst(false);
-        } else if(leftNode > rightNode) {
-            retNode = NodeManager::currentNM()->mkNode(kind::EQUAL, rightNode, leftNode);
-        } else if( leftNode != node[0] || rightNode != node[1]) {
-            retNode = NodeManager::currentNM()->mkNode(kind::EQUAL, leftNode, rightNode);
-        }
-    } else if(node.getKind() == kind::STRING_LENGTH) {
-        if(node[0].isConst()) {
-            retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) );
-        } /*else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) {
-            retNode = node[0][2];
-        }*/ else if(node[0].getKind() == kind::STRING_CONCAT) {
-            Node tmpNode = rewriteConcatString(node[0]);
-            if(tmpNode.isConst()) {
-                retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) );
-            } /*else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) {
-				retNode = tmpNode[2];
-            }*/ else {
-                // it has to be string concat
-                std::vector<Node> node_vec;
-                for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) {
-                    if(tmpNode[i].isConst()) {
-                        node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode[i].getConst<String>().size() ) ) );
-					} else if(tmpNode[i].getKind() == kind::STRING_SUBSTR_TOTAL) {
-                        node_vec.push_back( tmpNode[i][2] );
-                    } else {
-                        node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) );
-                    }
-                }
-                retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
-            }
+    if(leftNode == rightNode) {
+      retNode = NodeManager::currentNM()->mkConst(true);
+    } else if(leftNode.isConst() && rightNode.isConst()) {
+      retNode = NodeManager::currentNM()->mkConst(false);
+    } else if(leftNode > rightNode) {
+      retNode = NodeManager::currentNM()->mkNode(kind::EQUAL, rightNode, leftNode);
+    } else if( leftNode != node[0] || rightNode != node[1]) {
+      retNode = NodeManager::currentNM()->mkNode(kind::EQUAL, leftNode, rightNode);
+    }
+  } else if(node.getKind() == kind::STRING_LENGTH) {
+    if(node[0].isConst()) {
+      retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) );
+    } /*else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) {
+        retNode = node[0][2];
+    }*/ else if(node[0].getKind() == kind::STRING_CONCAT) {
+      Node tmpNode = rewriteConcatString(node[0]);
+      if(tmpNode.isConst()) {
+        retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) );
+      } /*else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) {
+      retNode = tmpNode[2];
+      }*/ else {
+        // it has to be string concat
+        std::vector<Node> node_vec;
+        for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) {
+          if(tmpNode[i].isConst()) {
+            node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode[i].getConst<String>().size() ) ) );
+          } else if(tmpNode[i].getKind() == kind::STRING_SUBSTR_TOTAL) {
+            node_vec.push_back( tmpNode[i][2] );
+          } else {
+            node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) );
+          }
         }
-    } else if(node.getKind() == kind::STRING_SUBSTR_TOTAL) {
+        retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
+      }
+    }
+  } else if(node.getKind() == kind::STRING_SUBSTR_TOTAL) {
 		Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
 		if(node[2] == zero) {
 			retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
@@ -552,15 +552,15 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
 }
 
 RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
-    Node retNode = node;
+  Node retNode = node;
 	Node orig = retNode;
-    Trace("strings-prerewrite") << "Strings::preRewrite start " << node << std::endl;
+  Trace("strings-prerewrite") << "Strings::preRewrite start " << node << std::endl;
 
-    if(node.getKind() == kind::STRING_CONCAT) {
-        retNode = rewriteConcatString(node);
-    } else if(node.getKind() == kind::REGEXP_CONCAT) {
-		retNode = prerewriteConcatRegExp(node);
-    } else if(node.getKind() == kind::REGEXP_UNION) {
+  if(node.getKind() == kind::STRING_CONCAT) {
+    retNode = rewriteConcatString(node);
+  } else if(node.getKind() == kind::REGEXP_CONCAT) {
+    retNode = prerewriteConcatRegExp(node);
+  } else if(node.getKind() == kind::REGEXP_UNION) {
 		retNode = prerewriteOrRegExp(node);
 	} else if(node.getKind() == kind::REGEXP_STAR) {
 		if(node[0].getKind() == kind::REGEXP_STAR) {
@@ -568,7 +568,7 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
 		}
 	} else if(node.getKind() == kind::REGEXP_PLUS) {
 		retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0],
-					NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, node[0]));
+      NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, node[0]));
 	} else if(node.getKind() == kind::REGEXP_OPT) {
 		retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_UNION,
 					NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ),
@@ -623,6 +623,6 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
 		Trace("strings-lp") << "Strings::lp " << node << " => " << retNode << std::endl;
 	}
 
-    Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl;
-    return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
+  Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl;
+  return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
 }
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index e4778e86c..9ffe9150d 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -26,7 +26,7 @@ namespace strings {
 class StringConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     return nodeManager->stringType();
   }
 };
@@ -34,22 +34,22 @@ public:
 class StringConcatTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ){
-		TNode::iterator it = n.begin();
-		TNode::iterator it_end = n.end();
-		int size = 0;
-		for (; it != it_end; ++ it) {
-		   TypeNode t = (*it).getType(check);
-		   if (!t.isString()) {
-			 throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat");
-		   }
-		   ++size;
-		}
-		if(size < 2) {
-		   throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in string concat");
-		}
-	}
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      int size = 0;
+      for (; it != it_end; ++ it) {
+       TypeNode t = (*it).getType(check);
+       if (!t.isString()) {
+         throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat");
+       }
+       ++size;
+      }
+      if(size < 2) {
+        throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in string concat");
+      }
+    }
     return nodeManager->stringType();
   }
 };
@@ -57,12 +57,12 @@ public:
 class StringLengthTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length");
+      }
     }
     return nodeManager->integerType();
   }
@@ -71,20 +71,20 @@ public:
 class StringSubstrTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr");
-        }
-		t = n[1].getType(check);
-        if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a start int term in substr");
-        }
-		t = n[2].getType(check);
-        if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a length int term in substr");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr");
+      }
+      t = n[1].getType(check);
+      if (!t.isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a start int term in substr");
+      }
+      t = n[2].getType(check);
+      if (!t.isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a length int term in substr");
+      }
     }
     return nodeManager->stringType();
   }
@@ -95,14 +95,14 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain");
-        }
-		t = n[1].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a target string term in string contain");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain");
+      }
+      t = n[1].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a target string term in string contain");
+      }
     }
     return nodeManager->booleanType();
   }
@@ -113,14 +113,14 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at 0");
-        }
-		t = n[1].getType(check);
-        if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string char at 1");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at 0");
+      }
+      t = n[1].getType(check);
+      if (!t.isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string char at 1");
+      }
     }
     return nodeManager->stringType();
   }
@@ -131,18 +131,18 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 0");
-        }
-		t = n[1].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 1");
-        }
-		t = n[2].getType(check);
-        if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string indexof 2");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 0");
+      }
+      t = n[1].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 1");
+      }
+      t = n[2].getType(check);
+      if (!t.isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string indexof 2");
+      }
     }
     return nodeManager->integerType();
   }
@@ -153,18 +153,18 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 0");
-        }
-		t = n[1].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 1");
-        }
-		t = n[2].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 2");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 0");
+      }
+      t = n[1].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 1");
+      }
+      t = n[2].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 2");
+      }
     }
     return nodeManager->stringType();
   }
@@ -175,14 +175,14 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 0");
-        }
-		t = n[1].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 1");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 0");
+      }
+      t = n[1].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 1");
+      }
     }
     return nodeManager->booleanType();
   }
@@ -193,14 +193,14 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 0");
-        }
-		t = n[1].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 1");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 0");
+      }
+      t = n[1].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 1");
+      }
     }
     return nodeManager->booleanType();
   }
@@ -211,10 +211,10 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an integer term in int to string 0");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an integer term in int to string 0");
+      }
     }
     return nodeManager->stringType();
   }
@@ -225,10 +225,10 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-        TypeNode t = n[0].getType(check);
-        if (!t.isString()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in string to int 0");
-        }
+      TypeNode t = n[0].getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string to int 0");
+      }
     }
     return nodeManager->integerType();
   }
@@ -247,20 +247,20 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-		TNode::iterator it = n.begin();
-		TNode::iterator it_end = n.end();
-		int size = 0;
-		for (; it != it_end; ++ it) {
-		   TypeNode t = (*it).getType(check);
-		   if (!t.isRegExp()) {
-			 throw TypeCheckingExceptionPrivate(n, "expecting regexp terms in regexp concat");
-		   }
-		   ++size;
-		}
-		if(size < 2) {
-		   throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat");
-		}
-	}
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      int size = 0;
+      for (; it != it_end; ++ it) {
+         TypeNode t = (*it).getType(check);
+         if (!t.isRegExp()) {
+           throw TypeCheckingExceptionPrivate(n, "expecting regexp terms in regexp concat");
+         }
+         ++size;
+      }
+      if(size < 2) {
+         throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat");
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -270,15 +270,15 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-		TNode::iterator it = n.begin();
-		TNode::iterator it_end = n.end();
-		for (; it != it_end; ++ it) {
-		   TypeNode t = (*it).getType(check);
-		   if (!t.isRegExp()) {
-			 throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-		   }
-		}
-	}
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      for (; it != it_end; ++ it) {
+         TypeNode t = (*it).getType(check);
+         if (!t.isRegExp()) {
+           throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
+         }
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -288,15 +288,15 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-		TNode::iterator it = n.begin();
-		TNode::iterator it_end = n.end();
-		for (; it != it_end; ++ it) {
-		   TypeNode t = (*it).getType(check);
-		   if (!t.isRegExp()) {
-			 throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-		   }
-		}
-	}
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      for (; it != it_end; ++ it) {
+       TypeNode t = (*it).getType(check);
+       if (!t.isRegExp()) {
+         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
+       }
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -306,12 +306,13 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-		TNode::iterator it = n.begin();
-		TypeNode t = (*it).getType(check);
-		if (!t.isRegExp()) {
-		  throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-		}
-	}
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      TypeNode t = (*it).getType(check);
+      if (!t.isRegExp()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -321,12 +322,13 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-		TNode::iterator it = n.begin();
-		TypeNode t = (*it).getType(check);
-		if (!t.isRegExp()) {
-		  throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-		}
-	}
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      TypeNode t = (*it).getType(check);
+      if (!t.isRegExp()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -336,12 +338,13 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-		TNode::iterator it = n.begin();
-		TypeNode t = (*it).getType(check);
-		if (!t.isRegExp()) {
-		  throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-		}
-	}
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      TypeNode t = (*it).getType(check);
+      if (!t.isRegExp()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -351,27 +354,28 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-		TNode::iterator it = n.begin();
-		char ch[2];
-
-		for(int i=0; i<2; ++i) {
-			TypeNode t = (*it).getType(check);
-			if (!t.isString()) {
-			  throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range");
-			}
-			if( (*it).getKind() != kind::CONST_STRING ) {
-			  throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range");
-			}
-			if( (*it).getConst<String>().size() != 1 ) {
-			  throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range");
-			}
-			ch[i] = (*it).getConst<String>().getFirstChar();
-			++it;
-		}
-		if(ch[0] > ch[1]) {
-			throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range");
-		}
-	}
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      char ch[2];
+
+      for(int i=0; i<2; ++i) {
+        TypeNode t = (*it).getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range");
+        }
+        if( (*it).getKind() != kind::CONST_STRING ) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range");
+        }
+        if( (*it).getConst<String>().size() != 1 ) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range");
+        }
+        ch[i] = (*it).getConst<String>().getFirstChar();
+        ++it;
+      }
+      if(ch[0] > ch[1]) {
+        throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range");
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -381,33 +385,33 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-		TNode::iterator it = n.begin();
-		TNode::iterator it_end = n.end();
-		TypeNode t = (*it).getType(check);
-		if (!t.isRegExp()) {
-		  throw TypeCheckingExceptionPrivate(n, "expecting a regexp term in regexp loop 1");
-		}
-		++it; t = (*it).getType(check);
-		if (!t.isInteger()) {
-		  throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 2");
-		}
-		if(!(*it).isConst()) {
-		  throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 2");
-		}
-		++it;
-		if(it != it_end) {
-			t = (*it).getType(check);
-			if (!t.isInteger()) {
-			  throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 3");
-			}
-			if(!(*it).isConst()) {
-			  throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 3");
-			}
-			//if(++it != it_end) {
-			//  throw TypeCheckingExceptionPrivate(n, "too many regexp");
-			//}
-		}
-	}
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      TypeNode t = (*it).getType(check);
+      if (!t.isRegExp()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting a regexp term in regexp loop 1");
+      }
+      ++it; t = (*it).getType(check);
+      if (!t.isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 2");
+      }
+      if(!(*it).isConst()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 2");
+      }
+      ++it;
+      if(it != it_end) {
+        t = (*it).getType(check);
+        if (!t.isInteger()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 3");
+        }
+        if(!(*it).isConst()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 3");
+        }
+        //if(++it != it_end) {
+        //  throw TypeCheckingExceptionPrivate(n, "too many regexp");
+        //}
+      }
+    }
     return nodeManager->regexpType();
   }
 };
@@ -417,15 +421,16 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-		TNode::iterator it = n.begin();
-		TypeNode t = (*it).getType(check);
-		if (!t.isString()) {
-		  throw TypeCheckingExceptionPrivate(n, "expecting string terms");
-		}
-		//if( (*it).getKind() != kind::CONST_STRING ) {
-		//  throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
-		//}
-	}
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      TypeNode t = (*it).getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting string terms");
+      }
+      //if( (*it).getKind() != kind::CONST_STRING ) {
+      //  throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
+      //}
+    }
     return nodeManager->regexpType();
   }
 };
@@ -435,17 +440,18 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-		TNode::iterator it = n.begin();
-		TypeNode t = (*it).getType(check);
-		if (!t.isString()) {
-		  throw TypeCheckingExceptionPrivate(n, "expecting string terms");
-		}
-		++it;
-		t = (*it).getType(check);
-		if (!t.isRegExp()) {
-		  throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-		}
-	}
+      TNode::iterator it = n.begin();
+      TNode::iterator it_end = n.end();
+      TypeNode t = (*it).getType(check);
+      if (!t.isString()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting string terms");
+      }
+      ++it;
+      t = (*it).getType(check);
+      if (!t.isRegExp()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
+      }
+    }
     return nodeManager->booleanType();
   }
 };
diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h
index 3dc12009b..1a101fa70 100644
--- a/src/theory/strings/type_enumerator.h
+++ b/src/theory/strings/type_enumerator.h
@@ -44,8 +44,8 @@ public:
     TypeEnumeratorBase<StringEnumerator>(type) {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == STRING_TYPE);
-	d_cardinality = 256;
-	mkCurr();
+    d_cardinality = 256;
+    mkCurr();
   }
   Node operator*() throw() {
     return d_curr;
@@ -89,10 +89,10 @@ private:
 	}
 public:
   StringEnumeratorLength(unsigned length, unsigned card = 256) : d_cardinality(card) {
-     for( unsigned i=0; i<length; i++ ){
-		d_data.push_back( 0 );
-	 }
-	 mkCurr();
+    for( unsigned i=0; i<length; i++ ){
+      d_data.push_back( 0 );
+	  }
+	  mkCurr();
   }
 
   Node operator*() throw() {
@@ -100,21 +100,21 @@ public:
   }
 
   StringEnumeratorLength& operator++() throw() {
-	bool changed = false;
-	for(unsigned i=0; i<d_data.size(); ++i) {
-		if( d_data[i] + 1 < d_cardinality ) {
-			++d_data[i]; changed = true;
-			break;
-		} else {
-			d_data[i] = 0;
-		}
-	}
-	
-	if(!changed) {
-		d_curr = Node::null();
-	}else{
-		mkCurr();
-	}
+    bool changed = false;
+    for(unsigned i=0; i<d_data.size(); ++i) {
+      if( d_data[i] + 1 < d_cardinality ) {
+        ++d_data[i]; changed = true;
+        break;
+      } else {
+        d_data[i] = 0;
+      }
+    }
+    
+    if(!changed) {
+      d_curr = Node::null();
+    }else{
+      mkCurr();
+    }
     return *this;
   }
 
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 3bc17b050..3e2fa948c 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -96,10 +96,7 @@ void String::getCharSet(std::set<unsigned int> &cset) const {
 }

 

 bool String::overlap(String &y) const {

-	unsigned n = y.size();

-	if(d_str.size() < y.size()) {

-		n = d_str.size();

-	}

+	unsigned n = d_str.size() < y.size() ? d_str.size() : y.size();

 	for(unsigned i=1; i<n; i++) {

 		String s = suffix(i);

 		String p = y.prefix(i);

diff --git a/src/util/regexp.h b/src/util/regexp.h
index 2bb2b5c4c..1ae01343d 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -34,29 +34,29 @@ namespace CVC4 {
 class CVC4_PUBLIC String {
 public:
   static unsigned int convertCharToUnsignedInt( char c ) {
-	int i = (int)c;
-	i = i-65;
-	return (unsigned int)(i<0 ? i+256 : i);
+    int i = (int)c;
+    i = i-65;
+    return (unsigned int)(i<0 ? i+256 : i);
   }
   static char convertUnsignedIntToChar( unsigned int i ){
-	int ii = i+65;
-	return (char)(ii>=256 ? ii-256 : ii);
+    int ii = i+65;
+    return (char)(ii>=256 ? ii-256 : ii);
   }
   static bool isPrintable( unsigned int i ){
-	char c = convertUnsignedIntToChar( i );
-	return isprint( (int)c );
+    char c = convertUnsignedIntToChar( i );
+    return isprint( (int)c );
   }
 
 private:
   std::vector<unsigned int> d_str;
 
   bool isVecSame(const std::vector<unsigned int> &a, const std::vector<unsigned int> &b) const {
-      if(a.size() != b.size()) return false;
-      else {
-          for(unsigned int i=0; i<a.size(); ++i)
-              if(a[i] != b[i]) return false;
-          return true;
-      }
+    if(a.size() != b.size()) return false;
+    else {
+      for(unsigned int i=0; i<a.size(); ++i)
+        if(a[i] != b[i]) return false;
+      return true;
+    }
   }
 
   //guarded
@@ -76,12 +76,12 @@ public:
   String() {}
 
   String(const std::string &s) {
-	toInternal(s);
+    toInternal(s);
   }
 
   String(const char* s) {
-	std::string stmp(s);
-	toInternal(stmp);
+    std::string stmp(s);
+    toInternal(stmp);
   }
 
   String(const char c) {
@@ -114,53 +114,53 @@ public:
   bool operator <(const String& y) const {
     if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size();
     else {
-        for(unsigned int i=0; i<d_str.size(); ++i)
-            if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
+      for(unsigned int i=0; i<d_str.size(); ++i)
+        if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
 
-        return false;
+      return false;
     }
   }
 
   bool operator >(const String& y) const {
     if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size();
     else {
-        for(unsigned int i=0; i<d_str.size(); ++i)
-            if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
+      for(unsigned int i=0; i<d_str.size(); ++i)
+        if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
 
-        return false;
+      return false;
     }
   }
 
   bool operator <=(const String& y) const {
     if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size();
     else {
-        for(unsigned int i=0; i<d_str.size(); ++i)
-            if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
+      for(unsigned int i=0; i<d_str.size(); ++i)
+        if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
 
-        return true;
+      return true;
     }
   }
 
   bool operator >=(const String& y) const {
     if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size();
     else {
-        for(unsigned int i=0; i<d_str.size(); ++i)
-            if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
+      for(unsigned int i=0; i<d_str.size(); ++i)
+        if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
 
-        return true;
+      return true;
     }
   }
 
   bool strncmp(const String &y, unsigned int n) const {
-      for(unsigned int i=0; i<n; ++i)
-          if(d_str[i] != y.d_str[i]) return false;
-      return true;
+    for(unsigned int i=0; i<n; ++i)
+      if(d_str[i] != y.d_str[i]) return false;
+    return true;
   }
 
   bool rstrncmp(const String &y, unsigned int n) const {
-      for(unsigned int i=0; i<n; ++i)
-          if(d_str[d_str.size() - i - 1] != y.d_str[y.d_str.size() - i - 1]) return false;
-      return true;
+    for(unsigned int i=0; i<n; ++i)
+      if(d_str[d_str.size() - i - 1] != y.d_str[y.d_str.size() - i - 1]) return false;
+    return true;
   }
 
   bool isEmptyString() const {
@@ -229,16 +229,16 @@ public:
   }
 
   String replace(const String &s, const String &t) const {
-	std::size_t ret = find(s);
-	if( ret != std::string::npos ) {
-		std::vector<unsigned int> vec;
-		vec.insert(vec.begin(), d_str.begin(), d_str.begin() + ret); 
-		vec.insert(vec.end(), t.d_str.begin(), t.d_str.end());
-		vec.insert(vec.end(), d_str.begin() + ret + s.d_str.size(), d_str.end());
-		return String(vec);
-	} else {
-		return *this;
-	}
+    std::size_t ret = find(s);
+    if( ret != std::string::npos ) {
+      std::vector<unsigned int> vec;
+      vec.insert(vec.begin(), d_str.begin(), d_str.begin() + ret); 
+      vec.insert(vec.end(), t.d_str.begin(), t.d_str.end());
+      vec.insert(vec.end(), d_str.begin() + ret + s.d_str.size(), d_str.end());
+      return String(vec);
+    } else {
+      return *this;
+    }
   }
 
   String substr(unsigned i) const {