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

37 files changed, 1671 insertions, 1005 deletions

diff --git a/.gitignore b/.gitignore
index bb0f165f3..ea21c49bc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -27,3 +27,5 @@ generated/
 config.reconfig
 *.swp
 /debug/
+/personal.conf
+/personal.mk
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 885a7c487..c7e088124 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1255,6 +1255,7 @@ builtinOp[CVC4::Kind& kind]
   | RESTAR_TOK     { $kind = CVC4::kind::REGEXP_STAR; }
   | REPLUS_TOK     { $kind = CVC4::kind::REGEXP_PLUS; }
   | REOPT_TOK      { $kind = CVC4::kind::REGEXP_OPT; }
+  | RERANGE_TOK      { $kind = CVC4::kind::REGEXP_RANGE; }
 
   // NOTE: Theory operators go here
   ;
@@ -1628,6 +1629,7 @@ REINTER_TOK : 're.itr';
 RESTAR_TOK : 're.*';
 REPLUS_TOK : 're.+';
 REOPT_TOK : 're.opt';
+RERANGE_TOK : 're.range';
 
 /**
  * A sequence of printable ASCII characters (except backslash) that starts
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index cbabc9542..c61a61940 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -9,9 +9,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief 
+ ** \brief
+ **
  **
- ** 
  **/
 
 #include "smt/model_postprocessor.h"
@@ -92,6 +92,9 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
     return n;
   }
   NodeBuilder<> b(n.getKind());
+  if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    b << n.getOperator();
+  }
   TypeNode::iterator t = asType.begin();
   for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) {
     Assert(t != asType.end());
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2505294e4..32d0d1703 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -883,16 +883,16 @@ void SmtEngine::setLogicInternal() throw() {
     }
   }
   // Turn on model-based arrays for QF_AX (unless models are enabled)
-  if(! options::arraysModelBased.wasSetByUser()) {
-    if (not d_logic.isQuantified() &&
-        d_logic.isTheoryEnabled(THEORY_ARRAY) &&
-        d_logic.isPure(THEORY_ARRAY) &&
-        !options::produceModels() &&
-        !options::checkModels()) {
-      Trace("smt") << "turning on model-based array solver" << endl;
-      options::arraysModelBased.set(true);
-    }
-  }
+  // if(! options::arraysModelBased.wasSetByUser()) {
+  //   if (not d_logic.isQuantified() &&
+  //       d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+  //       d_logic.isPure(THEORY_ARRAY) &&
+  //       !options::produceModels() &&
+  //       !options::checkModels()) {
+  //     Trace("smt") << "turning on model-based array solver" << endl;
+  //     options::arraysModelBased.set(true);
+  //   }
+  // }
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
   if(! options::repeatSimp.wasSetByUser()) {
     bool repeatSimp = !d_logic.isQuantified() &&
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index c827a8f07..686695f98 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -47,8 +47,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_infer_exp(c),
   d_notify( *this ),
   d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"),
-  d_selector_apps( c ),
   d_labels( c ),
+  d_selector_apps( c ),
   d_conflict( c, false ),
   d_collectTermsCache( c ){
 
@@ -83,6 +83,10 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( Node n, bool doMake
       if( n.getKind()==APPLY_CONSTRUCTOR ){
         ei->d_constructor = n;
       }
+      //add to selectors
+      NodeList* sel = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
+                                                               ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
+      d_selector_apps.insertDataFromContextMemory( n, sel );
       return ei;
     }else{
       return NULL;
@@ -118,6 +122,12 @@ void TheoryDatatypes::check(Effort e) {
   }
 
   if( e == EFFORT_FULL ) {
+    //check for cycles
+    checkCycles();
+    if( d_conflict ){
+      return;
+    }
+    //check for splits
     Debug("datatypes-split") << "Check for splits " << e << endl;
     bool addedFact = false;
     do {
@@ -159,20 +169,19 @@ 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
-                /*
+                // 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 );
                 Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n <<  endl;
@@ -196,6 +205,7 @@ void TheoryDatatypes::check(Effort e) {
       Trace("datatypes-debug") << "Flush pending facts..."  << std::endl;
       addedFact = !d_pending.empty() || !d_pending_merge.empty();
       flushPendingFacts();
+      /*
       if( !d_conflict ){
         if( options::dtRewriteErrorSel() ){
           bool innerAddedFact = false;
@@ -206,6 +216,7 @@ void TheoryDatatypes::check(Effort e) {
           }while( !d_conflict && innerAddedFact );
         }
       }
+      */
     }while( !d_conflict && addedFact );
     Trace("datatypes-debug") << "Finished. " << d_conflict << std::endl;
     if( !d_conflict ){
@@ -446,23 +457,23 @@ void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){
   Debug("datatypes-explain") << "Explain " << literal << std::endl;
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
+  std::vector<TNode> tassumptions;
   if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
-    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions);
   } else {
-    d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+    d_equalityEngine.explainPredicate(atom, polarity, tassumptions);
+  }
+  for( unsigned i=0; i<tassumptions.size(); i++ ){
+    if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
+      assumptions.push_back( tassumptions[i] );
+    }
   }
 }
 
 Node TheoryDatatypes::explain( TNode literal ){
   std::vector< TNode > assumptions;
   explain( literal, assumptions );
-  if( assumptions.empty() ){
-    return NodeManager::currentNM()->mkConst( true );
-  }else if( assumptions.size()==1 ){
-    return assumptions[0];
-  }else{
-    return NodeManager::currentNM()->mkNode( kind::AND, assumptions );
-  }
+  return mkAnd( assumptions );
 }
 
 /** Conflict when merging two constants */
@@ -472,7 +483,7 @@ void TheoryDatatypes::conflict(TNode a, TNode b){
   } else {
     d_conflictNode = explain( a.eqNode(b) );
   }
-  Debug("datatypes-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl;
+  Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl;
   d_out->conflict( d_conflictNode );
   d_conflict = true;
 }
@@ -508,9 +519,6 @@ 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();
@@ -518,12 +526,13 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         //check for clash
         Node cons1 = eqc1->d_constructor;
         Node cons2 = eqc2->d_constructor;
+        //if both have constructor, then either clash or unification
         if( !cons1.isNull() && !cons2.isNull() ){
           Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl;
           if( cons1.getOperator()!=cons2.getOperator() ){
             //check for clash
             d_conflictNode = explain( cons1.eqNode( cons2 ) );
-            Debug("datatypes-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
+            Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
             d_out->conflict( d_conflictNode );
             d_conflict = true;
             return;
@@ -547,30 +556,11 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         }
         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 );
+          addConstructor( eqc2->d_constructor.get(), eqc1, t1 );
+          if( d_conflict ){
+            return;
+          }
         }
       }else{
         Debug("datatypes-debug") << "No eqc info for " << t1 << ", must create" << std::endl;
@@ -578,10 +568,10 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         eqc1 = getOrMakeEqcInfo( t1, true );
         eqc1->d_inst.set( eqc2->d_inst );
         eqc1->d_constructor.set( eqc2->d_constructor );
+        eqc1->d_selectors.set( eqc2->d_selectors );
       }
 
 
-
       //merge labels
       NodeListMap::iterator lbl_i = d_labels.find( t2 );
       if( lbl_i != d_labels.end() ){
@@ -600,6 +590,14 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         eqc1->d_selectors = true;
         checkInst = true;
       }
+      NodeListMap::iterator sel_i = d_selector_apps.find( t2 );
+      if( sel_i != d_selector_apps.end() ){
+        Debug("datatypes-debug") << "Merge selectors from " << eqc2 << " " << t2 << std::endl;
+        NodeList* sel = (*sel_i).second;
+        for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
+          addSelector( *j, eqc1, t1, eqc2->d_constructor.get().isNull() );
+        }
+      }
       if( checkInst ){
         instantiate( eqc1, t1 );
         if( d_conflict ){
@@ -615,12 +613,16 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
       newRep = trep2;
     }
     bool result = d_cycle_check.addEdgeNode( oldRep, newRep );
-    d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
-    Debug("datatypes-cycles") << "DtCyc: Equal " << oldRep << " -> " << newRep << " " << d_hasSeenCycle.get() << endl;
-    if( d_hasSeenCycle.get() ){
+    //d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
+    Debug("datatypes-cycles") << "DtCyc: Equal " << oldRep << " -> " << newRep << " " << result << " " << d_hasSeenCycle.get() << endl;
+    if( result ){
       checkCycles();
       if( d_conflict ){
+        Debug("datatypes-cycles-find") << "Cycle found." << std::endl;
         return;
+      }else{
+        Debug("datatypes-cycles-find") << "WARNING : no cycle found." << std::endl;
+        d_cycle_check.debugPrint();
       }
     }
   }
@@ -677,108 +679,189 @@ 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 << " " << n << " " << eqc << std::endl;
-    bool tpolarity = t.getKind()!=NOT;
-    Node tt = ( t.getKind() == NOT ) ? t[0] : t;
-    int ttindex = Datatype::indexOf( tt.getOperator().toExpr() );
-    Node j, jt;
-    if( hasLabel( eqc, n ) ){
-      //if we already know the constructor type, check whether it is in conflict or redundant
-      int jtindex = getLabelIndex( eqc, n );
-      if( (jtindex==ttindex)!=tpolarity ){
+  Debug("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << 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() );
+  Node j, jt;
+  bool makeConflict = false;
+  if( hasLabel( eqc, n ) ){
+    //if we already know the constructor type, check whether it is in conflict or redundant
+    int jtindex = getLabelIndex( eqc, n );
+    if( (jtindex==ttindex)!=tpolarity ){
+      if( !eqc->d_constructor.get().isNull() ){
+        //conflict because equivalence class contains a constructor
+        std::vector< TNode > assumptions;
+        explain( t, assumptions );
+        explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions );
+        d_conflictNode = mkAnd( assumptions );
+        Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl;
+        d_out->conflict( d_conflictNode );
         d_conflict = true;
-        if( !eqc->d_constructor.get().isNull() ){
-          //conflict because equivalence class contains a constructor
-          std::vector< TNode > assumptions;
-          explain( t, assumptions );
-          explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions );
-          d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions );
-          Debug("datatypes-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl;
-          d_out->conflict( d_conflictNode );
-          return;
-        }else{
-          //conflict because the existing label is contradictory
-          j = getLabel( n );
-          jt = j;
-        }
-      }else{
         return;
+      }else{
+        makeConflict = true;
+        //conflict because the existing label is contradictory
+        j = getLabel( n );
+        jt = j;
       }
     }else{
-      //otherwise, scan list of labels
-      NodeListMap::iterator lbl_i = d_labels.find( n );
-      Assert( lbl_i != d_labels.end() );
-      NodeList* lbl = (*lbl_i).second;
-      for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
-        Assert( (*i).getKind()==NOT );
-        j = *i;
-        jt = j[0];
-        int jtindex = Datatype::indexOf( jt.getOperator().toExpr() );
-        if( jtindex==ttindex ){
-          if( tpolarity ){  //we are in conflict
-            d_conflict = true;
-            break;
-          }else{            //it is redundant
-            return;
-          }
+      return;
+    }
+  }else{
+    //otherwise, scan list of labels
+    NodeListMap::iterator lbl_i = d_labels.find( n );
+    Assert( lbl_i != d_labels.end() );
+    NodeList* lbl = (*lbl_i).second;
+    for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
+      Assert( (*i).getKind()==NOT );
+      j = *i;
+      jt = j[0];
+      int jtindex = Datatype::indexOf( jt.getOperator().toExpr() );
+      if( jtindex==ttindex ){
+        if( tpolarity ){  //we are in conflict
+          makeConflict = true;
+          break;
+        }else{            //it is redundant
+          return;
         }
       }
-      if( !d_conflict ){
-        Debug("datatypes-labels") << "Add to labels " << t << std::endl;
-        lbl->push_back( t );
-        const Datatype& dt = ((DatatypeType)(tt[0].getType()).toType()).getDatatype();
-        Debug("datatypes-labels") << "Labels at " << lbl->size() << " / " << dt.getNumConstructors() << std::endl;
-        if( tpolarity ){
-          instantiate( eqc, n );
-        }else{
-          //check if we have reached the maximum number of testers
-          // in this case, add the positive tester
-          if( lbl->size()==dt.getNumConstructors()-1 ){
-            std::vector< bool > pcons;
-            getPossibleCons( eqc, n, pcons );
-            int testerIndex = -1;
-            for( int i=0; i<(int)pcons.size(); i++ ) {
-              if( pcons[i] ){
-                testerIndex = i;
-                break;
-              }
+    }
+    if( !makeConflict ){
+      Debug("datatypes-labels") << "Add to labels " << t << std::endl;
+      lbl->push_back( t );
+      const Datatype& dt = ((DatatypeType)(tt[0].getType()).toType()).getDatatype();
+      Debug("datatypes-labels") << "Labels at " << lbl->size() << " / " << dt.getNumConstructors() << std::endl;
+      if( tpolarity ){
+        instantiate( eqc, n );
+      }else{
+        //check if we have reached the maximum number of testers
+        // in this case, add the positive tester
+        if( lbl->size()==dt.getNumConstructors()-1 ){
+          std::vector< bool > pcons;
+          getPossibleCons( eqc, n, pcons );
+          int testerIndex = -1;
+          for( int i=0; i<(int)pcons.size(); i++ ) {
+            if( pcons[i] ){
+              testerIndex = i;
+              break;
             }
-            Assert( testerIndex!=-1 );
-            //we must explain why each term in the set of testers for this equivalence class is equal
-            std::vector< Node > eq_terms;
-            NodeBuilder<> nb(kind::AND);
-            for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
-              nb << (*i);
-              if( std::find( eq_terms.begin(), eq_terms.end(), (*i)[0][0] )==eq_terms.end() ){
-                eq_terms.push_back( (*i)[0][0] );
-                if( (*i)[0][0]!=tt[0] ){
-                  nb << (*i)[0][0].eqNode( tt[0] );
-                }
+          }
+          Assert( testerIndex!=-1 );
+          //we must explain why each term in the set of testers for this equivalence class is equal
+          std::vector< Node > eq_terms;
+          NodeBuilder<> nb(kind::AND);
+          for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
+            nb << (*i);
+            if( std::find( eq_terms.begin(), eq_terms.end(), (*i)[0][0] )==eq_terms.end() ){
+              eq_terms.push_back( (*i)[0][0] );
+              if( (*i)[0][0]!=tt[0] ){
+                nb << (*i)[0][0].eqNode( tt[0] );
               }
             }
-            Node t_concl = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[unsigned(testerIndex)].getTester() ), tt[0] );
-            Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
-            d_pending.push_back( t_concl );
-            d_pending_exp[ t_concl ] = t_concl_exp;
-            Trace("datatypes-infer") << "DtInfer : " << t_concl << " by " << t_concl_exp << std::endl;
-            d_infer.push_back( t_concl );
-            d_infer_exp.push_back( t_concl_exp );
-            return;
           }
+          Node t_concl = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[unsigned(testerIndex)].getTester() ), tt[0] );
+          Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
+          d_pending.push_back( t_concl );
+          d_pending_exp[ t_concl ] = t_concl_exp;
+          Trace("datatypes-infer") << "DtInfer : " << t_concl << " by " << t_concl_exp << std::endl;
+          d_infer.push_back( t_concl );
+          d_infer_exp.push_back( t_concl_exp );
+          return;
         }
       }
     }
-    if( d_conflict ){
-      std::vector< TNode > assumptions;
-      explain( j, assumptions );
-      explain( t, assumptions );
-      explain( jt[0].eqNode( tt[0] ), assumptions );
-      d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions );
-      Debug("datatypes-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl;
-      d_out->conflict( d_conflictNode );
+  }
+  if( makeConflict ){
+    d_conflict = true;
+    Debug("datatypes-labels") << "Explain " << j << " " << t << std::endl;
+    std::vector< TNode > assumptions;
+    explain( j, assumptions );
+    explain( t, assumptions );
+    explain( jt[0].eqNode( tt[0] ), assumptions );
+    d_conflictNode = mkAnd( assumptions );
+    Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl;
+    d_out->conflict( d_conflictNode );
+  }
+}
+
+void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts ) {
+  Debug("datatypes-debug") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl;
+  //check to see if it is redundant
+  NodeListMap::iterator sel_i = d_selector_apps.find( n );
+  Assert( sel_i != d_selector_apps.end() );
+  if( sel_i != d_selector_apps.end() ){
+    NodeList* sel = (*sel_i).second;
+    for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
+      Node ss = *j;
+      if( s.getOperator()==ss.getOperator() ){
+        return;
+      }
+    }
+    //add it to the vector
+    sel->push_back( s );
+    eqc->d_selectors = true;
+  }
+  if( assertFacts && !eqc->d_constructor.get().isNull() ){
+    //conclude the collapsed merge
+    collapseSelector( s, eqc->d_constructor.get() );
+  }
+}
+
+void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
+  Debug("datatypes-debug") << "Add constructor : " << c << " to eqc(" << n << ")" << std::endl;
+  Assert( eqc->d_constructor.get().isNull() );
+  //check labels
+  NodeListMap::iterator lbl_i = d_labels.find( n );
+  if( lbl_i != d_labels.end() ){
+    size_t constructorIndex = Datatype::indexOf(c.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( c.eqNode( (*i)[0][0] ), assumptions );
+          d_conflictNode = mkAnd( assumptions );
+          Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
+          d_out->conflict( d_conflictNode );
+          d_conflict = true;
+          return;
+        }
+      }
     }
   }
