merged golden

21 files changed, 1325 insertions, 649 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c84046570..885a7c487 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -141,7 +141,7 @@ static bool isClosed(Expr e, std::set<Expr>& free, std::hash_set<Expr, ExprHashF
   if(e.getKind() == kind::FORALL || e.getKind() == kind::EXISTS || e.getKind() == kind::LAMBDA) {
     isClosed(e[1], free, closedCache);
     for(Expr::const_iterator i = e[0].begin(); i != e[0].end(); ++i) {
-      free.erase((*i)[0]);
+      free.erase(*i);
     }
   } else if(e.getKind() == kind::BOUND_VARIABLE) {
     free.insert(e);
@@ -870,10 +870,6 @@ 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]
@@ -1250,6 +1246,7 @@ builtinOp[CVC4::Kind& kind]
 
   | STRCON_TOK     { $kind = CVC4::kind::STRING_CONCAT; }
   | STRLEN_TOK     { $kind = CVC4::kind::STRING_LENGTH; }
+  | STRSUB_TOK     { $kind = CVC4::kind::STRING_SUBSTR; }
   | STRINRE_TOK    { $kind = CVC4::kind::STRING_IN_REGEXP; }
   | STRTORE_TOK    { $kind = CVC4::kind::STRING_TO_REGEXP; }
   | RECON_TOK      { $kind = CVC4::kind::REGEXP_CONCAT; }
@@ -1622,7 +1619,7 @@ INT2BV_TOK : 'int2bv';
 //STRCST_TOK : 'str.cst';
 STRCON_TOK : 'str.++';
 STRLEN_TOK : 'str.len';
-//STRSUB_TOK : 'str.sub' ;
+STRSUB_TOK : 'str.sub' ;
 STRINRE_TOK : 'str.in.re';
 STRTORE_TOK : 'str.to.re';
 RECON_TOK : 're.++';
diff --git a/src/smt/options b/src/smt/options
index 7a72881b4..d2455b520 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -49,7 +49,7 @@ option repeatSimp --repeat-simp bool :read-write
  make multiple passes with nonclausal simplifier
 
 option sortInference --sort-inference bool :read-write :default false
- apply sort inference to input problem
+ calculate sort inference of input problem, convert the input based on monotonic sorts
 
 common-option incrementalSolving incremental -i --incremental bool
  enable incremental solving
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 39ccc70c4..be6acd09c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -835,7 +835,7 @@ void SmtEngine::setLogicInternal() throw() {
 
   // Set the options for the theoryOf
   if(!options::theoryOfMode.wasSetByUser()) {
-    if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) {
+    if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV) && !d_logic.isTheoryEnabled(THEORY_STRINGS)) {
       Trace("smt") << "setting theoryof-mode to term-based" << endl;
       options::theoryOfMode.set(THEORY_OF_TERM_BASED);
     }
@@ -1031,6 +1031,10 @@ void SmtEngine::setLogicInternal() throw() {
       options::fmfInstGen.set( false );
     }
   }
+  if ( options::fmfBoundInt() ){
+    //if bounded integers are set, must use full model check for MBQI
+    options::fmfFullModelCheck.set( true );
+  }
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
   }
@@ -1979,7 +1983,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   }
   d_nonClausalLearnedLiterals.clear();
 
-  
+
   for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
     Node cProp = (*pos).first.eqNode((*pos).second);
     Assert(d_topLevelSubstitutions.apply(cProp) == cProp);
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 186444e0a..0bbef1601 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -32,7 +32,7 @@ class DatatypesRewriter {
 public:
 
   static RewriteResponse postRewrite(TNode in) {
-    Trace("datatypes-rewrite") << "post-rewriting " << in << std::endl;
+    Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl;
 
     if(in.getKind() == kind::APPLY_CONSTRUCTOR ){
       Type t = in.getType().toType();
@@ -41,7 +41,7 @@ public:
       // to ensure a normal form, all parameteric datatype constructors must have a type ascription
       if( dt.isParametric() ){
         if( in.getOperator().getKind()!=kind::APPLY_TYPE_ASCRIPTION ){
-          Trace("datatypes-rewrite") << "Ascribing type to parametric datatype constructor " << in << std::endl;
+          Trace("datatypes-rewrite-debug") << "Ascribing type to parametric datatype constructor " << in << std::endl;
           Node op = in.getOperator();
           //get the constructor object
           const DatatypeConstructor& dtc = Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())];
@@ -53,7 +53,7 @@ public:
           children.push_back( op_new );
           children.insert( children.end(), in.begin(), in.end() );
           Node inr = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
-          Trace("datatypes-rewrite") << "Created " << inr << std::endl;
+          Trace("datatypes-rewrite-debug") << "Created " << inr << std::endl;
           return RewriteResponse(REWRITE_DONE, inr);
         }
       }
@@ -214,7 +214,7 @@ public:
   }
 
   static RewriteResponse preRewrite(TNode in) {
-    Trace("datatypes-rewrite") << "pre-rewriting " << in << std::endl;
+    Trace("datatypes-rewrite-debug") << "pre-rewriting " << in << std::endl;
     return RewriteResponse(REWRITE_DONE, in);
   }
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index a0651efb4..c827a8f07 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -26,6 +26,8 @@
 #include "smt/options.h"
 #include "smt/boolean_terms.h"
 #include "theory/quantifiers/options.h"
+#include "theory/datatypes/options.h"
+#include "theory/type_enumerator.h"
 
 #include <map>
 
@@ -158,15 +160,18 @@ void TheoryDatatypes::check(Effort e) {
                 }
               }
               if( !needSplit && mustSpecifyAssignment() ){
+                // &&
                 //for the sake of termination, we must choose the constructor of a ground term
                 //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
                 //** TODO: this is probably not good enough, actually need fair enumeration strategy
+                /*
                 Node groundTerm = n.getType().mkGroundTerm();
                 int index = Datatype::indexOf( groundTerm.getOperator().toExpr() );
                 if( pcons[index] ){
                   consIndex = index;
                 }
                 needSplit = true;
+                */
               }
               if( needSplit && consIndex!=-1 ) {
                 Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n );
@@ -179,7 +184,7 @@ void TheoryDatatypes::check(Effort e) {
                 d_out->requirePhase( test, true );
                 return;
               }else{
-                Trace("dt-split") << "Do not split constructor for " << n << std::endl;
+                Trace("dt-split-debug") << "Do not split constructor for " << n << std::endl;
               }
             }
           }else{
@@ -503,6 +508,9 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         trep2 = eqc2->d_constructor.get();
       }
       EqcInfo* eqc1 = getOrMakeEqcInfo( t1 );
+
+
+
       if( eqc1 ){
         if( !eqc1->d_constructor.get().isNull() ){
           trep1 = eqc1->d_constructor.get();
@@ -538,6 +546,29 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
           eqc1->d_inst = true;
         }
         if( cons1.isNull() && !cons2.isNull() ){
+          Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl;
+          NodeListMap::iterator lbl_i = d_labels.find( t1 );
+          if( lbl_i != d_labels.end() ){
+            size_t constructorIndex = Datatype::indexOf(cons2.getOperator().toExpr());
+            NodeList* lbl = (*lbl_i).second;
+            for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
+              if( (*i).getKind()==NOT ){
+                if( Datatype::indexOf( (*i)[0].getOperator().toExpr() )==constructorIndex ){
+                  Node n = *i;
+                  std::vector< TNode > assumptions;
+                  explain( *i, assumptions );
+                  explain( cons2.eqNode( (*i)[0][0] ), assumptions );
+                  d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions );
+                  Debug("datatypes-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
+                  Debug("datatypes-conflict-temp") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
+                  d_out->conflict( d_conflictNode );
+                  d_conflict = true;
+                  return;
+                }
+              }
+            }
+          }
+
           checkInst = true;
           eqc1->d_constructor.set( eqc2->d_constructor );
         }
@@ -548,14 +579,18 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         eqc1->d_inst.set( eqc2->d_inst );
         eqc1->d_constructor.set( eqc2->d_constructor );
       }
+
+
+
       //merge labels
-      Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl;
       NodeListMap::iterator lbl_i = d_labels.find( t2 );
       if( lbl_i != d_labels.end() ){
+        Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl;
         NodeList* lbl = (*lbl_i).second;
         for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); ++j ){
           addTester( *j, eqc1, t1 );
           if( d_conflict ){
+            Debug("datatypes-debug") << "Conflict!" << std::endl;
             return;
           }
         }
@@ -643,7 +678,7 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >
 
 void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){
   if( !d_conflict ){
-    Debug("datatypes-labels") << "Add tester " << t << " " << eqc << std::endl;
+    Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl;
     bool tpolarity = t.getKind()!=NOT;
     Node tt = ( t.getKind() == NOT ) ? t[0] : t;
     int ttindex = Datatype::indexOf( tt.getOperator().toExpr() );
@@ -768,6 +803,28 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
   Trace("dt-model") << std::endl;
   printModelDebug( "dt-model" );
   m->assertEqualityEngine( &d_equalityEngine );
+
+  std::vector< TypeEnumerator > vec;
+  std::map< TypeNode, int > tes;
+  Trace("dt-cmi") << "Datatypes : Collect model info " << std::endl;
+
+  //get all constructors
+  eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
+  std::vector< Node > cons;
+  while( !eqccs_i.isFinished() ){
+    Node eqc = (*eqccs_i);
+    //for all equivalence classes that are datatypes
+    if( DatatypesRewriter::isTermDatatype( eqc ) ){
+      EqcInfo* ei = getOrMakeEqcInfo( eqc );
+      if( ei ){
+        if( !ei->d_constructor.get().isNull() ){
+          cons.push_back( ei->d_constructor.get() );
+        }
+      }
+    }
+    ++eqccs_i;
+  }
+
   //must choose proper representatives
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){
@@ -778,10 +835,63 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
       if( ei ){
         if( !ei->d_constructor.get().isNull() ){
           //specify that we should use the constructor as the representative
-          m->assertRepresentative( ei->d_constructor.get() );
+          //m->assertRepresentative( ei->d_constructor.get() );
         }else{
-          Trace("model-warn") << "WARNING: Datatypes: no constructor in equivalence class " << eqc << std::endl;
-          Trace("model-warn") << "   Type : " << eqc.getType() << std::endl;
+          Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl;
+          Trace("dt-cmi") << "   Type : " << eqc.getType() << std::endl;
+
+          std::vector< bool > pcons;
+          getPossibleCons( ei, eqc, pcons );
+          Trace("dt-cmi") << "Possible constructors : ";
+          for( unsigned i=0; i<pcons.size(); i++ ){
+            Trace("dt-cmi") << pcons[i] << " ";
+          }
+          Trace("dt-cmi") << std::endl;
+
+          if( tes.find( eqc.getType() )==tes.end() ){
+            tes[eqc.getType()]=vec.size();
+            vec.push_back( TypeEnumerator( eqc.getType() ) );
+          }
+          bool success;
+          Node n;
+          do {
+            success = true;
+            Assert( !vec[tes[eqc.getType()]].isFinished() );
+            n = *vec[tes[eqc.getType()]];
+            ++vec[tes[eqc.getType()]];
+
+            //applyTypeAscriptions( n, eqc.getType() );
+
+            Trace("dt-cmi-debug") << "Try " << n << "..." << std::endl;
+            //check if it is consistent with labels
+            size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr());
+            if( constructorIndex<pcons.size() && pcons[constructorIndex] ){
+              for( unsigned i=0; i<cons.size(); i++ ){
+                //check if it is modulo equality the same
+                if( cons[i].getOperator()==n.getOperator() ){
+                  bool diff = false;
+                  for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
+                    if( !m->areEqual( cons[i][j], n[j] ) ){
+                      diff = true;
+                      break;
+                    }
+                  }
+                  if( !diff ){
+                    Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl;
+                    success = false;
+                    break;
+                  }
+                }
+              }
+            }else{
+              Trace("dt-cmi-debug") << "...Not consistent with labels" << std::endl;
+              success = false;
+            }
+          }while( !success );
+          Trace("dt-cmi") << "Assign : " << n << std::endl;
+          //m->assertRepresentative( n );
+          m->assertEquality( eqc, n, true );
+
         }
       }else{
         Trace("model-warn") << "WARNING: Datatypes: no equivalence class info for " << eqc << std::endl;
@@ -871,7 +981,38 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index
     return n_ic;
   //}
 }
