adds some fixes. it solves kaluza problems

2 files changed, 705 insertions, 532 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 291af408b..a0058954d 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -96,14 +96,18 @@ bool TheoryStrings::areDisequal( Node a, Node b ){
   }
 }
 
-Node TheoryStrings::getLength( Node t ) {
-	EqcInfo * ei = getOrMakeEqcInfo( t );
-	Node length_term = ei->d_length_term;
+Node TheoryStrings::getLengthTerm( Node t ) {
+	EqcInfo * ei = getOrMakeEqcInfo( t, false );
+	Node length_term = ei ? ei->d_length_term : Node::null();
 	if( length_term.isNull()) {
 		//typically shouldnt be necessary
 		length_term = t;
 	}
-	return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term );
+	return length_term;
+}
+
+Node TheoryStrings::getLength( Node t ) {
+	return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) );
 }
 
 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -194,23 +198,29 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 	seperateByLength( nodes, col, lts );
 	//step 1 : get all values for known lengths
 	std::vector< Node > lts_values;
-	//std::map< Node, bool > values_used;
+	std::map< unsigned, bool > values_used;
 	for( unsigned i=0; i<col.size(); i++ ){
-		Trace("strings-model") << "Checking length for " << col[i][0] << " (length is " << lts[i] << ")" << std::endl;
+		Trace("strings-model") << "Checking length for {";
+		for( unsigned j=0; j<col[i].size(); j++ ){
+			if( j>0 ) Trace("strings-model") << ", ";
+			Trace("strings-model") << col[i][j];
+		}
+		Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl;
 		if( lts[i].isConst() ){
 			lts_values.push_back( lts[i] );
-			//values_used[ lts[i] ] = true;
+			unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt();
+			values_used[ lvalue ] = true;
 		}else{
 			//get value for lts[i];
 			if( !lts[i].isNull() ){
 				Node v = d_valuation.getModelValue(lts[i]);
-				//Node v = m->getValue(lts[i]);
 				Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl;
 				lts_values.push_back( v );
-				//values_used[ v ] = true;
+				unsigned lvalue =  v.getConst<Rational>().getNumerator().toUnsignedInt();
+				values_used[ lvalue ] = true;
 			}else{
-				Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl;
-				Assert( false );
+				//Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl;
+				//Assert( false );
 				lts_values.push_back( Node::null() );
 			}
 		}
@@ -240,26 +250,39 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 		}
 		Trace("strings-model") << "have length " << lts_values[i] << std::endl;
 		
-		Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes ";
-		for( unsigned j=0; j<pure_eq.size(); j++ ){
-			Trace("strings-model") << pure_eq[j] << " ";
-		}
-		Trace("strings-model") << std::endl;
-
-		//use type enumerator
-		StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt());
-		for( unsigned j=0; j<pure_eq.size(); j++ ){
-			Assert( !sel.isFinished() );
-			Node c = *sel;
-			while( d_equalityEngine.hasTerm( c ) ){
-				++sel;
+		//assign a new length if necessary
+		if( !pure_eq.empty() ){
+			if( lts_values[i].isNull() ){
+				unsigned lvalue = 0;
+				while( values_used.find( lvalue )!=values_used.end() ){
+					lvalue++;	
+				}
+				Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl;
+				lts_values[i] = NodeManager::currentNM()->mkConst( Rational( lvalue ) );
+				values_used[ lvalue ] = true;
+			}
+			Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes ";
+			for( unsigned j=0; j<pure_eq.size(); j++ ){
+				Trace("strings-model") << pure_eq[j] << " ";
+			}
+			Trace("strings-model") << std::endl;
+
+
+			//use type enumerator
+			StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt());
+			for( unsigned j=0; j<pure_eq.size(); j++ ){
 				Assert( !sel.isFinished() );
-				c = *sel;
+				Node c = *sel;
+				while( d_equalityEngine.hasTerm( c ) ){
+					++sel;
+					Assert( !sel.isFinished() );
+					c = *sel;
+				}
+				++sel;
+				Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl;
+				processed[pure_eq[j]] = c;
+				m->assertEquality( pure_eq[j], c, true );
 			}
-			++sel;
-			Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl;
-			processed[pure_eq[j]] = c;
-			m->assertEquality( pure_eq[j], c, true );
 		}
 	}
 	Trace("strings-model") << "String Model : Finished." << std::endl;
@@ -363,65 +386,21 @@ void TheoryStrings::check(Effort e) {
 
   bool addedLemma = false;
   if( e == EFFORT_FULL && !d_conflict ) {
-      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::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){
-					if( d_length_inst.find(n)==d_length_inst.end() ){
-						d_length_inst[n] = true;
-						Trace("strings-debug") << "get n: " << n << endl;
-						Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
-						d_length_intro_vars.push_back( sk );
-						Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
-						eq = Rewriter::rewrite(eq);
-						Trace("strings-lemma") << "Strings: Add term lemma " << eq << std::endl;
-						d_out->lemma(eq);
-						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 = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
-						}else{
-							//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: Add length lemma " << ceq << std::endl;
-						d_out->lemma(ceq);
-						addedLemma = true;
-					}
-				}
-				++eqc_i;
-			}
-        }
-        ++eqcs_i;
-	  }
+      addedLemma = checkLengths();
+	  Trace("strings-process") << "Done check (constant) lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
 	  if( !addedLemma ){
 		  addedLemma = checkNormalForms();
 		  Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
 		  if(!d_conflict && !addedLemma) {
-			  addedLemma = checkCardinality();
-			  Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-			  if( !d_conflict && !addedLemma ){
-				addedLemma = checkInductiveEquations();
-				Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+			  addedLemma = checkLengthsEqc();
+			  Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+			  if(!d_conflict && !addedLemma) {
+				  addedLemma = checkCardinality();
+				  Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+				  if( !d_conflict && !addedLemma ){
+					addedLemma = checkInductiveEquations();
+					Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+				  }
 			  }
 		  }
 	  }
@@ -430,7 +409,7 @@ void TheoryStrings::check(Effort e) {
   Trace("strings-process") << "Theory of strings, done check : " << e << std::endl;
 }
 
-TheoryStrings::EqcInfo::EqcInfo(  context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c) {
+TheoryStrings::EqcInfo::EqcInfo(  context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) {
 
 }
 
@@ -492,6 +471,9 @@ void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){
         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;
@@ -572,16 +554,17 @@ void TheoryStrings::doPendingLemmas() {
   }
 }
 
-void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
+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) {
     // EqcItr
     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
     while( !eqc_i.isFinished() ) {
         Node n = (*eqc_i);
-        Trace("strings-process") << "Process term " << n << std::endl;
+        Trace("strings-process-debug") << "Get Normal Form : Process term " << n << std::endl;
         if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
             std::vector<Node> nf_n;
             std::vector<Node> nf_exp_n;
+			bool result = true;
             if( n.getKind() == kind::CONST_STRING  ){
                 if( n!=d_emptyString ) {
                     nf_n.push_back( n );
@@ -591,37 +574,88 @@ void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
                     Node nr = d_equalityEngine.getRepresentative( n[i] );
                     std::vector< Node > nf_temp;
                     std::vector< Node > nf_exp_temp;
-                    Trace("strings-process") << "Normalizing subterm " << n[i] << " = "  << nr << std::endl;
-                    normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp );
+                    Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = "  << nr << std::endl;
+                    bool nresult = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp );
                     if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
-                        return;
-                    }
-                    if( nf.size()!=1 || nf[0]!=d_emptyString ) {
-                        for( unsigned r=0; r<nf_temp.size(); r++ ) {
-                            Assert( nf_temp[r].getKind()!=kind::STRING_CONCAT );
-                        }
-                        nf_n.insert( nf_n.end(), nf_temp.begin(), nf_temp.end() );
-                    }
-                    nf_exp_n.insert( nf_exp_n.end(), nf_exp_temp.begin(), nf_exp_temp.end() );
-                    if( nr!=n[i] ) {
-                        nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) );
+                        return true;
                     }
