Merge branch 'master' of github.com:tiliang/CVC4

30 files changed, 1266 insertions, 525 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 638c64a69..c84046570 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -870,6 +870,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_EXPR(kind, args);
       }
     }
+  //| /* substring */
+    //LPAREN_TOK STRSUB_TOK n1=INTEGER_LITERAL n2=INTEGER_LITERAL RPAREN_TOK
+	//{
+	//}
   | /* A non-built-in function application */
     LPAREN_TOK
     functionName[name, CHECK_DECLARED]
@@ -1615,14 +1619,15 @@ BV2NAT_TOK : 'bv2nat';
 INT2BV_TOK : 'int2bv';
 
 //STRING
-STRCST_TOK : 'str.const';
+//STRCST_TOK : 'str.cst';
 STRCON_TOK : 'str.++';
 STRLEN_TOK : 'str.len';
+//STRSUB_TOK : 'str.sub' ;
 STRINRE_TOK : 'str.in.re';
 STRTORE_TOK : 'str.to.re';
 RECON_TOK : 're.++';
 REOR_TOK : 're.or';
-REINTER_TOK : 're.inter';
+REINTER_TOK : 're.itr';
 RESTAR_TOK : 're.*';
 REPLUS_TOK : 're.+';
 REOPT_TOK : 're.opt';
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7fadb477b..df568f1ab 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -75,6 +75,7 @@
 #include "theory/quantifiers/macros.h"
 #include "theory/datatypes/options.h"
 #include "theory/quantifiers/first_order_reasoning.h"
+#include "theory/strings/theory_strings_preprocess.h"
 
 using namespace std;
 using namespace CVC4;
@@ -986,14 +987,16 @@ void SmtEngine::setLogicInternal() throw() {
          d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
          ) ||
         // Quantifiers
-        d_logic.isQuantified()
+        d_logic.isQuantified() ||
+		// Strings
+		d_logic.isTheoryEnabled(THEORY_STRINGS)
         ? decision::DECISION_STRATEGY_JUSTIFICATION
         : decision::DECISION_STRATEGY_INTERNAL
       );
 
     bool stoponly =
       // ALL_SUPPORTED
-      d_logic.hasEverything() ? false :
+      d_logic.hasEverything() || d_logic.isTheoryEnabled(THEORY_STRINGS) ? false :
       ( // QF_AUFLIA
         (not d_logic.isQuantified() &&
          d_logic.isTheoryEnabled(THEORY_ARRAY) &&
@@ -1005,7 +1008,7 @@ void SmtEngine::setLogicInternal() throw() {
          d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
          ) ||
         // Quantifiers
-        d_logic.isQuantified()
+        d_logic.isQuantified() 
         ? true : false
       );
 
@@ -2858,6 +2861,14 @@ void SmtEnginePrivate::processAssertions() {
 
   // Assertions ARE guaranteed to be rewritten by this point
 
+  if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ){
+	CVC4::theory::strings::StringsPreprocess sp;
+	sp.simplify( d_assertionsToPreprocess );
+    for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
+		d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
+	}
+  }
+
   dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
   if( options::preSkolemQuant() ){
     //apply pre-skolemization to existential quantifiers
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 120ac0154..6c7f622ec 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -87,6 +87,10 @@ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
   return d_internal->getEqualityStatus(a,b);
 }
 
+Node TheoryArith::getModelValue(TNode var) {
+  return d_internal->getModelValue( var );
+}
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 6b9fd5515..451f1e8ff 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -74,6 +74,8 @@ public:
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   void addSharedTerm(TNode n);
+
+  Node getModelValue(TNode var);
 };/* class TheoryArith */
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index f5b1d20ce..9d13dccb7 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -737,6 +737,19 @@ void TheoryArithPrivate::addSharedTerm(TNode n){
   }
 }
 
+Node TheoryArithPrivate::getModelValue(TNode term) {
+  try{
+    DeltaRational drv = getDeltaValue(term);
+    const Rational& delta = d_partialModel.getDelta();
+    Rational qmodel = drv.substituteDelta( delta );
+    return mkRationalNode( qmodel );
+  } catch (DeltaRationalException& dr) {
+    return Node::null();
+  } catch (ModelException& me) {
+    return Node::null();
+  }
+}
+
 namespace attr {
   struct ToIntegerTag { };
   struct LinearIntDivTag { };
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 7370cfc15..22fc8d4a7 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -383,6 +383,8 @@ public:
 
   void addSharedTerm(TNode n);
 
+  Node getModelValue(TNode var);
+
 private:
 
   /** The constant zero. */
diff --git a/src/theory/strings/Makefile.am b/src/theory/strings/Makefile.am
index 15bd04b88..38efa33f3 100644
--- a/src/theory/strings/Makefile.am
+++ b/src/theory/strings/Makefile.am
@@ -11,7 +11,9 @@ libstrings_la_SOURCES = \
 	theory_strings_rewriter.h \
 	theory_strings_rewriter.cpp \
 	theory_strings_type_rules.h \
-	type_enumerator.h
+	type_enumerator.h \
+	theory_strings_preprocess.h \
+	theory_strings_preprocess.cpp
 
 EXTRA_DIST = \
 	kinds
diff --git a/src/theory/strings/options b/src/theory/strings/options
index c90d654b1..9226f9999 100644
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -5,7 +5,7 @@
 
 module STRINGS "theory/strings/options.h" Strings theory
 
-option stringCharCardinality str-cardinality --str-cardinality=N int16_t :default 256 :read-write
+option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :default 256 :read-write
  the cardinality of the characters used by the theory of string, default 256
 
 endmodule
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 33bee4135..7d5edd0f7 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -23,8 +23,11 @@
 #include "theory/model.h"
 #include "smt/logic_exception.h"
 #include "theory/strings/options.h"
+#include "theory/strings/type_enumerator.h"
 #include <cmath>
 
+#define STR_UNROLL_INDUCTION
+
 using namespace std;
 using namespace CVC4::context;
 
@@ -43,7 +46,10 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_ind_map1(c),
     d_ind_map2(c),
     d_ind_map_exp(c),
-    d_ind_map_lemma(c)
+    d_ind_map_lemma(c),
+	//d_lit_to_decide_index( c, 0 ),
+	//d_lit_to_decide( c ),
+	d_lit_to_unroll( c )
 {
     // The kinds we are treating as function application in congruence
     d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
@@ -60,6 +66,46 @@ TheoryStrings::~TheoryStrings() {
 
 }
 
+Node TheoryStrings::getRepresentative( Node t ) {
+	if( d_equalityEngine.hasTerm( t ) ){
+		return d_equalityEngine.getRepresentative( t );
+	}else{
+		return t;
+	}
+}
+
+bool TheoryStrings::hasTerm( Node a ){
+  return d_equalityEngine.hasTerm( a );
+}
+
+bool TheoryStrings::areEqual( Node a, Node b ){
+  if( a==b ){
+    return true;
+  }else if( hasTerm( a ) && hasTerm( b ) ){
+    return d_equalityEngine.areEqual( a, b );
+  }else{
+    return false;
+  }
+}
+
+bool TheoryStrings::areDisequal( Node a, Node b ){
+  if( hasTerm( a ) && hasTerm( b ) ){
+    return d_equalityEngine.areDisequal( a, b, false );
+  }else{
+    return false;
+  }
+}
+
+Node TheoryStrings::getLength( Node t ) {
+	EqcInfo * ei = getOrMakeEqcInfo( t );
+	Node length_term = ei->d_length_term;
+	if( length_term.isNull()) {
+		//typically shouldnt be necessary
+		length_term = t;
+	}
+	return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term );
+}
+
 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
@@ -71,6 +117,20 @@ void TheoryStrings::addSharedTerm(TNode t) {
   Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl;
 }
 
+EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) {
+  if( d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b) ){
+    if (d_equalityEngine.areEqual(a, b)) {
+      // The terms are implied to be equal
+      return EQUALITY_TRUE;
+    }
+    if (d_equalityEngine.areDisequal(a, b, false)) {
+      // The terms are implied to be dis-equal
+      return EQUALITY_FALSE;
+    }
+  }
+  return EQUALITY_UNKNOWN;
+}
+
 void TheoryStrings::propagate(Effort e)
 {
   // direct propagation now
@@ -108,7 +168,7 @@ Node TheoryStrings::explain( TNode literal ){
   std::vector< TNode > assumptions;
   explain( literal, assumptions );
   if( assumptions.empty() ){
-    return NodeManager::currentNM()->mkConst( true );
+    return d_true;
   }else if( assumptions.size()==1 ){
     return assumptions[0];
   }else{
@@ -122,33 +182,114 @@ Node TheoryStrings::explain( TNode literal ){
 
 
 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
-    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 );
+	std::vector< Node > nodes;
+	getEquivalenceClasses( nodes );
+	std::map< Node, Node > processed;
+	std::vector< std::vector< Node > > col;
+	std::vector< Node > lts;
+	seperateByLength( nodes, col, lts );
+	//step 1 : get all values for known lengths
+	std::vector< Node > lts_values;
+	//std::map< Node, 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;
+		if( lts[i].isConst() ){
+			lts_values.push_back( lts[i] );
+			//values_used[ lts[i] ] = 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;
+			}else{
+				Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl;
+				Assert( false );
+				lts_values.push_back( Node::null() );
+			}
+		}
+	}
+	////step 2 : assign arbitrary values for unknown lengths?
+	//for( unsigned i=0; i<col.size(); i++ ){
+	//	if( 
+	//}
+	Trace("strings-model") << "Assign to equivalence classes..." << std::endl;
+	//step 3 : assign values to equivalence classes that are pure variables
+	for( unsigned i=0; i<col.size(); i++ ){
+		std::vector< Node > pure_eq;
+		Trace("strings-model") << "The equivalence classes ";
+		for( unsigned j=0; j<col[i].size(); j++ ) {
+			Trace("strings-model") << col[i][j] << " ";
+			//check if col[i][j] has only variables
+			EqcInfo* ei = getOrMakeEqcInfo( col[i][j], false );
             Node cst = ei ? ei->d_const_term : Node::null();
-            if( !cst.isNull() ){
-                //print out
-                Trace("strings-model-debug") << cst << std::endl;
-            }else{
-                //is there a length term?
-                //   is there a value for it?  if so, assign a constant via enumerator
-                //   otherwise: error
-                //otherwise: assign a new unique length, then assign a constant via enumerator
-            }
-        }else{
-            //should be length eqc
-            //if no constant, error
-        }
-
-        ++eqcs_i;
-    }
-*/
-    //TODO: not done
+			if( cst.isNull() ){
+				Assert( d_normal_forms.find( col[i][j] )!=d_normal_forms.end() );
+				if( d_normal_forms[col[i][j]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){
+					pure_eq.push_back( col[i][j] );
+				}
+			}else{
+				processed[col[i][j]] = cst;
+			}
+		}
+		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;
+				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 );
+		}
+	}
+	Trace("strings-model") << "String Model : Finished." << std::endl;
+	//step 4 : assign constants to all other equivalence classes
+	for( unsigned i=0; i<nodes.size(); i++ ){
+		if( processed.find( nodes[i] )==processed.end() ){
+			Assert( d_normal_forms.find( nodes[i] )!=d_normal_forms.end() );
+			Trace("strings-model") << "Construct model for " << nodes[i] << " based on normal form ";
+			for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) {
+				if( j>0 ) Trace("strings-model") << " ++ ";
+				Trace("strings-model") << d_normal_forms[nodes[i]][j];
+				Node r = getRepresentative( d_normal_forms[nodes[i]][j] );
+				if( !r.isConst() && processed.find( r )==processed.end() ){
+					Trace("strings-model") << "(UNPROCESSED)";
+				}
+			}
+			Trace("strings-model") << std::endl;
+			std::vector< Node > nc;
+			for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) {
+				Node r = getRepresentative( d_normal_forms[nodes[i]][j] );
+				Assert( r.isConst() || processed.find( r )!=processed.end() );
+				nc.push_back(r.isConst() ? r : processed[r]);
+			}
+			Node cc = mkConcat( nc );
+			Assert( cc.getKind()==kind::CONST_STRING );
+			Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl;
+			processed[nodes[i]] = cc;
+			m->assertEquality( nodes[i], cc, true );
+		}
+	}
 }
 
 /////////////////////////////////////////////////////////////////////////////