-
+/*
+Node TheoryDatatypes::applyTypeAscriptions( Node n, TypeNode tn ){
+  Debug("dt-ta-debug") << "Apply type ascriptions " << n << " " << tn << std::endl;
+  if( n.getKind()==APPLY_CONSTRUCTOR ){
+    //add type ascription for ambiguous constructor types
+    if(!n.getType().isComparableTo(tn)) {
+      size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr());
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      Assert( dt.isParametric() );
+      Debug("dt-ta-debug") << "Ambiguous type for " << n << ", ascribe to " << tn << std::endl;
+      Debug("dt-ta-debug") << "Constructor is " << dt[constructorIndex] << std::endl;
+      Type tspec = dt[constructorIndex].getSpecializedConstructorType(tn.toType());
+      Debug("dt-ta-debug") << "Type specification is " << tspec << std::endl;
+      Node op = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+                                                 NodeManager::currentNM()->mkConst(AscriptionType(tspec)), n.getOperator() );
+      std::vector< Node > children;
+      children.push_back( op );
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        children.push_back( applyTypeAscriptions( n[i], TypeNode::fromType( tspec )[i] ) );
+      }
+      n = Rewriter::rewrite( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ) );
+      Assert( n.getType()==tn );
+      return n;
+    }
+  }else{
+    if( n.getType()!=tn ){
+      Debug("dt-ta-debug") << "Bad type : " << n.getType() << std::endl;
+    }
+  }
+  return n;
+}
+*/
 void TheoryDatatypes::collapseSelectors(){
   //must check incorrect applications of selectors
   for( BoolMap::iterator it = d_selector_apps.begin(); it != d_selector_apps.end(); ++it ){
@@ -918,7 +1059,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
     int index = getLabelIndex( eqc, n );
     const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
     //must be finite or have a selector
-    if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){
+    //if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){
       //instantiate this equivalence class
       eqc->d_inst = true;
       Node tt_cons = getInstantiateCons( tt, dt, index );
@@ -933,7 +1074,10 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
         d_infer.push_back( eq );
         d_infer_exp.push_back( exp );
       }
-    }
+    //}
+    //else{
+    //  Debug("datatypes-inst") << "Do not instantiate" << std::endl;
+    //}
   }
 }
 
@@ -1094,43 +1238,45 @@ void TheoryDatatypes::printModelDebug( const char* c ){
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
-    if( DatatypesRewriter::isTermDatatype( eqc ) ){
-      Trace( c ) << "DATATYPE : ";
-    }
-    Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
-    Trace( c ) << "   { ";
-    //add terms to model
-    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-    while( !eqc_i.isFinished() ){
-      Trace( c ) << (*eqc_i) << " ";
-      ++eqc_i;
-    }
-    Trace( c ) << "}" << std::endl;
-    if( DatatypesRewriter::isTermDatatype( eqc ) ){
-      EqcInfo* ei = getOrMakeEqcInfo( eqc );
-      if( ei ){
-        Trace( c ) << "   Instantiated : " << ei->d_inst.get() << std::endl;
-        if( ei->d_constructor.get().isNull() ){
-          Trace("model-warn") << eqc << " has no constructor in equivalence class!" << std::endl;
-          Trace("model-warn") << "  Type : " << eqc.getType() << std::endl;
-          Trace( c ) << "   Constructor : " << std::endl;
-          Trace( c ) << "   Labels : ";
-          if( hasLabel( ei, eqc ) ){
-            Trace( c ) << getLabel( eqc );
-          }else{
-            NodeListMap::iterator lbl_i = d_labels.find( eqc );
-            if( lbl_i != d_labels.end() ){
-              NodeList* lbl = (*lbl_i).second;
-              for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){
-                Trace( c ) << *j << " ";
+    if( !eqc.getType().isBoolean() ){
+      if( DatatypesRewriter::isTermDatatype( eqc ) ){
+        Trace( c ) << "DATATYPE : ";
+      }
+      Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
+      Trace( c ) << "   { ";
+      //add terms to model
+      eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+      while( !eqc_i.isFinished() ){
+        Trace( c ) << (*eqc_i) << " ";
+        ++eqc_i;
+      }
+      Trace( c ) << "}" << std::endl;
+      if( DatatypesRewriter::isTermDatatype( eqc ) ){
+        EqcInfo* ei = getOrMakeEqcInfo( eqc );
+        if( ei ){
+          Trace( c ) << "   Instantiated : " << ei->d_inst.get() << std::endl;
+          if( ei->d_constructor.get().isNull() ){
+            Trace("debug-model-warn") << eqc << " has no constructor in equivalence class!" << std::endl;
+            Trace("debug-model-warn") << "  Type : " << eqc.getType() << std::endl;
+            Trace( c ) << "   Constructor : " << std::endl;
+            Trace( c ) << "   Labels : ";
+            if( hasLabel( ei, eqc ) ){
+              Trace( c ) << getLabel( eqc );
+            }else{
+              NodeListMap::iterator lbl_i = d_labels.find( eqc );
+              if( lbl_i != d_labels.end() ){
+                NodeList* lbl = (*lbl_i).second;
+                for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){
+                  Trace( c ) << *j << " ";
+                }
               }
             }
+            Trace( c ) << std::endl;
+          }else{
+            Trace( c ) << "   Constructor : " << ei->d_constructor.get() << std::endl;
           }
-          Trace( c ) << std::endl;
-        }else{
-          Trace( c ) << "   Constructor : " << ei->d_constructor.get() << std::endl;
+          Trace( c ) << "   Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl;
         }
-        Trace( c ) << "   Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl;
       }
     }
     ++eqcs_i;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index e38c522c5..203782a79 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -226,6 +226,8 @@ private:
   void collectTerms( Node n );
   /** get instantiate cons */
   Node getInstantiateCons( Node n, const Datatype& dt, int index );
+  /** apply type ascriptions */
+  //Node applyTypeAscriptions( Node n, TypeNode tn );
   /** process new term that was created internally */
   void processNewTerm( Node n );
   /** check instantiate */
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 778304f32..cec1dccfc 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -37,6 +37,8 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
   size_t d_zeroCtor;
   /** Delegate enumerators for the arguments of the current constructor */
   TypeEnumerator** d_argEnumerators;
+  /** type */
+  TypeNode d_type;
 
   /** Allocate and initialize the delegate enumerators */
   void newEnumerators() {
@@ -65,7 +67,8 @@ public:
     d_datatype(DatatypeType(type.toType()).getDatatype()),
     d_ctor(0),
     d_zeroCtor(0),
-    d_argEnumerators(NULL) {
+    d_argEnumerators(NULL),
+    d_type(type) {
 
     //Assert(type.isDatatype());
     Debug("te") << "datatype is datatype? " << type.isDatatype() << std::endl;
@@ -76,8 +79,21 @@ public:
     /* FIXME: this isn't sufficient for mutually-recursive datatypes! */
     while(d_zeroCtor < d_datatype.getNumConstructors()) {
       bool recursive = false;
-      for(size_t a = 0; a < d_datatype[d_zeroCtor].getNumArgs() && !recursive; ++a) {
-        recursive = (Node::fromExpr(d_datatype[d_zeroCtor][a].getSelector()).getType()[1] == type);
+      if( d_datatype.isParametric() ){
+        TypeNode tn = TypeNode::fromType( d_datatype[d_zeroCtor].getSpecializedConstructorType(d_type.toType()) );
+        for( unsigned i=0; i<tn.getNumChildren()-1; i++ ){
+          if( tn[i]==type ){
+            recursive = true;
+            break;
+          }
+        }
+      }else{
+        for(size_t a = 0; a < d_datatype[d_zeroCtor].getNumArgs() && !recursive; ++a) {
+          if(Node::fromExpr(d_datatype[d_zeroCtor][a].getSelector()).getType()[1] == type) {
+            recursive = true;
+            break;
+          }
+        }
       }
       if(!recursive) {
         break;
@@ -97,7 +113,8 @@ public:
     d_datatype(de.d_datatype),
     d_ctor(de.d_ctor),
     d_zeroCtor(de.d_zeroCtor),
-    d_argEnumerators(NULL) {
+    d_argEnumerators(NULL),
+    d_type(de.d_type) {
 
     if(de.d_argEnumerators != NULL) {
       newEnumerators();
@@ -117,18 +134,33 @@ public:
     if(d_ctor < d_datatype.getNumConstructors()) {
       DatatypeConstructor ctor = d_datatype[d_ctor];
       NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
-      b << ctor.getConstructor();
+      Type typ;
+      if( d_datatype.isParametric() ){
+        typ = d_datatype[d_ctor].getSpecializedConstructorType(d_type.toType());
+        b << NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+                                              NodeManager::currentNM()->mkConst(AscriptionType(typ)), Node::fromExpr( ctor.getConstructor() ) );
+      }else{
+        b << ctor.getConstructor();
+      }
       try {
         for(size_t a = 0; a < d_datatype[d_ctor].getNumArgs(); ++a) {
           if(d_argEnumerators[a] == NULL) {
-            d_argEnumerators[a] = new TypeEnumerator(Node::fromExpr(d_datatype[d_ctor][a].getSelector()).getType()[1]);
+            if( d_datatype.isParametric() ){
+              d_argEnumerators[a] = new TypeEnumerator(TypeNode::fromType( typ )[a]);
+            }else{
+              d_argEnumerators[a] = new TypeEnumerator(Node::fromExpr(d_datatype[d_ctor][a].getSelector()).getType()[1]);
+            }
           }
           b << **d_argEnumerators[a];
         }
       } catch(NoMoreValuesException&) {
         InternalError();
       }
-      return Node(b);
+      Node nnn = Node(b);
+      //if( nnn.getType()!=d_type || !nnn.getType().isComparableTo(d_type) ){
+      //  Debug("dt-warn") << "WARNING : Enum : " << nnn << " bad type : " << nnn.getType() << " " << d_type << std::endl;
+      //}
+      return nnn;
     } else {
       throw NoMoreValuesException(getType());
     }
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index cb8cb8154..b1a0c4ed4 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -139,6 +139,11 @@ bool ModelEngine::optOneQuantPerRound(){
 
 int ModelEngine::checkModel(){
   FirstOrderModel* fm = d_quantEngine->getModel();
+
+  //flatten the representatives
+  //Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
+  //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps );
+
   //for debugging
   if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){
     for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
@@ -149,7 +154,7 @@ int ModelEngine::checkModel(){
         Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
         for( size_t i=0; i<it->second.size(); i++ ){
           //Trace("model-engine-debug") << it->second[i] << "  ";
-          Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] );
+          Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
           Trace("model-engine-debug") << r << " ";
         }
         Trace("model-engine-debug") << std::endl;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 57211ade7..fd114df04 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -98,7 +98,7 @@ option finiteModelFind --finite-model-find bool :default false
 option fmfModelBasedInst /--disable-fmf-mbqi bool :default true
  disable model-based quantifier instantiation for finite model finding
 
-option fmfFullModelCheck --fmf-fmc bool :default false
+option fmfFullModelCheck --fmf-fmc bool :default false :read-write
  enable full model check for finite model finding
 option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
  disable simple models in full model check for finite model finding
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 0fe50aad6..c14ee01ce 100755
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -102,7 +102,7 @@ QuantifiersEngine::~QuantifiersEngine(){
   delete d_eq_query;
 }
 
-EqualityQuery* QuantifiersEngine::getEqualityQuery() {
+EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
   return d_eq_query;
 }
 
@@ -594,8 +594,9 @@ Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
   eq::EqualityEngine* ee = getEngine();
   if( ee->hasTerm( a ) ){
     return ee->getRepresentative( a );
+  }else{
+    return a;
   }
-  return a;
 }
 
 bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
@@ -631,66 +632,126 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
   if( !options::internalReps() ){
     return r;
   }else{
-    int sortId = 0;
-    if( optInternalRepSortInference() ){
-    //if( options::ufssSymBreak() ){
-      sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( f, f[0][index] );
-    }
-    if( d_int_rep[sortId].find( r )==d_int_rep[sortId].end() ){
+    if( d_int_rep.find( r )==d_int_rep.end() ){
       //find best selection for representative
       Node r_best;
-      if( options::fmfRelevantDomain() ){
+      if( options::fmfRelevantDomain() && !f.isNull() ){
         Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
         r_best = d_qe->getModelEngine()->getRelevantDomain()->getRelevantTerm( f, index, r );
         Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
       }else{
         std::vector< Node > eqc;
         getEquivalenceClass( r, eqc );
+        Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
+        for( unsigned i=0; i<eqc.size(); i++ ){
+          if( i>0 ) Trace("internal-rep-select") << ", ";
+          Trace("internal-rep-select") << eqc[i];
+        }
+        Trace("internal-rep-select")  << " } " << std::endl;
         int r_best_score = -1;
         for( size_t i=0; i<eqc.size(); i++ ){
-          int score = getRepScore( eqc[i], f, index );
+          //if cbqi is active, do not choose instantiation constant terms
           if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){
-            if( optInternalRepSortInference() ){
-              int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i]);
-              if( score>=0 && e_sortId!=sortId ){
-                score += 100;
-              }
-            }
+            int score = getRepScore( eqc[i], f, index );
             //score prefers earliest use of this term as a representative
             if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
               r_best = eqc[i];
               r_best_score = score;
             }
-		  }
+		      }
         }
         if( r_best.isNull() ){
-	      Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
-		  r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
-		}
+          if( !f.isNull() ){
+            Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
+            r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+          }else{
+            r_best = a;
+          }
+		    }
         //now, make sure that no other member of the class is an instance
-        if( !optInternalRepSortInference() ){
-          r_best = getInstance( r_best, eqc );
-        }
+        r_best = getInstance( r_best, eqc );
         //store that this representative was chosen at this point
         if( d_rep_score.find( r_best )==d_rep_score.end() ){
           d_rep_score[ r_best ] = d_reset_count;
         }
+        Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
       }
-      d_int_rep[sortId][r] = r_best;
+      d_int_rep[r] = r_best;
       if( r_best!=a ){
         Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
         Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
       }
-      if( optInternalRepSortInference() ){
-        int sortIdBest = d_qe->getTheoryEngine()->getSortInference()->getSortId( r_best );
-        if( sortId!=sortIdBest ){
-          Trace("sort-inf-rep") << "Choosing representative with bad type " << r_best << " " << sortId << " " << sortIdBest << std::endl;
-        }
-      }
       return r_best;
     }else{
-      return d_int_rep[sortId][r];
+      return d_int_rep[r];
+    }
+  }
+}
+
+void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) {
+  //make sure internal representatives currently exist
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){
+    if( it->first.isSort() ){
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        Node r = getInternalRepresentative( it->second[i], Node::null(), 0 );
+      }
+    }
+  }
+  Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl;
+  for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
+    Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
+  }
+  //store representatives for newly created terms
+  std::map< Node, Node > temp_rep_map;
+
+  bool success;
+  do {
+    success = false;
+    for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
+      if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
+        Node ni = it->second;
+        std::vector< Node > cc;
+        cc.push_back( it->second.getOperator() );
+        bool changed = false;
+        for( unsigned j=0; j<ni.getNumChildren(); j++ ){
+          if( ni[j].getType().isSort() ){
+            Node r = getRepresentative( ni[j] );
+            if( d_int_rep.find( r )==d_int_rep.end() ){
+              Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
+              r = temp_rep_map[r];
+            }
+            if( r==ni ){
+              //found sub-term as instance
+              Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
+              d_int_rep[it->first] = ni[j];
+              changed = false;
+              success = true;
+              break;
+            }else{
+              Node ir = d_int_rep[r];
+              cc.push_back( ir );
+              if( ni[j]!=ir ){
+                changed = true;
+              }
+            }
+          }else{
+            changed = false;
+            break;
+          }
+        }
+        if( changed ){
+          Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
+          Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
+          success = true;
+          d_int_rep[it->first] = n;
+          temp_rep_map[n] = it->first;
+        }
+      }
     }
+  }while( success );
+  Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
+  for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
+    Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
   }
 }
 
@@ -750,6 +811,3 @@ int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
   //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n );    //term depth
 }
 