+					//successfully computed normal form
+					if( nf.size()!=1 || nf[0]!=d_emptyString ) {
+						for( unsigned r=0; r<nf_temp.size(); r++ ) {
+							Assert( !nresult || nf_temp[r].getKind()!=kind::STRING_CONCAT );
+						}
+						nf_n.insert( nf_n.end(), nf_temp.begin(), nf_temp.end() );
+					}
+					nf_exp_n.insert( nf_exp_n.end(), nf_exp_temp.begin(), nf_exp_temp.end() );
+					if( nr!=n[i] ) {
+						nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) );
+					}
+					if( !nresult ){
+						//Trace("strings-process-debug") << "....Caused already asserted 
+						for( unsigned j=i+1; j<n.getNumChildren(); j++ ){
+							if( !areEqual( n[j], d_emptyString ) ){
+								nf_n.push_back( n[j] );
+							}
+						}
+						if( nf_n.size()>1 ){
+							result = false;
+							break;
+						}
+					}
                 }
             }
-            normal_forms.push_back(nf_n);
-            normal_forms_exp.push_back(nf_exp_n);
-            normal_form_src.push_back(n);
+			if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ){
+				if( nf_n.size()>1 ){
+					Trace("strings-process-debug") << "Check for component lemmas for normal form "; 
+					printConcat(nf_n,"strings-process-debug");
+					Trace("strings-process-debug") << "..." << std::endl;
+					for( unsigned i=0; i<nf_n.size(); i++ ){
+						//if a component is equal to whole,
+						if( areEqual( nf_n[i], n ) ){
+							//all others must be empty
+							std::vector< Node > ant;
+							if( nf_n[i]!=n ){
+								ant.push_back( nf_n[i].eqNode( n ) );
+							}
+							ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() );
+							std::vector< Node > cc;
+							for( unsigned j=0; j<nf_n.size(); j++ ){
+								if( i!=j ){
+									cc.push_back( nf_n[j].eqNode( d_emptyString ) );
+								}
+							}
+							std::vector< Node > empty_vec;
+							Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
+							sendLemma( mkExplain( ant ), conc, "Component" );
+							return true;
+						}
+					}
+				}
+				if( !result ){
+					//we have a normal form that will cause a component lemma at a higher level
+					normal_forms.clear();
+					normal_forms_exp.clear();
+					normal_form_src.clear();
+				}
+				normal_forms.push_back(nf_n);
+				normal_forms_exp.push_back(nf_exp_n);
+				normal_form_src.push_back(n);
+				if( !result ){
+					return false;
+				}
+			}else{
+				Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0];
+				//Assert( areEqual( nf_n[0], eqc ) );
+				if( !areEqual( nn, eqc ) ){
+					std::vector< Node > ant;
+					ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() );
+					ant.push_back( n.eqNode( eqc ) );
+					Node conc = nn.eqNode( eqc );
+					sendLemma( mkExplain( ant ), conc, "Trivial Equal Normal Form" );
+					return true;
+				}
+			}
         }
-        /* should we add these?
-        else {
-            //var/sk?
-            std::vector<Node> nf_n;
-            std::vector<Node> nf_exp_n;
-            nf_n.push_back(n);
-            normal_forms.push_back(nf_n);
-            normal_forms_exp.push_back(nf_exp_n);
-            normal_form_src.push_back(n);
-        }*/
         ++eqc_i;
     }
 
@@ -647,29 +681,36 @@ void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
             Trace("strings-solve") << std::endl;
         }
     }
+	return true;
 }
 //nf_exp is conjunction
-void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) {
+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() ){
-        //nf.push_back( eqc );
+        nf.push_back( eqc );
+		/*
         if( eqc.getKind()==kind::STRING_CONCAT ){
             for( unsigned i=0; i<eqc.getNumChildren(); i++ ){
-				if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc[i], d_emptyString ) ){
+				if( !areEqual( eqc[i], d_emptyString ) ){
 					nf.push_back( eqc[i] );
 				}
             }
-        }else if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc, d_emptyString ) ){
+        }else if(  !areEqual( eqc, d_emptyString ) ){
             nf.push_back( eqc );
         }
+		*/
         Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
-    } else if (d_equalityEngine.hasTerm(d_emptyString) && d_equalityEngine.areEqual( eqc, d_emptyString )){
+		return false;
+    } else if( areEqual( eqc, d_emptyString ) ){
         //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)
@@ -679,337 +720,336 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
             // record terms for each normal form (t)
             std::vector< Node > normal_form_src;
             //Get Normal Forms
-            getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src);
+            result = getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src);
             if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