@@ -167,11 +308,12 @@ void TheoryStrings::preRegisterTerm(TNode n) {
     break;
   default:
     if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) {
-      Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
-      Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) );
-      Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, zero);
-      Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl;
-      d_out->lemma(n_len_geq_zero);
+	  if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ){
+		  Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
+		  Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero);
+		  Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl;
+		  d_out->lemma(n_len_geq_zero);
+	  }
     }
     if (n.getType().isBoolean()) {
       // Get triggered for both equal and dis-equal
@@ -184,22 +326,14 @@ void TheoryStrings::preRegisterTerm(TNode n) {
   }
 }
 
-void TheoryStrings::dealPositiveWordEquation(TNode n) {
-  Trace("strings-pwe") << "Deal Positive Word Equation: " << n << endl;
-  Node node = n;
-
-  // length left = length right
-  //Node n_left = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[0]);
-  //Node n_right = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[1]);
-  if(node[0].getKind() == kind::CONST_STRING) {
-  } else if(node[0].getKind() == kind::STRING_CONCAT) {
-  }
-}
-
 void TheoryStrings::check(Effort e) {
   bool polarity;
   TNode atom;
 
+  if( !done() && !hasTerm( d_emptyString ) ){
+	 preRegisterTerm( d_emptyString );
+  }
+
  // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
   Trace("strings-check") << "Theory of strings, check : " << e << std::endl;
   while ( !done() && !d_conflict)
@@ -213,33 +347,16 @@ void TheoryStrings::check(Effort e) {
     polarity = fact.getKind() != kind::NOT;
     atom = polarity ? fact : fact[0];
     if (atom.getKind() == kind::EQUAL) {
-      //head
-      //if(atom[0].getKind() == kind::CONST_STRING) {
-          //if(atom[1].getKind() == kind::STRING_CONCAT) {
-          //}
-      //}
-      //tail
       d_equalityEngine.assertEquality(atom, polarity, fact);
     } else {
       d_equalityEngine.assertPredicate(atom, polarity, fact);
     }
-    switch(atom.getKind()) {
-        case kind::EQUAL:
-            if(polarity) {
-                //if(atom[0].isString() && atom[1].isString()) {
-                    //dealPositiveWordEquation(atom);
-                //}
-            } else {
-                // TODO: Word Equation negaitive
-            }
-            break;
-        case kind::STRING_IN_REGEXP:
-            // TODO: membership
-            break;
-        default:
-            //possibly error
-            break;
-    }
+#ifdef STR_UNROLL_INDUCTION
+	//check if it is a literal to unroll?
+	if( d_lit_to_unroll.find( atom )!=d_lit_to_unroll.end() ){
+		Trace("strings-ind") << "Strings-ind : Possibly unroll for : " << atom << ", polarity = " << polarity << std::endl;
+	}
+#endif
   }
   doPendingFacts();
 
@@ -266,6 +383,7 @@ void TheoryStrings::check(Effort e) {
                     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 lemma " << eq << std::endl;
@@ -298,10 +416,13 @@ void TheoryStrings::check(Effort e) {
   }
   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;
           }
       }
   }
@@ -386,7 +507,6 @@ void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){
               Node n = (*eqc_i);
               if( n.getKind()==kind::STRING_LENGTH ){
                 if( !hasTerm( d_emptyString ) || !areEqual(n[0], d_emptyString ) ){
-                    Trace("strings-debug") << "Processing possible inference." << n << std::endl;
                     //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 );
@@ -426,7 +546,9 @@ void TheoryStrings::doPendingFacts() {
       bool polarity = fact.getKind() != kind::NOT;
       TNode atom = polarity ? fact : fact[0];
       if (atom.getKind() == kind::EQUAL) {
-        d_equalityEngine.assertEquality( atom, polarity, exp );
+		Assert( d_equalityEngine.hasTerm( atom[0] ) );
+		Assert( d_equalityEngine.hasTerm( atom[1] ) );
+		d_equalityEngine.assertEquality( atom, polarity, exp );
       }else{
         d_equalityEngine.assertPredicate( atom, polarity, exp );
       }
@@ -435,6 +557,20 @@ void TheoryStrings::doPendingFacts() {
   d_pending.clear();
   d_pending_exp.clear();
 }
+void TheoryStrings::doPendingLemmas() {
+  if( !d_conflict && !d_lemma_cache.empty() ){
+	  for( unsigned i=0; i<d_lemma_cache.size(); i++ ){
+		  Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl;
+		  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 );
+	  }
+	d_lemma_cache.clear();
+	d_pending_req_phase.clear();
+  }
+}
 
 void 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) {
@@ -519,15 +655,19 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
         //nf.push_back( eqc );
         if( eqc.getKind()==kind::STRING_CONCAT ){
             for( unsigned i=0; i<eqc.getNumChildren(); i++ ){
-                nf.push_back( eqc[i] );
+				if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc[i], d_emptyString ) ){
+					nf.push_back( eqc[i] );
+				}
             }
-        }else{
+        }else if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.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 )){
         //do nothing
         Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl;
+		d_normal_forms[eqc].clear();
+		d_normal_forms_exp[eqc].clear();
     } else {
         visited.push_back( eqc );
         if(d_normal_forms.find(eqc)==d_normal_forms.end() ){
@@ -547,10 +687,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
             unsigned i = 0;
             //unify each normal form > 0 with normal_forms[0]
             for( unsigned j=1; j<normal_forms.size(); j++ ) {
-                std::vector< Node > loop_eqs_x;
-                std::vector< Node > loop_eqs_y;
-                std::vector< Node > loop_eqs_z;
-                std::vector< Node > loop_exps;
+
                 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;
@@ -573,10 +710,6 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                             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] );
-                                //add loop equations that we've accumulated
-                                for( unsigned r=0; r<loop_eqs_x.size(); r++ ){
-                                    addInductiveEquation( loop_eqs_x[r], loop_eqs_y[r], loop_eqs_z[r], loop_exps[r] );
-                                }
                             }else{
                                 //the remainder must be empty
                                 unsigned k = index_i==normal_forms[i].size() ? j : i;
@@ -585,7 +718,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                     //can infer that this string must be empty
                                     Node eq_exp;
                                     if( curr_exp.empty() ) {
-                                        eq_exp = NodeManager::currentNM()->mkConst(true);
+                                        eq_exp = d_true;
                                     } else if( curr_exp.size() == 1 ) {
                                         eq_exp = curr_exp[0];
                                     } else {
@@ -593,7 +726,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                     }
                                     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;
-                                    //d_equalityEngine.assertEquality( eq, true, eq_exp );
+									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);
@@ -616,19 +749,8 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                 index_i++;
                                 success = true;
                             }else{
-                                EqcInfo * ei = getOrMakeEqcInfo( normal_forms[i][index_i] );
-                                Node length_term_i = ei->d_length_term;
-                                if( length_term_i.isNull()) {
-                                    //typically shouldnt be necessary
-                                    length_term_i = normal_forms[i][index_i];
-                                }
-                                length_term_i = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term_i );
-                                EqcInfo * ej = getOrMakeEqcInfo( normal_forms[j][index_j] );
-                                Node length_term_j = ej->d_length_term;
-                                if( length_term_j.isNull()) {
-                                    length_term_j = normal_forms[j][index_j];
-                                }
-                                length_term_j = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term_j );
+								Node length_term_i = getLength( normal_forms[i][index_i] );
+								Node length_term_j = getLength( normal_forms[j][index_j] );
                                 //check if length(normal_forms[i][index]) == length(normal_forms[j][index])
                                 if( areEqual(length_term_i, length_term_j)  ){
                                     Trace("strings-solve-debug") << "Case 2 : string lengths are equal" << std::endl;
@@ -637,7 +759,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                     std::vector< Node > temp_exp;
                                     temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
                                     temp_exp.push_back(NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ));