-bool EqualityQueryQuantifiersEngine::optInternalRepSortInference() {
-  return false; //shown to be not effective
-}
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index b075f7be8..8f645afe7 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -142,7 +142,7 @@ public:
   TheoryEngine* getTheoryEngine() { return d_te; }
   /** get equality query object for the given type. The default is the
       generic one */
-  EqualityQuery* getEqualityQuery();
+  EqualityQueryQuantifiersEngine* getEqualityQuery();
   /** get instantiation engine */
   quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
   /** get model engine */
@@ -277,7 +277,7 @@ private:
   /** pointer to theory engine */
   QuantifiersEngine* d_qe;
   /** internal representatives */
-  std::map< int, std::map< Node, Node > > d_int_rep;
+  std::map< Node, Node > d_int_rep;
   /** rep score */
   std::map< Node, int > d_rep_score;
   /** reset count */
@@ -289,8 +289,6 @@ private:
   Node getInstance( Node n, std::vector< Node >& eqc );
   /** get score */
   int getRepScore( Node n, Node f, int index );
-  /** choose rep based on sort inference */
-  bool optInternalRepSortInference();
 public:
   EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){}
   ~EqualityQueryQuantifiersEngine(){}
@@ -308,6 +306,8 @@ public:
       not contain instantiation constants, if such a term exists.
    */
   Node getInternalRepresentative( Node a, Node f, int index );
+  /** flatten representatives */
+  void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
 
   void setLiberal( bool l ) { d_liberal = l; }
 }; /* EqualityQueryQuantifiersEngine */
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 814276a7c..fe7b9b3d9 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -16,6 +16,8 @@ operator STRING_IN_REGEXP 2 "membership"
 
 operator STRING_LENGTH 1 "string length"
 
+operator STRING_SUBSTR 3 "string substr"
+
 #sort CHAR_TYPE \
 #    Cardinality::INTEGERS \
 #    well-founded \
@@ -99,6 +101,7 @@ typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
 
 typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
 typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
+typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
 
 typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 7d5edd0f7..a0058954d 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -96,14 +96,18 @@ bool TheoryStrings::areDisequal( Node a, Node b ){
   }
 }
 
-Node TheoryStrings::getLength( Node t ) {
-	EqcInfo * ei = getOrMakeEqcInfo( t );
-	Node length_term = ei->d_length_term;
+Node TheoryStrings::getLengthTerm( Node t ) {
+	EqcInfo * ei = getOrMakeEqcInfo( t, false );
+	Node length_term = ei ? ei->d_length_term : Node::null();
 	if( length_term.isNull()) {
 		//typically shouldnt be necessary
 		length_term = t;
 	}
-	return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term );
+	return length_term;
+}
+
+Node TheoryStrings::getLength( Node t ) {
+	return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) );
 }
 
 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -194,23 +198,29 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 	seperateByLength( nodes, col, lts );
 	//step 1 : get all values for known lengths
 	std::vector< Node > lts_values;
-	//std::map< Node, bool > values_used;
+	std::map< unsigned, bool > values_used;
 	for( unsigned i=0; i<col.size(); i++ ){
-		Trace("strings-model") << "Checking length for " << col[i][0] << " (length is " << lts[i] << ")" << std::endl;
+		Trace("strings-model") << "Checking length for {";
+		for( unsigned j=0; j<col[i].size(); j++ ){
+			if( j>0 ) Trace("strings-model") << ", ";
+			Trace("strings-model") << col[i][j];
+		}
+		Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl;
 		if( lts[i].isConst() ){
 			lts_values.push_back( lts[i] );
-			//values_used[ lts[i] ] = true;
+			unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt();
+			values_used[ lvalue ] = true;
 		}else{
 			//get value for lts[i];
 			if( !lts[i].isNull() ){
 				Node v = d_valuation.getModelValue(lts[i]);
-				//Node v = m->getValue(lts[i]);
 				Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl;
 				lts_values.push_back( v );
-				//values_used[ v ] = true;
+				unsigned lvalue =  v.getConst<Rational>().getNumerator().toUnsignedInt();
+				values_used[ lvalue ] = true;
 			}else{
-				Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl;
-				Assert( false );
+				//Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl;
+				//Assert( false );
 				lts_values.push_back( Node::null() );
 			}
 		}
@@ -240,26 +250,39 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 		}
 		Trace("strings-model") << "have length " << lts_values[i] << std::endl;
 		
-		Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes ";
-		for( unsigned j=0; j<pure_eq.size(); j++ ){
-			Trace("strings-model") << pure_eq[j] << " ";
-		}
-		Trace("strings-model") << std::endl;
-
-		//use type enumerator
-		StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt());
-		for( unsigned j=0; j<pure_eq.size(); j++ ){
-			Assert( !sel.isFinished() );
-			Node c = *sel;
-			while( d_equalityEngine.hasTerm( c ) ){
-				++sel;
+		//assign a new length if necessary
+		if( !pure_eq.empty() ){
+			if( lts_values[i].isNull() ){
+				unsigned lvalue = 0;
+				while( values_used.find( lvalue )!=values_used.end() ){
+					lvalue++;	
+				}
+				Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl;
+				lts_values[i] = NodeManager::currentNM()->mkConst( Rational( lvalue ) );
+				values_used[ lvalue ] = true;
+			}
+			Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes ";
+			for( unsigned j=0; j<pure_eq.size(); j++ ){
+				Trace("strings-model") << pure_eq[j] << " ";
+			}
+			Trace("strings-model") << std::endl;
+
+
+			//use type enumerator
+			StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt());
+			for( unsigned j=0; j<pure_eq.size(); j++ ){
 				Assert( !sel.isFinished() );
-				c = *sel;
+				Node c = *sel;
+				while( d_equalityEngine.hasTerm( c ) ){
+					++sel;
+					Assert( !sel.isFinished() );
+					c = *sel;
+				}
+				++sel;
+				Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl;
+				processed[pure_eq[j]] = c;
+				m->assertEquality( pure_eq[j], c, true );
 			}
-			++sel;
-			Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl;
-			processed[pure_eq[j]] = c;
-			m->assertEquality( pure_eq[j], c, true );
 		}
 	}
 	Trace("strings-model") << "String Model : Finished." << std::endl;
@@ -363,74 +386,30 @@ void TheoryStrings::check(Effort e) {
 
   bool addedLemma = false;
   if( e == EFFORT_FULL && !d_conflict ) {
-      eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-      while( !eqcs_i.isFinished() ){
-        Node eqc = (*eqcs_i);
-        //if eqc.getType is string
-        if (eqc.getType().isString()) {
-            //EqcInfo* ei = getOrMakeEqcInfo( eqc, true );
-            //get the constant for the equivalence class
-            //int c_len = ...;
-            eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-            while( !eqc_i.isFinished() ){
-              Node n = (*eqc_i);
-
-              //if n is concat, and
-              //if n has not instantiatied the concat..length axiom
-              //then, add lemma
-              if( n.getKind() == kind::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){
-                if( d_length_inst.find(n)==d_length_inst.end() ){
-                    d_length_inst[n] = true;
-                    Trace("strings-debug") << "get n: " << n << endl;
-                    Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
-					d_length_intro_vars.push_back( sk );
-                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
-                    eq = Rewriter::rewrite(eq);
-                    Trace("strings-lemma") << "Strings: Add lemma " << eq << std::endl;
-                    d_out->lemma(eq);
-                    Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-                    Node lsum;
-                    if( n.getKind() == kind::STRING_CONCAT ){
-                        //add lemma
-                        std::vector<Node> node_vec;
-                        for( unsigned i=0; i<n.getNumChildren(); i++ ) {
-                            Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
-                            node_vec.push_back(lni);
-                        }
-                        lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
-                    }else{
-                        //add lemma
-                        lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
-                    }
-                    Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
-                    ceq = Rewriter::rewrite(ceq);
-                    Trace("strings-lemma") << "Strings: Add lemma " << ceq << std::endl;
-                    d_out->lemma(ceq);
-                    addedLemma = true;
-                }
-              }
-              ++eqc_i;
-            }
-        }
-        ++eqcs_i;
-  }
-  if( !addedLemma ){
-      addedLemma = checkNormalForms();
-	  Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-      if(!d_conflict && !addedLemma) {
-          addedLemma = checkCardinality();
-		  Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-          if( !d_conflict && !addedLemma ){
-            addedLemma = checkInductiveEquations();
-			Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-          }
-      }
-  }
+      addedLemma = checkLengths();
+	  Trace("strings-process") << "Done check (constant) lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+	  if( !addedLemma ){
+		  addedLemma = checkNormalForms();
+		  Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+		  if(!d_conflict && !addedLemma) {
+			  addedLemma = checkLengthsEqc();
+			  Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+			  if(!d_conflict && !addedLemma) {
+				  addedLemma = checkCardinality();
+				  Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+				  if( !d_conflict && !addedLemma ){
+					addedLemma = checkInductiveEquations();
+					Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+				  }
+			  }
+		  }
+	  }
   }
+  Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
   Trace("strings-process") << "Theory of strings, done check : " << e << std::endl;
 }
 
-TheoryStrings::EqcInfo::EqcInfo(  context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c) {
+TheoryStrings::EqcInfo::EqcInfo(  context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) {
 
 }
 
@@ -492,6 +471,9 @@ void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){
         if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) {
             e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k );
         }
+		if( !e2->d_normalized_length.get().isNull() ){
+			e1->d_normalized_length.set( e2->d_normalized_length );
+		}
     }
     if( hasTerm( d_zero ) ){
         Node leqc;
@@ -572,16 +554,17 @@ void TheoryStrings::doPendingLemmas() {
   }
 }
 