-                return;
-            }
-
-            unsigned i = 0;
-            //unify each normal form > 0 with normal_forms[0]
-            for( unsigned j=1; j<normal_forms.size(); j++ ) {
-
-                Trace("strings-solve") << "Process normal form #0 against #" << j << "..." << std::endl;
-                if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ){
-                    Trace("strings-solve") << "Already normalized (in cache)." << std::endl;
-                }else{
-                    Trace("strings-solve") << "Not in cache." << std::endl;
-                    //the current explanation for why the prefix is equal
-                    std::vector< Node > curr_exp;
-                    curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() );
-                    curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() );
-                    curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) );
-                    //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality
-                    unsigned index_i = 0;
-                    unsigned index_j = 0;
-                    bool success;
-                    do
-                    {
-                        success = false;
-                        //if we are at the end
-                        if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
-                            if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ){
-                                //we're done
-                                addNormalFormPair( normal_form_src[i], normal_form_src[j] );
-                            }else{
-                                //the remainder must be empty
-                                unsigned k = index_i==normal_forms[i].size() ? j : i;
-                                unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i;
-                                while(!d_conflict && index_k<normal_forms[k].size()) {
-                                    //can infer that this string must be empty
-                                    Node eq_exp;
-                                    if( curr_exp.empty() ) {
-                                        eq_exp = d_true;
-                                    } else if( curr_exp.size() == 1 ) {
-                                        eq_exp = curr_exp[0];
-                                    } else {
-                                        eq_exp = NodeManager::currentNM()->mkNode( kind::AND, curr_exp );
-                                    }
-                                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] );
-                                    Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
-									Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) );
-                                    d_pending.push_back( eq );
-                                    d_pending_exp[eq] = eq_exp;
-                                    d_infer.push_back(eq);
-                                    d_infer_exp.push_back(eq_exp);
-                                    index_k++;
-                                }
-                            }
-                        }else {
-                            Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl;
-                            if(areEqual(normal_forms[i][index_i],normal_forms[j][index_j])){
-                                Trace("strings-solve-debug") << "Case 1 : strings are equal" << std::endl;
-                                //terms are equal, continue
-                                if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){
-                                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,normal_forms[i][index_i],
-                                                                                                     normal_forms[j][index_j]);
-                                    Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl;
-                                    curr_exp.push_back(eq);
-                                }
-                                index_j++;
-                                index_i++;
-                                success = true;
-                            }else{
-								Node length_term_i = getLength( normal_forms[i][index_i] );
-								Node length_term_j = getLength( normal_forms[j][index_j] );
-                                //check  length(normal_forms[i][index]) == length(normal_forms[j][index])
-                                if( !areDisequal(length_term_i, length_term_j) &&
-									normal_forms[i][index_i].getKind()!=kind::CONST_STRING && 
-									normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) {
-		
-									//length terms are equal, merge equivalence classes if not already done so
-									Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j );
-									if( !areEqual(length_term_i, length_term_j) ) {
-										Trace("strings-solve-debug") << "Case 2.1 : string lengths neither equal nor disequal" << std::endl;
-										//try to make the lengths equal via splitting on demand
-										sendSplit( length_term_i, length_term_j, "Length" );
-										length_eq = Rewriter::rewrite( length_eq  );
-										d_pending_req_phase[ length_eq ] = true;
-										return;
-									}else{
-										Trace("strings-solve-debug") << "Case 2.2 : string lengths are explicitly equal" << std::endl;
-										//lengths are already equal, do unification
-										Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] );
-										std::vector< Node > temp_exp;
-										temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
-										temp_exp.push_back(length_eq);
-										Node eq_exp = temp_exp.empty() ? d_true :
-														temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp );
+                return true;
+            }else if( result ){
+				unsigned i = 0;
+				//unify each normal form > 0 with normal_forms[0]
+				for( unsigned j=1; j<normal_forms.size(); j++ ) {
+					Trace("strings-solve") << "Process normal form #0 against #" << j << "..." << std::endl;
+					if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ){
+						Trace("strings-solve") << "Already normalized (in cache)." << std::endl;
+					}else{
+						Trace("strings-solve") << "Not in cache." << std::endl;
+						//the current explanation for why the prefix is equal
+						std::vector< Node > curr_exp;
+						curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() );
+						curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() );
+						curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) );
+						//ensure that normal_forms[i] and normal_forms[j] are the same modulo equality
+						unsigned index_i = 0;
+						unsigned index_j = 0;
+						bool success;
+						do
+						{
+							success = false;
+							//if we are at the end
+							if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
+								if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ){
+									//we're done
+									addNormalFormPair( normal_form_src[i], normal_form_src[j] );
+								}else{
+									//the remainder must be empty
+									unsigned k = index_i==normal_forms[i].size() ? j : i;
+									unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i;
+									while(!d_conflict && index_k<normal_forms[k].size()) {
+										//can infer that this string must be empty
+										Node eq_exp;
+										if( curr_exp.empty() ) {
+											eq_exp = d_true;
+										} else if( curr_exp.size() == 1 ) {
+											eq_exp = curr_exp[0];
+										} else {
+											eq_exp = NodeManager::currentNM()->mkNode( kind::AND, curr_exp );
+										}
+										Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] );
 										Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
+										Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) );
 										d_pending.push_back( eq );
 										d_pending_exp[eq] = eq_exp;
 										d_infer.push_back(eq);
 										d_infer_exp.push_back(eq_exp);
-										return;
-									}
-								}else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || 
-										  ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){
-									Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl;
-                                    Node conc;
-                                    std::vector< Node > antec;
-									antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-                                    std::vector< Node > antec_new_lits;
-									std::vector< Node > eqn;
-									for( unsigned r=0; r<2; r++ ){
-										int index_k = r==0 ? index_i : index_j;
-										int k = r==0 ? i : j;
-										std::vector< Node > eqnc;
-										for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ){
-											eqnc.push_back( normal_forms[k][index_l] );
-										}
-										eqn.push_back( mkConcat( eqnc ) );
+										index_k++;
 									}
-									if( areEqual( eqn[0], eqn[1] ) ){
-										addNormalFormPair( normal_form_src[i], normal_form_src[j] );
-									}else{
-										conc = eqn[0].eqNode( eqn[1] );
-										Node ant = mkExplain( antec, antec_new_lits );
-										sendLemma( ant, conc, "Endpoint" );
-										return;
+								}
+							}else {
+								Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl;
+								if(areEqual(normal_forms[i][index_i],normal_forms[j][index_j])){
+									Trace("strings-solve-debug") << "Case 1 : strings are equal" << std::endl;
+									//terms are equal, continue
+									if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){
+										Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,normal_forms[i][index_i],
+																										 normal_forms[j][index_j]);
+										Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl;
+										curr_exp.push_back(eq);
 									}