-                                    Node eq_exp = temp_exp.empty() ? NodeManager::currentNM()->mkConst(true) :
+                                    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_equalityEngine.assertEquality( eq, true, eq_exp );
@@ -646,17 +768,34 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                     d_infer.push_back(eq);
                                     d_infer_exp.push_back(eq_exp);
                                     return;
-                                }else{
-                                    Trace("strings-solve-debug") << "Case 3 : must compare strings" << std::endl;
-                                    bool sendLemma = false;
-                                    Node loop_x;
-                                    Node loop_y;
-                                    Node loop_z;
+								}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 ) );
+									}
+									conc = eqn[0].eqNode( eqn[1] );
+									Node ant = mkExplain( antec, antec_new_lits );
+									sendLemma( ant, conc, "Endpoint" );
+									return;
+								}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;
+                                    //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);
@@ -680,128 +819,88 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                         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") << " ... " << normal_forms[other_n_index][other_index] << 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_lindex-1] = y * z
+                                        //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
-                                        int found_size_y = -1;
-                                        for( int size_y = 0; size_y<(loop_index-index); size_y++ ){
-                                            int size_z = (loop_index-index)-size_y;
-                                            bool success = true;
-                                            //check for z
-                                            for( int r = 0; r<size_z; r++ ){
-                                                if( other_index+1+r >= (int)normal_forms[other_n_index].size() ||
-                                                    normal_forms[other_n_index][other_index+1+r]!=normal_forms[loop_n_index][index+size_y+r] ) {
-                                                    success = false;
-                                                    break;
-                                                }
-                                            }
-                                            //check for y
-                                            if( success ){
-                                                for( int r=0; r<size_y; r++ ){
-                                                    if( other_index+1+r >= (int)normal_forms[other_n_index].size() ||
-                                                        normal_forms[other_n_index][other_index+1+size_y+r]!=normal_forms[loop_n_index][index+r] ) {
-                                                        success = false;
-                                                        break;
-                                                    }
-                                                }
-                                                if( success ){
-                                                    found_size_y = size_y;
-                                                    break;
-                                                }
-                                            }
-                                        }
-                                        if( found_size_y==-1 ){
-                                            //need to break
-                                            Node sk_y= NodeManager::currentNM()->mkSkolem( "ldssym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
-                                            Node sk_z= NodeManager::currentNM()->mkSkolem( "ldssym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
 
-                                            sendLemma = true;
-                                            antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-                                            //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 = c1c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c1c ) :
-                                                                    c1c.size()==1 ? c1c[0] : d_emptyString;
-                                            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 = c2c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c2c ) :
-                                                                    c2c.size()==1 ? c2c[0] : d_emptyString;
-                                            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,
-                                                            NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, 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 zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) );
-                                            //Node sk_y_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk_y_len, zero);
-                                            //Node sk_z_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk_z_len, zero);
-                                            conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, sk_y_len_geq_zero, sk_z_len_geq_zero );
-                                            loop_x = normal_forms[other_n_index][other_index];
-                                            loop_y = sk_y;
-                                            loop_z = sk_z;
-                                            //we will be done
-                                            addNormalFormPair( normal_form_src[i], normal_form_src[j] );
-                                        } else {
-                                            // x = (yz)*y
-                                            Trace("strings-loop") << "We have that " << normal_forms[loop_n_index][loop_index] << " = (";
-                                            loop_eqs_x.push_back( normal_forms[loop_n_index][loop_index] );
-                                            for( unsigned r=0; r<2; r++ ){
-                                                //print y
-                                                std::vector< Node > yc;
-                                                for( int rr = 0; rr<found_size_y; rr++ ){
-                                                    if( rr>0 ) Trace("strings-loop") << ".";
-                                                    Trace("strings-loop") << normal_forms[loop_n_index][index+rr];
-                                                    yc.push_back( normal_forms[loop_n_index][index+rr] );
-                                                }
-                                                if( r==0 ){
-                                                    loop_eqs_y.push_back( mkConcat( yc ) );
-                                                    Trace("strings-loop") <<"..";
-                                                    //print z
-                                                    int found_size_z = (loop_index-index)-found_size_y;
-                                                    std::vector< Node > zc;
-                                                    for( int rr = 0; rr<found_size_z; rr++ ){
-                                                        if( rr>0 ) Trace("strings-loop") << ".";
-                                                        Trace("strings-loop") << normal_forms[loop_n_index][index+found_size_y+rr];
-                                                        zc.push_back( normal_forms[loop_n_index][index+found_size_y+rr] );
-                                                    }
-                                                    Trace("strings-loop") << ")*";
-                                                    loop_eqs_z.push_back( mkConcat( zc ) );
-                                                }
-                                            }
-                                            Trace("strings-loop") << std::endl;
-                                            if( loop_n_index==(int)i ){
-                                                index_j += (loop_index+1)-index_i;
-                                                index_i = loop_index+1;
-                                            }else{
-                                                index_i += (loop_index+1)-index_j;
-                                                index_j = loop_index+1;
-                                            }
-                                            success = true;
-                                            std::vector< Node > empty_vec;
-                                            loop_exps.push_back( mkExplain( antec, empty_vec ) );
-                                        }
+										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;
                                     }else{
-                                        Trace("strings-loop") << "No loops detected." << std::endl;
+                                        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) {
-                                            Node const_str = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? normal_forms[i][index_i] : normal_forms[j][index_j];
-                                            Node other_str = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? normal_forms[j][index_j] : normal_forms[i][index_i];
+											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) ) {
@@ -811,77 +910,64 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                                     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( const_str.getConst<String>().substr(len_short) );
-                                                    Trace("strings-solve-debug") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
+                                                    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
-                                                    sendLemma = true;
                                                     antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+													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 split" );
-                                                // |sk| >= 0
-                                                Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-                                                Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) );
-                                                //Node sk_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk_len, zero);
-
-                                                Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString );
-                                                Node eq2_m = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str,
-                                                            NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) );
-                                                Node eq2 = eq2_m;//NodeManager::currentNM()->mkNode( kind::AND, eq2_m, sk_len_geq_zero );
-                                                conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
+												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 split" );
+
+												Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString );
+												Node eq2_m = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str,
+															NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) );
+												Node eq2 = eq2_m;//NodeManager::currentNM()->mkNode( kind::AND, eq2_m, sk_len_geq_zero );
+												conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
                                                 Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