-void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
+bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
     std::vector< std::vector< Node > > &normal_forms,  std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) {
     // EqcItr
     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
     while( !eqc_i.isFinished() ) {
         Node n = (*eqc_i);
-        Trace("strings-process") << "Process term " << n << std::endl;
+        Trace("strings-process-debug") << "Get Normal Form : Process term " << n << std::endl;
         if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
             std::vector<Node> nf_n;
             std::vector<Node> nf_exp_n;
+			bool result = true;
             if( n.getKind() == kind::CONST_STRING  ){
                 if( n!=d_emptyString ) {
                     nf_n.push_back( n );
@@ -591,37 +574,88 @@ void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
                     Node nr = d_equalityEngine.getRepresentative( n[i] );
                     std::vector< Node > nf_temp;
                     std::vector< Node > nf_exp_temp;
-                    Trace("strings-process") << "Normalizing subterm " << n[i] << " = "  << nr << std::endl;
-                    normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp );
+                    Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = "  << nr << std::endl;
+                    bool nresult = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp );
                     if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
-                        return;
-                    }
-                    if( nf.size()!=1 || nf[0]!=d_emptyString ) {
-                        for( unsigned r=0; r<nf_temp.size(); r++ ) {
-                            Assert( nf_temp[r].getKind()!=kind::STRING_CONCAT );
-                        }
-                        nf_n.insert( nf_n.end(), nf_temp.begin(), nf_temp.end() );
-                    }
-                    nf_exp_n.insert( nf_exp_n.end(), nf_exp_temp.begin(), nf_exp_temp.end() );
-                    if( nr!=n[i] ) {
-                        nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) );
+                        return true;
                     }
+					//successfully computed normal form
+					if( nf.size()!=1 || nf[0]!=d_emptyString ) {
+						for( unsigned r=0; r<nf_temp.size(); r++ ) {
+							Assert( !nresult || nf_temp[r].getKind()!=kind::STRING_CONCAT );
+						}
+						nf_n.insert( nf_n.end(), nf_temp.begin(), nf_temp.end() );
+					}
+					nf_exp_n.insert( nf_exp_n.end(), nf_exp_temp.begin(), nf_exp_temp.end() );
+					if( nr!=n[i] ) {
+						nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) );
+					}
+					if( !nresult ){
+						//Trace("strings-process-debug") << "....Caused already asserted 
+						for( unsigned j=i+1; j<n.getNumChildren(); j++ ){
+							if( !areEqual( n[j], d_emptyString ) ){
+								nf_n.push_back( n[j] );
+							}
+						}
+						if( nf_n.size()>1 ){
+							result = false;
+							break;
+						}
+					}
                 }
             }
-            normal_forms.push_back(nf_n);
-            normal_forms_exp.push_back(nf_exp_n);
-            normal_form_src.push_back(n);
+			if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ){
+				if( nf_n.size()>1 ){
+					Trace("strings-process-debug") << "Check for component lemmas for normal form "; 
+					printConcat(nf_n,"strings-process-debug");
+					Trace("strings-process-debug") << "..." << std::endl;
+					for( unsigned i=0; i<nf_n.size(); i++ ){
+						//if a component is equal to whole,
+						if( areEqual( nf_n[i], n ) ){
+							//all others must be empty
+							std::vector< Node > ant;
+							if( nf_n[i]!=n ){
+								ant.push_back( nf_n[i].eqNode( n ) );
+							}
+							ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() );
+							std::vector< Node > cc;
+							for( unsigned j=0; j<nf_n.size(); j++ ){
+								if( i!=j ){
+									cc.push_back( nf_n[j].eqNode( d_emptyString ) );
+								}
+							}
+							std::vector< Node > empty_vec;
+							Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
+							sendLemma( mkExplain( ant ), conc, "Component" );
+							return true;
+						}
+					}
+				}
+				if( !result ){
+					//we have a normal form that will cause a component lemma at a higher level
+					normal_forms.clear();
+					normal_forms_exp.clear();
+					normal_form_src.clear();
+				}
+				normal_forms.push_back(nf_n);
+				normal_forms_exp.push_back(nf_exp_n);
+				normal_form_src.push_back(n);
+				if( !result ){
+					return false;
+				}
+			}else{
+				Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0];
+				//Assert( areEqual( nf_n[0], eqc ) );
+				if( !areEqual( nn, eqc ) ){
+					std::vector< Node > ant;
+					ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() );
+					ant.push_back( n.eqNode( eqc ) );
+					Node conc = nn.eqNode( eqc );
+					sendLemma( mkExplain( ant ), conc, "Trivial Equal Normal Form" );
+					return true;
+				}
+			}
         }
-        /* should we add these?
-        else {
-            //var/sk?
-            std::vector<Node> nf_n;
-            std::vector<Node> nf_exp_n;
-            nf_n.push_back(n);
-            normal_forms.push_back(nf_n);
-            normal_forms_exp.push_back(nf_exp_n);
-            normal_form_src.push_back(n);
-        }*/
         ++eqc_i;
     }
 
@@ -647,29 +681,36 @@ void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
             Trace("strings-solve") << std::endl;
         }
     }
+	return true;
 }
 //nf_exp is conjunction
-void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) {
+bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) {
     Trace("strings-process") << "Process equivalence class " << eqc << std::endl;
     if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){
-        //nf.push_back( eqc );
+        nf.push_back( eqc );
+		/*
         if( eqc.getKind()==kind::STRING_CONCAT ){
             for( unsigned i=0; i<eqc.getNumChildren(); i++ ){
-				if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc[i], d_emptyString ) ){
+				if( !areEqual( eqc[i], d_emptyString ) ){
 					nf.push_back( eqc[i] );
 				}
             }
-        }else if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc, d_emptyString ) ){
+        }else if(  !areEqual( eqc, d_emptyString ) ){
             nf.push_back( eqc );
         }
+		*/
         Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
-    } else if (d_equalityEngine.hasTerm(d_emptyString) && d_equalityEngine.areEqual( eqc, d_emptyString )){
+		return false;
+    } else if( areEqual( eqc, d_emptyString ) ){
         //do nothing
         Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl;
+		d_normal_forms_base[eqc] = d_emptyString;
 		d_normal_forms[eqc].clear();
 		d_normal_forms_exp[eqc].clear();
+		return true;
     } else {
         visited.push_back( eqc );
+		bool result;
         if(d_normal_forms.find(eqc)==d_normal_forms.end() ){
             //phi => t = s1 * ... * sn
             // normal form for each non-variable term in this eqc (s1...sn)
@@ -679,302 +720,336 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
             // record terms for each normal form (t)
             std::vector< Node > normal_form_src;
             //Get Normal Forms
-            getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src);
+            result = getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src);
             if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
-                return;
-            }
-
-            unsigned i = 0;
-            //unify each normal form > 0 with normal_forms[0]
-            for( unsigned j=1; j<normal_forms.size(); j++ ) {
-
-                Trace("strings-solve") << "Process normal form #0 against #" << j << "..." << std::endl;
-                if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ){
-                    Trace("strings-solve") << "Already normalized (in cache)." << std::endl;
-                }else{
-                    Trace("strings-solve") << "Not in cache." << std::endl;
-                    //the current explanation for why the prefix is equal
-                    std::vector< Node > curr_exp;
-                    curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() );
-                    curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() );
-                    curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) );
-                    //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality
-                    unsigned index_i = 0;
-                    unsigned index_j = 0;
-                    bool success;
-                    do
-                    {
-                        success = false;
-                        //if we are at the end
-                        if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
-                            if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ){
-                                //we're done
-                                addNormalFormPair( normal_form_src[i], normal_form_src[j] );
-                            }else{
-                                //the remainder must be empty
-                                unsigned k = index_i==normal_forms[i].size() ? j : i;
-                                unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i;
-                                while(!d_conflict && index_k<normal_forms[k].size()) {
-                                    //can infer that this string must be empty
-                                    Node eq_exp;
-                                    if( curr_exp.empty() ) {
-                                        eq_exp = d_true;
-                                    } else if( curr_exp.size() == 1 ) {
-                                        eq_exp = curr_exp[0];
-                                    } else {
-                                        eq_exp = NodeManager::currentNM()->mkNode( kind::AND, curr_exp );
-                                    }
-                                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] );
-                                    Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
-									Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) );
-                                    d_pending.push_back( eq );
-                                    d_pending_exp[eq] = eq_exp;
-                                    d_infer.push_back(eq);
-                                    d_infer_exp.push_back(eq_exp);
-                                    index_k++;
-                                }
-                            }
-                        }else {
-                            Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl;
-                            if(areEqual(normal_forms[i][index_i],normal_forms[j][index_j])){
-                                Trace("strings-solve-debug") << "Case 1 : strings are equal" << std::endl;
-                                //terms are equal, continue
-                                if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){
-                                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,normal_forms[i][index_i],
-                                                                                                     normal_forms[j][index_j]);
-                                    Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl;
-                                    curr_exp.push_back(eq);
-                                }
-                                index_j++;
-                                index_i++;
-                                success = true;
-                            }else{
-								Node length_term_i = getLength( normal_forms[i][index_i] );
-								Node length_term_j = getLength( normal_forms[j][index_j] );
-                                //check 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;
-                                    //length terms are equal, merge equivalence classes if not already done so
-                                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] );
-                                    std::vector< Node > temp_exp;
-                                    temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
-                                    temp_exp.push_back(NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ));
-                                    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 );
-                                    d_pending.push_back( eq );
-                                    d_pending_exp[eq] = eq_exp;
-                                    d_infer.push_back(eq);
-                                    d_infer_exp.push_back(eq_exp);
-                                    return;
-								}else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || 
-										  ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){
-									Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl;
-                                    Node conc;
-                                    std::vector< Node > antec;
-									antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-                                    std::vector< Node > antec_new_lits;
-									std::vector< Node > eqn;
-									for( unsigned r=0; r<2; r++ ){
-										int index_k = r==0 ? index_i : index_j;
-										int k = r==0 ? i : j;
-										std::vector< Node > eqnc;
-										for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ){
-											eqnc.push_back( normal_forms[k][index_l] );
+                return true;
+            }else if( result ){
+				unsigned i = 0;
+				//unify each normal form > 0 with normal_forms[0]
+				for( unsigned j=1; j<normal_forms.size(); j++ ) {
+					Trace("strings-solve") << "Process normal form #0 against #" << j << "..." << std::endl;
+					if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ){
+						Trace("strings-solve") << "Already normalized (in cache)." << std::endl;
+					}else{
+						Trace("strings-solve") << "Not in cache." << std::endl;
+						//the current explanation for why the prefix is equal
+						std::vector< Node > curr_exp;
+						curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() );
+						curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() );
+						curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) );
+						//ensure that normal_forms[i] and normal_forms[j] are the same modulo equality
+						unsigned index_i = 0;
+						unsigned index_j = 0;
+						bool success;
+						do
+						{
+							success = false;
+							//if we are at the end
+							if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
+								if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ){
+									//we're done
+									addNormalFormPair( normal_form_src[i], normal_form_src[j] );
+								}else{
+									//the remainder must be empty
+									unsigned k = index_i==normal_forms[i].size() ? j : i;
+									unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i;
+									while(!d_conflict && index_k<normal_forms[k].size()) {
+										//can infer that this string must be empty
+										Node eq_exp;
+										if( curr_exp.empty() ) {
+											eq_exp = d_true;
+										} else if( curr_exp.size() == 1 ) {
+											eq_exp = curr_exp[0];
+										} else {
+											eq_exp = NodeManager::currentNM()->mkNode( kind::AND, curr_exp );
 										}
-										eqn.push_back( mkConcat( eqnc ) );
+										Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] );
+										Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
+										Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) );
+										d_pending.push_back( eq );
+										d_pending_exp[eq] = eq_exp;
+										d_infer.push_back(eq);
+										d_infer_exp.push_back(eq_exp);
+										index_k++;
+									}
+								}
+							}else {
+								Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl;
+								if(areEqual(normal_forms[i][index_i],normal_forms[j][index_j])){
+									Trace("strings-solve-debug") << "Case 1 : strings are equal" << std::endl;
+									//terms are equal, continue
+									if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){
+										Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,normal_forms[i][index_i],
+																										 normal_forms[j][index_j]);
+										Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl;
+										curr_exp.push_back(eq);
 									}