+									index_j++;
+									index_i++;
+									success = true;
 								}else{
-                                    Trace("strings-solve-debug") << "Case 4 : must compare strings" << std::endl;
-                                    Node conc;
-                                    std::vector< Node > antec;
-                                    std::vector< Node > antec_new_lits;
-                                    //check for loops
-                                    //Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl;
-                                    int has_loop[2] = { -1, -1 };
-                                    for( unsigned r=0; r<2; r++ ){
-                                        int index = (r==0 ? index_i : index_j);
-                                        int other_index = (r==0 ? index_j : index_i );
-                                        int n_index = (r==0 ? i : j);
-                                        int other_n_index = (r==0 ? j : i);
-                                        if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) {
-                                            for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){
-                                                if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){
-                                                    has_loop[r] = lp;
-                                                    break;
-                                                }
-                                            }
-                                        }
-                                    }
-                                    if( has_loop[0]!=-1 || has_loop[1]!=-1 ){
-                                        int loop_n_index = has_loop[0]!=-1 ? i : j;
-                                        int other_n_index = has_loop[0]!=-1 ? j : i;
-                                        int loop_index = has_loop[0]!=-1 ? has_loop[0] : has_loop[1];
-                                        int index = has_loop[0]!=-1 ? index_i : index_j;
-                                        int other_index = has_loop[0]!=-1 ? index_j : index_i;
-                                        Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index];
-                                        Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl;
-										
-										Trace("strings-loop") << " ... T(Y.Z)= ";
-										for(int lp=index; lp<loop_index; ++lp) {
-											if(lp != index) Trace("strings-loop") << " ++ ";
-											Trace("strings-loop") << normal_forms[loop_n_index][lp];
-										}
-										Trace("strings-loop") << std::endl;
-										Trace("strings-loop") << " ... S(Z.Y)= ";
-										for(int lp=other_index+1; lp<(int)normal_forms[other_n_index].size(); ++lp) {
-											if(lp != other_index+1) Trace("strings-loop") << " ++ ";
-											Trace("strings-loop") << normal_forms[other_n_index][lp];
+									Node length_term_i = getLength( normal_forms[i][index_i] );
+									Node length_term_j = getLength( normal_forms[j][index_j] );
+									//check  length(normal_forms[i][index]) == length(normal_forms[j][index])
+									if( !areDisequal(length_term_i, length_term_j) &&
+										normal_forms[i][index_i].getKind()!=kind::CONST_STRING && 
+										normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) {
+			
+										//length terms are equal, merge equivalence classes if not already done so
+										Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j );
+										if( !areEqual(length_term_i, length_term_j) ) {
+											Trace("strings-solve-debug") << "Case 2.1 : string lengths neither equal nor disequal" << std::endl;
+											//try to make the lengths equal via splitting on demand
+											sendSplit( length_term_i, length_term_j, "Length" );
+											length_eq = Rewriter::rewrite( length_eq  );
+											d_pending_req_phase[ length_eq ] = true;
+											return true;
+										}else{
+											Trace("strings-solve-debug") << "Case 2.2 : string lengths are explicitly equal" << std::endl;
+											//lengths are already equal, do unification
+											Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] );
+											std::vector< Node > temp_exp;
+											temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
+											temp_exp.push_back(length_eq);
+											Node eq_exp = temp_exp.empty() ? d_true :
+															temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp );
+											Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
+											d_pending.push_back( eq );
+											d_pending_exp[eq] = eq_exp;
+											d_infer.push_back(eq);
+											d_infer_exp.push_back(eq_exp);
+											return true;
 										}
-										Trace("strings-loop") << std::endl;
-										Trace("strings-loop") << " ... R= ";
-										for(int lp=loop_index+1; lp<(int)normal_forms[loop_n_index].size(); ++lp) {
-											if(lp != loop_index+1) Trace("strings-loop") << " ++ ";
-											Trace("strings-loop") << normal_forms[loop_n_index][lp];
-										}
-										Trace("strings-loop") << std::endl;
-
-                                        //we have x * s1 * .... * sm = t1 * ... * tn * x * r1 * ... * rp
-                                        //check if
-                                        //t1 * ... * tn = n[loop_n_index][index]....n[loop_n_index][loop_index-1] = y * z
-                                        // and
-                                        //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] = z * y
-                                        // for some y,z,k
-
-										Trace("strings-loop") << "Must add lemma." << std::endl;
-										//need to break
-										Node sk_y= NodeManager::currentNM()->mkSkolem( "ysym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
-										Node sk_z= NodeManager::currentNM()->mkSkolem( "zsym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
-
+									}else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || 
+											  ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){
+										Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl;
+										Node conc;
+										std::vector< Node > antec;
 										antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-										//require that x is non-empty
-										Node x_empty = normal_forms[loop_n_index][loop_index].eqNode( d_emptyString );
-										x_empty = Rewriter::rewrite( x_empty );
-										//if( d_equalityEngine.hasTerm( d_emptyString ) && d_equalityEngine.areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString, true ) ){
-										//	antec.push_back( x_empty.negate() );
-										//}else{
-										antec_new_lits.push_back( x_empty.negate() );
-										//}
-										d_pending_req_phase[ x_empty ] = true;
-
-
-										//t1 * ... * tn = y * z
-										std::vector< Node > c1c;
-										//n[loop_n_index][index]....n[loop_n_index][loop_lindex-1]
-										for( int r=index; r<=loop_index-1; r++ ) {
-											c1c.push_back( normal_forms[loop_n_index][r] );
+										std::vector< Node > antec_new_lits;
+										std::vector< Node > eqn;
+										for( unsigned r=0; r<2; r++ ){
+											int index_k = r==0 ? index_i : index_j;
+											int k = r==0 ? i : j;
+											std::vector< Node > eqnc;
+											for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ){
+												eqnc.push_back( normal_forms[k][index_l] );
+											}
+											eqn.push_back( mkConcat( eqnc ) );
 										}
-										Node conc1 = mkConcat( c1c );
-										conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1,
-														NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) );
-										std::vector< Node > c2c;
-										//s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1]
-										for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) {
-											c2c.push_back( normal_forms[other_n_index][r] );
+										if( areEqual( eqn[0], eqn[1] ) ){
+											addNormalFormPair( normal_form_src[i], normal_form_src[j] );
+										}else{
+											conc = eqn[0].eqNode( eqn[1] );
+											Node ant = mkExplain( antec, antec_new_lits );
+											sendLemma( ant, conc, "Endpoint" );
+											return true;
 										}
-										Node left2 = mkConcat( c2c );
-										std::vector< Node > c3c;
-										c3c.push_back( sk_z );
-										c3c.push_back( sk_y );
-										//r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1]
-										for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) {
-											c3c.push_back( normal_forms[loop_n_index][r] );
+									}else{
+										Trace("strings-solve-debug") << "Case 4 : must compare strings" << std::endl;
+										Node conc;
+										std::vector< Node > antec;
+										std::vector< Node > antec_new_lits;
+										//check for loops
+										//Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl;
+										int has_loop[2] = { -1, -1 };
+										for( unsigned r=0; r<2; r++ ){
+											int index = (r==0 ? index_i : index_j);
+											int other_index = (r==0 ? index_j : index_i );
+											int n_index = (r==0 ? i : j);
+											int other_n_index = (r==0 ? j : i);
+											if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) {
+												for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){
+													if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){
+														has_loop[r] = lp;
+														break;
+													}
+												}
+											}
 										}