-                                                sendLemma = true;
+
+												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);
-                                            }
-                                            Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for 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 );
-                                            sendLemma = true;
-                                            // |sk| > 0
-                                            Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-                                            Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 0 ) );
-                                            Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, zero);
-                                            Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl;
-                                            //d_out->lemma(sk_gt_zero);
-                                            d_lemma_cache.push_back( sk_gt_zero );
-                                        }
-                                    }
-                                    Trace("strings-solve-debug2") << "sendLemma/success : " << sendLemma << " " << success << std::endl;
-                                    if( sendLemma ){
-                                        Node ant = mkExplain( antec, antec_new_lits );
-                                        if( conc.isNull() ){
-                                            d_out->conflict(ant);
-                                            Trace("strings-conflict") << "Strings conflict : " << ant << std::endl;
-                                            d_conflict = true;
-                                        }else{
-                                            Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
-                                            Trace("strings-lemma") << "Strings compare lemma : " << lem << std::endl;
-                                            //d_out->lemma(lem);
-                                            d_lemma_cache.push_back( lem );
-                                        }
-                                        if( !loop_y.isNull() ){
-                                            addInductiveEquation( loop_x, loop_y, loop_z, ant );
+
+											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 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;
                                         }
-                                        return;
                                     }
                                 }
                             }
@@ -918,22 +1004,66 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
         visited.pop_back();
     }
 }
-bool TheoryStrings::hasTerm( Node a ){
-  return d_equalityEngine.hasTerm( a );
-}
 
-bool TheoryStrings::areEqual( Node a, Node b ){
-  if( a==b ){
-    return true;
-  }else if( hasTerm( a ) && hasTerm( b ) ){
-    return d_equalityEngine.areEqual( a, b );
-  }else{
-    return false;
-  }
+bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
+	//Assert( areDisequal( ni, nj ) );
+	if( d_normal_forms[ni].size()>1 || d_normal_forms[nj].size()>1 ){
+		unsigned index = 0;
+		while( index<d_normal_forms[ni].size() ){
+			Node i = d_normal_forms[ni][index];
+			Node j = d_normal_forms[nj][index];
+			Trace("strings-solve-debug")  << "...Processing " << i << " " << j << std::endl;
+			if( !areEqual( i, j ) ){
+				Node li = getLength( i );
+				Node lj = getLength( j );
+				if( !areEqual(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 ) );
+					std::vector< Node > conc;
+					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 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( areDisequal( i, j ) ){
+					Trace("strings-solve") << "Case 1 : found equal length disequal sub strings " << i << " " << j << std::endl;
+					//we are done
+					return false;
+				}
+			}
+			index++;
+		}
+		Assert( false );
+	}
+	return false;
 }
 
 void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) {
-    //Trace("strings-debug") << "add normal form pair. " << n1 << " " << n2 << std::endl;
   if( !isNormalFormPair( n1, n2 ) ){
         NodeList* lst;
         NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
@@ -945,11 +1075,17 @@ void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) {
           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 );
-    }
+		Assert( isNormalFormPair( n1, n2 ) );
+    }else{
+		Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl;
+	}
+
 }
 bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) {
     //TODO: modulo equality?
@@ -971,8 +1107,39 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
   return false;
 }
 
-void TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp ) {
+bool TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c ) {
     Trace("strings-solve-debug") << "add inductive equation for " << x << " = (" << y << " " << z << ")* " << y << std::endl;
+#ifdef STR_UNROLL_INDUCTION
+	Node w = NodeManager::currentNM()->mkSkolem( "wsym_$$", x.getType(), "created for induction" );
+	Node x_eq_y_w = NodeManager::currentNM()->mkNode( kind::EQUAL, x, 
+							NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, w ) );
+	Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, x_eq_y_w );
+	Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl;
+	d_lemma_cache.push_back( lem );
+
+	//add initial induction
+	Node lit1 = w.eqNode( d_emptyString );
+	lit1 = Rewriter::rewrite( lit1 );
+	Node wp = NodeManager::currentNM()->mkSkolem( "wpsym_$$", x.getType(), "created for induction" );
+	Node lit2 = w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, z, y, wp ) );
+	lit2 = Rewriter::rewrite( lit2 );
+	Node split_lem = NodeManager::currentNM()->mkNode( kind::OR, lit1, lit2 );
+	Trace("strings-ind") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl;
+	Trace("strings-lemma") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl;
+	d_lemma_cache.push_back( split_lem );
+
+	//d_lit_to_decide.push_back( lit1 );
+	d_lit_to_unroll[lit2] = true;
+	d_pending_req_phase[lit1] = true;
+	d_pending_req_phase[lit2] = false;
+
+	x = w;
+	std::vector< Node > skc;
+	skc.push_back( y );
+	skc.push_back( z );
+	y = d_emptyString;
+	z = mkConcat( skc );
+#endif
 
     NodeListMap::iterator itr_x_y = d_ind_map1.find(x);
     NodeList* lst1;
@@ -1008,10 +1175,38 @@ void TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp ) {
     lst1->push_back( y );
     lst2->push_back( z );
     lste->push_back( exp );
+#ifdef STR_UNROLL_INDUCTION
+	return true;
+#else
+	return false;
+#endif
+}
+
+void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
+	if( conc.isNull() ){
+		d_out->conflict(ant);
+		Trace("strings-conflict") << "CONFLICT : Strings conflict : " << ant << std::endl;
+		d_conflict = true;
+	}else{
+		Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
+		Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl;
+		d_lemma_cache.push_back( lem );
+	}
+}
+
+void TheoryStrings::sendSplit( Node a, Node b, const char * c ) {
+	Node eq = a.eqNode( b );
+	eq = Rewriter::rewrite( eq );
+	Node neq = NodeManager::currentNM()->mkNode( kind::NOT, eq );
+	Node lemma_or = NodeManager::currentNM()->mkNode( kind::OR, eq, neq );
+	Trace("strings-lemma") << "Strings " << c << " split lemma : " << lemma_or << std::endl;
+	d_lemma_cache.push_back(lemma_or);
+	d_pending_req_phase[eq] = true;
 }
 
 Node TheoryStrings::mkConcat( std::vector< Node >& c ) {
-    return 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 );
 }
 
 Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) {
@@ -1028,176 +1223,228 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an )
             Assert( hasTerm(a[i][0][1]) );
             Assert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
         }
+		unsigned ps = antec_exp.size();
         explain(a[i], antec_exp);
-        Trace("strings-solve-debug") << "Done." << std::endl;
+        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++ ){
+		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 = NodeManager::currentNM()->mkConst(true);
+        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;
 }
 
 bool TheoryStrings::checkNormalForms() {
     Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
-  eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
-  while( !eqcs2_i.isFinished() ){
-    Node eqc = (*eqcs2_i);
-    //if (eqc.getType().isString()) {
-        eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-        Trace("strings-eqc") << "Eqc( " << eqc << " ) : ";
-        while( !eqc2_i.isFinished() ) {
-            Trace("strings-eqc") << (*eqc2_i) << " ";
-            ++eqc2_i;
+	eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
+	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;
+		}
+		++eqcs2_i;
+		}
+		Trace("strings-eqc") << std::endl;
+	}
+	Trace("strings-eqc") << std::endl;
+	for( NodeListMap::const_iterator it = d_nf_pairs.begin(); it != d_nf_pairs.end(); ++it ){
+		NodeList* lst = (*it).second;
+		NodeList::const_iterator it2 = lst->begin();
+		Trace("strings-nf") << (*it).first << " has been unified with ";
+		while( it2!=lst->end() ){
+			Trace("strings-nf") << (*it2);
+			++it2;
+		}
+		Trace("strings-nf") << std::endl;
+	}
+	Trace("strings-nf") << std::endl;
+	Trace("strings-nf") << "Current inductive equations : " << std::endl;
+	for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){
+        Node x = (*it).first;
+        NodeList* lst1 = (*it).second;
+        NodeList* lst2 = (*d_ind_map2.find(x)).second;
+        NodeList::const_iterator i1 = lst1->begin();
+        NodeList::const_iterator i2 = lst2->begin();
+        while( i1!=lst1->end() ){
+            Node y = *i1;
+            Node z = *i2;
+			Trace("strings-nf") << "Inductive equation : " << x << " = ( " << y << " ++ " << z << " ) * " << y << std::endl;
+            ++i1;
+            ++i2;
         }
-        Trace("strings-eqc") << std::endl;
-    //}
-    ++eqcs2_i;
-  }
+    }
 
-  bool addedFact = false;
+  bool addedFact;
   do {
+	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;
-      eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-      d_lemma_cache.clear();
-      while( !eqcs_i.isFinished() ){
-        Node eqc = (*eqcs_i);
-        //if eqc.getType is string
-        if (eqc.getType().isString()) {
-            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);
-            if( d_conflict ){
-                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() ? NodeManager::currentNM()->mkConst(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 = 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] );
-                    Trace("strings-lemma") << "Strings (by normal forms) : Infer " << eq << " from " << eq_exp << std::endl;
-                    //d_equalityEngine.assertEquality( eq, true, eq_exp );
-                    d_pending.push_back( eq );
-                    d_pending_exp[eq] = eq_exp;
-                    d_infer.push_back(eq);
-                    d_infer_exp.push_back(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;
-        }
-        ++eqcs_i;
-      }
+    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);
+		if( d_conflict ){
+			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 = 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] );
+				Trace("strings-lemma") << "Strings (by normal forms) : Infer " << eq << " from " << eq_exp << std::endl;
+				//d_equalityEngine.assertEquality( eq, true, eq_exp );
+				d_pending.push_back( eq );
+				d_pending_exp[eq] = eq_exp;
+				d_infer.push_back(eq);
+				d_infer_exp.push_back(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 ){
+		Trace("strings-nf-debug") << "  normal_form(" << it->second << ") = " << it->first << std::endl;
+	  }
+	  Trace("strings-nf-debug") << std::endl;
       addedFact = !d_pending.empty();
       doPendingFacts();