-									conc = eqn[0].eqNode( eqn[1] );
-									Node ant = mkExplain( antec, antec_new_lits );
-									sendLemma( ant, conc, "Endpoint" );
-									return;
+									index_j++;
+									index_i++;
+									success = true;
 								}else{
-                                    Trace("strings-solve-debug") << "Case 4 : must compare strings" << std::endl;
-                                    Node conc;
-                                    std::vector< Node > antec;
-                                    std::vector< Node > antec_new_lits;
-                                    //check for loops
-                                    //Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl;
-                                    int has_loop[2] = { -1, -1 };
-                                    for( unsigned r=0; r<2; r++ ){
-                                        int index = (r==0 ? index_i : index_j);
-                                        int other_index = (r==0 ? index_j : index_i );
-                                        int n_index = (r==0 ? i : j);
-                                        int other_n_index = (r==0 ? j : i);
-                                        if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) {
-                                            for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){
-                                                if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){
-                                                    has_loop[r] = lp;
-                                                    break;
-                                                }
-                                            }
-                                        }
-                                    }
-                                    if( has_loop[0]!=-1 || has_loop[1]!=-1 ){
-                                        int loop_n_index = has_loop[0]!=-1 ? i : j;
-                                        int other_n_index = has_loop[0]!=-1 ? j : i;
-                                        int loop_index = has_loop[0]!=-1 ? has_loop[0] : has_loop[1];
-                                        int index = has_loop[0]!=-1 ? index_i : index_j;
-                                        int other_index = has_loop[0]!=-1 ? index_j : index_i;
-                                        Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index];
-                                        Trace("strings-loop") << " ... " << 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_index-1] = y * z
-                                        // and
-                                        //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] = z * y
-                                        // for some y,z,k
-
-										Trace("strings-loop") << "Must add lemma." << std::endl;
-										//need to break
-										Node sk_y= NodeManager::currentNM()->mkSkolem( "ysym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
-										Node sk_z= NodeManager::currentNM()->mkSkolem( "zsym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
-
+									Node length_term_i = getLength( normal_forms[i][index_i] );
+									Node length_term_j = getLength( normal_forms[j][index_j] );
+									//check  length(normal_forms[i][index]) == length(normal_forms[j][index])
+									if( !areDisequal(length_term_i, length_term_j) &&
+										normal_forms[i][index_i].getKind()!=kind::CONST_STRING && 
+										normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) {
+			
+										//length terms are equal, merge equivalence classes if not already done so
+										Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j );
+										if( !areEqual(length_term_i, length_term_j) ) {
+											Trace("strings-solve-debug") << "Case 2.1 : string lengths neither equal nor disequal" << std::endl;
+											//try to make the lengths equal via splitting on demand
+											sendSplit( length_term_i, length_term_j, "Length" );
+											length_eq = Rewriter::rewrite( length_eq  );
+											d_pending_req_phase[ length_eq ] = true;
+											return true;
+										}else{
+											Trace("strings-solve-debug") << "Case 2.2 : string lengths are explicitly equal" << std::endl;
+											//lengths are already equal, do unification
+											Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] );
+											std::vector< Node > temp_exp;
+											temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
+											temp_exp.push_back(length_eq);
+											Node eq_exp = temp_exp.empty() ? d_true :
+															temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp );
+											Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
+											d_pending.push_back( eq );
+											d_pending_exp[eq] = eq_exp;
+											d_infer.push_back(eq);
+											d_infer_exp.push_back(eq_exp);
+											return true;
+										}
+									}else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || 
+											  ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){
+										Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl;
+										Node conc;
+										std::vector< Node > antec;
 										antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-										//require that x is non-empty
-										Node x_empty = normal_forms[loop_n_index][loop_index].eqNode( d_emptyString );
-										x_empty = Rewriter::rewrite( x_empty );
-										//if( d_equalityEngine.hasTerm( d_emptyString ) && d_equalityEngine.areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString, true ) ){
-										//	antec.push_back( x_empty.negate() );
-										//}else{
-										antec_new_lits.push_back( x_empty.negate() );
-										//}
-										d_pending_req_phase[ x_empty ] = true;
-
-
-										//t1 * ... * tn = y * z
-										std::vector< Node > c1c;
-										//n[loop_n_index][index]....n[loop_n_index][loop_lindex-1]
-										for( int r=index; r<=loop_index-1; r++ ) {
-											c1c.push_back( normal_forms[loop_n_index][r] );
+										std::vector< Node > antec_new_lits;
+										std::vector< Node > eqn;
+										for( unsigned r=0; r<2; r++ ){
+											int index_k = r==0 ? index_i : index_j;
+											int k = r==0 ? i : j;
+											std::vector< Node > eqnc;
+											for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ){
+												eqnc.push_back( normal_forms[k][index_l] );
+											}
+											eqn.push_back( mkConcat( eqnc ) );
 										}
-										Node conc1 = mkConcat( c1c );
-										conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1,
-														NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) );
-										std::vector< Node > c2c;
-										//s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1]
-										for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) {
-											c2c.push_back( normal_forms[other_n_index][r] );
+										if( areEqual( eqn[0], eqn[1] ) ){
+											addNormalFormPair( normal_form_src[i], normal_form_src[j] );
+										}else{
+											conc = eqn[0].eqNode( eqn[1] );
+											Node ant = mkExplain( antec, antec_new_lits );
+											sendLemma( ant, conc, "Endpoint" );
+											return true;
 										}
-										Node left2 = mkConcat( c2c );
-										std::vector< Node > c3c;
-										c3c.push_back( sk_z );
-										c3c.push_back( sk_y );
-										//r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1]
-										for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) {
-											c3c.push_back( normal_forms[loop_n_index][r] );
+									}else{
+										Trace("strings-solve-debug") << "Case 4 : must compare strings" << std::endl;
+										Node conc;
+										std::vector< Node > antec;
+										std::vector< Node > antec_new_lits;
+										//check for loops
+										//Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl;
+										int has_loop[2] = { -1, -1 };
+										for( unsigned r=0; r<2; r++ ){
+											int index = (r==0 ? index_i : index_j);
+											int other_index = (r==0 ? index_j : index_i );
+											int n_index = (r==0 ? i : j);
+											int other_n_index = (r==0 ? j : i);
+											if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) {
+												for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){
+													if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){
+														has_loop[r] = lp;
+														break;
+													}
+												}
+											}
 										}
-										Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2,
-														mkConcat( c3c ) );
-										
-										Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y );
-										//Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z );
-										//Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y_len, d_zero);
-										//Node len_z_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z_len, d_zero);
-										//Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y, d_emptyString);
-										//Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, len_z_eq_zero, len_y_eq_zero);
-										
-										//Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate();
-										//Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, 
-										//						NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]),
-										//						sk_y_len );
-										Node ant = mkExplain( antec, antec_new_lits );
-										conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y
-
-										//Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString);
-										//conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc );
-
-										//we will be done
-										addNormalFormPair( normal_form_src[i], normal_form_src[j] );
-										sendLemma( ant, conc, "Loop" );
-										addInductiveEquation( normal_forms[other_n_index][other_index], sk_y, sk_z, ant, "Loop Induction" );
-										return;
-                                    }else{
-                                        Trace("strings-solve-debug") << "No loops detected." << std::endl;
-                                        if( normal_forms[i][index_i].getKind() == kind::CONST_STRING ||
-                                            normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
-											unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j;
-											unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j;
-											unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i;
-											unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i;
-                                            Node const_str = normal_forms[const_k][const_index_k];
-                                            Node other_str = normal_forms[nconst_k][nconst_index_k];
-                                            if( other_str.getKind() == kind::CONST_STRING ) {
-                                                unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
-                                                if( const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short) ) {
-                                                    //same prefix
-                                                    //k is the index of the string that is shorter
-                                                    int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j;
-                                                    int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j;
-                                                    int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i;
-                                                    int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i;
-                                                    Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(len_short) );
-                                                    Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
-                                                    normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
-                                                    normal_forms[l][index_l] = normal_forms[k][index_k];
-                                                    success = true;
-                                                } else {
-                                                    //curr_exp is conflict
-                                                    antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+										if( has_loop[0]!=-1 || has_loop[1]!=-1 ){
+											int loop_n_index = has_loop[0]!=-1 ? i : j;
+											int other_n_index = has_loop[0]!=-1 ? j : i;
+											int loop_index = has_loop[0]!=-1 ? has_loop[0] : has_loop[1];
+											int index = has_loop[0]!=-1 ? index_i : index_j;
+											int other_index = has_loop[0]!=-1 ? index_j : index_i;
+											Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index];
+											Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl;
+											
+											Trace("strings-loop") << " ... T(Y.Z)= ";
+											for(int lp=index; lp<loop_index; ++lp) {
+												if(lp != index) Trace("strings-loop") << " ++ ";
+												Trace("strings-loop") << normal_forms[loop_n_index][lp];
+											}
+											Trace("strings-loop") << std::endl;
+											Trace("strings-loop") << " ... S(Z.Y)= ";
+											for(int lp=other_index+1; lp<(int)normal_forms[other_n_index].size(); ++lp) {
+												if(lp != other_index+1) Trace("strings-loop") << " ++ ";
+												Trace("strings-loop") << normal_forms[other_n_index][lp];
+											}
+											Trace("strings-loop") << std::endl;
+											Trace("strings-loop") << " ... R= ";
+											for(int lp=loop_index+1; lp<(int)normal_forms[loop_n_index].size(); ++lp) {
+												if(lp != loop_index+1) Trace("strings-loop") << " ++ ";
+												Trace("strings-loop") << normal_forms[loop_n_index][lp];
+											}
+											Trace("strings-loop") << std::endl;
+
+											//we have x * s1 * .... * sm = t1 * ... * tn * x * r1 * ... * rp
+											//check if
+											//t1 * ... * tn = n[loop_n_index][index]....n[loop_n_index][loop_index-1] = y * z
+											// and
+											//s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] = z * y
+											// for some y,z,k
+
+											Trace("strings-loop") << "Must add lemma." << std::endl;
+											//need to break
+											Node sk_y= NodeManager::currentNM()->mkSkolem( "ysym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
+											Node sk_z= NodeManager::currentNM()->mkSkolem( "zsym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
+
+											antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+											//require that x is non-empty
+											Node x_empty = normal_forms[loop_n_index][loop_index].eqNode( d_emptyString );
+											x_empty = Rewriter::rewrite( x_empty );
+											//if( d_equalityEngine.hasTerm( d_emptyString ) && d_equalityEngine.areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString, true ) ){
+											//	antec.push_back( x_empty.negate() );
+											//}else{
+											antec_new_lits.push_back( x_empty.negate() );
+											//}
+											d_pending_req_phase[ x_empty ] = true;
+
+
+											//t1 * ... * tn = y * z
+											std::vector< Node > c1c;
+											//n[loop_n_index][index]....n[loop_n_index][loop_lindex-1]
+											for( int r=index; r<=loop_index-1; r++ ) {
+												c1c.push_back( normal_forms[loop_n_index][r] );
+											}
+											Node conc1 = mkConcat( c1c );
+											conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1,
+															NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) );
+											std::vector< Node > c2c;
+											//s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1]
+											for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) {
+												c2c.push_back( normal_forms[other_n_index][r] );
+											}
+											Node left2 = mkConcat( c2c );
+											std::vector< Node > c3c;
+											c3c.push_back( sk_z );
+											c3c.push_back( sk_y );
+											//r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1]
+											for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) {
+												c3c.push_back( normal_forms[loop_n_index][r] );
+											}
+											Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2,
+															mkConcat( c3c ) );
+											
+											Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y );
+											//Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z );
+											//Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y_len, d_zero);
+											//Node len_z_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z_len, d_zero);
+											//Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y, d_emptyString);
+											//Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, len_z_eq_zero, len_y_eq_zero);
+											
+											//Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate();
+											//Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, 
+											//						NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]),
+											//						sk_y_len );
+											Node ant = mkExplain( antec, antec_new_lits );
+											conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y
+
+											//Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString);
+											//conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc );
+
+											//we will be done
+											addNormalFormPair( normal_form_src[i], normal_form_src[j] );
+											sendLemma( ant, conc, "Loop" );
+											addInductiveEquation( normal_forms[other_n_index][other_index], sk_y, sk_z, ant, "Loop Induction" );
+											return true;
+										}else{
+											Trace("strings-solve-debug") << "No loops detected." << std::endl;
+											if( normal_forms[i][index_i].getKind() == kind::CONST_STRING ||
+												normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
+												unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j;
+												unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j;
+												unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i;
+												unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i;
+												Node const_str = normal_forms[const_k][const_index_k];
+												Node other_str = normal_forms[nconst_k][nconst_index_k];
+												if( other_str.getKind() == kind::CONST_STRING ) {
+													unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
+													if( const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short) ) {
+														//same prefix
+														//k is the index of the string that is shorter
+														int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j;
+														int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j;
+														int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i;
+														int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i;
+														Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(len_short) );
+														Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
+														normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
+														normal_forms[l][index_l] = normal_forms[k][index_k];
+														success = true;
+													} else {
+														//curr_exp is conflict
+														antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+														Node ant = mkExplain( antec, antec_new_lits );
+														sendLemma( ant, conc, "Conflict" );
+														return true;
+													}
+												} else {
+													Assert( other_str.getKind()!=kind::STRING_CONCAT );
+													antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+													Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
+														NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
+													//split the string
+													Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/c split" );
+
+													Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString );
+													Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str,
+																NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) );
+													conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
+													Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
+
 													Node ant = mkExplain( antec, antec_new_lits );