+  //check selectors
+  NodeListMap::iterator sel_i = d_selector_apps.find( n );
+  if( sel_i != d_selector_apps.end() ){
+    NodeList* sel = (*sel_i).second;
+    for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
+      //collapse the selector
+      collapseSelector( *j, c );
+    }
+  }
+  eqc->d_constructor.set( c );
+}
+
+void TheoryDatatypes::collapseSelector( Node s, Node c ) {
+  Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, s.getOperator(), c );
+  Node rr = Rewriter::rewrite( r );
+  //if( r!=rr ){
+    //Node eq_exp = NodeManager::currentNM()->mkConst(true);
+    //Node eq = r.getType().isBoolean() ? r.iffNode( rr ) : r.eqNode( rr );
+  if( s!=rr ){
+    Node eq_exp = c.eqNode( s[0] );
+    Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr );
+
+
+    d_pending.push_back( eq );
+    d_pending_exp[ eq ] = eq_exp;
+    Trace("datatypes-infer") << "DtInfer : " << eq << " by " << eq_exp << " (collapse selector)" << std::endl;
+    d_infer.push_back( eq );
+    d_infer_exp.push_back( eq_exp );
+  }
 }
 
 EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){
@@ -800,14 +883,15 @@ void TheoryDatatypes::computeCareGraph(){
 }
 
 void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
+  Trace("dt-cmi") << "Datatypes : Collect model info " << d_equalityEngine.consistent() << std::endl;
   Trace("dt-model") << std::endl;
   printModelDebug( "dt-model" );
+  Trace("dt-model") << std::endl;
   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;
@@ -816,90 +900,139 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
     //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() );
-        }
+      if( !ei->d_constructor.get().isNull() ){
+        cons.push_back( ei->d_constructor.get() );
       }
     }
     ++eqccs_i;
   }
 
   //must choose proper representatives
+  std::vector< Node > nodes;
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
     //for all equivalence classes that are datatypes
     if( DatatypesRewriter::isTermDatatype( eqc ) ){
       EqcInfo* ei = getOrMakeEqcInfo( eqc );
-      if( ei ){
-        if( !ei->d_constructor.get().isNull() ){
-          //specify that we should use the constructor as the representative
-          //m->assertRepresentative( ei->d_constructor.get() );
-        }else{
-          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] << " ";
+      if( !ei->d_constructor.get().isNull() ){
+        //specify that we should use the constructor as the representative
+        //m->assertRepresentative( ei->d_constructor.get() );
+      }else{
+        nodes.push_back( eqc );
+      }
+    }
+    ++eqcs_i;
+  }
+  unsigned index = 0;
+  while( index<nodes.size() ){
+    Node eqc = nodes[index];
+    Node neqc;
+    if( !d_equalityEngine.hasTerm( eqc ) ){
+      Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc << std::endl;
+      Trace("dt-cmi") << "   Type : " << eqc.getType() << std::endl;
+      //can assign arbitrary term
+      TypeEnumerator te(eqc.getType());
+      bool success;
+      do{
+        success = true;
+        Assert( !te.isFinished() );
+        neqc = *te;
+        Trace("dt-cmi-debug") << "Try " << neqc << " ... " << std::endl;
+        ++te;
+        for( unsigned i=0; i<cons.size(); i++ ){
+          //check if it is modulo equality the same
+          if( cons[i].getOperator()==neqc.getOperator() ){
+            bool diff = false;
+            for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
+              if( !m->areEqual( cons[i][j], neqc[j] ) ){
+                diff = true;
+                break;
+              }
+            }
+            if( !diff ){
+              Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl;
+              success = false;
+              break;
+            }
           }
-          Trace("dt-cmi") << std::endl;
-
-          if( tes.find( eqc.getType() )==tes.end() ){
-            tes[eqc.getType()]=vec.size();
-            vec.push_back( TypeEnumerator( eqc.getType() ) );
+        }
+      }while( !success );
+    }else{
+      Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl;
+      Trace("dt-cmi") << "   Type : " << eqc.getType() << std::endl;
+      EqcInfo* ei = getOrMakeEqcInfo( eqc );
+      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()]];
+        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;
+              }
+            }
           }
-          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 );
+      */
+      const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype();
+      for( unsigned r=0; r<2; r++ ){
+        if( neqc.isNull() ){
+          for( unsigned i=0; i<pcons.size(); i++ ){
+            if( pcons[i] && (r==1)==dt[ i ].isFinite() ){
+              neqc = getInstantiateCons( eqc, dt, i, false, false );
+              for( unsigned j=0; j<neqc.getNumChildren(); j++ ){
+                if( !d_equalityEngine.hasTerm( neqc[j] ) && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
+                  nodes.push_back( neqc[j] );
                 }
               }
-            }else{
-              Trace("dt-cmi-debug") << "...Not consistent with labels" << std::endl;
-              success = false;
+              break;
             }
-          }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;
-        Trace("model-warn") << "   Type : " << eqc.getType() << std::endl;
       }
     }
-    ++eqcs_i;
+    Assert( !neqc.isNull() );
+    Trace("dt-cmi") << "Assign : " << neqc << std::endl;
+    m->assertEquality( eqc, neqc, true );
+    //m->assertRepresentative( neqc );
+    cons.push_back( neqc );
+    ++index;
   }
+
 }
 
 
@@ -912,27 +1045,29 @@ void TheoryDatatypes::collectTerms( Node n ) {
     if( n.getKind() == APPLY_CONSTRUCTOR ){
       //we must take into account subterm relation when checking for cycles
       for( int i=0; i<(int)n.getNumChildren(); i++ ) {
-        Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << endl;
         bool result = d_cycle_check.addEdgeNode( n, n[i] );
+        Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << " " << result << endl;
+        if( result && !d_hasSeenCycle.get() ){
+          Debug("datatypes-cycles") << "FOUND CYCLE" << std::endl;
+        }
         d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
+        //Node r = getRepresentative( n[i] );
+        //EqcInfo* eqc = getOrMakeEqcInfo( r, true );
+        //eqc->d_selectors = true;
       }
     }else if( n.getKind() == APPLY_SELECTOR ){
-      if( d_selector_apps.find( n )==d_selector_apps.end() ){
-        d_selector_apps[n] = false;
-        //we must also record which selectors exist
-        Debug("datatypes") << "  Found selector " << n << endl;
-        if (n.getType().isBoolean()) {
-          d_equalityEngine.addTriggerPredicate( n );
-        }else{
-          d_equalityEngine.addTerm( n );
-        }
-        Node rep = getRepresentative( n[0] );
-        EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
-        if( !eqc->d_selectors ){
-          eqc->d_selectors = true;
-          instantiate( eqc, rep );
-        }
+      //we must also record which selectors exist
+      Debug("datatypes") << "  Found selector " << n << endl;
+      if (n.getType().isBoolean()) {
+        d_equalityEngine.addTriggerPredicate( n );
+      }else{
+        d_equalityEngine.addTerm( n );
       }
+      Node rep = getRepresentative( n[0] );
+      //record it in the selectors
+      EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
+      //add it to the eqc info
+      addSelector( n, eqc, rep );
     }
   }
 }
@@ -941,7 +1076,7 @@ void TheoryDatatypes::processNewTerm( Node n ){
   Trace("dt-terms") << "Created term : " << n << std::endl;
   //see if it is rewritten to be something different
   Node rn = Rewriter::rewrite( n );
-  if( rn!=n ){
+  if( rn!=n && !areEqual( rn, n ) ){
     Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n );
     d_pending.push_back( eq );
     d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true );
@@ -950,20 +1085,35 @@ void TheoryDatatypes::processNewTerm( Node n ){
   }
 }
 
-Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index ){
+Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar, bool isActive ){
   //if( !d_inst_map[n][index].isNull() ){
   //  return d_inst_map[n][index];
   //}else{
     //add constructor to equivalence class
+    Type tspec;
+    if( dt.isParametric() ){
+      tspec = dt[index].getSpecializedConstructorType(n.getType().toType());
+    }
     std::vector< Node > children;
     children.push_back( Node::fromExpr( dt[index].getConstructor() ) );
     for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){
       Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[index][i].getSelector() ), n );
+      if( mkVar ){
+        TypeNode tn = nc.getType();
+        if( dt.isParametric() ){
+          tn = TypeNode::fromType( tspec )[i];
+        }
+        nc = NodeManager::currentNM()->mkSkolem( "m_$$", tn, "created during model gen" );
+      }
       children.push_back( nc );
-      processNewTerm( nc );
+      if( isActive ){
+        processNewTerm( nc );
+      }
     }
     Node n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
-    collectTerms( n_ic );
+    if( isActive ){
+      collectTerms( n_ic );
+    }
     //add type ascription for ambiguous constructor types
     if(!n_ic.getType().isComparableTo(n.getType())) {
       Assert( dt.isParametric() );
@@ -977,72 +1127,11 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index
       Assert( n_ic.getType()==n.getType() );
     }
     n_ic = Rewriter::rewrite( n_ic );
+    Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl;
     //d_inst_map[n][index] = n_ic;
     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 ){
-    if( !(*it).second ){
-      Node n = getRepresentative( (*it).first[0] );
-      Trace("datatypes-collapse") << "Datatypes collapse selector? : " << n << std::endl;
-      EqcInfo* ei = getOrMakeEqcInfo( n, true );
-      if( ei ){
-        if( !ei->d_constructor.get().isNull() ){
-          Node op = (*it).first.getOperator();
-          Node cons = ei->d_constructor;
-          Node sn = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, op, cons );
-          Node s = Rewriter::rewrite( sn );
-          if( sn!=s ){
-            Node eq = s.getType().isBoolean() ? s.iffNode( sn ) : s.eqNode( sn );
-            d_pending.push_back( eq );
-            d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true );
-            Trace("datatypes-infer") << "DtInfer : " << eq << ", by rewrite" << std::endl;
-            d_infer.push_back( eq );
-          }
-          d_selector_apps[ (*it).first ] = true;
-        }else{
-          Trace("datatypes-collapse") << "No constructor." << std::endl;
-        }
-      }else{
-        Trace("datatypes-collapse") << "No e info." << std::endl;
-      }
-    }
-  }
-}
 
 void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
   //add constructor to equivalence class if not done so already
@@ -1059,21 +1148,21 @@ 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() ){
-      //instantiate this equivalence class
-      eqc->d_inst = true;
-      Node tt_cons = getInstantiateCons( tt, dt, index );
-      Node eq;
-      if( tt!=tt_cons ){
-        eq = tt.eqNode( tt_cons );
-        Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl;
-        d_pending.push_back( eq );
-        d_pending_exp[ eq ] = exp;
-        Trace("datatypes-infer") << "DtInfer : " << eq << " by " << exp << std::endl;
-        //eqc->d_inst.set( eq );
-        d_infer.push_back( eq );
-        d_infer_exp.push_back( exp );
-      }
+    //if( eqc->d_selectors || dt[ index ].isFinite() ){ // || mustSpecifyAssignment()
+    //instantiate this equivalence class
+    eqc->d_inst = true;
+    Node tt_cons = getInstantiateCons( tt, dt, index );
+    Node eq;
+    if( tt!=tt_cons ){
+      eq = tt.eqNode( tt_cons );
+      Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl;
+      d_pending.push_back( eq );
+      d_pending_exp[ eq ] = exp;
+      Trace("datatypes-infer") << "DtInfer : " << eq << " by " << exp << std::endl;
+      //eqc->d_inst.set( eq );
+      d_infer.push_back( eq );
+      d_infer_exp.push_back( exp );
+    }
     //}
     //else{
     //  Debug("datatypes-inst") << "Do not instantiate" << std::endl;
@@ -1086,26 +1175,34 @@ void TheoryDatatypes::checkCycles() {
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
-    map< Node, bool > visited;
-    std::vector< TNode > expl;
-    if( searchForCycle( eqc, eqc, visited, expl ) ) {
-      Assert( expl.size()>0 );
-      if( expl.size() == 1 ){
-        d_conflictNode = expl[ 0 ];
-      }else{
-        d_conflictNode = NodeManager::currentNM()->mkNode( AND, expl );
+    if( DatatypesRewriter::isTermDatatype( eqc ) ) {
+      map< Node, bool > visited;
+      std::vector< TNode > expl;
+      Node cn = searchForCycle( eqc, eqc, visited, expl );
+      //if we discovered a different cycle while searching this one
+      if( !cn.isNull() && cn!=eqc ){
+        visited.clear();
+        expl.clear();
+        Node prev = cn;
+        cn = searchForCycle( cn, cn, visited, expl );
+        Assert( prev==cn );
+      }
+
+      if( !cn.isNull() ) {
+        Assert( expl.size()>0 );
+        d_conflictNode = mkAnd( expl );
+        Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl;
+        d_out->conflict( d_conflictNode );
+        d_conflict = true;
+        return;
       }
-      Debug("datatypes-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl;
-      d_out->conflict( d_conflictNode );
-      d_conflict = true;
-      return;
     }
     ++eqcs_i;
   }
 }
 
 //postcondition: if cycle detected, explanation is why n is a subterm of on
-bool TheoryDatatypes::searchForCycle( Node n, Node on,
+Node TheoryDatatypes::searchForCycle( Node n, Node on,
                                       map< Node, bool >& visited,
                                       std::vector< TNode >& explanation, bool firstTime ) {
   Debug("datatypes-cycle-check") << "Search for cycle " << n << " " << on << endl;
@@ -1116,19 +1213,20 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on,
     if( nn==on ){
       Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, nn );
       explain( lit, explanation );
-      return true;
+      return on;
     }
   }else{
     nn = n;
   }
   if( visited.find( nn ) == visited.end() ) {
     visited[nn] = true;
-    EqcInfo* eqc = getOrMakeEqcInfo( nn );
+    EqcInfo* eqc = getOrMakeEqcInfo( nn, false );
     if( eqc ){
       Node ncons = eqc->d_constructor.get();
       if( !ncons.isNull() ) {
         for( int i=0; i<(int)ncons.getNumChildren(); i++ ) {
-          if( searchForCycle( ncons[i], on, visited, explanation, false ) ) {
+          Node cn = searchForCycle( ncons[i], on, visited, explanation, false );
+          if( cn==on ) {
             if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){
               Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl;
             }
@@ -1137,13 +1235,18 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on,
               Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, ncons );
               explain( lit, explanation );
             }
-            return true;
+            return on;
+          }else if( !cn.isNull() ){
+            return cn;
           }
         }
       }
     }
+    visited.erase( nn );
+    return Node::null();
+  }else{
+    return nn;
   }
-  return false;
 }
 
 bool TheoryDatatypes::mustSpecifyAssignment(){
@@ -1255,30 +1358,45 @@ void TheoryDatatypes::printModelDebug( const char* c ){
         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 ) << "   Constructor : ";
+          if( !ei->d_constructor.get().isNull() ){
+            Trace( c )<< ei->d_constructor.get();
+          }
+          Trace( c ) << std::endl << "   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 ) << "   Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl;
+          Trace( c ) << std::endl;
+          Trace( c ) << "   Selectors : " << ( ei->d_selectors ? "yes, " : "no " );
+          NodeListMap::iterator sel_i = d_selector_apps.find( eqc );
+          if( sel_i != d_selector_apps.end() ){
+            NodeList* sel = (*sel_i).second;
+            for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){
+              Trace( c ) << *j << " ";
+            }
+          }
+          Trace( c ) << std::endl;
         }
       }
     }
     ++eqcs_i;
   }
 }
+
+Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) {
+  if( assumptions.empty() ){
+    return NodeManager::currentNM()->mkConst( true );
+  }else if( assumptions.size()==1 ){
+    return assumptions[0];
+  }else{
+    return NodeManager::currentNM()->mkNode( AND, assumptions );
+  }
+}
\ No newline at end of file
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 203782a79..4f061507c 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -51,6 +51,8 @@ private:
   NodeList d_infer;
   NodeList d_infer_exp;
 