-      if( !d_conflict ){
-          for( unsigned i=0; i<d_lemma_cache.size(); i++ ){
-              Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl;
-              d_out->lemma( d_lemma_cache[i] );
-          }
-          if( !d_lemma_cache.empty() ){
-            d_lemma_cache.clear();
-            return true;
-          }
-      }
-  } while (!d_conflict && addedFact);
-  return false;
+  } while ( !d_conflict && d_lemma_cache.empty() && addedFact );
+
+
+  //process disequalities between equivalence classes
+  if( !d_conflict && d_lemma_cache.empty() ){
+	  std::vector< Node > eqcs;
+	  getEquivalenceClasses( eqcs );
+	  std::vector< std::vector< Node > > cols;
+	  std::vector< Node > lts;
+	  seperateByLength( eqcs, cols, lts );
+	  for( unsigned i=0; i<cols.size(); i++ ){
+	    if( cols[i].size()>1 && d_lemma_cache.empty() ){
+			Trace("strings-solve") << "- Verify disequalities are processed for ";
+			printConcat( d_normal_forms[cols[i][0]], "strings-solve" );
+			Trace("strings-solve")  << "..." << std::endl;
+			//must ensure that normal forms are disequal
+			for( unsigned j=1; j<cols[i].size(); j++ ){
+				if( !d_equalityEngine.areDisequal( cols[i][0], cols[i][j], false ) ){
+					sendSplit( cols[i][0], cols[i][j], "Disequality Normalization" );
+					break;
+				}else{
+					Trace("strings-solve") << "  against ";
+					printConcat( d_normal_forms[cols[i][j]], "strings-solve" );
+					Trace("strings-solve")  << "..." << std::endl;
+					if( normalizeDisequality( cols[i][0], cols[i][j] ) ){
+						break;
+					}
+				}
+			}
+		}
+	  }
+  }
+
+  //flush pending lemmas
+  if( !d_conflict && !d_lemma_cache.empty() ){
+	doPendingLemmas();
+	return true;
+  }else{
+	return false;
+  }
 }
 
 bool TheoryStrings::checkCardinality() {
   int cardinality = options::stringCharCardinality();
   Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl;
 
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-  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;
-  while( !eqcs_i.isFinished() ){
-    Node eqc = (*eqcs_i);
-    //if eqc.getType is string
-    if (eqc.getType().isString()) {
-        EqcInfo* ei = getOrMakeEqcInfo( eqc, true );
-        Node lt = ei->d_length_term;
-        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++;
-        }
-    }
-    ++eqcs_i;
-  }
-  for( std::map< unsigned, std::vector< Node > >::iterator it = eqc_to_strings.begin(); it != eqc_to_strings.end(); ++it ){
-    Node lr = leqc_to_eqc[it->first];
-    Trace("string-cardinality") << "Number of strings with length equal to " << lr << " is " << it->second.size() << std::endl;
+  std::vector< Node > eqcs;
+  getEquivalenceClasses( eqcs );
+
+  std::vector< std::vector< Node > > cols;
+  std::vector< Node > lts;
+  seperateByLength( eqcs, cols, lts );
+
+  for( unsigned i = 0; i<cols.size(); ++i ){
+    Node lr = lts[i];
+    Trace("string-cardinality") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl;
     // size > c^k
-    double k = std::log( it->second.size() ) / log((double) cardinality);
+    double k = std::log( cols[i].size() ) / log((double) cardinality);
     unsigned int int_k = (unsigned int)k;
     Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) );
     //double c_k = pow ( (double)cardinality, (double)lr );
-    if( it->second.size() > 1 ) {
+    if( cols[i].size() > 1 ) {
         bool allDisequal = true;
-        for( std::vector< Node >::iterator itr1 = it->second.begin();
-              itr1 != it->second.end(); ++itr1) {
+        for( std::vector< Node >::iterator itr1 = cols[i].begin();
+              itr1 != cols[i].end(); ++itr1) {
             for( std::vector< Node >::iterator itr2 = itr1 + 1;
-                  itr2 != it->second.end(); ++itr2) {
+                  itr2 != cols[i].end(); ++itr2) {
                 if(!d_equalityEngine.areDisequal( *itr1, *itr2, false )) {
                     allDisequal = false;
                     // add split lemma
-                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, *itr1, *itr2 );
-                    Node neq = NodeManager::currentNM()->mkNode( kind::NOT, eq );
-                    Node lemma_or = NodeManager::currentNM()->mkNode( kind::OR, eq, neq );
-                    Trace("strings-lemma") << "Strings split lemma : " << lemma_or << std::endl;
-                    d_out->lemma(lemma_or);
-                    return true;
+					sendSplit( *itr1, *itr2, "Cardinality" );
+					doPendingLemmas();
+					return true;
                 }
             }
         }
         if(allDisequal) {
             EqcInfo* ei = getOrMakeEqcInfo( lr, true );
-            Trace("string-cardinality") << "Previous cardinality used for " << lr << " is " << ei->d_cardinality_lem_k << std::endl;
-            if( int_k > ei->d_cardinality_lem_k.get() ){
+            Trace("string-cardinality") << "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() ){
                 //add cardinality lemma
-                Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, it->second );
+                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 = it->second.begin();
-                      itr1 != it->second.end(); ++itr1) {
+                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 = NodeManager::currentNM()->mkNode( kind::EQUAL, lr, len );
@@ -1205,13 +1452,24 @@ bool TheoryStrings::checkCardinality() {
                     }
                 }
                 Node antc = NodeManager::currentNM()->mkNode( kind::AND, vec_node );
-                Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, it->second[0] );
+                Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] );
                 Node cons = NodeManager::currentNM()->mkNode( kind::GT, 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 );
-                Trace("strings-lemma") << "Strings cardinaliry lemma : " << lemma << std::endl;
-                d_out->lemma(lemma);
-                ei->d_cardinality_lem_k.set( k );
-                return true;
+				lemma = Rewriter::rewrite( lemma );
+				ei->d_cardinality_lem_k.set( int_k+1 );
+				if( lemma!=d_true ){
+					Trace("strings-lemma") << "Strings cardinality lemma : " << lemma << std::endl;
+					d_out->lemma(lemma);
+					return true;
+				}
             }
         }
     }
@@ -1219,67 +1477,235 @@ bool TheoryStrings::checkCardinality() {
   return false;
 }
 