-													sendLemma( ant, conc, "Conflict" );
-													return;
-                                                }
-                                            } else {
-                                                Assert( other_str.getKind()!=kind::STRING_CONCAT );
-                                                antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-												Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
-													NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
-												//split the string
-												Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for 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 );
+													sendLemma( ant, conc, "Constant Split" );
+													return true;
+												}
+											}else{
+												antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+
+												Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
+												if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){
+													antec.push_back( ldeq );
+												}else{
+													antec_new_lits.push_back(ldeq);
+												}
+												Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/v split" );
+												Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i],
+															NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) );
+												Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j],
+															NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) );
 												conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
-                                                Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
+												// |sk| > 0
+												//Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
+												//Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero);
+												Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate();
+												Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl;
+												//d_out->lemma(sk_gt_zero);
+												d_lemma_cache.push_back( sk_gt_zero );
 
 												Node ant = mkExplain( antec, antec_new_lits );
-												sendLemma( ant, conc, "Constant Split" );
-												return;
-                                            }
-                                        }else{
-                                            antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-
-											Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
-											if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){
-												antec.push_back( ldeq );
-											}else{
-												antec_new_lits.push_back(ldeq);
+												sendLemma( ant, conc, "Split" );
+												return true;
 											}
-											Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" );
-											Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i],
-														NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) );
-											Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j],
-														NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) );
-											conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
-											// |sk| > 0
-											//Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-											//Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero);
-											Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate();
-											Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl;
-											//d_out->lemma(sk_gt_zero);
-											d_lemma_cache.push_back( sk_gt_zero );
-
-											Node ant = mkExplain( antec, antec_new_lits );
-											sendLemma( ant, conc, "Split" );
-											return;
-                                        }
-                                    }
-                                }
-                            }
-                        }
-                    }while(success);
-                }
-            }
+										}
+									}
+								}
+							}
+						}while(success);
+					}
+				}
+			}
 
             //construct the normal form
             if( normal_forms.empty() ){
@@ -990,73 +1065,150 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                 }
                 Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl;
             }
-            //if( visited.empty() ){
-                //TODO : cache?
-            //}
+
+    	    d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0];
             d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() );
             d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() );
-            Trace("strings-process") << "Return process equivalence class " << eqc << " : returned." << std::endl;
+            Trace("strings-process") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl;
         }else{
-            Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed." << std::endl;
+            Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl;
             nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() );
             nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() );
+			result = true;
         }
         visited.pop_back();
+		return result;
     }
 }
 
 bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
 	//Assert( areDisequal( ni, nj ) );
 	if( d_normal_forms[ni].size()>1 || d_normal_forms[nj].size()>1 ){
+		std::vector< Node > nfi;
+		nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() );
+		std::vector< Node > nfj;
+		nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() );
+
 		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;
+		while( index<nfi.size() || index<nfj.size() ){
+			if( index>=nfi.size() || index>=nfj.size() ){
+				std::vector< Node > ant;
+				//we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
+				Node lni = getLength( ni );
+				Node lnj = getLength( nj );
+				ant.push_back( lni.eqNode( lnj ) );
+				ant.push_back( getLengthTerm( ni ).eqNode( d_normal_forms_base[ni] ) );
+				ant.push_back( getLengthTerm( nj ).eqNode( d_normal_forms_base[nj] ) );
+				ant.insert( ant.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
+				ant.insert( ant.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
+				std::vector< Node > cc;
+				std::vector< Node >& nfk = index>=nfi.size() ? nfj : nfi;
+				for( unsigned index_k=index; index_k<nfk.size(); index_k++ ){
+					cc.push_back( nfk[index_k].eqNode( d_emptyString ) );
+				}
+				Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
+				conc = Rewriter::rewrite( conc );
+				sendLemma(mkExplain( ant ), conc, "Disequality Normalize Empty");
+				return true;
+			}else{
+				Node i = nfi[index];
+				Node j = nfj[index];
+				Trace("strings-solve-debug")  << "...Processing " << i << " " << j << std::endl;
+				if( !areEqual( i, j ) ) {
+					if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ){
+						unsigned int len_short = i.getConst<String>().size() < j.getConst<String>().size() ? i.getConst<String>().size() : j.getConst<String>().size();
+						String si = i.getConst<String>().substr(0, len_short);
+						String sj = j.getConst<String>().substr(0, len_short);
+						if(si == sj) {
+							if( i.getConst<String>().size() < j.getConst<String>().size() ) {
+								Node remainderStr = NodeManager::currentNM()->mkConst( j.getConst<String>().substr(len_short) );
+								Trace("strings-solve-debug-test") << "Break normal form of " << nfj[index] << " into " << nfi[index] << ", " << remainderStr << std::endl;
+								nfj.insert( nfj.begin() + index + 1, remainderStr );
+								nfj[index] = nfi[index];
+							} else {
+								Node remainderStr = NodeManager::currentNM()->mkConst( i.getConst<String>().substr(len_short) );
+								Trace("strings-solve-debug-test") << "Break normal form of " << nfi[index] << " into " << nfj[index] << ", " << remainderStr << std::endl;
+								nfi.insert( nfi.begin() + index + 1, remainderStr );
+								nfi[index] = nfj[index];
+							}
+						} else {
+							//conflict
+							return false;
+						}
+					}else{
+						Node li = getLength( i );
+						Node lj = getLength( j );
+						if( areDisequal(li, lj) ){
+							Trace("strings-solve") << "Case 2 : add lemma " << std::endl;
+							//must add lemma
+							std::vector< Node > antec;
+							std::vector< Node > antec_new_lits;
+							antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
+							antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
+							antec.push_back( ni.eqNode( nj ).negate() );
+							antec_new_lits.push_back( li.eqNode( lj ).negate() );
+							std::vector< Node > conc;
+							Node sk1 = NodeManager::currentNM()->mkSkolem( "xpdsym_$$", ni.getType(), "created for disequality normalization" );
+							Node sk2 = NodeManager::currentNM()->mkSkolem( "ypdsym_$$", ni.getType(), "created for disequality normalization" );
+							Node sk3 = NodeManager::currentNM()->mkSkolem( "zpdsym_$$", ni.getType(), "created for disequality normalization" );
+							Node lsk1 = getLength( sk1 );
+							conc.push_back( lsk1.eqNode( li ) );
+							Node lsk2 = getLength( sk2 );
+							conc.push_back( lsk2.eqNode( lj ) );
+							conc.push_back( NodeManager::currentNM()->mkNode( kind::OR,
+												j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
+							
+							/*
+							Node sk1 = NodeManager::currentNM()->mkSkolem( "w1sym_$$", ni.getType(), "created for disequality normalization" );
+							Node sk2 = NodeManager::currentNM()->mkSkolem( "w2sym_$$", ni.getType(), "created for disequality normalization" );
+							Node sk3 = NodeManager::currentNM()->mkSkolem( "w3sym_$$", ni.getType(), "created for disequality normalization" );
+							Node sk4 = NodeManager::currentNM()->mkSkolem( "w4sym_$$", ni.getType(), "created for disequality normalization" );
+							Node sk5 = NodeManager::currentNM()->mkSkolem( "w5sym_$$", ni.getType(), "created for disequality normalization" );
+							Node w1w2w3 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 );
+							Node w1w4w5 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk4, sk5 );
+							Node s_eq_w1w2w3 = NodeManager::currentNM()->mkNode( kind::EQUAL, ni, w1w2w3 );
+							conc.push_back( s_eq_w1w2w3 );
+							Node t_eq_w1w4w5 = NodeManager::currentNM()->mkNode( kind::EQUAL, nj, w1w4w5 );
+							conc.push_back( t_eq_w1w4w5 );
+							Node w2_neq_w4 = sk2.eqNode( sk4 ).negate();
+							conc.push_back( w2_neq_w4 );
+							Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
+							Node w2_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), one);
+							conc.push_back( w2_len_one );
+							Node w4_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4), one);
+							conc.push_back( w4_len_one );
+							Node c = NodeManager::currentNM()->mkNode( kind::AND, conc );
+							*/
+							//Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2),
+							//													     NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4) );
+							//conc.push_back( eq );
+							sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "Disequality Normalize" );
+							return true;
+						}else if( areEqual( li, lj ) ){
+							if( areDisequal( i, j ) ){
+								Trace("strings-solve") << "Case 1 : found equal length disequal sub strings " << i << " " << j << std::endl;
+								//we are done
+								return false;
+							} else {
+								//splitting on demand : try to make them disequal
+								Node eq = i.eqNode( j );
+								sendSplit( i, j, "Disequality : disequal terms" );
+								eq = Rewriter::rewrite( eq );
+								d_pending_req_phase[ eq ] = false;
+								return true;
+							}
+						}else{
+							//splitting on demand : try to make lengths equal
+							Node eq = li.eqNode( lj );
+							sendSplit( li, lj, "Disequality : equal length" );
+							eq = Rewriter::rewrite( eq );
+							d_pending_req_phase[ eq ] = true;
+							return true;
+						}
+					}
 				}
+				index++;
 			}
-			index++;
 		}
 		Assert( false );
 	}
@@ -1183,7 +1335,7 @@ bool TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp, cons
 }
 
 void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
-	if( conc.isNull() ){
+	if( conc.isNull() || conc==d_false ){
 		d_out->conflict(ant);
 		Trace("strings-conflict") << "CONFLICT : Strings conflict : " << ant << std::endl;
 		d_conflict = true;
@@ -1204,11 +1356,23 @@ void TheoryStrings::sendSplit( Node a, Node b, const char * c ) {
 	d_pending_req_phase[eq] = true;
 }
 
+Node TheoryStrings::mkConcat( Node n1, Node n2 ) {
+	std::vector< Node > c;
+	c.push_back( n1 );
+	c.push_back( n2 );
+	return mkConcat( c );
+}
+
 Node TheoryStrings::mkConcat( std::vector< Node >& c ) {
     Node cc = c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString );
 	return Rewriter::rewrite( cc );
 }
 
+Node TheoryStrings::mkExplain( std::vector< Node >& a ) {
+	std::vector< Node > an;
+	return mkExplain( a, an );
+}
+
 Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) {
     std::vector< TNode > antec_exp;
     for( unsigned i=0; i<a.size(); i++ ){
@@ -1247,6 +1411,61 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an )
     return ant;
 }
 