+  /** mkAnd */
+  Node mkAnd( std::vector< TNode >& assumptions );
 private:
   //notification class for equality engine
   class NotifyClass : public eq::EqualityEngineNotify {
@@ -137,7 +139,7 @@ private:
   /** information necessary for equivalence classes */
   std::map< Node, EqcInfo* > d_eqc_info;
   /** selector applications */
-  BoolMap d_selector_apps;
+  //BoolMap d_selector_apps;
   /** map from nodes to their instantiated equivalent for each constructor type */
   std::map< Node, std::map< int, Node > > d_inst_map;
   /** which instantiation lemmas we have sent */
@@ -152,6 +154,8 @@ private:
    *   is_[constructor_(n+1)]( t ), each of which is a unique tester.
   */
   NodeListMap d_labels;
+  /** selector apps for eqch equivalence class */
+  NodeListMap d_selector_apps;
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
   /** The conflict node */
@@ -215,25 +219,27 @@ public:
 private:
   /** add tester to equivalence class info */
   void addTester( Node t, EqcInfo* eqc, Node n );
+  /** add selector to equivalence class info */
+  void addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts = true );
+  /** add constructor */
+  void addConstructor( Node c, EqcInfo* eqc, Node n );
   /** merge the equivalence class info of t1 and t2 */
   void merge( Node t1, Node t2 );
+  /** collapse selector, s is of the form sel( n ) where n = c */
+  void collapseSelector( Node s, Node c );
   /** for checking if cycles exist */
   void checkCycles();
-  bool searchForCycle( Node n, Node on,
+  Node searchForCycle( Node n, Node on,
                        std::map< Node, bool >& visited,
                        std::vector< TNode >& explanation, bool firstTime = true );
   /** collect terms */
   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 );
+  Node getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar = false, bool isActive = true );
   /** process new term that was created internally */
   void processNewTerm( Node n );
   /** check instantiate */
   void instantiate( EqcInfo* eqc, Node n );
-  /** collapse selectors */
-  void collapseSelectors();
   /** must specify model
     *  This returns true when the datatypes theory is expected to specify the constructor
     *  type for all equivalence classes.
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 840c8bc3a..393f3883c 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -28,17 +28,22 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 
 TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels) :
-  d_substitutions(c, false), d_equalityEngine(c, name), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
+  d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
+
+  d_eeContext = new context::Context();
+  d_equalityEngine = new eq::EqualityEngine(d_eeContext, name);
+
   // The kinds we are treating as function application in congruence
-  d_equalityEngine.addFunctionKind(kind::APPLY_UF);
-  d_equalityEngine.addFunctionKind(kind::SELECT);
-  // d_equalityEngine.addFunctionKind(kind::STORE);
-  d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
-  d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR);
-  d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
+  d_equalityEngine->addFunctionKind(kind::APPLY_UF);
+  d_equalityEngine->addFunctionKind(kind::SELECT);
+  // d_equalityEngine->addFunctionKind(kind::STORE);
+  d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
+  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR);
+  d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
+  d_eeContext->push();
 }
 
 void TheoryModel::reset(){
@@ -46,6 +51,8 @@ void TheoryModel::reset(){
   d_rep_set.clear();
   d_uf_terms.clear();
   d_uf_models.clear();
+  d_eeContext->pop();
+  d_eeContext->push();
 }
 
 Node TheoryModel::getValue(TNode n) const {
@@ -98,7 +105,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
     // no good.  Instead, return the quantifier itself.  If we're in
     // checkModel(), and the quantifier actually matters, we'll get an
     // assert-fail since the quantifier isn't a constant.
-    if(!d_equalityEngine.hasTerm(Rewriter::rewrite(n))) {
+    if(!d_equalityEngine->hasTerm(Rewriter::rewrite(n))) {
       return n;
     } else {
       n = Rewriter::rewrite(n);
@@ -158,13 +165,13 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
       return val;
     }
 
-    if (!d_equalityEngine.hasTerm(n)) {
+    if (!d_equalityEngine->hasTerm(n)) {
       // Unknown term - return first enumerated value for this type
       TypeEnumerator te(n.getType());
       return *te;
     }
   }
-  Node val = d_equalityEngine.getRepresentative(n);
+  Node val = d_equalityEngine->getRepresentative(n);
   Assert(d_reps.find(val) != d_reps.end());
   std::map< Node, Node >::const_iterator it = d_reps.find( val );
   if( it!=d_reps.end() ){
@@ -237,7 +244,7 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
 
 /** add term */
 void TheoryModel::addTerm(TNode n ){
-  Assert(d_equalityEngine.hasTerm(n));
+  Assert(d_equalityEngine->hasTerm(n));
   //must collect UF terms
   if (n.getKind()==APPLY_UF) {
     Node op = n.getOperator();
@@ -254,8 +261,8 @@ void TheoryModel::assertEquality(TNode a, TNode b, bool polarity ){
     return;
   }
   Trace("model-builder-assertions") << "(assert " << (polarity ? "(= " : "(not (= ") << a << " " << b << (polarity ? "));" : ")));") << endl;
-  d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() );
-  Assert(d_equalityEngine.consistent());
+  d_equalityEngine->assertEquality( a.eqNode(b), polarity, Node::null() );
+  Assert(d_equalityEngine->consistent());
 }
 
 /** assert predicate */
@@ -266,11 +273,11 @@ void TheoryModel::assertPredicate(TNode a, bool polarity ){
   }
   if (a.getKind() == EQUAL) {
     Trace("model-builder-assertions") << "(assert " << (polarity ? " " : "(not ") << a << (polarity ? ");" : "));") << endl;
-    d_equalityEngine.assertEquality( a, polarity, Node::null() );
+    d_equalityEngine->assertEquality( a, polarity, Node::null() );
   } else {
     Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl;
-    d_equalityEngine.assertPredicate( a, polarity, Node::null() );
-    Assert(d_equalityEngine.consistent());
+    d_equalityEngine->assertPredicate( a, polarity, Node::null() );
+    Assert(d_equalityEngine->consistent());
   }
 }
 
@@ -309,8 +316,8 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>*
           }
           else {
             Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl;
-            d_equalityEngine.mergePredicates(*eqc_i, rep, Node::null());
-            Assert(d_equalityEngine.consistent());
+            d_equalityEngine->mergePredicates(*eqc_i, rep, Node::null());
+            Assert(d_equalityEngine->consistent());
           }
         }
       } else {
@@ -334,13 +341,13 @@ void TheoryModel::assertRepresentative(TNode n )
 
 bool TheoryModel::hasTerm(TNode a)
 {
-  return d_equalityEngine.hasTerm( a );
+  return d_equalityEngine->hasTerm( a );
 }
 
 Node TheoryModel::getRepresentative(TNode a)
 {
-  if( d_equalityEngine.hasTerm( a ) ){
-    Node r = d_equalityEngine.getRepresentative( a );
+  if( d_equalityEngine->hasTerm( a ) ){
+    Node r = d_equalityEngine->getRepresentative( a );
     if( d_reps.find( r )!=d_reps.end() ){
       return d_reps[ r ];
     }else{
@@ -355,8 +362,8 @@ bool TheoryModel::areEqual(TNode a, TNode b)
 {
   if( a==b ){
     return true;
-  }else if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
-    return d_equalityEngine.areEqual( a, b );
+  }else if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){
+    return d_equalityEngine->areEqual( a, b );
   }else{
     return false;
   }
@@ -364,8 +371,8 @@ bool TheoryModel::areEqual(TNode a, TNode b)
 
 bool TheoryModel::areDisequal(TNode a, TNode b)
 {
-  if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
-    return d_equalityEngine.areDisequal( a, b, false );
+  if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){
+    return d_equalityEngine->areDisequal( a, b, false );
   }else{
     return false;
   }
@@ -422,7 +429,7 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac
     return;
   }
   if (isAssignable(n)) {
-    tm->d_equalityEngine.addTerm(n);
+    tm->d_equalityEngine->addTerm(n);
   }
   for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
     checkTerms(*child_it, tm, cache);
@@ -448,11 +455,11 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   d_te->collectModelInfo(tm, fullModel);
 
   // Loop through all terms and make sure that assignable sub-terms are in the equality engine
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_equalityEngine );
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine );
   {
     NodeSet cache;
     for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
-      eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i), &tm->d_equalityEngine);
+      eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i),tm->d_equalityEngine);
       for ( ; !eqc_i.isFinished(); ++eqc_i) {
         checkTerms(*eqc_i, tm, cache);
       }
@@ -465,20 +472,20 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   std::map< Node, Node > assertedReps, constantReps;
   TypeSet typeConstSet, typeRepSet, typeNoRepSet;
   std::set< TypeNode > allTypes;
-  eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine);
+  eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
   for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
 
     // eqc is the equivalence class representative
     Node eqc = (*eqcs_i);
     Trace("model-builder") << "Processing EC: " << eqc << endl;
-    Assert(tm->d_equalityEngine.getRepresentative(eqc) == eqc);
+    Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc);
     TypeNode eqct = eqc.getType();
     Assert(assertedReps.find(eqc) == assertedReps.end());
     Assert(constantReps.find(eqc) == constantReps.end());
 
     // Loop through terms in this EC
     Node rep, const_rep;
-    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &tm->d_equalityEngine);
+    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
     for ( ; !eqc_i.isFinished(); ++eqc_i) {
       Node n = *eqc_i;
       Trace("model-builder") << "  Processing Term: " << n << endl;
@@ -556,7 +563,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
             assignable = false;
             evaluable = false;
             evaluated = false;
-            eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine);
+            eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine);
             for ( ; !eqc_i.isFinished(); ++eqc_i) {
               Node n = *eqc_i;
               if (isAssignable(n)) {
@@ -653,7 +660,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       for (i = noRepSet.begin(); i != noRepSet.end(); ) {
         i2 = i;
         ++i;
-        eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine);
+        eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine);
         assignable = false;
         evaluable = false;
         for ( ; !eqc_i.isFinished(); ++eqc_i) {
@@ -744,7 +751,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
 #ifdef CVC4_ASSERTIONS
   if (fullModel) {
     // Check that every term evaluates to its representative in the model
-    for (eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) {
+    for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) {
       // eqc is the equivalence class representative
       Node eqc = (*eqcs_i);
       Node rep;
@@ -757,7 +764,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
         Assert(itMap != constantReps.end());
         rep = itMap->second;
       }
-      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &tm->d_equalityEngine);
+      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
       for ( ; !eqc_i.isFinished(); ++eqc_i) {
         Node n = *eqc_i;
         static int repCheckInstance = 0;
@@ -795,18 +802,19 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node
     bool childrenConst = true;
     for (size_t i=0; i < r.getNumChildren(); ++i) {
       Node ri = r[i];
+      bool recurse = true;
       if (!ri.isConst()) {
-        if (m->d_equalityEngine.hasTerm(ri)) {
-          ri = m->d_equalityEngine.getRepresentative(ri);
-          itMap = constantReps.find(ri);
+        if (m->d_equalityEngine->hasTerm(ri)) {
+          itMap = constantReps.find(m->d_equalityEngine->getRepresentative(ri));
           if (itMap != constantReps.end()) {
             ri = (*itMap).second;
+	    recurse = false;
           }
-          else if (evalOnly) {
-            ri = normalize(m, r[i], constantReps, evalOnly);
-          }
+          else if (!evalOnly) {
+	    recurse = false;
+	  }
         }
-        else {
+        if (recurse) {
           ri = normalize(m, ri, constantReps, evalOnly);
         }
         if (!ri.isConst()) {
diff --git a/src/theory/model.h b/src/theory/model.h
index 03a641df4..a18d66ab0 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -42,8 +42,11 @@ protected:
 public:
   TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
   virtual ~TheoryModel(){}
+
+  /** special local context for our equalityEngine so we can clear it independently of search context */
+  context::Context* d_eeContext;
   /** equality engine containing all known equalities/disequalities */
-  eq::EqualityEngine d_equalityEngine;
+  eq::EqualityEngine* d_equalityEngine;
   /** map of representatives of equality engine to used representatives in representative set */
   std::map< Node, Node > d_reps;
   /** stores set of representatives for each type */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c14ee01ce..07b0ebea3 100755
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -283,32 +283,32 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
     d_temp_inst_debug[f]++;
     d_total_inst_count_debug++;
     Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
-    uint64_t maxInstLevel = 0;
-    for( int i=0; i<(int)terms.size(); i++ ){
-      if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){
-        Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
-        for( int i=0; i<(int)terms.size(); i++ ){
-          Debug("inst") << "   " << terms[i] << std::endl;
-        }
-        Unreachable("Bad instantiation");
-      }else{
-        Trace("inst") << "   " << terms[i];
-        //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute());
-        Trace("inst") << std::endl;
-        if( terms[i].hasAttribute(InstLevelAttribute()) ){
-          if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
-            maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
+    //uint64_t maxInstLevel = 0;
+    if( options::cbqi() ){
+      for( int i=0; i<(int)terms.size(); i++ ){
+        if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){
+          Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
+          for( int i=0; i<(int)terms.size(); i++ ){
+            Debug("inst") << "   " << terms[i] << std::endl;
           }
+          Unreachable("Bad instantiation");
         }else{
-          setInstantiationLevelAttr( terms[i], 0 );
+          Trace("inst") << "   " << terms[i];
+          //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute());
+          Trace("inst") << std::endl;
+          //if( terms[i].hasAttribute(InstLevelAttribute()) ){
+            //if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
+            //  maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
+            //}
+          //}else{
+            //setInstantiationLevelAttr( terms[i], 0 );
+          //}
         }
       }
     }
     Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
-    setInstantiationLevelAttr( body, maxInstLevel+1 );
+    //setInstantiationLevelAttr( body, maxInstLevel+1 );
     ++(d_statistics.d_instantiations);
-    d_statistics.d_total_inst_var += (int)terms.size();
-    d_statistics.d_max_instantiation_level.maxAssign( maxInstLevel+1 );
     return true;
   }else{
     ++(d_statistics.d_inst_duplicate);
@@ -326,10 +326,32 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
   }
 }
 
+Node QuantifiersEngine::doSubstitute( Node n, std::vector< Node >& terms ){
+  if( n.getKind()==INST_CONSTANT ){
+    Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
+    return terms[n.getAttribute(InstVarNumAttribute())];
+  }else if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
+    Debug("check-inst") << "No inst const attr : " << n << std::endl;
+    return n;
+  }else{
+    Debug("check-inst") << "Recurse on : " << n << std::endl;
+    std::vector< Node > cc;
+    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      cc.push_back( n.getOperator() );
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      cc.push_back( doSubstitute( n[i], terms ) );
+    }
+    return NodeManager::currentNM()->mkNode( n.getKind(), cc );
+  }
+}
+
+
 Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
-  Node body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+  Node body;
   //process partial instantiation if necessary
   if( d_term_db->d_vars[f].size()!=vars.size() ){
+    body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
     std::vector< Node > uninst_vars;
     //doing a partial instantiation, must add quantifier for all uninstantiated variables
     for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
@@ -341,6 +363,16 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std
     body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
     Trace("partial-inst") << "Partial instantiation : " << f << std::endl;
     Trace("partial-inst") << "                      : " << body << std::endl;
+  }else{
+    //do optimized version
+    Node icb = d_term_db->getInstConstantBody( f );
+    body = doSubstitute( icb, terms );
+    if( Debug.isOn("check-inst") ){
+      Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+      if( body!=body2 ){
+        Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
+      }
+    }
   }
   return body;
 }
@@ -440,11 +472,7 @@ bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
   n = Rewriter::rewrite( n );
   Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() );
   if( addLemma( lem ) ){
-    ++(d_statistics.d_splits);
     Debug("inst") << "*** Add split " << n<< std::endl;
-    //if( reqPhase ){
-    //  d_curr_out->requirePhase( n, reqPhasePol );
-    //}
     return true;
   }
   return false;
@@ -503,12 +531,8 @@ QuantifiersEngine::Statistics::Statistics():
   d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
   d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
   d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
-  d_max_instantiation_level("QuantifiersEngine::Max_Instantiation_Level", 0),
-  d_splits("QuantifiersEngine::Total_Splits", 0),
-  d_total_inst_var("QuantifiersEngine::Vars_Inst", 0),
-  d_total_inst_var_unspec("QuantifiersEngine::Vars_Inst_Unspecified", 0),
-  d_inst_unspec("QuantifiersEngine::Unspecified_Inst", 0),
   d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
+  d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
   d_lit_phase_req("QuantifiersEngine::lit_phase_req", 0),
   d_lit_phase_nreq("QuantifiersEngine::lit_phase_nreq", 0),
   d_triggers("QuantifiersEngine::Triggers", 0),
@@ -528,12 +552,8 @@ QuantifiersEngine::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_instantiation_rounds);
   StatisticsRegistry::registerStat(&d_instantiation_rounds_lc);
   StatisticsRegistry::registerStat(&d_instantiations);
-  StatisticsRegistry::registerStat(&d_max_instantiation_level);
-  StatisticsRegistry::registerStat(&d_splits);
-  StatisticsRegistry::registerStat(&d_total_inst_var);
-  StatisticsRegistry::registerStat(&d_total_inst_var_unspec);
-  StatisticsRegistry::registerStat(&d_inst_unspec);
   StatisticsRegistry::registerStat(&d_inst_duplicate);
+  StatisticsRegistry::registerStat(&d_inst_duplicate_eq);
   StatisticsRegistry::registerStat(&d_lit_phase_req);
   StatisticsRegistry::registerStat(&d_lit_phase_nreq);
   StatisticsRegistry::registerStat(&d_triggers);
@@ -555,12 +575,8 @@ QuantifiersEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_instantiation_rounds);
   StatisticsRegistry::unregisterStat(&d_instantiation_rounds_lc);
   StatisticsRegistry::unregisterStat(&d_instantiations);
-  StatisticsRegistry::unregisterStat(&d_max_instantiation_level);
-  StatisticsRegistry::unregisterStat(&d_splits);
-  StatisticsRegistry::unregisterStat(&d_total_inst_var);
-  StatisticsRegistry::unregisterStat(&d_total_inst_var_unspec);
-  StatisticsRegistry::unregisterStat(&d_inst_unspec);
   StatisticsRegistry::unregisterStat(&d_inst_duplicate);
+  StatisticsRegistry::unregisterStat(&d_inst_duplicate_eq);
   StatisticsRegistry::unregisterStat(&d_lit_phase_req);
   StatisticsRegistry::unregisterStat(&d_lit_phase_nreq);
   StatisticsRegistry::unregisterStat(&d_triggers);
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 8f645afe7..6de13ff3c 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -111,7 +111,7 @@ private:
   /** list of all quantifiers seen */
   std::vector< Node > d_quants;
   /** list of all lemmas produced */
-  std::map< Node, bool > d_lemmas_produced;
+  //std::map< Node, bool > d_lemmas_produced;
   BoolMap d_lemmas_produced_c;
   /** lemmas waiting */
   std::vector< Node > d_lemmas_waiting;
@@ -187,6 +187,8 @@ private:
   bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
   /** set instantiation level attr */
   void setInstantiationLevelAttr( Node n, uint64_t level );
+  /** do substitution */
+  Node doSubstitute( Node n, std::vector< Node >& terms );
 public:
   /** get instantiation */
   Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
@@ -234,12 +236,8 @@ public:
     IntStat d_instantiation_rounds;
     IntStat d_instantiation_rounds_lc;
     IntStat d_instantiations;
-    IntStat d_max_instantiation_level;
-    IntStat d_splits;
-    IntStat d_total_inst_var;
-    IntStat d_total_inst_var_unspec;
-    IntStat d_inst_unspec;
     IntStat d_inst_duplicate;
+    IntStat d_inst_duplicate_eq;
     IntStat d_lit_phase_req;
     IntStat d_lit_phase_nreq;
     IntStat d_triggers;
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index fe7b9b3d9..e325708c2 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -3,7 +3,7 @@
 
 theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h"
 
-properties check parametric propagate
+properties check parametric propagate getNextDecisionRequest
 
 rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_strings_rewriter.h"
 
@@ -70,6 +70,7 @@ operator REGEXP_INTER 2: "regexp intersection"
 operator REGEXP_STAR 1 "regexp *"
 operator REGEXP_PLUS 1 "regexp +"
 operator REGEXP_OPT 1 "regexp ?"
+operator REGEXP_RANGE 2 "regexp range"
 
 #constant REGEXP_EMPTY \
 #	::CVC4::RegExp \
@@ -95,6 +96,7 @@ typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule
 typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule
 typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule
 typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule
+typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule
 
 typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
 
diff --git a/src/theory/strings/options b/src/theory/strings/options
index 9226f9999..2832c7833 100644
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -6,6 +6,12 @@
 module STRINGS "theory/strings/options.h" Strings theory
 
 option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :default 256 :read-write
- the cardinality of the characters used by the theory of string, default 256
+ the cardinality of the characters used by the theory of strings, default 256
+
+option stringRegExpUnrollDepth str-regexp-depth --str-regexp-depth=N int16_t :default 10 :read-write
+ the depth of unrolloing regular expression used by the theory of strings, default 10
+
+option stringFMF fmf-strings --fmf-strings bool :default false
+ the finite model finding used by the theory of strings
 
 endmodule
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index a0058954d..a50c295da 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -26,8 +26,6 @@
 #include "theory/strings/type_enumerator.h"
 #include <cmath>
 
-#define STR_UNROLL_INDUCTION
-
 using namespace std;
 using namespace CVC4::context;
 
@@ -43,16 +41,17 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_infer(c),
     d_infer_exp(c),
     d_nf_pairs(c),
-    d_ind_map1(c),
-    d_ind_map2(c),
-    d_ind_map_exp(c),
-    d_ind_map_lemma(c),
+    //d_ind_map1(c),
+    //d_ind_map2(c),
+    //d_ind_map_exp(c),
+    //d_ind_map_lemma(c),
 	//d_lit_to_decide_index( c, 0 ),
 	//d_lit_to_decide( c ),
-	d_lit_to_unroll( c )
+	d_reg_exp_mem( c ),
+	d_curr_cardinality( c, 0 )
 {
     // The kinds we are treating as function application in congruence
-    d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
+    //d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
     d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
     d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
 
@@ -60,6 +59,10 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
     d_true = NodeManager::currentNM()->mkConst( true );
     d_false = NodeManager::currentNM()->mkConst( false );
+
+	//option
+	//d_regexp_unroll_depth = options::stringRegExpUnrollDepth();
+	//d_fmf = options::stringFMF();
 }
 
 TheoryStrings::~TheoryStrings() {
@@ -107,7 +110,7 @@ Node TheoryStrings::getLengthTerm( Node t ) {
 }
 
 Node TheoryStrings::getLength( Node t ) {
-	return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) );
+	return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) ) );
 }
 
 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -158,13 +161,24 @@ bool TheoryStrings::propagate(TNode literal) {
 
 /** explain */
 void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions){
-  Debug("strings-explain") << "Explain " << literal << std::endl;
+  Debug("strings-explain") << "Explain " << literal << " " << d_conflict << std::endl;
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
+  unsigned ps = assumptions.size();
+  std::vector< TNode > tassumptions;
   if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
-    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions);
   } else {
-    d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+    d_equalityEngine.explainPredicate(atom, polarity, tassumptions);
+  }
+  for( unsigned i=0; i<tassumptions.size(); i++ ){
+	if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
+		assumptions.push_back( tassumptions[i] );
+	}
+  }
+  Debug("strings-explain-debug") << "Explanation for " << literal << " was " << std::endl;
+  for( unsigned i=ps; i<assumptions.size(); i++ ){
+	Debug("strings-explain-debug") << "   " << assumptions[i] << std::endl;
   }
 }
 