+int TheoryStrings::gcd ( int a, int b ) {
+  int c;
+  while ( a != 0 ) {
+     c = a; a = b%a;  b = c;
+  }
+  return b;
+}
+
 bool TheoryStrings::checkInductiveEquations() {
     bool hasEq = false;
-    Trace("strings-ind")  << "We are sat, with these inductive equations : " << std::endl;
-    for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){
-        Node x = (*it).first;
-        NodeList* lst1 = (*it).second;
-        NodeList* lst2 = (*d_ind_map2.find(x)).second;
-        NodeList* lste = (*d_ind_map_exp.find(x)).second;
-        NodeList* lstl = (*d_ind_map_lemma.find(x)).second;
-        NodeList::const_iterator i1 = lst1->begin();
-        NodeList::const_iterator i2 = lst2->begin();
-        NodeList::const_iterator ie = lste->begin();
-        NodeList::const_iterator il = lstl->begin();
-        while( i1!=lst1->end() ){
-            Node y = *i1;
-            Node z = *i2;
-            Node exp = *ie;
-            Trace("strings-ind") << "Inductive equation : " << x << " = ( " << y << "..." << z << " )* " << y << std::endl;
-            if( il==lstl->end() ) {
-                Trace("strings-ind") << "Add length lemma..." << std::endl;
-                Node lemma_len;
-                if( y.getKind()!=kind::STRING_CONCAT || z.getKind()!=kind::STRING_CONCAT ) {
-                    Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x );
-                    Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y );
-                    lemma_len = NodeManager::currentNM()->mkNode( kind::GEQ, len_x, len_y );
-                } else {
-                    // both constants
-                    Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x );
-                    Node sk = NodeManager::currentNM()->mkSkolem( "argsym_$$", NodeManager::currentNM()->integerType(), "created for length inductive lemma" );
-                    Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y );
-                    Node len_z = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, z );
-                    Node len_y_plus_len_z =    NodeManager::currentNM()->mkNode( kind::PLUS, len_y, len_z );
-                    Node y_p_z_t_a =    NodeManager::currentNM()->mkNode( kind::MULT, len_y_plus_len_z, sk );
-                    Node y_p_z_t_a_p_y =    NodeManager::currentNM()->mkNode( kind::PLUS, y_p_z_t_a, len_y );
-                    lemma_len =     NodeManager::currentNM()->mkNode( kind::EQUAL, y_p_z_t_a_p_y, len_x );
-                    Node sk_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk, d_zero );
-                    lemma_len = NodeManager::currentNM()->mkNode( kind::AND, lemma_len, sk_geq_zero );
-                }
-                lemma_len =     NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, lemma_len );
-                Trace("strings-lemma") << "Strings: Add lemma " << lemma_len << std::endl;
-                d_out->lemma(lemma_len);
-                lstl->push_back( d_true );
-                return true;
-            }
-
-            ++i1;
-            ++i2;
-            ++ie;
-            ++il;
-            hasEq = true;
-        }
-    }
+	if(d_ind_map1.size() != 0){
+		Trace("strings-ind")  << "We are sat, with these inductive equations : " << std::endl;
+		for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){
+			Node x = (*it).first;
+			Trace("strings-ind-debug") << "Check eq for " << x << std::endl;
+			NodeList* lst1 = (*it).second;
+			NodeList* lst2 = (*d_ind_map2.find(x)).second;
+			NodeList* lste = (*d_ind_map_exp.find(x)).second;
+			//NodeList* lstl = (*d_ind_map_lemma.find(x)).second;
+			NodeList::const_iterator i1 = lst1->begin();
+			NodeList::const_iterator i2 = lst2->begin();
+			NodeList::const_iterator ie = lste->begin();
+			//NodeList::const_iterator il = lstl->begin();
+			while( i1!=lst1->end() ){
+				Node y = *i1;
+				Node z = *i2;
+				//Trace("strings-ind-debug") << "Check y=" << y << " , z=" << z << std::endl;
+				//if( il==lstl->end() ) {
+					std::vector< Node > nf_y, nf_z, exp_y, exp_z;
+					
+					//getFinalNormalForm( y, nf_y, exp_y);
+					//getFinalNormalForm( z, nf_z, exp_z);
+					//std::vector< Node > vec_empty;
+					//Node nexp_y = mkExplain( exp_y, vec_empty );
+					//Trace("strings-ind-debug") << "Check nexp_y=" << nexp_y << std::endl;
+					//Node nexp_z = mkExplain( exp_z, vec_empty );
+
+					//Node exp = *ie;
+					//Trace("strings-ind-debug") << "Check exp=" << exp << std::endl;
+
+					//exp = NodeManager::currentNM()->mkNode( kind::AND, exp, nexp_y, nexp_z );
+					//exp = Rewriter::rewrite( exp );
+
+					Trace("strings-ind") << "Inductive equation : " << x << " = ( " << y << " ++ " << z << " )* " << y << std::endl;
+					/*
+					for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) {
+						Trace("strings-ind") << (*itr) << " ";
+					}
+					Trace("strings-ind") << " ++ ";
+					for( std::vector< Node >::const_iterator itr = nf_z.begin(); itr != nf_z.end(); ++itr) {
+						Trace("strings-ind") << (*itr) << " ";
+					}
+					Trace("strings-ind") << " )* ";
+					for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) {
+						Trace("strings-ind") << (*itr) << " ";
+					}
+					Trace("strings-ind") << std::endl;
+					*/
+					/*
+					Trace("strings-ind") << "Explanation is : " << exp << std::endl;
+					std::vector< Node > nf_yz;
+					nf_yz.insert( nf_yz.end(), nf_y.begin(), nf_y.end() );
+					nf_yz.insert( nf_yz.end(), nf_z.begin(), nf_z.end() );
+					std::vector< std::vector< Node > > cols;
+					std::vector< Node > lts;
+					seperateByLength( nf_yz, cols, lts );
+					Trace("strings-ind") << "This can be grouped into collections : " << std::endl;
+					for( unsigned j=0; j<cols.size(); j++ ){
+						Trace("strings-ind") << "  : ";
+						for( unsigned k=0; k<cols[j].size(); k++ ){
+							Trace("strings-ind") << cols[j][k] << " ";
+						}
+						Trace("strings-ind") << std::endl;
+					}
+					Trace("strings-ind") << std::endl;
+					
+					Trace("strings-ind") << "Add length lemma..." << std::endl;
+					std::vector< int > co;
+					co.push_back(0);
+					for(unsigned int k=0; k<lts.size(); ++k) {
+						if(lts[k].isConst() && lts[k].getType().isInteger()) {
+							int len = lts[k].getConst<Rational>().getNumerator().toUnsignedInt();
+							co[0] += cols[k].size() * len;
+						} else {
+							co.push_back( cols[k].size() );
+						}
+					}
+					int g_co = co[0];
+					for(unsigned k=1; k<co.size(); ++k) {
+						g_co = gcd(g_co, co[k]);
+					}
+					Node lemma_len;
+					// both constants
+					Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x );
+					Node sk = NodeManager::currentNM()->mkSkolem( "argsym_$$", NodeManager::currentNM()->integerType(), "created for length inductive lemma" );
+					Node g_co_node = NodeManager::currentNM()->mkConst( CVC4::Rational(g_co) );
+					Node sk_m_gcd = NodeManager::currentNM()->mkNode( kind::MULT, g_co_node, sk );
+					Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y );
+					Node sk_m_g_p_y =    NodeManager::currentNM()->mkNode( kind::PLUS, sk_m_gcd, len_y );
+					lemma_len =     NodeManager::currentNM()->mkNode( kind::EQUAL, sk_m_g_p_y, len_x );
+					//Node sk_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk, d_zero );
+					//lemma_len = NodeManager::currentNM()->mkNode( kind::AND, lemma_len, sk_geq_zero );
+					lemma_len =     NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, lemma_len );
+					Trace("strings-lemma") << "Strings: Add lemma " << lemma_len << std::endl;
+					d_out->lemma(lemma_len);
+					lstl->push_back( d_true );
+					return true;*/
+				//}
+				++i1;
+				++i2;
+				++ie;
+				//++il;
+				if( !d_equalityEngine.hasTerm( d_emptyString ) || !d_equalityEngine.areEqual( y, d_emptyString ) || !d_equalityEngine.areEqual( x, d_emptyString ) ){
+					hasEq = true;
+				}
+			}
+		}
+	}
     if( hasEq ){
+		Trace("strings-ind") << "It is incomplete." << std::endl;
         d_out->setIncomplete();
-    }
+    }else{
+		Trace("strings-ind") << "We can answer SAT." << std::endl;
+	}
   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;
+    }
+}
+
+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++ ){
+				getFinalNormalForm( n[i], nf, exp );
+			}
+		}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() ){
+				nf.push_back( nc );
+				if( n!=nc ){
+					exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n, nc ) );
+				}
+			}else{
+				Assert( d_normal_forms.find( nr )!=d_normal_forms.end() );
+				if( d_normal_forms[nr][0]==nr ){
+					Assert( d_normal_forms[nr].size()==1 );
+					nf.push_back( 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++ ){
+						Assert( d_normal_forms[nr][i]!=nr );
+						getFinalNormalForm( d_normal_forms[nr][i], nf, exp );
+					}
+					exp.insert( exp.end(), d_normal_forms_exp[nr].begin(), d_normal_forms_exp[nr].end() );
+				}
+			}
+			Trace("strings-ind-nf") << "The final normal form of " << n << " is " << nf << std::endl;
+		}
+	}
+}
 
+void TheoryStrings::seperateByLength( 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( 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 );
+  }
+}
 
+void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) {
+	for( unsigned i=0; i<n.size(); i++ ){
+		if( i>0 ) Trace(c) << " ++ ";
+		Trace(c) << n[i];
+	}
+}
 