-										Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2,
-														mkConcat( c3c ) );
-										
-										Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y );
-										//Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z );
-										//Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y_len, d_zero);
-										//Node len_z_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z_len, d_zero);
-										//Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y, d_emptyString);
-										//Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, len_z_eq_zero, len_y_eq_zero);
-										
-										//Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate();
-										//Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, 
-										//						NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]),
-										//						sk_y_len );
-										Node ant = mkExplain( antec, antec_new_lits );
-										conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y
-
-										//Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString);
-										//conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc );
-
-										//we will be done
-										addNormalFormPair( normal_form_src[i], normal_form_src[j] );
-										sendLemma( ant, conc, "Loop" );
-										addInductiveEquation( normal_forms[other_n_index][other_index], sk_y, sk_z, ant, "Loop Induction" );
-										return;
-                                    }else{
-                                        Trace("strings-solve-debug") << "No loops detected." << std::endl;
-                                        if( normal_forms[i][index_i].getKind() == kind::CONST_STRING ||
-                                            normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
-											unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j;
-											unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j;
-											unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i;
-											unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i;
-                                            Node const_str = normal_forms[const_k][const_index_k];
-                                            Node other_str = normal_forms[nconst_k][nconst_index_k];
-                                            if( other_str.getKind() == kind::CONST_STRING ) {
-                                                unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
-                                                if( const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short) ) {
-                                                    //same prefix
-                                                    //k is the index of the string that is shorter
-                                                    int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j;
-                                                    int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j;
-                                                    int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i;
-                                                    int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i;
-                                                    Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(len_short) );
-                                                    Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
-                                                    normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
-                                                    normal_forms[l][index_l] = normal_forms[k][index_k];
-                                                    success = true;
-                                                } else {
-                                                    //curr_exp is conflict
-                                                    antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+										if( has_loop[0]!=-1 || has_loop[1]!=-1 ){
+											int loop_n_index = has_loop[0]!=-1 ? i : j;
+											int other_n_index = has_loop[0]!=-1 ? j : i;
+											int loop_index = has_loop[0]!=-1 ? has_loop[0] : has_loop[1];
+											int index = has_loop[0]!=-1 ? index_i : index_j;
+											int other_index = has_loop[0]!=-1 ? index_j : index_i;
+											Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index];
+											Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl;
+											
+											Trace("strings-loop") << " ... T(Y.Z)= ";
+											for(int lp=index; lp<loop_index; ++lp) {
+												if(lp != index) Trace("strings-loop") << " ++ ";
+												Trace("strings-loop") << normal_forms[loop_n_index][lp];
+											}
+											Trace("strings-loop") << std::endl;
+											Trace("strings-loop") << " ... S(Z.Y)= ";
+											for(int lp=other_index+1; lp<(int)normal_forms[other_n_index].size(); ++lp) {
+												if(lp != other_index+1) Trace("strings-loop") << " ++ ";
+												Trace("strings-loop") << normal_forms[other_n_index][lp];
+											}
+											Trace("strings-loop") << std::endl;
+											Trace("strings-loop") << " ... R= ";
+											for(int lp=loop_index+1; lp<(int)normal_forms[loop_n_index].size(); ++lp) {
+												if(lp != loop_index+1) Trace("strings-loop") << " ++ ";
+												Trace("strings-loop") << normal_forms[loop_n_index][lp];
+											}
+											Trace("strings-loop") << std::endl;
+
+											//we have x * s1 * .... * sm = t1 * ... * tn * x * r1 * ... * rp
+											//check if
+											//t1 * ... * tn = n[loop_n_index][index]....n[loop_n_index][loop_index-1] = y * z
+											// and
+											//s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] = z * y
+											// for some y,z,k
+
+											Trace("strings-loop") << "Must add lemma." << std::endl;
+											//need to break
+											Node sk_y= NodeManager::currentNM()->mkSkolem( "ysym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
+											Node sk_z= NodeManager::currentNM()->mkSkolem( "zsym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
+
+											antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+											//require that x is non-empty
+											Node x_empty = normal_forms[loop_n_index][loop_index].eqNode( d_emptyString );
+											x_empty = Rewriter::rewrite( x_empty );
+											//if( d_equalityEngine.hasTerm( d_emptyString ) && d_equalityEngine.areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString, true ) ){
+											//	antec.push_back( x_empty.negate() );
+											//}else{
+											antec_new_lits.push_back( x_empty.negate() );
+											//}
+											d_pending_req_phase[ x_empty ] = true;
+
+
+											//t1 * ... * tn = y * z
+											std::vector< Node > c1c;
+											//n[loop_n_index][index]....n[loop_n_index][loop_lindex-1]
+											for( int r=index; r<=loop_index-1; r++ ) {
+												c1c.push_back( normal_forms[loop_n_index][r] );
+											}
+											Node conc1 = mkConcat( c1c );
+											conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1,
+															NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) );
+											std::vector< Node > c2c;
+											//s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1]
+											for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) {
+												c2c.push_back( normal_forms[other_n_index][r] );
+											}
+											Node left2 = mkConcat( c2c );
+											std::vector< Node > c3c;
+											c3c.push_back( sk_z );
+											c3c.push_back( sk_y );
+											//r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1]
+											for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) {
+												c3c.push_back( normal_forms[loop_n_index][r] );
+											}
+											Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2,
+															mkConcat( c3c ) );
+											
+											Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y );
+											//Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z );
+											//Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y_len, d_zero);
+											//Node len_z_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z_len, d_zero);
+											//Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y, d_emptyString);
+											//Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, len_z_eq_zero, len_y_eq_zero);
+											
+											//Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate();
+											//Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, 
+											//						NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]),
+											//						sk_y_len );
+											Node ant = mkExplain( antec, antec_new_lits );
+											conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y
+
+											//Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString);
+											//conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc );
+
+											//we will be done
+											addNormalFormPair( normal_form_src[i], normal_form_src[j] );
+											sendLemma( ant, conc, "Loop" );
+											addInductiveEquation( normal_forms[other_n_index][other_index], sk_y, sk_z, ant, "Loop Induction" );
+											return true;
+										}else{
+											Trace("strings-solve-debug") << "No loops detected." << std::endl;
+											if( normal_forms[i][index_i].getKind() == kind::CONST_STRING ||
+												normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
+												unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j;
+												unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j;
+												unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i;
+												unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i;
+												Node const_str = normal_forms[const_k][const_index_k];
+												Node other_str = normal_forms[nconst_k][nconst_index_k];
+												if( other_str.getKind() == kind::CONST_STRING ) {
+													unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
+													if( const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short) ) {
+														//same prefix
+														//k is the index of the string that is shorter
+														int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j;
+														int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j;
+														int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i;
+														int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i;
+														Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(len_short) );
+														Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
+														normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
+														normal_forms[l][index_l] = normal_forms[k][index_k];
+														success = true;
+													} else {
+														//curr_exp is conflict
+														antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+														Node ant = mkExplain( antec, antec_new_lits );
+														sendLemma( ant, conc, "Conflict" );
+														return true;
+													}
+												} else {
+													Assert( other_str.getKind()!=kind::STRING_CONCAT );
+													antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+													Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
+														NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
+													//split the string
+													Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/c split" );
+
+													Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString );
+													Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str,
+																NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) );
+													conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
+													Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
+
 													Node ant = mkExplain( antec, antec_new_lits );