@@ -327,7 +341,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
     d_equalityEngine.addTriggerEquality(n);
     break;
   case kind::STRING_IN_REGEXP:
-    d_equalityEngine.addTriggerPredicate(n);
+    //d_equalityEngine.addTriggerPredicate(n);
     break;
   default:
     if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) {
@@ -337,6 +351,12 @@ void TheoryStrings::preRegisterTerm(TNode n) {
 		  Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl;
 		  d_out->lemma(n_len_geq_zero);
 	  }
+	  // FMF
+	  if( options::stringFMF() && n.getKind() == kind::VARIABLE ) {
+		  if( std::find(d_in_vars.begin(), d_in_vars.end(), n) == d_in_vars.end() ) {
+			  d_in_vars.push_back( n );
+		  }
+	  }
     }
     if (n.getType().isBoolean()) {
       // Get triggered for both equal and dis-equal
@@ -350,6 +370,8 @@ void TheoryStrings::preRegisterTerm(TNode n) {
 }
 
 void TheoryStrings::check(Effort e) {
+  //Assert( d_pending.empty() );
+
   bool polarity;
   TNode atom;
 
@@ -369,17 +391,16 @@ void TheoryStrings::check(Effort e) {
 
     polarity = fact.getKind() != kind::NOT;
     atom = polarity ? fact : fact[0];
-    if (atom.getKind() == kind::EQUAL) {
+	//must record string in regular expressions
+	if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
+		//if(fact[0].getKind() != kind::CONST_STRING) {
+		 d_reg_exp_mem.push_back( assertion );
+		//}
+	}else if (atom.getKind() == kind::EQUAL) {
       d_equalityEngine.assertEquality(atom, polarity, fact);
     } else {
       d_equalityEngine.assertPredicate(atom, polarity, fact);
     }
-#ifdef STR_UNROLL_INDUCTION
-	//check if it is a literal to unroll?
-	if( d_lit_to_unroll.find( atom )!=d_lit_to_unroll.end() ){
-		Trace("strings-ind") << "Strings-ind : Possibly unroll for : " << atom << ", polarity = " << polarity << std::endl;
-	}
-#endif
   }
   doPendingFacts();
 
@@ -398,8 +419,8 @@ void TheoryStrings::check(Effort e) {
 				  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 = checkMemberships();
+					Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
 				  }
 			  }
 		  }
@@ -407,6 +428,8 @@ void TheoryStrings::check(Effort e) {
   }
   Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
   Trace("strings-process") << "Theory of strings, done check : " << e << std::endl;
+  Assert( d_pending.empty() );
+  Assert( d_lemma_cache.empty() );
 }
 
 TheoryStrings::EqcInfo::EqcInfo(  context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) {
@@ -431,15 +454,18 @@ TheoryStrings::EqcInfo * TheoryStrings::getOrMakeEqcInfo( Node eqc, bool doMake
 
 /** Conflict when merging two constants */
 void TheoryStrings::conflict(TNode a, TNode b){
-  Node conflictNode;
-  if (a.getKind() == kind::CONST_BOOLEAN) {
-    conflictNode = explain( a.iffNode(b) );
-  } else {
-    conflictNode = explain( a.eqNode(b) );
+  if( !d_conflict ){
+	  Trace("strings-conflict-debug") << "Making conflict..." << std::endl;
+	  d_conflict = true;
+	  Node conflictNode;
+	  if (a.getKind() == kind::CONST_BOOLEAN) {
+		conflictNode = explain( a.iffNode(b) );
+	  } else {
+		conflictNode = explain( a.eqNode(b) );
+	  }
+	  Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
+	  d_out->conflict( conflictNode );
   }
-  Debug("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
-  d_out->conflict( conflictNode );
-  d_conflict = true;
 }
 
 /** called when a new equivalance class is created */
@@ -528,8 +554,13 @@ void TheoryStrings::doPendingFacts() {
       bool polarity = fact.getKind() != kind::NOT;
       TNode atom = polarity ? fact : fact[0];
       if (atom.getKind() == kind::EQUAL) {
-		Assert( d_equalityEngine.hasTerm( atom[0] ) );
-		Assert( d_equalityEngine.hasTerm( atom[1] ) );
+		//Assert( d_equalityEngine.hasTerm( atom[0] ) );
+		//Assert( d_equalityEngine.hasTerm( atom[1] ) );
+		for( unsigned j=0; j<2; j++ ){
+			if( !d_equalityEngine.hasTerm( atom[j] ) ){
+				d_equalityEngine.addTerm( atom[j] );
+			}
+		}
 		d_equalityEngine.assertEquality( atom, polarity, exp );
       }else{
         d_equalityEngine.assertPredicate( atom, polarity, exp );
@@ -549,19 +580,20 @@ void TheoryStrings::doPendingLemmas() {
 		Trace("strings-pending") << "Require phase : " << it->first << ", polarity = " << it->second << std::endl;
 		d_out->requirePhase( it->first, it->second );
 	  }
-	d_lemma_cache.clear();
-	d_pending_req_phase.clear();
   }
+  d_lemma_cache.clear();
+  d_pending_req_phase.clear();
 }
 
 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) {
+	Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
     // EqcItr
     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
     while( !eqc_i.isFinished() ) {
         Node n = (*eqc_i);
-        Trace("strings-process-debug") << "Get Normal Form : Process term " << n << std::endl;
         if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
+			Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl;
             std::vector<Node> nf_n;
             std::vector<Node> nf_exp_n;
 			bool result = true;
@@ -582,6 +614,13 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
 					//successfully computed normal form
 					if( nf.size()!=1 || nf[0]!=d_emptyString ) {
 						for( unsigned r=0; r<nf_temp.size(); r++ ) {
+							if( nresult && nf_temp[r].getKind()==kind::STRING_CONCAT ){
+								Trace("strings-error") << "From eqc = " << eqc << ", " << n << " index " << i << ", bad normal form : ";
+								for( unsigned rr=0; rr<nf_temp.size(); rr++ ) {
+									Trace("strings-error") << nf_temp[rr] << " ";
+								}
+								Trace("strings-error") << std::endl;
+							}
 							Assert( !nresult || nf_temp[r].getKind()!=kind::STRING_CONCAT );
 						}
 						nf_n.insert( nf_n.end(), nf_temp.begin(), nf_temp.end() );
@@ -687,21 +726,22 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
 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 );
-		/*
-        if( eqc.getKind()==kind::STRING_CONCAT ){
-            for( unsigned i=0; i<eqc.getNumChildren(); i++ ){
-				if( !areEqual( eqc[i], d_emptyString ) ){
-					nf.push_back( eqc[i] );
-				}
-            }
-        }else if(  !areEqual( eqc, d_emptyString ) ){
-            nf.push_back( eqc );
-        }
-		*/
+		getConcatVec( eqc, nf );
         Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
 		return false;
     } else if( areEqual( eqc, d_emptyString ) ){
+		eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+		while( !eqc_i.isFinished() ) {
+			Node n = (*eqc_i);
+			if( n.getKind()==kind::STRING_CONCAT ){
+				for( unsigned i=0; i<n.getNumChildren(); i++ ){
+					if( !areEqual( n[i], d_emptyString ) ){
+						sendLemma( n.eqNode( d_emptyString ), n[i].eqNode( d_emptyString ), "Empty Concatenation" );
+					}
+				}
+			}
+			++eqc_i;
+		}
         //do nothing
         Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl;
 		d_normal_forms_base[eqc] = d_emptyString;
@@ -765,7 +805,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 										}
 										Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] );
 										Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
-										Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) );
+										Assert( !areEqual( d_emptyString, normal_forms[k][index_k] ) );
 										d_pending.push_back( eq );
 										d_pending_exp[eq] = eq_exp;
 										d_infer.push_back(eq);
@@ -792,35 +832,33 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 									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) &&
+										!areEqual(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 ) || 
+										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 if( areEqual(length_term_i, length_term_j) ) {
+										Trace("strings-solve-debug") << "Case 2.2 : string lengths are equal" << std::endl;
+										Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] );
+										Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_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;
@@ -873,27 +911,37 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 											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") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index] << std::endl;
 											Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl;
 											
+											
 											Trace("strings-loop") << " ... T(Y.Z)= ";
+											std::vector< Node > vec_t;
 											for(int lp=index; lp<loop_index; ++lp) {
 												if(lp != index) Trace("strings-loop") << " ++ ";
 												Trace("strings-loop") << normal_forms[loop_n_index][lp];
+												vec_t.push_back( normal_forms[loop_n_index][lp] );
 											}
-											Trace("strings-loop") << std::endl;
+											Node t_yz = mkConcat( vec_t );
+											Trace("strings-loop") << " (" << t_yz << ")" << std::endl;
 											Trace("strings-loop") << " ... S(Z.Y)= ";
+											std::vector< Node > vec_s;
 											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];
+												vec_s.push_back( normal_forms[other_n_index][lp] );
 											}
-											Trace("strings-loop") << std::endl;
+											Node s_zy = mkConcat( vec_s );
+											Trace("strings-loop") << " (" << s_zy << ")" << std::endl;
 											Trace("strings-loop") << " ... R= ";
+											std::vector< Node > vec_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];
+												vec_r.push_back( normal_forms[loop_n_index][lp] );
 											}
-											Trace("strings-loop") << std::endl;
+											Node r = mkConcat( vec_r );
+											Trace("strings-loop") << " (" << r << ")" << std::endl;
 
 											//we have x * s1 * .... * sm = t1 * ... * tn * x * r1 * ... * rp
 											//check if