+/*
+Node TheoryStrings::getNextDecisionRequest() {
+	if( d_lit_to_decide_index.get()<d_lit_to_decide.size() ){
+		Node l = d_lit_to_decide[d_lit_to_decide_index.get()];
+		d_lit_to_decide_index.set( d_lit_to_decide_index.get() + 1 );
+		Trace("strings-ind") << "Strings-ind : decide on " << l << std::endl;
+		return l;
+	}else{
+		return Node::null();
+	}
+}
+*/
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index a6644b8bb..6b8144d6e 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -36,6 +36,7 @@ namespace strings {
 class TheoryStrings : public Theory {
   typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   public:
 
   TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
@@ -45,7 +46,11 @@ class TheoryStrings : public Theory {
 
   std::string identify() const { return std::string("TheoryStrings"); }
 
-
+  Node getRepresentative( Node t );
+  bool hasTerm( Node a );
+  bool areEqual( Node a, Node b );
+  bool areDisequal( Node a, Node b );
+  Node getLength( Node t );
   public:
 
   void propagate(Effort e);
@@ -113,7 +118,7 @@ class TheoryStrings : public Theory {
     eq::EqualityEngine d_equalityEngine;
     /** Are we in conflict */
     context::CDO<bool> d_conflict;
-
+	std::vector< Node > d_length_intro_vars;
     Node d_emptyString;
     Node d_true;
     Node d_false;
@@ -122,8 +127,7 @@ class TheoryStrings : public Theory {
       std::map< Node, Node > d_pending_exp;
       std::vector< Node > d_pending;
       std::vector< Node > d_lemma_cache;
-  bool hasTerm( Node a );
-  bool areEqual( Node a, Node b );
+	  std::map< Node, bool > d_pending_req_phase;
   /** inferences */
   NodeList d_infer;
   NodeList d_infer_exp;
@@ -137,7 +141,11 @@ class TheoryStrings : public Theory {
   NodeListMap d_ind_map2;
   NodeListMap d_ind_map_exp;
   NodeListMap d_ind_map_lemma;
-  void addInductiveEquation( Node x, Node y, Node z, Node exp );
+  bool addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c );
+
+  //for unrolling inductive equations
+  NodeBoolMap d_lit_to_unroll;
+
 
   /////////////////////////////////////////////////////////////////////////////
   // MODEL GENERATION
@@ -158,8 +166,8 @@ class TheoryStrings : public Theory {
   // MAIN SOLVER
   /////////////////////////////////////////////////////////////////////////////
   private:
-  void dealPositiveWordEquation(TNode n);
   void addSharedTerm(TNode n);
+  EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   private:
   class EqcInfo
@@ -183,11 +191,12 @@ class TheoryStrings : public Theory {
     void 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 areLengthsEqual( Node n1, Node n2 ); //TODO
+    bool normalizeDisequality( Node n1, Node n2 );
 
     bool checkNormalForms();
     bool checkCardinality();
     bool checkInductiveEquations();
+	int gcd(int a, int b);
   public:
   void preRegisterTerm(TNode n);
   void check(Effort e);
@@ -208,11 +217,24 @@ protected:
 
   //do pending merges
   void doPendingFacts();
+  void doPendingLemmas();
 
+  void sendLemma( Node ant, Node conc, const char * c );
+  void sendSplit( Node a, Node b, const char * c );
   /** mkConcat **/
   Node mkConcat( std::vector< Node >& c );
   /** mkExplain **/
   Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
+
+  //get equivalence classes
+  void getEquivalenceClasses( std::vector< Node >& eqcs );
+  //get final normal form
+  void getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp );
+
+  //seperate into collections with equal length
+  void seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
+private:
+  void printConcat( std::vector< Node >& n, const char * c );
 };/* class TheoryStrings */
 
 }/* CVC4::theory::strings namespace */
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
new file mode 100644
index 000000000..d62fd4c9e
--- /dev/null
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -0,0 +1,120 @@
+/*********************                                                        */

+/*! \file theory_strings_preprocess.cpp

+ ** \verbatim

+ ** Original author: Tianyi Liang

+ ** Major contributors: Tianyi Liang, Andrew Reynolds

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2013-2013  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Strings Preprocess

+ **

+ ** Strings Preprocess.

+ **/

+

+#include "theory/strings/theory_strings_preprocess.h"

+#include "expr/kind.h"

+

+namespace CVC4 {

+namespace theory {

+namespace strings {

+

+void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) {

+	int k = r.getKind();

+	switch( k ) {

+		case kind::STRING_TO_REGEXP:

+		{

+			Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] );

+			ret.push_back( eq );

+		}

+			break;

+		case kind::REGEXP_CONCAT:

+		{

+			std::vector< Node > cc;

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

+				Node sk = NodeManager::currentNM()->mkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" );

+				simplifyRegExp( sk, r[i], ret );

+				cc.push_back( sk );

+			}

+			Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, 

+						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) );

+			ret.push_back( cc_eq );

+		}

+			break;

+		case kind::REGEXP_OR:

+		{

+			std::vector< Node > c_or;

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

+				simplifyRegExp( s, r[i], c_or );

+			}

+			Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or );

+			ret.push_back( eq );

+		}

+			break;

+		case kind::REGEXP_INTER:

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

+				simplifyRegExp( s, r[i], ret );

+			}

+			break;

+		case kind::REGEXP_STAR:

+		{

+			Node sk = NodeManager::currentNM()->mkSkolem( "ressym_$$", s.getType(), "created for regular expression star" );

+			Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,

+						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, s ),

+						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, sk ));

+			ret.push_back( eq );

+			simplifyRegExp( sk, r[0], ret );

+		}

+			break;

+		case kind::REGEXP_OPT:

+		{

+			Node eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );

+			std::vector< Node > rr;

+			simplifyRegExp( s, r[0], rr );

+			Node nrr = rr.size()==1 ? rr[0] : NodeManager::currentNM()->mkNode( kind::AND, rr );

+			ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) );

+		}

+			break;

+		default:

+			//TODO:case kind::REGEXP_PLUS:

+			//TODO: special sym: sigma, none, all

+			break;

+	}

+}

+

+Node StringsPreprocess::simplify( Node t ) {

+	if( t.getKind() == kind::STRING_IN_REGEXP ){

+		// t0 in t1

+		//rewrite it

+		std::vector< Node > ret;

+		simplifyRegExp( t[0], t[1], ret );

+

+		return ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );

+    }else if( t.getNumChildren()>0 ){

+		std::vector< Node > cc;

+		if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {

+			cc.push_back(t.getOperator());

+		}

+		bool changed = false;

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

+			Node tn = simplify( t[i] );

+			cc.push_back( tn );

+			changed = changed || tn!=t[i];

+		}

+		return changed ? NodeManager::currentNM()->mkNode( t.getKind(), cc ) : t;

+	}else{

+		return t;

+	}

+}

+

+void StringsPreprocess::simplify(std::vector< Node > &vec_node) {

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

+		vec_node[i] = simplify( vec_node[i] );

+	}

+}

+

+}/* CVC4::theory::strings namespace */

+}/* CVC4::theory namespace */

+}/* CVC4 namespace */

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
new file mode 100644
index 000000000..2b2e7dfea
--- /dev/null
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -0,0 +1,41 @@
+/*********************                                                        */

+/*! \file theory_strings_preprocess.h

+ ** \verbatim

+ ** Original author: Tianyi Liang

+ ** Major contributors: Tianyi Liang, Andrew Reynolds

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2013-2013  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Strings Preprocess

+ **

+ ** Strings Preprocess.

+ **/

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__THEORY__STRINGS__PREPROCESS_H

+#define __CVC4__THEORY__STRINGS__PREPROCESS_H

+

+#include <vector>

+#include "theory/theory.h"

+

+namespace CVC4 {

+namespace theory {

+namespace strings {

+

+class StringsPreprocess {

+private:

+	void simplifyRegExp( Node s, Node r, std::vector< Node > &ret );

+	Node simplify( Node t );

+public:

+void simplify(std::vector< Node > &vec_node);

+};

+

+}/* CVC4::theory::strings namespace */

+}/* CVC4::theory namespace */

+}/* CVC4 namespace */

+

+#endif /* __CVC4__THEORY__STRINGS__PREPROCESS_H */

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index bf284ea7b..9c3d6c71e 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -181,6 +181,9 @@ public:
     if (!t.isString()) {
       throw TypeCheckingExceptionPrivate(n, "expecting string terms");
     }
+	if( (*it).getKind() != kind::CONST_STRING ) {
+      throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
+	}
     if(++it != it_end) {
       throw TypeCheckingExceptionPrivate(n, "too many terms");
     }
diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h
index 3ab9df0cd..3dc12009b 100644
--- a/src/theory/strings/type_enumerator.h
+++ b/src/theory/strings/type_enumerator.h
@@ -31,34 +31,98 @@ namespace theory {
 namespace strings {
 
 class StringEnumerator : public TypeEnumeratorBase<StringEnumerator> {
-  unsigned d_int;
-
+	std::vector< unsigned > d_data;
+	unsigned d_cardinality;
+	Node d_curr;
+	void mkCurr() {
+		//make constant from d_data
+		d_curr = NodeManager::currentNM()->mkConst( ::CVC4::String( d_data ) );
+	}
 public:
 
   StringEnumerator(TypeNode type) throw(AssertionException) :
-    TypeEnumeratorBase<StringEnumerator>(type),
-    d_int(0) {
+    TypeEnumeratorBase<StringEnumerator>(type) {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == STRING_TYPE);
+	d_cardinality = 256;
+	mkCurr();
   }
-
   Node operator*() throw() {
-    std::stringstream ss;
-    ss << d_int;
-    return NodeManager::currentNM()->mkConst( ::CVC4::String( ss.str() ) );
+    return d_curr;
   }
-
   StringEnumerator& operator++() throw() {
-    d_int++;
+	bool changed = false;
+	do{
+		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_data.push_back( 0 );
+		}
+	}while(!changed);
+
+	mkCurr();
     return *this;
   }
 
   bool isFinished() throw() {
-    return false;
+    return d_curr.isNull();
   }
 
 };/* class StringEnumerator */
 
+
+class StringEnumeratorLength {
+private:
+	unsigned d_cardinality;
+	std::vector< unsigned > d_data;
+	Node d_curr;
+	void mkCurr() {
+		//make constant from d_data
+		d_curr = NodeManager::currentNM()->mkConst( ::CVC4::String( d_data ) );
+	}
+public:
+  StringEnumeratorLength(unsigned length, unsigned card = 256) : d_cardinality(card) {
+     for( unsigned i=0; i<length; i++ ){
+		d_data.push_back( 0 );
+	 }
+	 mkCurr();
+  }
+
+  Node operator*() throw() {
+    return d_curr;
+  }
+
+  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();
+	}
+    return *this;
+  }
+
+  bool isFinished() throw() {
+    return d_curr.isNull();
+  }
+};
+
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 448e3a8fa..d4f08fcdd 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -371,6 +371,7 @@ void TheoryEngine::check(Theory::Effort effort) {
 
     // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
     if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) {
+		//d_theoryTable[THEORY_STRINGS]->check(Theory::EFFORT_LAST_CALL);
       if(d_logicInfo.isQuantified()) {
         // quantifiers engine must pass effort last call check
         d_quantEngine->check(Theory::EFFORT_LAST_CALL);
diff --git a/src/util/regexp.h b/src/util/regexp.h
index debb57e4c..58f58a40f 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -122,13 +122,13 @@ public:
 
   String(const std::string &s) {
     for(unsigned int i=0; i<s.size(); ++i) {
-        d_str.push_back( (unsigned int)s[i] );
+        d_str.push_back( convertCharToUnsignedInt(s[i]) );
     }
   }
 
   String(const char* s) {
     for(unsigned int i=0,len=strlen(s); i<len; ++i) {
-        d_str.push_back( (unsigned int)s[i] );
+        d_str.push_back( convertCharToUnsignedInt(s[i]) );
     }
   }
 
@@ -207,7 +207,8 @@ public:
   std::string toString() const {
     std::string str;
     for(unsigned int i=0; i<d_str.size(); ++i) {
-      str += (char)d_str[i];
+      str += convertUnsignedIntToChar( d_str[i] );
+	  //TODO isPrintable: ( "\\" + (convertUnsignedIntToChar( d_str[i] ) );
     }
     return str;
   }
@@ -232,6 +233,22 @@ public:
     ret_vec.insert( ret_vec.end(), itr, itr + j );
       return String(ret_vec);
   }
+
+public:
+  static unsigned int convertCharToUnsignedInt( char c ) {
+	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);
+  }
+  static bool isPrintable( unsigned int i ){
+	char c = convertUnsignedIntToChar( i );
+	return isprint( (int)c );
+  }
+
 };/* class String */
 
 namespace strings {
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 269ec49ed..a1ae66a5f 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -25,11 +25,14 @@ TESTS =	\
   str003.smt2 \
   str004.smt2 \
   str005.smt2 \
-  loop001.smt2
-# loop002.smt2 \
-# loop003.smt2 \
-# loop004.smt2 \
-# loop005.smt2 \
+  model001.smt2 \
+  loop001.smt2 \
+  loop003.smt2 \
+  loop007.smt2
+
+# loop002.smt2
+# loop004.smt2
+# loop005.smt2
 # loop006.smt2
 
 FAILING_TESTS =
diff --git a/test/regress/regress0/strings/cardinality.smt2 b/test/regress/regress0/strings/cardinality.smt2
index 5c4771d71..465ea0b5e 100644
--- a/test/regress/regress0/strings/cardinality.smt2
+++ b/test/regress/regress0/strings/cardinality.smt2
@@ -1,7 +1,7 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status unsat)
 
-(set-option :str-cardinality 2)
+(set-option :str-alphabet-card 2)
 
 (declare-fun x () String)
 (declare-fun y () String)
diff --git a/test/regress/regress0/strings/loop002.smt2 b/test/regress/regress0/strings/loop002.smt2
index a47b959f5..2f96241dc 100644
--- a/test/regress/regress0/strings/loop002.smt2
+++ b/test/regress/regress0/strings/loop002.smt2
@@ -1,16 +1,9 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-; EXIT: 10
-;
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-fun x () String)
 (declare-fun y () String)
 (declare-fun z () String)
-(declare-fun w () String)
-(declare-fun w1 () String)
-(declare-fun w2 () String)
 
 (assert (= (str.++ x "ba") (str.++ "ab" x)))
 
diff --git a/test/regress/regress0/strings/loop003.smt2 b/test/regress/regress0/strings/loop003.smt2
index a535f7583..b4fbcf7d5 100644
--- a/test/regress/regress0/strings/loop003.smt2
+++ b/test/regress/regress0/strings/loop003.smt2
@@ -1,7 +1,3 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-; EXIT: 10
-;
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 
diff --git a/test/regress/regress0/strings/loop004.smt2 b/test/regress/regress0/strings/loop004.smt2
index 7b39bf2d3..8d2ff8096 100644
--- a/test/regress/regress0/strings/loop004.smt2
+++ b/test/regress/regress0/strings/loop004.smt2
@@ -1,8 +1,4 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-; EXIT: 10
-;
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status sat)
 
 (declare-fun x () String)
diff --git a/test/regress/regress0/strings/loop005.smt2 b/test/regress/regress0/strings/loop005.smt2
index ec294b9bb..6e5fc96d4 100644
--- a/test/regress/regress0/strings/loop005.smt2
+++ b/test/regress/regress0/strings/loop005.smt2
@@ -2,7 +2,7 @@
 ; EXPECT: sat
 ; EXIT: 10
 ;
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status sat)
 
 (declare-fun x () String)
diff --git a/test/regress/regress0/strings/loop006.smt2 b/test/regress/regress0/strings/loop006.smt2
index 8c3690c61..288a5f60c 100644
--- a/test/regress/regress0/strings/loop006.smt2
+++ b/test/regress/regress0/strings/loop006.smt2
@@ -1,8 +1,4 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-; EXIT: 10
-;
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status sat)
 
 (declare-fun x () String)
@@ -12,6 +8,8 @@
 (declare-fun w1 () String)
 (declare-fun w2 () String)
 
-(assert (= (str.++ x y z) (str.++ x z y)))
+;(assert (= (str.++ x y) (str.++ y x)))
+
+(assert (not (= (str.++ x y) (str.++ y x))))
 
 (check-sat)
diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2
new file mode 100644
index 000000000..8d789edb3
--- /dev/null
+++ b/test/regress/regress0/strings/loop007.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL_SUPPORTED)

+(set-info :status sat)

+

+(declare-fun x () String)

+(declare-fun y () String)

+

+(assert (= (str.++ x y "aa") (str.++ "aa" y x)))

+(assert (= (str.len x) 1))

+

+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/model001.smt2 b/test/regress/regress0/strings/model001.smt2
new file mode 100644
index 000000000..e4e35f40d
--- /dev/null
+++ b/test/regress/regress0/strings/model001.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL_SUPPORTED)

+(set-info :status sat)

+(set-option :produce-models true)

+

+(declare-fun x () String)

+(declare-fun y () String)

+

+(assert (not (= x y)))

+(assert (= (str.len x) (str.len y)))

+

+(check-sat)

+;(get-model)

diff --git a/test/regress/regress0/strings/str001.smt2 b/test/regress/regress0/strings/str001.smt2
index 8ae10edbe..bb2b701d8 100644
--- a/test/regress/regress0/strings/str001.smt2
+++ b/test/regress/regress0/strings/str001.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status unsat)
 
 (declare-fun xx () String)
diff --git a/test/regress/regress0/strings/str002.smt2 b/test/regress/regress0/strings/str002.smt2
index 98b3e1e00..62512ef79 100644
--- a/test/regress/regress0/strings/str002.smt2
+++ b/test/regress/regress0/strings/str002.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status unsat)
 
 (declare-fun xx () String)
diff --git a/test/regress/regress0/strings/str003.smt2 b/test/regress/regress0/strings/str003.smt2
index c88e1233e..0ced7f447 100644
--- a/test/regress/regress0/strings/str003.smt2
+++ b/test/regress/regress0/strings/str003.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status unsat)
 
 (declare-fun xx () String)
diff --git a/test/regress/regress0/strings/str004.smt2 b/test/regress/regress0/strings/str004.smt2
index d4763adee..8a03f4481 100644
--- a/test/regress/regress0/strings/str004.smt2
+++ b/test/regress/regress0/strings/str004.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status unsat)
 
 (declare-fun xx () String)
diff --git a/test/regress/regress0/strings/str005.smt2 b/test/regress/regress0/strings/str005.smt2
index 4916b1df4..84cb5af01 100644
--- a/test/regress/regress0/strings/str005.smt2
+++ b/test/regress/regress0/strings/str005.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status unsat)
 
 (declare-fun xx () String)