-													sendLemma( ant, conc, "Conflict" );
-													return;
-                                                }
-                                            } else {
-                                                Assert( other_str.getKind()!=kind::STRING_CONCAT );
-                                                antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-												Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
-													NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
-												//split the string
-												Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/c split" );
-
-												Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString );
-												Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str,
-															NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) );
+													sendLemma( ant, conc, "Constant Split" );
+													return true;
+												}
+											}else{
+												antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+
+												Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
+												if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){
+													antec.push_back( ldeq );
+												}else{
+													antec_new_lits.push_back(ldeq);
+												}
+												Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/v split" );
+												Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i],
+															NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) );
+												Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j],
+															NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) );
 												conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
-                                                Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
+												// |sk| > 0
+												//Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
+												//Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero);
+												Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate();
+												Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl;
+												//d_out->lemma(sk_gt_zero);
+												d_lemma_cache.push_back( sk_gt_zero );
 
 												Node ant = mkExplain( antec, antec_new_lits );
-												sendLemma( ant, conc, "Constant Split" );
-												return;
-                                            }
-                                        }else{
-                                            antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-
-											Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
-											if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){
-												antec.push_back( ldeq );
-											}else{
-												antec_new_lits.push_back(ldeq);
+												sendLemma( ant, conc, "Split" );
+												return true;
 											}
-											Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/v split" );
-											Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i],
-														NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) );
-											Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j],
-														NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) );
-											conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
-											// |sk| > 0
-											//Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-											//Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero);
-											Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate();
-											Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl;
-											//d_out->lemma(sk_gt_zero);
-											d_lemma_cache.push_back( sk_gt_zero );
-
-											Node ant = mkExplain( antec, antec_new_lits );
-											sendLemma( ant, conc, "Split" );
-											return;
-                                        }
-                                    }
-                                }
-                            }
-                        }
-                    }while(success);
-                }
-            }
+										}
+									}
+								}
+							}
+						}while(success);
+					}
+				}
+			}
 
             //construct the normal form
             if( normal_forms.empty() ){
@@ -1025,18 +1065,19 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                 }
                 Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl;
             }
-            //if( visited.empty() ){
-                //TODO : cache?
-            //}
+
+    	    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." << std::endl;
+            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." << std::endl;
+            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;
     }
 }
 
@@ -1049,104 +1090,125 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
 		nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() );
 
 		unsigned index = 0;