@@ -902,71 +950,122 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 											//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" );
+											Trace("strings-loop") << "Lemma Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl;
+
+											if( s_zy.isConst() && r.isConst() && r != d_emptyString) {
+												int c;
+												bool flag = true;
+												if(s_zy.getConst<String>().tailcmp( r.getConst<String>(), c ) ) {
+													if(c >= 0) {
+														s_zy = NodeManager::currentNM()->mkConst( s_zy.getConst<String>().substr(0, c) );
+														r = d_emptyString;
+														vec_r.clear();
+														Trace("strings-loop") << "Refactor : S(Z.Y)= " << s_zy << ", c=" << c << std::endl;
+														flag = false;
+													}
+												}
+												if(flag) {
+													Trace("strings-loop") << "Loop different tail." << std::endl;
+													antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+													Node ant = mkExplain( antec, antec_new_lits );
+													sendLemma( ant, conc, "Conflict" );
+													return true;
+												}
+											}
+
+											//Node loop_eq = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL,
+											//				NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[other_n_index][other_index], s_zy ),
+											//				NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, t_yz, normal_forms[other_n_index][other_index], r ) ) );
 
 											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 );
+											//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() );
+											//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] );
+											//d_pending_req_phase[ x_empty ] = true;
+											if( !areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString ) ){
+												//try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
+												sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop Empty" );
+												return true;
+											} else if( !areDisequal( t_yz, d_emptyString ) ) {
+												//TODO...........
+												//try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
+												sendSplit( t_yz, d_emptyString, "Loop Empty" );
+												return true;
+											} else {
+												//need to break
+												antec.push_back( normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ).negate() );
+												antec.push_back( t_yz.eqNode( d_emptyString ).negate() );
+												Node ant = mkExplain( antec, antec_new_lits );
+												Node str_in_re;
+												if( s_zy == t_yz &&
+													r == d_emptyString &&
+													s_zy.isConst() &&
+													s_zy.getConst<String>().isRepeated()
+													) {
+													Node rep_c = NodeManager::currentNM()->mkConst( s_zy.getConst<String>().substr(0, 1) );
+													Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl;
+													Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl;
+													//special case
+													//conc = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( rep_c, sk_w ) );
+													str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index], 
+																  NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
+																	NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) );
+													//conc = NodeManager::currentNM()->mkNode( kind::AND, conc, str_in_re );
+													conc = str_in_re;
+												} else {
+													Trace("strings-loop") << "Strings::loop: ...Normal Splitting." << std::endl;
+													Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
+													Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
+													Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
+													//t1 * ... * tn = y * z
+													Node conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, t_yz,
+																	NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) );
+													// s1 * ... * sk = z * y * r
+													vec_r.insert(vec_r.begin(), sk_y);
+													vec_r.insert(vec_r.begin(), sk_z);
+													Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, s_zy,
+																	mkConcat( vec_r ) );
+													Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( sk_y, sk_w ) );
+													str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, 
+																	NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
+																		NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) );
+													
+													//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_z_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_z_len, d_zero );
+													//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, sk_z.eqNode(d_emptyString), sk_y.eqNode(d_emptyString));
+													
+													//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 );
+													conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, conc3, str_in_re );//, 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 );
+												} // normal case
+
+												//set its antecedant to ant, to say when it is relevant
+												d_reg_exp_ant[str_in_re] = ant;
+												//unroll the str in re constraint once
+												unrollStar( str_in_re );
+												//conc = NodeManager::currentNM()->mkNode( kind::OR, x_empty, conc );
+												sendLemma( ant, conc, "Loop" );
+
+												//we will be done
+												addNormalFormPair( normal_form_src[i], normal_form_src[j] );
+												//Assert( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) );
+												return true;
 											}
-											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{
+										} 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) {
@@ -1003,11 +1102,12 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 													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 sk = NodeManager::currentNM()->mkSkolem( "c_split_$$", 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 ) );
+													Node eq1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ) );
+													Node eq2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, other_str,
+																NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ) );
+													d_pending_req_phase[ eq1 ] = true;
 													conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
 													Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
 
@@ -1024,7 +1124,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 												}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 sk = NodeManager::currentNM()->mkSkolem( "v_split_$$", 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],
@@ -1054,7 +1154,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
             //construct the normal form
             if( normal_forms.empty() ){
                 Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
-                nf.push_back( eqc );
+				getConcatVec( eqc, nf );
             } else {
                 Trace("strings-solve-debug2") << "just take the first normal form" << std::endl;
                 //just take the first normal form
@@ -1148,9 +1248,9 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
 							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 sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit_$$", ni.getType(), "created for disequality normalization" );
+							Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit_$$", ni.getType(), "created for disequality normalization" );
+							Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit_$$", ni.getType(), "created for disequality normalization" );
 							Node lsk1 = getLength( sk1 );
 							conc.push_back( lsk1.eqNode( li ) );
 							Node lsk2 = getLength( sk2 );
@@ -1158,30 +1258,6 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
 							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 ) ){
@@ -1217,6 +1293,7 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
 
 void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) {
   if( !isNormalFormPair( n1, n2 ) ){
+		//Assert( !isNormalFormPair( n1, n2 ) );
         NodeList* lst;
         NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
         if( nf_i == d_nf_pairs.end() ){
@@ -1259,81 +1336,6 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
   return false;
 }
 
-bool TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c ) {
-    Trace("strings-solve-debug") << "add inductive equation for " << x << " = (" << y << " " << z << ")* " << y << std::endl;
-#ifdef STR_UNROLL_INDUCTION
-	Node w = NodeManager::currentNM()->mkSkolem( "wsym_$$", x.getType(), "created for induction" );
-	Node x_eq_y_w = NodeManager::currentNM()->mkNode( kind::EQUAL, x, 
-							NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, w ) );
-	Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, x_eq_y_w );
-	Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl;
-	d_lemma_cache.push_back( lem );
-
-	//add initial induction
-	Node lit1 = w.eqNode( d_emptyString );
-	lit1 = Rewriter::rewrite( lit1 );
-	Node wp = NodeManager::currentNM()->mkSkolem( "wpsym_$$", x.getType(), "created for induction" );
-	Node lit2 = w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, z, y, wp ) );
-	lit2 = Rewriter::rewrite( lit2 );
-	Node split_lem = NodeManager::currentNM()->mkNode( kind::OR, lit1, lit2 );
-	Trace("strings-ind") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl;
-	Trace("strings-lemma") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl;
-	d_lemma_cache.push_back( split_lem );
-
-	//d_lit_to_decide.push_back( lit1 );
-	d_lit_to_unroll[lit2] = true;
-	d_pending_req_phase[lit1] = true;
-	d_pending_req_phase[lit2] = false;
-
-	x = w;
-	std::vector< Node > skc;
-	skc.push_back( y );
-	skc.push_back( z );
-	y = d_emptyString;
-	z = mkConcat( skc );
-#endif
-
-    NodeListMap::iterator itr_x_y = d_ind_map1.find(x);
-    NodeList* lst1;
-    NodeList* lst2;
-    NodeList* lste;
-    NodeList* lstl;
-    if( itr_x_y == d_ind_map1.end() ) {
-        // add x->y
-        lst1 = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
-                                                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
-        d_ind_map1.insertDataFromContextMemory( x, lst1 );
-        // add x->z
-        lst2 = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
-                                                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
-        d_ind_map2.insertDataFromContextMemory( x, lst2 );
-        // add x->exp
-        lste = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
-                                                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
-        d_ind_map_exp.insertDataFromContextMemory( x, lste );
-        // add x->hasLemma false
-        lstl = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
-                                                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
-        d_ind_map_lemma.insertDataFromContextMemory( x, lstl );
-    } else {
-        //TODO: x in (yz)*y (exp) vs  x in (y1 z1)*y1 (exp1)
-        lst1 = (*itr_x_y).second;
-        lst2 = (*d_ind_map2.find(x)).second;
-        lste = (*d_ind_map_exp.find(x)).second;
-        lstl = (*d_ind_map_lemma.find(x)).second;
-        Trace("strings-solve-debug") << "Already in maps " << x << " = (" << lst1 << " " << lst2 << ")* " << lst1 << std::endl;
-        Trace("strings-solve-debug") << "... with exp = " << lste << std::endl;
-    }
-    lst1->push_back( y );
-    lst2->push_back( z );
-    lste->push_back( exp );
-#ifdef STR_UNROLL_INDUCTION
-	return true;
-#else
-	return false;
-#endif
-}
-
 void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
 	if( conc.isNull() || conc==d_false ){
 		d_out->conflict(ant);
@@ -1376,28 +1378,38 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a ) {
 Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) {
     std::vector< TNode > antec_exp;
     for( unsigned i=0; i<a.size(); i++ ){
-        Trace("strings-solve-debug") << "Ask for explanation of " << a[i] << std::endl;
-        //assert
-        if(a[i].getKind() == kind::EQUAL) {
-            //assert( hasTerm(a[i][0]) );
-            //assert( hasTerm(a[i][1]) );
-            Assert( areEqual(a[i][0], a[i][1]) );
-        } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ){
-            Assert( hasTerm(a[i][0][0]) );
-            Assert( hasTerm(a[i][0][1]) );
-            Assert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
-        }
-		unsigned ps = antec_exp.size();
-        explain(a[i], antec_exp);
-        Trace("strings-solve-debug") << "Done, explanation was : " << std::endl;
-		for( unsigned j=ps; j<antec_exp.size(); j++ ){
-			Trace("strings-solve-debug") << "  " << antec_exp[j] << std::endl;
+		if( std::find( a.begin(), a.begin() + i, a[i] )==a.begin() + i ){
+			bool exp = true;
+			Trace("strings-solve-debug") << "Ask for explanation of " << a[i] << std::endl;
+			//assert
+			if(a[i].getKind() == kind::EQUAL) {
+				//assert( hasTerm(a[i][0]) );
+				//assert( hasTerm(a[i][1]) );
+				Assert( areEqual(a[i][0], a[i][1]) );
+				if( a[i][0]==a[i][1] ){
+					exp = false;
+				}
+			} else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ){
+				Assert( hasTerm(a[i][0][0]) );
+				Assert( hasTerm(a[i][0][1]) );
+				AlwaysAssert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
+			}
+			if( exp ){
+				unsigned ps = antec_exp.size();
+				explain(a[i], antec_exp);
+				Trace("strings-solve-debug") << "Done, explanation was : " << std::endl;
+				for( unsigned j=ps; j<antec_exp.size(); j++ ){
+					Trace("strings-solve-debug") << "  " << antec_exp[j] << std::endl;
+				}
+				Trace("strings-solve-debug") << std::endl;
+			}
 		}
-		Trace("strings-solve-debug") << std::endl;
     }
     for( unsigned i=0; i<an.size(); i++ ){
-		Trace("strings-solve-debug") << "Add to explanation (new literal) " << an[i] << std::endl;
-        antec_exp.push_back(an[i]);
+		if( std::find( an.begin(), an.begin() + i, an[i] )==an.begin() + i ){
+			Trace("strings-solve-debug") << "Add to explanation (new literal) " << an[i] << std::endl;
+			antec_exp.push_back(an[i]);
+		}
     }
     Node ant;
     if( antec_exp.empty() ) {
@@ -1411,6 +1423,18 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an )
     return ant;
 }
 