+bool TheoryStrings::checkLengths() {
+  bool addedLemma = false;
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+  while( !eqcs_i.isFinished() ) {
+	Node eqc = (*eqcs_i);
+	//if eqc.getType is string
+	if (eqc.getType().isString()) {
+		//EqcInfo* ei = getOrMakeEqcInfo( eqc, true );
+		//get the constant for the equivalence class
+		//int c_len = ...;
+		eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+		while( !eqc_i.isFinished() ){
+			Node n = (*eqc_i);
+			//if n is concat, and
+			//if n has not instantiatied the concat..length axiom
+			//then, add lemma
+			if( n.getKind() == kind::CONST_STRING ){	//n.getKind() == kind::STRING_CONCAT ||
+				if( d_length_inst.find(n)==d_length_inst.end() ){
+					d_length_inst[n] = true;
+					Trace("strings-debug") << "get n: " << n << endl;
+					Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
+					d_length_intro_vars.push_back( sk );
+					Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
+					eq = Rewriter::rewrite(eq);
+					Trace("strings-lemma") << "Strings: Add term lemma " << eq << std::endl;
+					d_out->lemma(eq);
+					Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
+					Node lsum;
+					if( n.getKind() == kind::STRING_CONCAT ){
+						//add lemma
+						std::vector<Node> node_vec;
+						for( unsigned i=0; i<n.getNumChildren(); i++ ) {
+							Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
+							node_vec.push_back(lni);
+						}
+						lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
+					}else{
+						//add lemma
+						lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
+					}
+					Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
+					ceq = Rewriter::rewrite(ceq);
+					Trace("strings-lemma") << "Strings: Add length lemma " << ceq << std::endl;
+					d_out->lemma(ceq);
+					addedLemma = true;
+				}
+			}
+			++eqc_i;
+		}
+	}
+	++eqcs_i;
+  }
+  return addedLemma;
+}
+
 bool TheoryStrings::checkNormalForms() {
     Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
 	eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
@@ -1257,14 +1476,20 @@ bool TheoryStrings::checkNormalForms() {
 		bool print = (t==0 && eqc.getType().isString() ) || (t==1 && !eqc.getType().isString() );
 		if (print) {
 			eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-			Trace("strings-eqc") << "Eqc( " << eqc << " ) : ";
+			Trace("strings-eqc") << "Eqc( " << eqc << " ) : { ";
 			while( !eqc2_i.isFinished() ) {
 				if( (*eqc2_i)!=eqc ){
 					Trace("strings-eqc") << (*eqc2_i) << " ";
 				}
 				++eqc2_i;
 			}
-			Trace("strings-eqc") << std::endl;
+			Trace("strings-eqc") << " } " << std::endl;
+			EqcInfo * ei = getOrMakeEqcInfo( eqc, false );
+			if( ei ){
+				Trace("strings-eqc-debug") << "* Length term : " << ei->d_length_term.get() << std::endl;
+				Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei->d_cardinality_lem_k.get() << std::endl;
+				Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei->d_normalized_length.get() << std::endl;
+			}
 		}
 		++eqcs2_i;
 		}
@@ -1318,6 +1543,7 @@ bool TheoryStrings::checkNormalForms() {
 		std::vector< Node > nf;
 		std::vector< Node > nf_exp;
 		normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
+		Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
 		if( d_conflict ){
 			return true;
 		}else if ( d_pending.empty() && d_lemma_cache.empty() ){
@@ -1401,6 +1627,42 @@ bool TheoryStrings::checkNormalForms() {
   }
 }
 
+bool TheoryStrings::checkLengthsEqc() {
+	bool addedLemma = false;
+	std::vector< Node > nodes;
+	getEquivalenceClasses( nodes );
+	for( unsigned i=0; i<nodes.size(); i++ ){
+		if( d_normal_forms[nodes[i]].size()>1 ){
+			Trace("strings-process-debug") << "Process length constraints for " << nodes[i] << std::endl;
+			//check if there is a length term for this equivalence class
+			EqcInfo* ei = getOrMakeEqcInfo( nodes[i], false );
+			Node lt = ei ? ei->d_length_term : Node::null();
+			if( !lt.isNull() ){
+			  Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
+			  //now, check if length normalization has occurred
+			  if( ei->d_normalized_length.get().isNull() ){
+				//if not, add the lemma
+				std::vector< Node > ant;
+				ant.insert( ant.end(), d_normal_forms_exp[nodes[i]].begin(), d_normal_forms_exp[nodes[i]].end() );
+				ant.push_back( d_normal_forms_base[nodes[i]].eqNode( lt ) );
+				Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[nodes[i]] ) );
+				lc = Rewriter::rewrite( lc );
+				Node eq = llt.eqNode( lc );
+				ei->d_normalized_length.set( eq );
+				sendLemma( mkExplain( ant ), eq, "Length Normalization" );
+				addedLemma = true;
+			  }
+			}
+		}else{
+			Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
+		}
+	}
+	if( addedLemma ){
+		doPendingLemmas();
+	}
+	return addedLemma;
+}
+
 bool TheoryStrings::checkCardinality() {
   int cardinality = options::stringCharCardinality();
   Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 6b8144d6e..16c3d4876 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -50,6 +50,7 @@ class TheoryStrings : public Theory {
   bool hasTerm( Node a );
   bool areEqual( Node a, Node b );
   bool areDisequal( Node a, Node b );
+  Node getLengthTerm( Node t );
   Node getLength( Node t );
   public:
 
@@ -131,6 +132,10 @@ class TheoryStrings : public Theory {
   /** inferences */
   NodeList d_infer;
   NodeList d_infer_exp;
+  /** normal forms */
+  std::map< Node, Node > d_normal_forms_base;
+  std::map< Node, std::vector< Node > > d_normal_forms;
+  std::map< Node, std::vector< Node > > d_normal_forms_exp;
   //map of pairs of terms that have the same normal form
   NodeListMap d_nf_pairs;
   void addNormalFormPair( Node n1, Node n2 );
@@ -179,6 +184,8 @@ class TheoryStrings : public Theory {
     context::CDO< Node > d_const_term;
     context::CDO< Node > d_length_term;
     context::CDO< unsigned > d_cardinality_lem_k;
+	// 1 = added length lemma
+	context::CDO< Node > d_normalized_length;
   };
   /** map from representatives to information necessary for equivalence classes */
   std::map< Node, EqcInfo* > d_eqc_info;
@@ -186,14 +193,14 @@ class TheoryStrings : public Theory {
   //maintain which concat terms have the length lemma instantiatied
   std::map< Node, bool > d_length_inst;
   private:
-    std::map< Node, std::vector< Node > > d_normal_forms;
-    std::map< Node, std::vector< Node > > d_normal_forms_exp;
-    void getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
+    bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
     std::vector< std::vector< Node > > &normal_forms,  std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src);
-    void normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
+    bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
     bool normalizeDisequality( Node n1, Node n2 );
 
+	bool checkLengths();
     bool checkNormalForms();
+	bool checkLengthsEqc();
     bool checkCardinality();
     bool checkInductiveEquations();
 	int gcd(int a, int b);
@@ -222,8 +229,10 @@ protected:
   void sendLemma( Node ant, Node conc, const char * c );
   void sendSplit( Node a, Node b, const char * c );
   /** mkConcat **/
+  Node mkConcat( Node n1, Node n2 );
   Node mkConcat( std::vector< Node >& c );
   /** mkExplain **/
+  Node mkExplain( std::vector< Node >& a );
   Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
 
   //get equivalence classes
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 8fa4345e5..f303fd333 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -84,7 +84,8 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret
 	}
 }
 
-Node StringsPreprocess::simplify( Node t ) {
+
+Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
     if(i != d_cache.end()) {
       return (*i).second.isNull() ? t : (*i).second;
@@ -92,21 +93,39 @@ Node StringsPreprocess::simplify( Node t ) {
 
 	if( t.getKind() == kind::STRING_IN_REGEXP ){
 		// t0 in t1
+		Node t0 = simplify( t[0], new_nodes );
 		//rewrite it
 		std::vector< Node > ret;
-		simplifyRegExp( t[0], t[1], ret );
+		simplifyRegExp( t0, t[1], ret );
 
 		Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
 		d_cache[t] = (t == n) ? Node::null() : n;
 		return n;
-    }else if( t.getNumChildren()>0 ){
+	}else if( t.getKind() == kind::STRING_SUBSTR ){
+		Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" );
+		Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" );
+		Node sk3 = NodeManager::currentNM()->mkSkolem( "st3sym_$$", t.getType(), "created for substr" );
+		Node x = simplify( t[0], new_nodes );
+		Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
+							NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
+		new_nodes.push_back( x_eq_123 );
+		Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
+								NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+		new_nodes.push_back( len_sk1_eq_i );
+		Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2],
+								NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
+		new_nodes.push_back( len_sk2_eq_j );
+
+		d_cache[t] = sk2;
+		return sk2;
+	} 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] );
+			Node tn = simplify( t[i], new_nodes );
 			cc.push_back( tn );
 			changed = changed || tn!=t[i];
 		}
@@ -125,9 +144,11 @@ Node StringsPreprocess::simplify( Node t ) {
 }
 
 void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
+	std::vector< Node > new_nodes;
 	for( unsigned i=0; i<vec_node.size(); i++ ){
-		vec_node[i] = simplify( vec_node[i] );
+		vec_node[i] = simplify( vec_node[i], new_nodes );
 	}
+	vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() );
 }
 
 }/* CVC4::theory::strings namespace */
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index f82a3cf24..d07249a02 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -32,7 +32,7 @@ class StringsPreprocess {
 	std::hash_map<TNode, Node, TNodeHashFunction> d_cache;
 private:
 	void simplifyRegExp( Node s, Node r, std::vector< Node > &ret );
-	Node simplify( Node t );
+	Node simplify( Node t, std::vector< Node > &new_nodes );
 public:
 void simplify(std::vector< Node > &vec_node);
 };
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 412135675..3a7ad1ee0 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -137,7 +137,20 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                 retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
             }
         }
-    }
+    } else if(node.getKind() == kind::STRING_SUBSTR) {
+		if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {
+			int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
+			int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
+			if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) {
+				retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) );
+			} else {
+				// TODO: some issues, must be guarded by users
+				retNode = NodeManager::currentNM()->mkConst( false );
+			}
+		} else {
+			//handled by preprocess
+		}
+	}
 
   Trace("strings-postrewrite") << "Strings::postRewrite returning " << node << std::endl;
   return RewriteResponse(REWRITE_DONE, retNode);
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 8fc630206..ef8f58f80 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -61,6 +61,28 @@ public:
   }
 };
 
+class StringSubstrTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if( check ){
+        TypeNode t = n[0].getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting string terms in substr");
+        }
+		t = n[1].getType(check);
+        if (!t.isInteger()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting start int terms in substr");
+        }
+		t = n[2].getType(check);
+        if (!t.isInteger()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting length int terms in substr");
+        }
+    }
+    return nodeManager->stringType();
+  }
+};
+
 class RegExpConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 163dd3c1f..8c85e4dd2 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1152,7 +1152,7 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu
     clique.pop_back();
   }
   //debugging information
-  if( options::ufssSymBreak() ){
+  if( Trace.isOn("uf-ss-cliques") ){
     std::vector< Node > clique_vec;
     clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
     addClique( d_cardinality, clique_vec );
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index b66d1cbe4..682e1e1e7 100644
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -21,6 +21,7 @@
 
 #include "util/sort_inference.h"
 #include "theory/uf/options.h"
+#include "smt/options.h"
 //#include "theory/rewriter.h"
 
 using namespace CVC4;
@@ -75,10 +76,11 @@ bool SortInference::UnionFind::isValid() {
 }
 
 
-void SortInference::recordSubsort( int s ){
+void SortInference::recordSubsort( TypeNode tn, int s ){
   s = d_type_union_find.getRepresentative( s );
   if( std::find( d_sub_sorts.begin(), d_sub_sorts.end(), s )==d_sub_sorts.end() ){
     d_sub_sorts.push_back( s );
+    d_type_sub_sorts[tn].push_back( s );
   }
 }
 
@@ -91,7 +93,25 @@ void SortInference::printSort( const char* c, int t ){
   }
 }
 
-void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){
+void SortInference::reset() {
+  d_sub_sorts.clear();
+  d_non_monotonic_sorts.clear();
+  d_type_sub_sorts.clear();
+  //reset info
+  sortCount = 1;
+  d_type_union_find.clear();
+  d_type_types.clear();
+  d_id_for_types.clear();
+  d_op_return_types.clear();
+  d_op_arg_types.clear();
+  d_var_types.clear();
+  //for rewriting
+  d_symbol_map.clear();
+  d_const_map.clear();
+}
+
+bool SortInference::simplify( std::vector< Node >& assertions ){
+  Trace("sort-inference") << "Calculating sort inference..." << std::endl;
   //process all assertions
   for( unsigned i=0; i<assertions.size(); i++ ){
     Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl;
@@ -100,53 +120,62 @@ void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){
   }
   for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
     Trace("sort-inference") << it->first << " : ";
+    TypeNode retTn = it->first.getType();
     if( !d_op_arg_types[ it->first ].empty() ){
       Trace("sort-inference") << "( ";
       for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){
-        recordSubsort( d_op_arg_types[ it->first ][i] );
+        recordSubsort( retTn[i], d_op_arg_types[ it->first ][i] );
         printSort( "sort-inference", d_op_arg_types[ it->first ][i] );
         Trace("sort-inference") << " ";
       }
       Trace("sort-inference") << ") -> ";
+      retTn = retTn[(int)retTn.getNumChildren()-1];
     }
-    recordSubsort( it->second );
+    recordSubsort( retTn, it->second );
     printSort( "sort-inference", it->second );
     Trace("sort-inference") << std::endl;
   }
   for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){
     Trace("sort-inference") << "Quantified formula : " << it->first << " : " << std::endl;
-    for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-      printSort( "sort-inference", it2->second );
+    for( unsigned i=0; i<it->first[0].getNumChildren(); i++ ){
+      recordSubsort( it->first[0][i].getType(), it->second[it->first[0][i]] );
+      printSort( "sort-inference", it->second[it->first[0][i]] );
       Trace("sort-inference") << std::endl;
     }
     Trace("sort-inference") << std::endl;
   }
 
-  //determine monotonicity of sorts
-  for( unsigned i=0; i<assertions.size(); i++ ){
-    Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl;
-    std::map< Node, Node > var_bound;
-    processMonotonic( assertions[i], true, true, var_bound );
-  }
+  if( !options::ufssSymBreak() ){
+    bool rewritten = false;
+    //determine monotonicity of sorts
+    for( unsigned i=0; i<assertions.size(); i++ ){
+      Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl;
+      std::map< Node, Node > var_bound;
+      processMonotonic( assertions[i], true, true, var_bound );
+    }
 
-  Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl;
-  for( unsigned i=0; i<d_sub_sorts.size(); i++ ){
-    printSort( "sort-inference", d_sub_sorts[i] );
-    if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){
-      Trace("sort-inference") << " is interpreted." << std::endl;
-    }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){
-      Trace("sort-inference") << " is monotonic." << std::endl;
-    }else{
-      Trace("sort-inference") << " is not monotonic." << std::endl;
+    Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl;
+    for( unsigned i=0; i<d_sub_sorts.size(); i++ ){
+      printSort( "sort-inference", d_sub_sorts[i] );
+      if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){
+        Trace("sort-inference") << " is interpreted." << std::endl;
+      }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){
+        Trace("sort-inference") << " is monotonic." << std::endl;
+      }else{
+        Trace("sort-inference") << " is not monotonic." << std::endl;
+      }
     }