-		while( index<nfi.size() ){
-			Node i = nfi[index];
-			Node j = nfj[index];
-			Trace("strings-solve-debug")  << "...Processing " << i << " " << j << std::endl;
-			if( !areEqual( i, j ) ) {
-				if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ){
-					unsigned int len_short = i.getConst<String>().size() < j.getConst<String>().size() ? i.getConst<String>().size() : j.getConst<String>().size();
-					String si = i.getConst<String>().substr(0, len_short);
-					String sj = j.getConst<String>().substr(0, len_short);
-					if(si == sj) {
-						if( i.getConst<String>().size() < j.getConst<String>().size() ) {
-							Node remainderStr = NodeManager::currentNM()->mkConst( j.getConst<String>().substr(len_short) );
-							Trace("strings-solve-debug-test") << "Break normal form of " << nfj[index] << " into " << nfi[index] << ", " << remainderStr << std::endl;
-							nfj.insert( nfj.begin() + index + 1, remainderStr );
-							nfj[index] = nfi[index];
+		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 );
+				Node lnj = getLength( nj );
+				ant.push_back( lni.eqNode( lnj ) );
+				ant.push_back( getLengthTerm( ni ).eqNode( d_normal_forms_base[ni] ) );
+				ant.push_back( getLengthTerm( nj ).eqNode( d_normal_forms_base[nj] ) );
+				ant.insert( ant.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
+				ant.insert( ant.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
+				std::vector< Node > cc;
+				std::vector< Node >& nfk = index>=nfi.size() ? nfj : nfi;
+				for( unsigned index_k=index; index_k<nfk.size(); index_k++ ){
+					cc.push_back( nfk[index_k].eqNode( d_emptyString ) );
+				}
+				Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
+				conc = Rewriter::rewrite( conc );
+				sendLemma(mkExplain( ant ), conc, "Disequality Normalize Empty");
+				return true;
+			}else{
+				Node i = nfi[index];
+				Node j = nfj[index];
+				Trace("strings-solve-debug")  << "...Processing " << i << " " << j << std::endl;
+				if( !areEqual( i, j ) ) {
+					if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ){
+						unsigned int len_short = i.getConst<String>().size() < j.getConst<String>().size() ? i.getConst<String>().size() : j.getConst<String>().size();
+						String si = i.getConst<String>().substr(0, len_short);
+						String sj = j.getConst<String>().substr(0, len_short);
+						if(si == sj) {
+							if( i.getConst<String>().size() < j.getConst<String>().size() ) {
+								Node remainderStr = NodeManager::currentNM()->mkConst( j.getConst<String>().substr(len_short) );
+								Trace("strings-solve-debug-test") << "Break normal form of " << nfj[index] << " into " << nfi[index] << ", " << remainderStr << std::endl;
+								nfj.insert( nfj.begin() + index + 1, remainderStr );
+								nfj[index] = nfi[index];
+							} else {
+								Node remainderStr = NodeManager::currentNM()->mkConst( i.getConst<String>().substr(len_short) );
+								Trace("strings-solve-debug-test") << "Break normal form of " << nfi[index] << " into " << nfj[index] << ", " << remainderStr << std::endl;
+								nfi.insert( nfi.begin() + index + 1, remainderStr );
+								nfi[index] = nfj[index];
+							}
 						} else {
-							Node remainderStr = NodeManager::currentNM()->mkConst( i.getConst<String>().substr(len_short) );
-							Trace("strings-solve-debug-test") << "Break normal form of " << nfi[index] << " into " << nfj[index] << ", " << remainderStr << std::endl;
-							nfi.insert( nfi.begin() + index + 1, remainderStr );
-							nfi[index] = nfj[index];
-						}
-					} else {
-						//conflict
-						return false;
-					}
-				}else{
-					Node li = getLength( i );
-					Node lj = getLength( j );
-					if( areDisequal(li, lj) ){
-						Trace("strings-solve") << "Case 2 : add lemma " << std::endl;
-						//must add lemma
-						std::vector< Node > antec;
-						std::vector< Node > antec_new_lits;
-						antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
-						antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
-						antec.push_back( ni.eqNode( nj ).negate() );
-						antec_new_lits.push_back( li.eqNode( lj ).negate() );
-						std::vector< Node > conc;
-						Node sk1 = NodeManager::currentNM()->mkSkolem( "xpdsym_$$", ni.getType(), "created for disequality normalization" );
-						Node sk2 = NodeManager::currentNM()->mkSkolem( "ypdsym_$$", ni.getType(), "created for disequality normalization" );
-						Node sk3 = NodeManager::currentNM()->mkSkolem( "zpdsym_$$", ni.getType(), "created for disequality normalization" );
-						Node lsk1 = getLength( sk1 );
-						conc.push_back( lsk1.eqNode( li ) );
-						Node lsk2 = getLength( sk2 );
-						conc.push_back( lsk2.eqNode( lj ) );
-						conc.push_back( NodeManager::currentNM()->mkNode( kind::OR,
-											j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
-						
-						/*
-						Node sk1 = NodeManager::currentNM()->mkSkolem( "w1sym_$$", ni.getType(), "created for disequality normalization" );
-						Node sk2 = NodeManager::currentNM()->mkSkolem( "w2sym_$$", ni.getType(), "created for disequality normalization" );
-						Node sk3 = NodeManager::currentNM()->mkSkolem( "w3sym_$$", ni.getType(), "created for disequality normalization" );
-						Node sk4 = NodeManager::currentNM()->mkSkolem( "w4sym_$$", ni.getType(), "created for disequality normalization" );
-						Node sk5 = NodeManager::currentNM()->mkSkolem( "w5sym_$$", ni.getType(), "created for disequality normalization" );
-						Node w1w2w3 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 );
-						Node w1w4w5 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk4, sk5 );
-						Node s_eq_w1w2w3 = NodeManager::currentNM()->mkNode( kind::EQUAL, ni, w1w2w3 );
-						conc.push_back( s_eq_w1w2w3 );
-						Node t_eq_w1w4w5 = NodeManager::currentNM()->mkNode( kind::EQUAL, nj, w1w4w5 );
-						conc.push_back( t_eq_w1w4w5 );
-						Node w2_neq_w4 = sk2.eqNode( sk4 ).negate();
-						conc.push_back( w2_neq_w4 );
-						Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
-						Node w2_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), one);
-						conc.push_back( w2_len_one );
-						Node w4_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4), one);
-						conc.push_back( w4_len_one );
-						Node c = NodeManager::currentNM()->mkNode( kind::AND, conc );
-						*/
-						//Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2),
-						//													     NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4) );
-						//conc.push_back( eq );
-						sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "Disequality Normalize" );
-						return true;
-					}else if( areEqual( li, lj ) ){
-						if( areDisequal( i, j ) ){
-							Trace("strings-solve") << "Case 1 : found equal length disequal sub strings " << i << " " << j << std::endl;
-							//we are done
+							//conflict
 							return false;
-						} else {
-							//splitting on demand : try to make them disequal
-							Node eq = i.eqNode( j );
-							sendSplit( i, j, "Disequality : disequal terms" );
+						}
+					}else{
+						Node li = getLength( i );
+						Node lj = getLength( j );
+						if( areDisequal(li, lj) ){
+							Trace("strings-solve") << "Case 2 : add lemma " << std::endl;
+							//must add lemma
+							std::vector< Node > antec;
+							std::vector< Node > antec_new_lits;
+							antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
+							antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
+							antec.push_back( ni.eqNode( nj ).negate() );
+							antec_new_lits.push_back( li.eqNode( lj ).negate() );
+							std::vector< Node > conc;
+							Node sk1 = NodeManager::currentNM()->mkSkolem( "xpdsym_$$", ni.getType(), "created for disequality normalization" );
+							Node sk2 = NodeManager::currentNM()->mkSkolem( "ypdsym_$$", ni.getType(), "created for disequality normalization" );
+							Node sk3 = NodeManager::currentNM()->mkSkolem( "zpdsym_$$", ni.getType(), "created for disequality normalization" );
+							Node lsk1 = getLength( sk1 );
+							conc.push_back( lsk1.eqNode( li ) );
+							Node lsk2 = getLength( sk2 );
+							conc.push_back( lsk2.eqNode( lj ) );
+							conc.push_back( NodeManager::currentNM()->mkNode( kind::OR,
+												j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
+							
+							/*
+							Node sk1 = NodeManager::currentNM()->mkSkolem( "w1sym_$$", ni.getType(), "created for disequality normalization" );
+							Node sk2 = NodeManager::currentNM()->mkSkolem( "w2sym_$$", ni.getType(), "created for disequality normalization" );
+							Node sk3 = NodeManager::currentNM()->mkSkolem( "w3sym_$$", ni.getType(), "created for disequality normalization" );
+							Node sk4 = NodeManager::currentNM()->mkSkolem( "w4sym_$$", ni.getType(), "created for disequality normalization" );
+							Node sk5 = NodeManager::currentNM()->mkSkolem( "w5sym_$$", ni.getType(), "created for disequality normalization" );
+							Node w1w2w3 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 );
+							Node w1w4w5 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk4, sk5 );
+							Node s_eq_w1w2w3 = NodeManager::currentNM()->mkNode( kind::EQUAL, ni, w1w2w3 );
+							conc.push_back( s_eq_w1w2w3 );
+							Node t_eq_w1w4w5 = NodeManager::currentNM()->mkNode( kind::EQUAL, nj, w1w4w5 );
+							conc.push_back( t_eq_w1w4w5 );
+							Node w2_neq_w4 = sk2.eqNode( sk4 ).negate();
+							conc.push_back( w2_neq_w4 );
+							Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
+							Node w2_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), one);
+							conc.push_back( w2_len_one );
+							Node w4_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4), one);
+							conc.push_back( w4_len_one );
+							Node c = NodeManager::currentNM()->mkNode( kind::AND, conc );
+							*/
+							//Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2),
+							//													     NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4) );
+							//conc.push_back( eq );
+							sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "Disequality Normalize" );
+							return true;
+						}else if( areEqual( li, lj ) ){
+							if( areDisequal( i, j ) ){
+								Trace("strings-solve") << "Case 1 : found equal length disequal sub strings " << i << " " << j << std::endl;
+								//we are done
+								return false;
+							} else {
+								//splitting on demand : try to make them disequal
+								Node eq = i.eqNode( j );
+								sendSplit( i, j, "Disequality : disequal terms" );
+								eq = Rewriter::rewrite( eq );
+								d_pending_req_phase[ eq ] = false;
+								return true;
+							}
+						}else{
+							//splitting on demand : try to make lengths equal
+							Node eq = li.eqNode( lj );
+							sendSplit( li, lj, "Disequality : equal length" );
 							eq = Rewriter::rewrite( eq );
-							d_pending_req_phase[ eq ] = false;
+							d_pending_req_phase[ eq ] = true;
 							return true;
 						}
-					}else{
-						//splitting on demand : try to make lengths equal
-						Node eq = li.eqNode( lj );
-						sendSplit( li, lj, "Disequality : equal length" );
-						eq = Rewriter::rewrite( eq );
-						d_pending_req_phase[ eq ] = true;
-						return true;
 					}
 				}
+				index++;
 			}
-			index++;
 		}
 		Assert( false );
 	}
@@ -1273,7 +1335,7 @@ bool TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp, cons
 }
 
 void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
-	if( conc.isNull() ){
+	if( conc.isNull() || conc==d_false ){
 		d_out->conflict(ant);
 		Trace("strings-conflict") << "CONFLICT : Strings conflict : " << ant << std::endl;
 		d_conflict = true;
@@ -1306,6 +1368,11 @@ Node TheoryStrings::mkConcat( std::vector< Node >& c ) {
 	return Rewriter::rewrite( cc );
 }
 
+Node TheoryStrings::mkExplain( std::vector< Node >& a ) {
+	std::vector< Node > an;
+	return mkExplain( a, an );
+}
+
 Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) {
     std::vector< TNode > antec_exp;
     for( unsigned i=0; i<a.size(); i++ ){
@@ -1344,6 +1411,61 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an )
     return ant;
 }
 
+bool TheoryStrings::checkLengths() {
+  bool addedLemma = false;
+  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_inst.find(n)==d_length_inst.end() ){
+					d_length_inst[n] = true;
+					Trace("strings-debug") << "get n: " << n << endl;
+					Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
+					d_length_intro_vars.push_back( sk );
+					Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
+					eq = Rewriter::rewrite(eq);
+					Trace("strings-lemma") << "Strings: Add term lemma " << eq << std::endl;
+					d_out->lemma(eq);
+					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 = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
+					}else{
+						//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: Add length lemma " << ceq << std::endl;
+					d_out->lemma(ceq);
+					addedLemma = true;
+				}
+			}
+			++eqc_i;
+		}
+	}
+	++eqcs_i;
+  }
+  return addedLemma;
+}
+
 bool TheoryStrings::checkNormalForms() {
     Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
 	eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
@@ -1354,14 +1476,20 @@ bool TheoryStrings::checkNormalForms() {
 		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 << " ) : ";
+			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;
+			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;
 		}
@@ -1415,6 +1543,7 @@ bool TheoryStrings::checkNormalForms() {
 		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 ){
 			return true;
 		}else if ( d_pending.empty() && d_lemma_cache.empty() ){
@@ -1498,6 +1627,42 @@ bool TheoryStrings::checkNormalForms() {
   }
 }
 
+bool TheoryStrings::checkLengthsEqc() {
+	bool addedLemma = false;
+	std::vector< Node > nodes;
+	getEquivalenceClasses( nodes );
+	for( unsigned i=0; i<nodes.size(); i++ ){
+		if( d_normal_forms[nodes[i]].size()>1 ){
+			Trace("strings-process-debug") << "Process length constraints for " << nodes[i] << std::endl;
+			//check if there is a length term for this equivalence class
+			EqcInfo* ei = getOrMakeEqcInfo( nodes[i], false );
+			Node lt = ei ? ei->d_length_term : Node::null();
+			if( !lt.isNull() ){
+			  Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
+			  //now, check if length normalization has occurred
+			  if( ei->d_normalized_length.get().isNull() ){
+				//if not, add the lemma
+				std::vector< Node > ant;
+				ant.insert( ant.end(), d_normal_forms_exp[nodes[i]].begin(), d_normal_forms_exp[nodes[i]].end() );
+				ant.push_back( d_normal_forms_base[nodes[i]].eqNode( lt ) );
+				Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[nodes[i]] ) );
+				lc = Rewriter::rewrite( lc );
+				Node eq = llt.eqNode( lc );
+				ei->d_normalized_length.set( eq );
+				sendLemma( mkExplain( ant ), eq, "Length Normalization" );
+				addedLemma = true;
+			  }
+			}
+		}else{
+			Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
+		}
+	}
+	if( addedLemma ){
+		doPendingLemmas();
+	}
+	return addedLemma;
+}
+
 bool TheoryStrings::checkCardinality() {
   int cardinality = options::stringCharCardinality();
   Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 52c7288a8..16c3d4876 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -50,6 +50,7 @@ class TheoryStrings : public Theory {
   bool hasTerm( Node a );
   bool areEqual( Node a, Node b );
   bool areDisequal( Node a, Node b );
+  Node getLengthTerm( Node t );
   Node getLength( Node t );
   public:
 
@@ -131,6 +132,10 @@ class TheoryStrings : public Theory {
   /** inferences */
   NodeList d_infer;
   NodeList d_infer_exp;
+  /** normal forms */
+  std::map< Node, Node > d_normal_forms_base;
+  std::map< Node, std::vector< Node > > d_normal_forms;
+  std::map< Node, std::vector< Node > > d_normal_forms_exp;
   //map of pairs of terms that have the same normal form
   NodeListMap d_nf_pairs;
   void addNormalFormPair( Node n1, Node n2 );
@@ -179,6 +184,8 @@ class TheoryStrings : public Theory {
     context::CDO< Node > d_const_term;
     context::CDO< Node > d_length_term;
     context::CDO< unsigned > d_cardinality_lem_k;
+	// 1 = added length lemma
+	context::CDO< Node > d_normalized_length;
   };
   /** map from representatives to information necessary for equivalence classes */
   std::map< Node, EqcInfo* > d_eqc_info;
@@ -186,14 +193,14 @@ class TheoryStrings : public Theory {
   //maintain which concat terms have the length lemma instantiatied
   std::map< Node, bool > d_length_inst;
   private:
-    std::map< Node, std::vector< Node > > d_normal_forms;
-    std::map< Node, std::vector< Node > > d_normal_forms_exp;
-    void getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
+    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);
-    void normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
+    bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
     bool normalizeDisequality( Node n1, Node n2 );
 
+	bool checkLengths();
     bool checkNormalForms();
+	bool checkLengthsEqc();
     bool checkCardinality();
     bool checkInductiveEquations();
 	int gcd(int a, int b);
@@ -225,6 +232,7 @@ protected:
   Node mkConcat( Node n1, Node n2 );
   Node mkConcat( std::vector< Node >& c );
   /** mkExplain **/
+  Node mkExplain( std::vector< Node >& a );
   Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
 
   //get equivalence classes