+void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) {
+	if( n.getKind()==kind::STRING_CONCAT ){
+		for( unsigned i=0; i<n.getNumChildren(); i++ ){
+			if( !areEqual( n[i], d_emptyString ) ){
+				c.push_back( n[i] );
+			}
+		}
+	}else{
+		c.push_back( n );
+	}
+}
+
 bool TheoryStrings::checkLengths() {
   bool addedLemma = false;
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
@@ -1427,7 +1451,7 @@ bool TheoryStrings::checkLengths() {
 			//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( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { // || 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;
@@ -1507,6 +1531,7 @@ bool TheoryStrings::checkNormalForms() {
 		Trace("strings-nf") << std::endl;
 	}
 	Trace("strings-nf") << std::endl;
+	/*
 	Trace("strings-nf") << "Current inductive equations : " << std::endl;
 	for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){
         Node x = (*it).first;
@@ -1522,6 +1547,7 @@ bool TheoryStrings::checkNormalForms() {
             ++i2;
         }
     }
+	*/
 
   bool addedFact;
   do {
@@ -1545,6 +1571,8 @@ bool TheoryStrings::checkNormalForms() {
 		normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
 		Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
 		if( d_conflict ){
+			doPendingFacts();
+			doPendingLemmas();
 			return true;
 		}else if ( d_pending.empty() && d_lemma_cache.empty() ){
 			Node nf_term;
@@ -1587,7 +1615,6 @@ bool TheoryStrings::checkNormalForms() {
       doPendingFacts();
   } while ( !d_conflict && d_lemma_cache.empty() && addedFact );
 
-
   //process disequalities between equivalence classes
   if( !d_conflict && d_lemma_cache.empty() ){
 	  std::vector< Node > eqcs;
@@ -1619,7 +1646,7 @@ bool TheoryStrings::checkNormalForms() {
   }
 
   //flush pending lemmas
-  if( !d_conflict && !d_lemma_cache.empty() ){
+  if( !d_lemma_cache.empty() ){
 	doPendingLemmas();
 	return true;
   }else{
@@ -1747,125 +1774,6 @@ int TheoryStrings::gcd ( int a, int b ) {
   return b;
 }
 
-bool TheoryStrings::checkInductiveEquations() {
-    bool hasEq = false;
-	if(d_ind_map1.size() != 0){
-		Trace("strings-ind")  << "We are sat, with these inductive equations : " << std::endl;
-		for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){
-			Node x = (*it).first;
-			Trace("strings-ind-debug") << "Check eq for " << x << std::endl;
-			NodeList* lst1 = (*it).second;
-			NodeList* lst2 = (*d_ind_map2.find(x)).second;
-			NodeList* lste = (*d_ind_map_exp.find(x)).second;
-			//NodeList* lstl = (*d_ind_map_lemma.find(x)).second;
-			NodeList::const_iterator i1 = lst1->begin();
-			NodeList::const_iterator i2 = lst2->begin();
-			NodeList::const_iterator ie = lste->begin();
-			//NodeList::const_iterator il = lstl->begin();
-			while( i1!=lst1->end() ){
-				Node y = *i1;
-				Node z = *i2;
-				//Trace("strings-ind-debug") << "Check y=" << y << " , z=" << z << std::endl;
-				//if( il==lstl->end() ) {
-					std::vector< Node > nf_y, nf_z, exp_y, exp_z;
-					
-					//getFinalNormalForm( y, nf_y, exp_y);
-					//getFinalNormalForm( z, nf_z, exp_z);
-					//std::vector< Node > vec_empty;
-					//Node nexp_y = mkExplain( exp_y, vec_empty );
-					//Trace("strings-ind-debug") << "Check nexp_y=" << nexp_y << std::endl;
-					//Node nexp_z = mkExplain( exp_z, vec_empty );
-
-					//Node exp = *ie;
-					//Trace("strings-ind-debug") << "Check exp=" << exp << std::endl;
-
-					//exp = NodeManager::currentNM()->mkNode( kind::AND, exp, nexp_y, nexp_z );
-					//exp = Rewriter::rewrite( exp );
-
-					Trace("strings-ind") << "Inductive equation : " << x << " = ( " << y << " ++ " << z << " )* " << y << std::endl;
-					/*
-					for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) {
-						Trace("strings-ind") << (*itr) << " ";
-					}
-					Trace("strings-ind") << " ++ ";
-					for( std::vector< Node >::const_iterator itr = nf_z.begin(); itr != nf_z.end(); ++itr) {
-						Trace("strings-ind") << (*itr) << " ";
-					}
-					Trace("strings-ind") << " )* ";
-					for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) {
-						Trace("strings-ind") << (*itr) << " ";
-					}
-					Trace("strings-ind") << std::endl;
-					*/
-					/*
-					Trace("strings-ind") << "Explanation is : " << exp << std::endl;
-					std::vector< Node > nf_yz;
-					nf_yz.insert( nf_yz.end(), nf_y.begin(), nf_y.end() );
-					nf_yz.insert( nf_yz.end(), nf_z.begin(), nf_z.end() );
-					std::vector< std::vector< Node > > cols;
-					std::vector< Node > lts;
-					seperateByLength( nf_yz, cols, lts );
-					Trace("strings-ind") << "This can be grouped into collections : " << std::endl;
-					for( unsigned j=0; j<cols.size(); j++ ){
-						Trace("strings-ind") << "  : ";
-						for( unsigned k=0; k<cols[j].size(); k++ ){
-							Trace("strings-ind") << cols[j][k] << " ";
-						}
-						Trace("strings-ind") << std::endl;
-					}
-					Trace("strings-ind") << std::endl;
-					
-					Trace("strings-ind") << "Add length lemma..." << std::endl;
-					std::vector< int > co;
-					co.push_back(0);
-					for(unsigned int k=0; k<lts.size(); ++k) {
-						if(lts[k].isConst() && lts[k].getType().isInteger()) {
-							int len = lts[k].getConst<Rational>().getNumerator().toUnsignedInt();
-							co[0] += cols[k].size() * len;
-						} else {
-							co.push_back( cols[k].size() );
-						}
-					}
-					int g_co = co[0];
-					for(unsigned k=1; k<co.size(); ++k) {
-						g_co = gcd(g_co, co[k]);
-					}
-					Node lemma_len;
-					// both constants
-					Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x );
-					Node sk = NodeManager::currentNM()->mkSkolem( "argsym_$$", NodeManager::currentNM()->integerType(), "created for length inductive lemma" );
-					Node g_co_node = NodeManager::currentNM()->mkConst( CVC4::Rational(g_co) );
-					Node sk_m_gcd = NodeManager::currentNM()->mkNode( kind::MULT, g_co_node, sk );
-					Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y );
-					Node sk_m_g_p_y =    NodeManager::currentNM()->mkNode( kind::PLUS, sk_m_gcd, len_y );
-					lemma_len =     NodeManager::currentNM()->mkNode( kind::EQUAL, sk_m_g_p_y, len_x );
-					//Node sk_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk, d_zero );
-					//lemma_len = NodeManager::currentNM()->mkNode( kind::AND, lemma_len, sk_geq_zero );
-					lemma_len =     NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, lemma_len );
-					Trace("strings-lemma") << "Strings: Add lemma " << lemma_len << std::endl;
-					d_out->lemma(lemma_len);
-					lstl->push_back( d_true );
-					return true;*/
-				//}
-				++i1;
-				++i2;
-				++ie;
-				//++il;
-				if( !d_equalityEngine.hasTerm( d_emptyString ) || !d_equalityEngine.areEqual( y, d_emptyString ) || !d_equalityEngine.areEqual( x, d_emptyString ) ){
-					hasEq = true;
-				}
-			}
-		}
-	}
-    if( hasEq ){
-		Trace("strings-ind") << "It is incomplete." << std::endl;
-        d_out->setIncomplete();
-    }else{
-		Trace("strings-ind") << "We can answer SAT." << std::endl;
-	}
-  return false;
-}
-
 void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) {
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
     while( !eqcs_i.isFinished() ) {
@@ -1956,18 +1864,182 @@ void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) {
 	}
 }
 
-/*
-Node TheoryStrings::getNextDecisionRequest() {
-	if( d_lit_to_decide_index.get()<d_lit_to_decide.size() ){
-		Node l = d_lit_to_decide[d_lit_to_decide_index.get()];
-		d_lit_to_decide_index.set( d_lit_to_decide_index.get() + 1 );
-		Trace("strings-ind") << "Strings-ind : decide on " << l << std::endl;
-		return l;
+bool TheoryStrings::unrollStar( Node atom ) {
+	Node x = atom[0];
+	Node r = atom[1];
+	int depth = d_reg_exp_unroll_depth.find( atom )==d_reg_exp_unroll_depth.end() ? 0 : d_reg_exp_unroll_depth[atom];
+	if( depth <= options::stringRegExpUnrollDepth() ) {
+		Trace("strings-regex") << "Strings::regex: Unroll " << atom << " for " << ( depth + 1 ) << " times." << std::endl;
+		d_reg_exp_unroll[atom] = true;
+		//add lemma?
+		Node xeqe = x.eqNode( d_emptyString );
+		xeqe = Rewriter::rewrite( xeqe );
+		d_pending_req_phase[xeqe] = true;
+		Node sk_s= NodeManager::currentNM()->mkSkolem( "s_unroll_$$", x.getType(), "created for unrolling" );
+		Node sk_xp= NodeManager::currentNM()->mkSkolem( "x_unroll_$$", x.getType(), "created for unrolling" );
+		std::vector< Node >cc;
+
+		// must also call preprocessing on unr1
+		Node unr1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_s, r[0] ) );
+		if(unr1.getKind() == kind::EQUAL) {
+			sk_s = unr1[0] == sk_s ? unr1[1] : unr1[2];
+			Node unr0 = sk_s.eqNode( d_emptyString ).negate();
+			cc.push_back(unr0);
+		} else {
+			std::vector< Node > urc;
+			urc.push_back( unr1 );
+
+			StringsPreprocess spp;
+			spp.simplify( urc );
+			for( unsigned i=1; i<urc.size(); i++ ){
+				//add the others as lemmas
+				sendLemma( d_true, urc[i], "RegExp Definition");
+			}
+			Node unr0 = sk_s.eqNode( d_emptyString ).negate();
+			cc.push_back(unr0);	cc.push_back(urc[0]);
+		}
+
+		Node unr2 = x.eqNode( mkConcat( sk_s, sk_xp ) );
+		Node unr3 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_xp, r );
+		unr3 = Rewriter::rewrite( unr3 );
+		d_reg_exp_unroll_depth[unr3] = depth + 1;
+		if( d_reg_exp_ant.find( atom )!=d_reg_exp_ant.end() ){
+			d_reg_exp_ant[unr3] = d_reg_exp_ant[atom];
+		}
+
+		//|x|>|xp|
+		Node len_x_gt_len_xp = NodeManager::currentNM()->mkNode( kind::GT, 
+								NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ),
+								NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_xp ) );
+
+		//Node len_x_eq_s_xp = NodeManager::currentNM()->mkNode( kind::EQUAL, 
+		//						NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ),
+		//						NodeManager::currentNM()->mkNode( kind::PLUS,
+		//							NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_s ),
+		//							NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_xp ) ));
+
+		cc.push_back(unr2); cc.push_back(unr3); cc.push_back(len_x_gt_len_xp);
+		//cc.push_back(len_x_eq_s_xp);
+
+		Node unr = NodeManager::currentNM()->mkNode( kind::AND, cc );
+		Node lem = NodeManager::currentNM()->mkNode( kind::OR, xeqe, unr );
+		Node ant = atom;
+		if( d_reg_exp_ant.find( atom )!=d_reg_exp_ant.end() ) {
+			ant = d_reg_exp_ant[atom];
+		}
+		sendLemma( ant, lem, "Unroll" );
+		return true;
 	}else{
-		return Node::null();
+		Trace("strings-regex") << "Strings::regex: Stop unrolling " << atom << " the max (" << depth << ") is reached." << std::endl;
+		return false;
 	}
 }
-*/
+
+bool TheoryStrings::checkMemberships() {
+	bool is_unk = false;
+	bool addedLemma = false;
+	for( unsigned i=0; i<d_reg_exp_mem.size(); i++ ){
+		//check regular expression membership
+		Node assertion = d_reg_exp_mem[i];
+		Trace("strings-regex") << "We have regular expression assertion : " << assertion << std::endl;
+		Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion;
+		bool polarity = assertion.getKind()!=kind::NOT;
+		if( polarity ){
+			if( d_reg_exp_unroll.find(atom)==d_reg_exp_unroll.end() ){
+				Assert( atom.getKind()==kind::STRING_IN_REGEXP );
+				Node x = atom[0];
+				Node r = atom[1];
+				//TODO
+				Assert( r.getKind()==kind::REGEXP_STAR );
+				if( !areEqual( x, d_emptyString ) ){
+					if( unrollStar( atom ) ){
+						addedLemma = true;
+					}else{
+						Trace("strings-regex") << "RegEx is incomplete due to " << assertion << ", depth = " << options::stringRegExpUnrollDepth() << std::endl;
+						is_unk = true;
+					}
+				}else{
+					Trace("strings-regex") << "...is satisfied." << std::endl;
+				}
+			}else{
+				Trace("strings-regex") << "...Already unrolled." << std::endl;
+			}
+		}else{
+			//TODO: negative membership
+			Trace("strings-regex") << "RegEx is incomplete due to " << assertion << "." << std::endl;
+			is_unk = true;
+		}
+	}
+	if( addedLemma ){
+		doPendingLemmas();
+		return true;
+	}else{
+		if( is_unk ){
+			Trace("strings-regex") << "SET INCOMPLETE" << std::endl;
+			d_out->setIncomplete();
+		}
+		return false;
+	}
+}
+
+Node TheoryStrings::getNextDecisionRequest() {
+	if(options::stringFMF() && !d_conflict) {
+		//Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl;
+		//initialize the term we will minimize
+		if( d_in_var_lsum.isNull() && !d_in_vars.empty() ){
+			Trace("strings-fmf-debug") << "Input variables: ";
+			std::vector< Node > ll;
+			for(std::vector< Node >::iterator itr = d_in_vars.begin();
+				itr != d_in_vars.end(); ++itr) {
+				Trace("strings-fmf-debug") << " " << (*itr) ;
+				ll.push_back( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr ) );
+			}
+			Trace("strings-fmf-debug") << std::endl;
+			d_in_var_lsum = ll.size()==1 ? ll[0] : NodeManager::currentNM()->mkNode( kind::PLUS, ll );
+			d_in_var_lsum = Rewriter::rewrite( d_in_var_lsum );
+		}
+		if( !d_in_var_lsum.isNull() ){
+			//Trace("strings-fmf") << "Get next decision request." << std::endl;
+			//check if we need to decide on something
+			int decideCard = d_curr_cardinality.get();
+			if( d_cardinality_lits.find( decideCard )!=d_cardinality_lits.end() ){
+				bool value;
+				if( d_valuation.hasSatValue( d_cardinality_lits[ d_curr_cardinality.get() ], value ) ) {
+					if( !value ){
+						d_curr_cardinality.set( d_curr_cardinality.get() + 1 );
+						decideCard = d_curr_cardinality.get();
+						Trace("strings-fmf-debug") << "Has false SAT value, increment and decide." << std::endl;
+					}else{
+						decideCard = -1;
+						Trace("strings-fmf-debug") << "Has true SAT value, do not decide." << std::endl;
+					}
+				}else{
+					Trace("strings-fmf-debug") << "No SAT value, decide." << std::endl;
+				}
+			}
+			if( decideCard!=-1 ){
+				if( d_cardinality_lits.find( decideCard )==d_cardinality_lits.end() ){
+					Node lit = NodeManager::currentNM()->mkNode( kind::LEQ, d_in_var_lsum, NodeManager::currentNM()->mkConst( Rational( decideCard ) ) );
+					lit = Rewriter::rewrite( lit );
+					d_cardinality_lits[decideCard] = lit;
+					Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() );
+					Trace("strings-fmf") << "Strings FMF: Add split lemma " << lem << ", decideCard = " << decideCard << std::endl;
+					d_out->lemma( lem );
+					d_out->requirePhase( lit, true );
+				}
+				Trace("strings-fmf") << "Strings FMF: Decide positive on " << d_cardinality_lits[ decideCard ] << std::endl;
+				return d_cardinality_lits[ decideCard ];
+			}
+		}
+	}
+
+	return Node::null();
+}
+
+void TheoryStrings::assertNode( Node lit ) {
+	
+}
+
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 16c3d4876..8f21888a2 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -21,6 +21,7 @@
 
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/strings/theory_strings_preprocess.h"
 
 #include "context/cdchunk_list.h"
 
@@ -37,6 +38,7 @@ class TheoryStrings : public Theory {
   typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+  typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   public:
 
   TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
@@ -124,6 +126,8 @@ class TheoryStrings : public Theory {
     Node d_true;
     Node d_false;
     Node d_zero;
+	// RegExp depth
+	//int d_regexp_unroll_depth;
     //list of pairs of nodes to merge
       std::map< Node, Node > d_pending_exp;
       std::vector< Node > d_pending;
@@ -142,15 +146,15 @@ class TheoryStrings : public Theory {
   bool isNormalFormPair( Node n1, Node n2 );
   bool isNormalFormPair2( Node n1, Node n2 );
 
-  NodeListMap d_ind_map1;
-  NodeListMap d_ind_map2;
-  NodeListMap d_ind_map_exp;
-  NodeListMap d_ind_map_lemma;
-  bool addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c );
-
-  //for unrolling inductive equations
-  NodeBoolMap d_lit_to_unroll;
+  //loop
+  //std::map< Node, bool > d_loop_processed;
 
+  //regular expression memberships
+  NodeList d_reg_exp_mem;
+  std::map< Node, bool > d_reg_exp_unroll;
+  std::map< Node, int > d_reg_exp_unroll_depth;
+  //antecedant for why reg exp membership must be true
+  std::map< Node, Node > d_reg_exp_ant;
 
   /////////////////////////////////////////////////////////////////////////////
   // MODEL GENERATION
@@ -197,12 +201,14 @@ class TheoryStrings : public Theory {
     std::vector< std::vector< Node > > &normal_forms,  std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src);
     bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
     bool normalizeDisequality( Node n1, Node n2 );
+	bool unrollStar( Node atom );
 
 	bool checkLengths();
     bool checkNormalForms();
 	bool checkLengthsEqc();
     bool checkCardinality();
     bool checkInductiveEquations();
+	bool checkMemberships();
 	int gcd(int a, int b);
   public:
   void preRegisterTerm(TNode n);
@@ -234,6 +240,8 @@ protected:
   /** mkExplain **/
   Node mkExplain( std::vector< Node >& a );
   Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
+  /** get concat vector */
+  void getConcatVec( Node n, std::vector< Node >& c );
 
   //get equivalence classes
   void getEquivalenceClasses( std::vector< Node >& eqcs );
@@ -242,8 +250,20 @@ protected:
 
   //seperate into collections with equal length
   void seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
-private:
   void printConcat( std::vector< Node >& n, const char * c );
+
+private:
+	// Finite Model Finding
+	//bool d_fmf;
+	std::vector< Node > d_in_vars;
+	Node d_in_var_lsum;
+	std::map< int, Node > d_cardinality_lits;
+	context::CDO< int > d_curr_cardinality;
+public:
+	//for finite model finding
+    Node getNextDecisionRequest();
+	void assertNode( Node lit );
+
 };/* class TheoryStrings */
 
 }/* CVC4::theory::strings namespace */
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index f303fd333..c54cbb3b2 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -21,7 +21,7 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) {
+void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) {
 	int k = r.getKind();
 	switch( k ) {
 		case kind::STRING_TO_REGEXP:
@@ -34,20 +34,24 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret
 		{
 			std::vector< Node > cc;
 			for(unsigned i=0; i<r.getNumChildren(); ++i) {
-				Node sk = NodeManager::currentNM()->mkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" );
-				simplifyRegExp( sk, r[i], ret );
-				cc.push_back( sk );
+				if(r[i].getKind() == kind::STRING_TO_REGEXP) {
+					cc.push_back( r[i][0] );
+				} else {
+					Node sk = NodeManager::currentNM()->mkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" );
+					simplifyRegExp( sk, r[i], ret, nn );
+					cc.push_back( sk );
+				}
 			}
 			Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, 
 						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) );
-			ret.push_back( cc_eq );
+			nn.push_back( cc_eq );
 		}
 			break;
 		case kind::REGEXP_OR:
 		{
 			std::vector< Node > c_or;
 			for(unsigned i=0; i<r.getNumChildren(); ++i) {
-				simplifyRegExp( s, r[i], c_or );
+				simplifyRegExp( s, r[i], c_or, nn );
 			}
 			Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or );
 			ret.push_back( eq );
@@ -55,35 +59,33 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret
 			break;
 		case kind::REGEXP_INTER:
 			for(unsigned i=0; i<r.getNumChildren(); ++i) {
-				simplifyRegExp( s, r[i], ret );
+				simplifyRegExp( s, r[i], ret, nn );
 			}
 			break;
 		case kind::REGEXP_STAR:
 		{
-			Node sk = NodeManager::currentNM()->mkSkolem( "ressym_$$", s.getType(), "created for regular expression star" );
-			Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,
-						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, s ),
-						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, sk ));
+			Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
 			ret.push_back( eq );
-			simplifyRegExp( sk, r[0], ret );
-		}
-			break;
-		case kind::REGEXP_OPT:
-		{
-			Node eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );
-			std::vector< Node > rr;
-			simplifyRegExp( s, r[0], rr );
-			Node nrr = rr.size()==1 ? rr[0] : NodeManager::currentNM()->mkNode( kind::AND, rr );
-			ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) );
 		}
 			break;
 		default:
-			//TODO:case kind::REGEXP_PLUS:
 			//TODO: special sym: sigma, none, all
+			Trace("strings-preprocess") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl;
+			Assert( false );
 			break;
 	}
 }
 
+bool StringsPreprocess::checkStarPlus( Node t ) {
+	if( t.getKind() != kind::REGEXP_STAR && t.getKind() != kind::REGEXP_PLUS ) {
+		for( unsigned i = 0; i<t.getNumChildren(); ++i ) {
+			if( checkStarPlus(t[i]) ) return true;
+		}
+		return false;
+	} else {
+		return true;
+	}
+}
 
 Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
@@ -91,17 +93,27 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       return (*i).second.isNull() ? t : (*i).second;
     }
 