-  }
 
-  if( doRewrite ){
-    //simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers)
+    //simplify all assertions by introducing new symbols wherever necessary
     for( unsigned i=0; i<assertions.size(); i++ ){
+      Node prev = assertions[i];
       std::map< Node, Node > var_bound;
       assertions[i] = simplify( assertions[i], var_bound );
-      Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl;
+      if( prev!=assertions[i] ){
+        rewritten = true;
+        Trace("sort-inference-rewrite") << prev << std::endl;
+        Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl;
+      }
     }
     //now, ensure constants are distinct
     for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){
@@ -154,33 +183,79 @@ void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){
       for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
         consts.push_back( it2->second );
       }
-      //add lemma enforcing introduced constants to be distinct?
+      //TODO: add lemma enforcing introduced constants to be distinct
     }
-  }else if( !options::ufssSymBreak() ){
-    std::map< int, Node > constants;
-    //just add a bunch of unit lemmas
+
+    //enforce constraints based on monotonicity
+    for( std::map< TypeNode, std::vector< int > >::iterator it = d_type_sub_sorts.begin(); it != d_type_sub_sorts.end(); ++it ){
+      int nmonSort = -1;
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
+          nmonSort = it->second[i];
+          break;
+        }
+      }
+      if( nmonSort!=-1 ){
+        std::vector< Node > injections;
+        TypeNode base_tn = getOrCreateTypeForId( nmonSort, it->first );
+        for( unsigned i=0; i<it->second.size(); i++ ){
+          if( it->second[i]!=nmonSort ){
+            TypeNode new_tn = getOrCreateTypeForId( it->second[i], it->first );
+            //make injection to nmonSort
+            Node a1 = mkInjection( new_tn, base_tn );
+            injections.push_back( a1 );
+            if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
+              //also must make injection from nmonSort to this
+              Node a2 = mkInjection( base_tn, new_tn );
+              injections.push_back( a2 );
+            }
+          }
+        }
+        Trace("sort-inference-rewrite") << "Add the following injections for " << it->first << " to ensure consistency wrt non-monotonic sorts : " << std::endl;
+        for( unsigned j=0; j<injections.size(); j++ ){
+          Trace("sort-inference-rewrite") << "   " << injections[j] << std::endl;
+        }
+        assertions.insert( assertions.end(), injections.begin(), injections.end() );
+        if( !injections.empty() ){
+          rewritten = true;
+        }
+      }
+    }
+    //no sub-sort information is stored
+    reset();
+    return rewritten;
+  }
+  /*
+  else if( !options::ufssSymBreak() ){
+    //just add the unit lemmas between constants
+    std::map< TypeNode, std::map< int, Node > > constants;
     for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
       int rt = d_type_union_find.getRepresentative( it->second );
-      if( d_op_arg_types[ it->first ].empty() && constants.find( rt )==constants.end() ){
-        constants[ rt ] = it->first;
+      if( d_op_arg_types[ it->first ].empty() ){
+        TypeNode tn = it->first.getType();
+        if( constants[ tn ].find( rt )==constants[ tn ].end() ){
+          constants[ tn ][ rt ] = it->first;
+        }
       }
     }
     //add unit lemmas for each constant
-    Node first_const;
-    for( std::map< int, Node >::iterator it = constants.begin(); it != constants.end(); ++it ){
-      if( first_const.isNull() ){
-        first_const = it->second;
-      }else{
-        Node eq = first_const.eqNode( it->second );
-        //eq = Rewriter::rewrite( eq );
-        Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl;
-        assertions.push_back( eq );
+    for( std::map< TypeNode, std::map< int, Node > >::iterator it = constants.begin(); it != constants.end(); ++it ){
+      Node first_const;
+      for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+        if( first_const.isNull() ){
+          first_const = it2->second;
+        }else{
+          Node eq = first_const.eqNode( it2->second );
+          //eq = Rewriter::rewrite( eq );
+          Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl;
+          assertions.push_back( eq );
+        }
       }
     }
-
-
   }
+  */
   initialSortCount = sortCount;
+  return false;
 }
 
 void SortInference::setEqual( int t1, int t2 ){
@@ -234,7 +309,7 @@ int SortInference::getIdForType( TypeNode tn ){
 }
 
 int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
-  Trace("sort-inference-debug") << "Process " << n << std::endl;
+  Trace("sort-inference-debug") << "...Process " << n << std::endl;
   //add to variable bindings
   if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
     if( d_var_types.find( n )!=d_var_types.end() ){
@@ -284,9 +359,14 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
   }else if( n.getKind()==kind::APPLY_UF ){
     Node op = n.getOperator();
     if( d_op_return_types.find( op )==d_op_return_types.end() ){
-      //assign arbitrary sort for return type
-      d_op_return_types[op] = sortCount;
-      sortCount++;
+      if( n.getType().isBoolean() ){
+        //use booleans
+        d_op_return_types[op] = getIdForType( n.getType() );
+      }else{
+        //assign arbitrary sort for return type
+        d_op_return_types[op] = sortCount;
+        sortCount++;
+      }
       //d_type_eq_class[sortCount].push_back( op );
       //assign arbitrary sort for argument types
       for( size_t i=0; i<n.getNumChildren(); i++ ){
@@ -306,7 +386,7 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
       Trace("sort-inference-debug") << n << " is a bound variable." << std::endl;
       //the return type was specified while binding
       retType = d_var_types[it->second][n];
-    }else if( n.getKind() == kind::VARIABLE ){
+    }else if( n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM ){
       Trace("sort-inference-debug") << n << " is a variable." << std::endl;
       if( d_op_return_types.find( n )==d_op_return_types.end() ){
         //assign arbitrary sort
@@ -333,13 +413,14 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
       retType = getIdForType( n.getType() );
     }
   }
-  Trace("sort-inference-debug") << "Type( " << n << " ) = ";
+  Trace("sort-inference-debug") << "...Type( " << n << " ) = ";
   printSort("sort-inference-debug", retType );
   Trace("sort-inference-debug") << std::endl;
   return retType;
 }
 
 void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ) {
+  Trace("sort-inference-debug") << "...Process monotonic " << pol << " " << hasPol << " " << n << std::endl;
   if( n.getKind()==kind::FORALL ){
     for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
       var_bound[n[0][i]] = n;
@@ -351,25 +432,24 @@ void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< N
   }else if( n.getKind()==kind::EQUAL ){
     if( !hasPol || pol ){
       for( unsigned i=0; i<2; i++ ){
-        if( var_bound.find( n[i] )==var_bound.end() ){
+        if( var_bound.find( n[i] )!=var_bound.end() ){
           int sid = getSortId( var_bound[n[i]], n[i] );
           d_non_monotonic_sorts[sid] = true;
           break;
         }
       }
     }
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      bool npol = pol;
-      bool nhasPol = hasPol;
-      if( n.getKind()==kind::NOT || ( n.getKind()==kind::IMPLIES && i==0 ) ){
-        npol = !npol;
-      }
-      if( ( n.getKind()==kind::ITE && i==0 ) || n.getKind()==kind::XOR || n.getKind()==kind::IFF ){
-        nhasPol = false;
-      }
-      processMonotonic( n[i], npol, nhasPol, var_bound );
+  }
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    bool npol = pol;
+    bool nhasPol = hasPol;
+    if( n.getKind()==kind::NOT || ( n.getKind()==kind::IMPLIES && i==0 ) ){
+      npol = !npol;
     }
+    if( ( n.getKind()==kind::ITE && i==0 ) || n.getKind()==kind::XOR || n.getKind()==kind::IFF ){
+      nhasPol = false;
+    }
+    processMonotonic( n[i], npol, nhasPol, var_bound );
   }
 }
 
@@ -384,15 +464,14 @@ TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){
     if( !pref.isNull() && d_id_for_types.find( pref )==d_id_for_types.end() ){
       retType = pref;
     }else{
-      if( d_subtype_count.find( pref )==d_subtype_count.end() ){
-        d_subtype_count[pref] = 0;
-      }
       //must create new type
       std::stringstream ss;
-      ss << "it_" << d_subtype_count[pref] << "_" << pref;
-      d_subtype_count[pref]++;
+      ss << "it_" << t << "_" << pref;
       retType = NodeManager::currentNM()->mkSort( ss.str() );
     }
+    Trace("sort-inference") << "-> Make type " << retType << " to correspond to ";
+    printSort("sort-inference", t );
+    Trace("sort-inference") << std::endl;
     d_id_for_types[ retType ] = rt;
     d_type_types[ rt ] = retType;
     return retType;
@@ -419,6 +498,10 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){
       d_const_map[tn][ old ] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "constant created during sort inference" );  //use mkConst???
     }
     return d_const_map[tn][ old ];
+  }else if( old.getKind()==kind::BOUND_VARIABLE ){
+    std::stringstream ss;
+    ss << "b_" << old;
+    return NodeManager::currentNM()->mkBoundVar( ss.str(), tn );
   }else{
     std::stringstream ss;
     ss << "i_$$_" << old;
@@ -473,7 +556,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
         Assert( false );
       }
     }
-    return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
+    return NodeManager::currentNM()->mkNode( kind::EQUAL, children );
   }else if( n.getKind()==kind::APPLY_UF ){
     Node op = n.getOperator();
     if( d_symbol_map.find( op )==d_symbol_map.end() ){
@@ -519,7 +602,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
     std::map< Node, Node >::iterator it = var_bound.find( n );
     if( it!=var_bound.end() ){
       return it->second;
-    }else if( n.getKind() == kind::VARIABLE ){
+    }else if( n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM ){
       if( d_symbol_map.find( n )==d_symbol_map.end() ){
         TypeNode tn = getOrCreateTypeForId( d_op_return_types[n], n.getType() );
         d_symbol_map[n] = getNewSymbol( n, tn );
@@ -534,6 +617,22 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
   }
 
 }
+
+Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) {
+  std::vector< TypeNode > tns;
+  tns.push_back( tn1 );
+  TypeNode typ = NodeManager::currentNM()->mkFunctionType( tns, tn2 );
+  Node f = NodeManager::currentNM()->mkSkolem( "inj_$$", typ, "injection for monotonicity constraint" );
+  Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl;
+  Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 );
+  Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 );
+  return NodeManager::currentNM()->mkNode( kind::FORALL,
+           NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ),
+           NodeManager::currentNM()->mkNode( kind::IMPLIES,
+             NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ),
+             v1.eqNode( v2 ) ) );
+}
+
 int SortInference::getSortId( Node n ) {
   Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n;
   if( d_op_return_types.find( op )!=d_op_return_types.end() ){
@@ -554,6 +653,7 @@ int SortInference::getSortId( Node f, Node v ) {
 void SortInference::setSkolemVar( Node f, Node v, Node sk ){
   Trace("sort-inference-temp") << "Set skolem var for " << f << ", variable " << v << std::endl;
   if( isWellSortedFormula( f ) && d_var_types.find( f )==d_var_types.end() ){
+    //calculate the sort for variables if not done so already
     std::map< Node, Node > var_bound;
     process( f, var_bound );
   }
diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h
index 8f0fc5e9f..cd80f57d8 100644
--- a/src/util/sort_inference.h
+++ b/src/util/sort_inference.h
@@ -31,7 +31,8 @@ private:
   //all subsorts
   std::vector< int > d_sub_sorts;
   std::map< int, bool > d_non_monotonic_sorts;
-  void recordSubsort( int s );
+  std::map< TypeNode, std::vector< int > > d_type_sub_sorts;
+  void recordSubsort( TypeNode tn, int s );
 public:
   class UnionFind {
   public:
@@ -79,20 +80,21 @@ private:
   std::map< Node, Node > d_symbol_map;
   //mapping from constants to new symbols
   std::map< TypeNode, std::map< Node, Node > > d_const_map;
-  //number of subtypes generated
-  std::map< TypeNode, int > d_subtype_count;
   //helper functions for simplify
   TypeNode getOrCreateTypeForId( int t, TypeNode pref );
   TypeNode getTypeForId( int t );
   Node getNewSymbol( Node old, TypeNode tn );
   //simplify
   Node simplify( Node n, std::map< Node, Node >& var_bound );
-
+  //make injection
+  Node mkInjection( TypeNode tn1, TypeNode tn2 );
+  //reset
+  void reset();
 public:
   SortInference() : sortCount( 1 ){}
   ~SortInference(){}
 
-  void simplify( std::vector< Node >& assertions, bool doRewrite = false );
+  bool simplify( std::vector< Node >& assertions );
   //get sort id for term n
   int getSortId( Node n );
   //get sort id for variable of quantified formula f