-	if( t.getKind() == kind::STRING_IN_REGEXP ){
+	Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl;
+	Node retNode = 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( t0, t[1], ret );
+		
+		//if(!checkStarPlus( t[1] )) {
+			//rewrite it
+			std::vector< Node > ret;
+			std::vector< Node > nn;
+			simplifyRegExp( t0, t[1], ret, nn );
+			new_nodes.insert( new_nodes.end(), nn.begin(), nn.end() );
 
-		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.getKind() == kind::STRING_SUBSTR ){
+			Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
+			d_cache[t] = (t == n) ? Node::null() : n;
+			retNode = n;
+		//} else {
+			// TODO
+		//	return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] );
+		//}
+	} 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" );
@@ -117,7 +129,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 		new_nodes.push_back( len_sk2_eq_j );
 
 		d_cache[t] = sk2;
-		return sk2;
+		retNode = sk2;
 	} else if( t.getNumChildren()>0 ){
 		std::vector< Node > cc;
 		if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
@@ -132,15 +144,26 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 		if(changed) {
 			Node n = NodeManager::currentNM()->mkNode( t.getKind(), cc );
 			d_cache[t] = n;
-			return n;
+			retNode = n;
 		} else {
 			d_cache[t] = Node::null();
-			return t;
+			retNode = t;
 		}
 	}else{
 		d_cache[t] = Node::null();
-		return t;
+		retNode = t;
 	}
+
+	Trace("strings-preprocess") << "StringsPreprocess::simplify returns: " << retNode << std::endl;
+	if(!new_nodes.empty()) {
+		Trace("strings-preprocess") << " ... new nodes:";
+		for(unsigned int i=0; i<new_nodes.size(); ++i) {
+			Trace("strings-preprocess") << " " << new_nodes[i];
+		}
+		Trace("strings-preprocess") << std::endl;
+	}
+
+	return retNode;
 }
 
 void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index d07249a02..7bc60c1a1 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -31,10 +31,11 @@ class StringsPreprocess {
 	// NOTE: this class is NOT context-dependent
 	std::hash_map<TNode, Node, TNodeHashFunction> d_cache;
 private:
-	void simplifyRegExp( Node s, Node r, std::vector< Node > &ret );
+	bool checkStarPlus( Node t );
+	void simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn );
 	Node simplify( Node t, std::vector< Node > &new_nodes );
 public:
-void simplify(std::vector< Node > &vec_node);
+    void simplify(std::vector< Node > &vec_node);
 };
 
 }/* CVC4::theory::strings namespace */
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 3a7ad1ee0..73f17a146 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -21,7 +21,7 @@ using namespace CVC4::kind;
 using namespace CVC4::theory;
 using namespace CVC4::theory::strings;
 
-Node TheoryStringsRewriter::rewriteConcatString(TNode node) {
+Node TheoryStringsRewriter::rewriteConcatString( TNode node ) {
     Trace("strings-prerewrite") << "Strings::rewriteConcatString start " << node << std::endl;
     Node retNode = node;
     std::vector<Node> node_vec;
@@ -53,7 +53,7 @@ Node TheoryStringsRewriter::rewriteConcatString(TNode node) {
         }
         if(!tmpNode.isConst()) {
             if(preNode != Node::null()) {
-                if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().toString()=="" ) {
+                if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ) {
                     preNode = Node::null();
                 } else {
                     node_vec.push_back( preNode );
@@ -81,9 +81,221 @@ Node TheoryStringsRewriter::rewriteConcatString(TNode node) {
     return retNode;
 }
 
+Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) {
+	Assert( node.getKind() == kind::REGEXP_CONCAT );
+    Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp start " << node << std::endl;
+    Node retNode = node;
+    std::vector<Node> node_vec;
+    Node preNode = Node::null();
+    for(unsigned int i=0; i<node.getNumChildren(); ++i) {
+		Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp preNode: " << preNode << std::endl;
+        Node tmpNode = node[i];
+        if(node[i].getKind() == kind::REGEXP_CONCAT) {
+            tmpNode = prerewriteConcatRegExp(node[i]);
+            if(tmpNode.getKind() == kind::REGEXP_CONCAT) {
+                unsigned int j=0;
+                if(!preNode.isNull()) {
+                    if(tmpNode[0].getKind() == kind::STRING_TO_REGEXP) {
+                        preNode = rewriteConcatString(
+							NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) );
+                        node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
+                        preNode = Node::null();
+                        ++j;
+                    } else {
+                        node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
+                        preNode = Node::null();
+                        node_vec.push_back( tmpNode[0] );
+                        ++j;
+                    }
+                }
+                for(; j<tmpNode.getNumChildren() - 1; ++j) {
+                    node_vec.push_back( tmpNode[j] );
+                }
+                tmpNode = tmpNode[j];
+            }
+        }
+        if( tmpNode.getKind() == kind::STRING_TO_REGEXP ) {
+            if(preNode.isNull()) {
+                preNode = tmpNode[0];
+            } else {
+				preNode = rewriteConcatString(
+							NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0] ) );
+            }
+        } else {
+            if(!preNode.isNull()) {
+                if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ) {
+                    preNode = Node::null();
+                } else {
+                    node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
+                    preNode = Node::null();
+                }
+            }
+            node_vec.push_back( tmpNode );
+        }
+    }
+    if(!preNode.isNull()) {
+        node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
+    }
+    if(node_vec.size() > 1) {
+        retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, node_vec);
+    } else {
+        retNode = node_vec[0];
+    }
+    Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp end " << retNode << std::endl;
+    return retNode;
+}
+
+Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) {
+	Assert( node.getKind() == kind::REGEXP_OR );
+    Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl;
+    Node retNode = node;
+    std::vector<Node> node_vec;
+	bool flag = true;
+    for(unsigned int i=0; i<node.getNumChildren(); ++i) {
+		if(node[i].getKind() == kind::REGEXP_OR) {
+			Node tmpNode = prerewriteOrRegExp( node[i] );
+			for(unsigned int j=0; j<tmpNode.getNumChildren(); ++j) {
+				node_vec.push_back( tmpNode[i] );
+			}
+			flag = false;
+		} else {
+			node_vec.push_back( node[i] );
+		}
+	}
+	if(flag) {
+		retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_OR, node_vec);
+	}
+	Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl;
+    return retNode;
+}
+
+bool TheoryStringsRewriter::checkConstRegExp( TNode t ) {
+	if( t.getKind() != kind::STRING_TO_REGEXP ) {
+		for( unsigned i = 0; i<t.getNumChildren(); ++i ) {
+			if( !checkConstRegExp(t[i]) ) return false;
+		}
+		return true;
+	} else {
+		if( t[0].getKind() == kind::CONST_STRING ) {
+			return true;
+		} else {
+			return false;
+		}
+	}
+}
+
+bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r ) {
+	Assert( index_start <= s.size() );
+	int k = r.getKind();
+	switch( k ) {
+		case kind::STRING_TO_REGEXP:
+		{
+			CVC4::String s2 = s.substr( index_start, s.size() - index_start );
+			if(r[0].getKind() == kind::CONST_STRING) {
+				return ( s2 == r[0].getConst<String>() );
+			} else {
+				Assert( false, "RegExp contains variable" );
+			}
+		}
+		case kind::REGEXP_CONCAT:
+		{
+			if( s.size() != index_start ) {
+				std::vector<int> vec_k( r.getNumChildren(), -1 );
+				int start = 0;
+				int left = (int) s.size();
+				int i=0;
+				while( i<(int) r.getNumChildren() ) {
+					bool flag = true;
+					if( i == (int) r.getNumChildren() - 1 ) {
+						if( testConstStringInRegExp( s, index_start + start, r[i] ) ) {
+							return true;
+						}
+					} else if( i == -1 ) {
+						return false;
+					} else {
+						for(vec_k[i] = vec_k[i] + 1; vec_k[i] <= left; ++vec_k[i]) {
+							CVC4::String t = s.substr(index_start + start, vec_k[i]);
+							if( testConstStringInRegExp( t, 0, r[i] ) ) {
+								start += vec_k[i]; left -= vec_k[i]; flag = false;
+								++i; vec_k[i] = -1;
+								break;
+							}
+						}
+					}
+
+					if(flag) {
+						--i;
+						if(i >= 0) {
+							start -= vec_k[i]; left += vec_k[i];
+						}
+					}
+				}
+				return false;
+			} else {
+				return true;
+			}
+		}
+		case kind::REGEXP_OR:
+		{
+			for(unsigned i=0; i<r.getNumChildren(); ++i) {
+				if(testConstStringInRegExp( s, index_start, r[i] )) return true;
+			}
+			return false;
+		}
+		case kind::REGEXP_INTER:
+		{
+			for(unsigned i=0; i<r.getNumChildren(); ++i) {
+				if(!testConstStringInRegExp( s, index_start, r[i] )) return false;
+			}
+			return true;
+		}
+		case kind::REGEXP_STAR:
+		{
+			if( s.size() != index_start ) {
+				for(unsigned int k=s.size() - index_start; k>0; --k) {
+					CVC4::String t = s.substr(index_start, k);
+					if( testConstStringInRegExp( t, 0, r[0] ) ) {
+						if( index_start + k == s.size() || testConstStringInRegExp( s, index_start + k, r ) ) {
+							return true;
+						}
+					}
+				}
+				return false;
+			} else {
+				return true;
+			}
+		}
+		default:
+			//TODO: special sym: sigma, none, all
+			Trace("strings-postrewrite") << "Unsupported term: " << r << " in testConstStringInRegExp." << std::endl;
+			Assert( false );
+			return false;
+	}
+}
+Node TheoryStringsRewriter::rewriteMembership(TNode node) {
+	Node retNode = node;
+	Node x = node[0];
+
+	if(node[0].getKind() == kind::STRING_CONCAT) {
+		x = rewriteConcatString(node[0]);
+	}
+
+	if( x.getKind() == kind::CONST_STRING && checkConstRegExp(node[1]) ) {
+		//test whether x in node[1]
+		CVC4::String s = x.getConst<String>();
+		retNode = NodeManager::currentNM()->mkConst( testConstStringInRegExp( s, 0, node[1] ) );
+	} else {
+		if( x != node[0] ) {
+			retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, node[1] );
+		}
+	}
+    return retNode;
+}
+
 RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
   Trace("strings-postrewrite") << "Strings::postRewrite start " << node << std::endl;
   Node retNode = node;
+  Node orig = retNode;
 
     if(node.getKind() == kind::STRING_CONCAT) {
         retNode = rewriteConcatString(node);
@@ -106,17 +318,6 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
         } else if( leftNode != node[0] || rightNode != node[1]) {
             retNode = NodeManager::currentNM()->mkNode(kind::EQUAL, leftNode, rightNode);
         }
-    } else if(node.getKind() == kind::STRING_IN_REGEXP) {
-        Node leftNode  = node[0];
-        if(node[0].getKind() == kind::STRING_CONCAT) {
-            leftNode = rewriteConcatString(node[0]);
-        }
-        // TODO: right part
-        Node rightNode = node[1];
-        // merge
-        if( leftNode != node[0] || rightNode != node[1]) {
-            retNode = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, leftNode, rightNode);
-        }
     } else if(node.getKind() == kind::STRING_LENGTH) {
         if(node[0].isConst()) {
             retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) );
@@ -150,20 +351,47 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
 		} else {
 			//handled by preprocess
 		}
+	} else if(node.getKind() == kind::STRING_IN_REGEXP) {
+		retNode = rewriteMembership(node);
 	}
 
-  Trace("strings-postrewrite") << "Strings::postRewrite returning " << node << std::endl;
-  return RewriteResponse(REWRITE_DONE, retNode);
+  Trace("strings-postrewrite") << "Strings::postRewrite returning " << retNode << std::endl;
+  return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
 }
 
 RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
     Node retNode = node;
+	Node orig = retNode;
     Trace("strings-prerewrite") << "Strings::preRewrite start " << node << std::endl;
 
     if(node.getKind() == kind::STRING_CONCAT) {
         retNode = rewriteConcatString(node);
-    }
+    } else if(node.getKind() == kind::REGEXP_CONCAT) {
+		retNode = prerewriteConcatRegExp(node);
+    } else if(node.getKind() == kind::REGEXP_OR) {
+		retNode = prerewriteOrRegExp(node);
+	} else if(node.getKind() == kind::REGEXP_PLUS) {
+		retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0],
+					NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, node[0]));
+	} else if(node.getKind() == kind::REGEXP_OPT) {
+		retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR,
+					NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ),
+					node[0]);
+	} else if(node.getKind() == kind::REGEXP_RANGE) {
+		std::vector< Node > vec_nodes;
+		char c = node[0].getConst<String>().getFirstChar();
+		char end = node[1].getConst<String>().getFirstChar();
+		for(; c<=end; ++c) {
+			Node n = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String( c ) ) );
+			vec_nodes.push_back( n );
+		}
+		if(vec_nodes.size() == 1) {
+			retNode = vec_nodes[0];
+		} else {
+			retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );
+		}
+	}
 
     Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl;
-    return RewriteResponse(REWRITE_DONE, retNode);
+    return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
 }
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 3bccd91de..78f0da59e 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -29,9 +29,14 @@ namespace theory {
 namespace strings {
 
 class TheoryStringsRewriter {
-
 public:
+  static bool checkConstRegExp( TNode t );
+  static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r );
+
   static Node rewriteConcatString(TNode node);
+  static Node prerewriteConcatRegExp(TNode node);
+  static Node prerewriteOrRegExp(TNode node);
+  static Node rewriteMembership(TNode node);
 
   static RewriteResponse postRewrite(TNode node);
 
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index ef8f58f80..080d6abf5 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -37,12 +37,17 @@ public:
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
+	int size = 0;
     for (; it != it_end; ++ it) {
        TypeNode t = (*it).getType(check);
        if (!t.isString()) {
          throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat");
        }
+	   ++size;
     }
+	if(size < 2) {
+       throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in string concat");
+	}
     return nodeManager->stringType();
   }
 };
@@ -97,12 +102,17 @@ public:
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
+	int size = 0;
     for (; it != it_end; ++ it) {
        TypeNode t = (*it).getType(check);
        if (!t.isRegExp()) {
-         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
+         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms in regexp concat");
        }
+	   ++size;
     }
+	if(size < 2) {
+       throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat");
+	}
     return nodeManager->regexpType();
   }
 };
@@ -193,6 +203,40 @@ public:
   }
 };
 
+class RegExpRangeTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TNode::iterator it = n.begin();
+    TNode::iterator it_end = n.end();
+	char ch[2];
+
+	for(int i=0; i<2; ++i) {
+		TypeNode t = (*it).getType(check);
+		if (!t.isString()) {
+		  throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range");
+		}
+		if( (*it).getKind() != kind::CONST_STRING ) {
+		  throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range");
+		}
+		if( (*it).getConst<String>().size() != 1 ) {
+		  throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range");
+		}
+		ch[i] = (*it).getConst<String>().getFirstChar();
+		++it;
+	}
+	if(ch[0] > ch[1]) {
+		throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range");
+	}
+
+    if( it != it_end ) {
+      throw TypeCheckingExceptionPrivate(n, "too many terms in regexp range");
+    }
+
+    return nodeManager->regexpType();
+  }
+};
+
 class StringToRegExpTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -203,9 +247,9 @@ public:
     if (!t.isString()) {
       throw TypeCheckingExceptionPrivate(n, "expecting string terms");
     }
-    if( (*it).getKind() != kind::CONST_STRING ) {
-      throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
-    }
+    //if( (*it).getKind() != kind::CONST_STRING ) {
+    //  throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
+    //}
     if(++it != it_end) {
       throw TypeCheckingExceptionPrivate(n, "too many terms");
     }
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 8c85e4dd2..8aa7d625d 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1382,7 +1382,7 @@ void StrongSolverTheoryUF::SortModel::debugPrint( const char* c ){
 void StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){
   if( Trace.isOn("uf-ss-warn") ){
     std::vector< Node > eqcs;
-    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine );
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( m->d_equalityEngine );
     while( !eqcs_i.isFinished() ){
       Node eqc = (*eqcs_i);
       if( eqc.getType()==d_type ){
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 96e8692f5..8db91da69 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -107,6 +107,7 @@ void Datatype::resolve(ExprManager* em,
     Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
   }
   d_self = self;
+  //d_card = getCardinality();
 }
 
 void Datatype::addConstructor(const DatatypeConstructor& c) {
@@ -125,6 +126,10 @@ Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
     c += (*i).getCardinality();
   }
+  //if( d_card!=c ){
+    //std::cout << "Bad card " << std::endl;
+  //}
+
   return c;
 }
 
diff --git a/src/util/datatype.h b/src/util/datatype.h
index c46c10c97..01558fd30 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -404,6 +404,7 @@ private:
   std::vector<DatatypeConstructor> d_constructors;
   bool d_resolved;
   Type d_self;
+  Cardinality d_card;
 
   /**
    * Datatypes refer to themselves, recursively, and we have a
@@ -616,7 +617,8 @@ inline Datatype::Datatype(std::string name) :
   d_params(),
   d_constructors(),
   d_resolved(false),
-  d_self() {
+  d_self(),
+  d_card(1) {
 }
 
 inline Datatype::Datatype(std::string name, const std::vector<Type>& params) :
@@ -624,7 +626,8 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params) :
   d_params(params),
   d_constructors(),
   d_resolved(false),
-  d_self() {
+  d_self(),
+  d_card(1) {
 }
 
 inline std::string Datatype::getName() const throw() {
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 58f58a40f..85e827a8d 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -22,87 +22,12 @@
 
 #include <iostream>
 #include <string>
-//#include "util/exception.h"
+//#include "util/cvc4_assert.h"
 //#include "util/integer.h"
 #include "util/hash.h"
 
 namespace CVC4 {
 
-class CVC4_PUBLIC Char {
-
-private:
-  unsigned int d_char;
-
-public:
-  Char() {}
-
-  Char(const unsigned int c)
-      : d_char(c) {}
-
-  ~Char() {}
-
-  Char& operator =(const Char& y) {
-    if(this != &y) d_char = y.d_char;
-    return *this;
-  }
-
-  bool operator ==(const Char& y) const {
-    return d_char == y.d_char ;
-  }
-
-  bool operator !=(const Char& y) const {
-    return d_char != y.d_char ;
-  }
-
-  bool operator <(const Char& y) const {
-    return d_char < y.d_char;
-  }
-
-  bool operator >(const Char& y) const {
-    return d_char > y.d_char ;
-  }
-
-  bool operator <=(const Char& y) const {
-    return d_char <= y.d_char;
-  }
-
-  bool operator >=(const Char& y) const {
-    return d_char >= y.d_char ;
-  }
-
-  /*
-   * Convenience functions
-   */
-  std::string toString() const {
-    std::string str = "1";
-    str[0] = (char) d_char;
-    return str;
-  }
-
-  unsigned size() const {
-    return 1;
-  }
-
-  const char* c_str() const {
-    return toString().c_str();
-  }
-};/* class Char */
-
-namespace strings {
-
-struct CharHashFunction {
-  size_t operator()(const ::CVC4::Char& c) const {
-    return __gnu_cxx::hash<const char*>()(c.toString().c_str());
-  }
-};/* struct CharHashFunction */
-
-}
-
-inline std::ostream& operator <<(std::ostream& os, const Char& c) CVC4_PUBLIC;
-inline std::ostream& operator <<(std::ostream& os, const Char& c) {
-  return os << "\"" << c.toString() << "\"";
-}
-
 class CVC4_PUBLIC String {
 
 private:
@@ -132,6 +57,10 @@ public:
     }
   }
 
+  String(const char c) {
+    d_str.push_back( convertCharToUnsignedInt(c) );
+  }
+
   String(const std::vector<unsigned int> &s) : d_str(s) { }
 
   ~String() {}
@@ -201,6 +130,15 @@ public:
       return true;
   }
 
+
+  bool isEmptyString() const {
+	  return ( d_str.size() == 0 );
+  }
+
+  unsigned int operator[] (const unsigned int i) const {
+	//Assert( i < d_str.size() && i >= 0);
+    return d_str[i];
+  }
   /*
    * Convenience functions
    */
@@ -217,6 +155,34 @@ public:
     return d_str.size();
   }
 
+  char getFirstChar() const {
+    return convertUnsignedIntToChar( d_str[0] );
+  }
+
+  bool isRepeated() const {
+	if(d_str.size() > 1) {
+		unsigned int f = d_str[0];
+		for(unsigned i=1; i<d_str.size(); ++i) {
+			if(f != d_str[i]) return false;
+		}
+	}
+	return true;
+  }
+
+  bool tailcmp(const String &y, int &c) const {
+	  int id_x = d_str.size() - 1;
+	  int id_y = y.d_str.size() - 1;
+	  while(id_x>=0 && id_y>=0) {
+		  if(d_str[id_x] != y.d_str[id_y]) {
+			  c = id_x;
+			  return false;
+		  }
+		  --id_x; --id_y;
+	  }
+	  c = id_x == -1 ? ( - (id_y+1) ) : (id_x + 1);
+	  return true;
+  }
+
   String substr(unsigned i) const {
     std::vector<unsigned int> ret_vec;
     std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
@@ -330,9 +296,6 @@ public:
     return d_str;
   }
 
-  unsigned size() const {
-    return d_str.size();
-  }
 };/* class String */
 
 /**
diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp
index 90b069485..970d2542e 100644
--- a/src/util/trans_closure.cpp
+++ b/src/util/trans_closure.cpp
@@ -37,16 +37,22 @@ TransitiveClosure::~TransitiveClosure() {
 
 bool TransitiveClosure::addEdge(unsigned i, unsigned j)
 {
+  Debug("trans-closure") << "Add edge " << i << " -> " << j << std::endl;
   // Check for loops
   Assert(i != j, "Cannot add self-loop");
-  if (adjMatrix.size() > j && adjMatrix[j] != NULL && adjMatrix[j]->read(i)) {
+  if (adjIndex.get() > j && adjMatrix[j] != NULL && adjMatrix[j]->read(i)) {
     return true;
   }
 
   // Grow matrix if necessary
   unsigned maxSize = ((i > j) ? i : j) + 1;
-  while (maxSize > adjMatrix.size()) {
-    adjMatrix.push_back(NULL);
+  while (maxSize > adjIndex.get()) {
+    if( maxSize > adjMatrix.size() ){
+      adjMatrix.push_back(NULL);
+    }else if( adjMatrix[adjIndex.get()]!=NULL ){
+      adjMatrix[adjIndex.get()]->clear();
+    }
+    adjIndex.set( adjIndex.get() + 1 );
   }
 
   // Add edge from i to j and everything j can reach
@@ -60,7 +66,7 @@ bool TransitiveClosure::addEdge(unsigned i, unsigned j)
 
   // Add edges from everything that can reach i to j and everything that j can reach
   unsigned k;
-  for (k = 0; k < adjMatrix.size(); ++k) {
+  for (k = 0; k < adjIndex.get(); ++k) {
     if (adjMatrix[k] != NULL && adjMatrix[k]->read(i)) {
       adjMatrix[k]->write(j);
       if (adjMatrix[j] != NULL) {
@@ -74,7 +80,7 @@ bool TransitiveClosure::addEdge(unsigned i, unsigned j)
 
 bool TransitiveClosure::isConnected(unsigned i, unsigned j)
 {
-  if( i>=adjMatrix.size() || j>adjMatrix.size() ){
+  if( i>=adjIndex.get() || j>adjIndex.get() ){//adjMatrix.size() ){
     return false;
   }else{
     return adjMatrix[i] != NULL && adjMatrix[i]->read(j);
@@ -84,15 +90,15 @@ bool TransitiveClosure::isConnected(unsigned i, unsigned j)
 void TransitiveClosure::debugPrintMatrix()
 {
   unsigned i,j;
-  for (i = 0; i < adjMatrix.size(); ++i) {
-    for (j = 0; j < adjMatrix.size(); ++j) {
+  for (i = 0; i < adjIndex.get(); ++i) {
+    for (j = 0; j < adjIndex.get(); ++j) {
       if (adjMatrix[i] != NULL && adjMatrix[i]->read(j)) {
         Debug("trans-closure") << "1 ";
       }
       else Debug("trans-closure") << "0 ";
     }
     Debug("trans-closure") << endl;
-  }      
+  }
 }
 
 unsigned TransitiveClosureNode::getId( Node i ){
@@ -108,10 +114,14 @@ unsigned TransitiveClosureNode::getId( Node i ){
 
 void TransitiveClosureNode::debugPrint(){
   for( int i=0; i<(int)currEdges.size(); i++ ){
-    Debug("trans-closure") << "currEdges[ " << i << " ] = " 
+    Debug("trans-closure") << "currEdges[ " << i << " ] = "
                            << currEdges[i].first << " -> " << currEdges[i].second;
+    int id1 = getId( currEdges[i].first );
+    int id2 = getId( currEdges[i].second );
+    Debug("trans-closure") << " { " << id1 << " -> " << id2 << " } ";
     Debug("trans-closure") << std::endl;
   }
+  debugPrintMatrix();
 }
 
 
diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h
index ce846637d..14e7ab95f 100644
--- a/src/util/trans_closure.h
+++ b/src/util/trans_closure.h
@@ -57,17 +57,17 @@ protected:
   CDBV* next() { return d_next; }
 
 public:
-  CDBV(context::Context* context) : 
+  CDBV(context::Context* context) :
     ContextObj(context), d_data(0), d_next(NULL)
   {}
 
-  ~CDBV() { 
+  ~CDBV() {
     if (d_next != NULL) {
       d_next->deleteSelf();
     }
     destroy();
   }
-
+  void clear() { d_data = 0; if( d_next ) d_next->clear(); }
   bool read(unsigned index) {
     if (index < 64) return (d_data & (uint64_t(1) << index)) != 0;
     else if (d_next == NULL) return false;
@@ -88,7 +88,7 @@ public:
       makeCurrent();
       d_next = new(true) CDBV(getContext());
       d_next->write(index - 64);
-    }      
+    }
   }
 
   void merge(CDBV* pcdbv) {
@@ -108,9 +108,10 @@ public:
 class TransitiveClosure {
   context::Context* d_context;
   std::vector<CDBV* > adjMatrix;
+  context::CDO<unsigned> adjIndex;
 
 public:
-  TransitiveClosure(context::Context* context) : d_context(context) {}
+  TransitiveClosure(context::Context* context) : d_context(context), adjIndex(context,0) {}
   virtual ~TransitiveClosure();
 
   /* Add an edge from node i to node j.  Return false if successful, true if this edge would create a cycle */
@@ -130,7 +131,7 @@ class TransitiveClosureNode : public TransitiveClosure{
   //for debugging
   context::CDList< std::pair< Node, Node > > currEdges;
 public:
-  TransitiveClosureNode(context::Context* context) : 
+  TransitiveClosureNode(context::Context* context) :
     TransitiveClosure(context), d_counter( context, 0 ), nodeMap( context ), currEdges(context) {}
   ~TransitiveClosureNode(){}
 
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 601d65799..bfbc851ef 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -19,6 +19,7 @@ MAKEFLAGS = -k
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =	\
+	array_card.smt2 \
 	agree466.smt2 \
 	ALG008-1.smt2 \
 	german169.smt2 \
@@ -29,7 +30,7 @@ TESTS =	\
 	german73.smt2 \
 	PUZ001+1.smt2 \
 	refcount24.cvc.smt2 \
-	bug0909.smt2 
+	bug0909.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/array_card.smt2 b/test/regress/regress0/fmf/array_card.smt2
new file mode 100644
index 000000000..9ee00d13a
--- /dev/null
+++ b/test/regress/regress0/fmf/array_card.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+; EXIT: 10
+(set-logic AUFLIA)
+(set-option :produce-models true)
+(declare-sort U 0)
+(declare-fun f () (Array U U))
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+
+(assert (distinct a b c))
+
+(assert (distinct (select f a) (select f b)))
+
+(assert (forall ((x U)) (or (= (select f x) c) (= (select f x) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 9b9fdef7a..c98f37958 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -25,15 +25,22 @@ TESTS =	\
   str003.smt2 \
   str004.smt2 \
   str005.smt2 \
+  str006.smt2 \
+  fmf001.smt2 \
+  fmf002.smt2 \
   model001.smt2 \
   substr001.smt2 \
+  regexp001.smt2 \
+  regexp002.smt2 \
   loop001.smt2 \
   loop002.smt2 \
   loop003.smt2 \
   loop004.smt2 \
   loop005.smt2 \
   loop006.smt2 \
-  loop007.smt2
+  loop007.smt2 \
+  loop008.smt2 \
+  loop009.smt2
 
 FAILING_TESTS =
 
diff --git a/test/regress/regress0/strings/fmf001.smt2 b/test/regress/regress0/strings/fmf001.smt2
new file mode 100644
index 000000000..a8874b59f
--- /dev/null
+++ b/test/regress/regress0/strings/fmf001.smt2
@@ -0,0 +1,19 @@
+(set-logic QF_S)

+(set-option :fmf-strings true)

+(set-info :status sat)

+

+(declare-fun x () String)

+(declare-fun y () String)

+

+(assert (str.in.re x

+		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))

+	))

+

+(assert (str.in.re y

+		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))

+	))

+

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

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

+

+(check-sat)

diff --git a/test/regress/regress0/strings/fmf002.smt2 b/test/regress/regress0/strings/fmf002.smt2
new file mode 100644
index 000000000..14f50c710
--- /dev/null
+++ b/test/regress/regress0/strings/fmf002.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_S)

+(set-option :fmf-strings true)

+(set-info :status sat)

+

+(declare-fun x () String)

+(declare-fun y () String)

+(declare-fun z () String)

+

+(assert (str.in.re x

+                (re.+ (re.range "a" "c"))

+				                ))

+

+(assert (= x (str.++ y "c" z "b")))

+(assert (> (str.len z) 1))

+

+(check-sat)

diff --git a/test/regress/regress0/strings/loop005.smt2 b/test/regress/regress0/strings/loop005.smt2
index 4401ef794..039409ea6 100644
--- a/test/regress/regress0/strings/loop005.smt2
+++ b/test/regress/regress0/strings/loop005.smt2
@@ -5,11 +5,13 @@
 (declare-fun y () String)
 (declare-fun z () String)
 (declare-fun w () String)
-(declare-fun w1 () String)
-(declare-fun w2 () String)
 
-(assert (= (str.++ x y z) (str.++ x z y)))
-(assert (= (str.++ x w z) (str.++ x z w)))
+;(assert (= (str.++ x y z) (str.++ x z y)))
+;(assert (= (str.++ x w z) (str.++ x z w)))
+
+(assert (= (str.++ y z) (str.++ z y)))
+(assert (= (str.++ w z) (str.++ z w)))
+
 (assert (not (= y w)))
 (assert (> (str.len z) 0))
 
diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2
index bea4037d1..b292de512 100644
--- a/test/regress/regress0/strings/loop007.smt2
+++ b/test/regress/regress0/strings/loop007.smt2
@@ -5,6 +5,7 @@
 (declare-fun y () String)
 
 (assert (= (str.++ x y "aa") (str.++ "aa" y x)))
-(assert (= (str.len x) 1))
+(assert (= (str.len x) (* 2 (str.len y))))
+(assert (> (str.len x) 0))
 
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/strings/loop008.smt2 b/test/regress/regress0/strings/loop008.smt2
new file mode 100644
index 000000000..91ed8cdf0
--- /dev/null
+++ b/test/regress/regress0/strings/loop008.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_S)

+(set-info :status sat)

+

+(declare-fun x () String)

+

+(assert (= (str.++ x "ab") (str.++ "ba" x)))

+(assert (> (str.len x) 5))

+

+(check-sat)

diff --git a/test/regress/regress0/strings/loop009.smt2 b/test/regress/regress0/strings/loop009.smt2
new file mode 100644
index 000000000..41eab0f35
--- /dev/null
+++ b/test/regress/regress0/strings/loop009.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_S)

+(set-info :status sat)

+

+(declare-fun x () String)

+

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

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

+

+(check-sat)

diff --git a/test/regress/regress0/strings/regexp001.smt2 b/test/regress/regress0/strings/regexp001.smt2
new file mode 100644
index 000000000..41aefbd41
--- /dev/null
+++ b/test/regress/regress0/strings/regexp001.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_S)

+(set-info :status sat)

+

+(declare-fun x () String)

+

+(assert (str.in.re x

+		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))

+	))

+

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

+

+(check-sat)

diff --git a/test/regress/regress0/strings/regexp002.smt2 b/test/regress/regress0/strings/regexp002.smt2
new file mode 100644
index 000000000..e2a44a9ab
--- /dev/null
+++ b/test/regress/regress0/strings/regexp002.smt2
@@ -0,0 +1,19 @@
+(set-logic QF_S)

+(set-info :status sat)

+

+(declare-fun x () String)

+(declare-fun y () String)

+

+(assert (str.in.re x

+		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))

+	))

+

+(assert (str.in.re y

+		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))

+	))

+

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

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

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

+

+(check-sat)

diff --git a/test/regress/regress0/strings/str006.smt2 b/test/regress/regress0/strings/str006.smt2
new file mode 100644
index 000000000..592ef6a7f
--- /dev/null
+++ b/test/regress/regress0/strings/str006.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_S)

+(set-info :status sat)

+

+(declare-fun x () String)

+(declare-fun y () String)

+(declare-fun z () String)

+

+;plandowski p469 1

+(assert (= (str.++ x "ab" y) (str.++ y "ba" z)))

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

+(assert (not (= (str.++ x "a") (str.++ "a" x))))

+

+(check-sat)

+