Clean up explanations involving string length. Add regression.

6 files changed, 94 insertions, 88 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ad1163d05..607552188 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -172,25 +172,21 @@ bool TheoryStrings::areDisequal( Node a, Node b ){
   }
 }
 
-Node TheoryStrings::getLengthTerm( Node t ) {
+Node TheoryStrings::getLengthExp( Node t, std::vector< Node >& exp, Node te ) {
+  Assert( areEqual( t, te ) );
   EqcInfo * ei = getOrMakeEqcInfo( t, false );
   Node length_term = ei ? ei->d_length_term : Node::null();
-  if( length_term.isNull()) {
+  if( length_term.isNull() ){
     //typically shouldnt be necessary
     length_term = t;
   }
-  Debug("strings") << "TheoryStrings::getLengthTerm" << t << std::endl;
-  return length_term;
+  Debug("strings") << "TheoryStrings::getLengthTerm " << t << " is " << length_term << std::endl;
+  addToExplanation( length_term, te, exp );
+  return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term ) );
 }
 
-Node TheoryStrings::getLength( Node t, bool use_t ) {
-  Node retNode;
-  if( use_t ){
-    retNode = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t );
-  } else {
-    retNode = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) );
-  }
-  return Rewriter::rewrite( retNode );
+Node TheoryStrings::getLength( Node t, std::vector< Node >& exp ) {
+  return getLengthExp( t, exp, t );
 }
 
 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -658,7 +654,7 @@ void TheoryStrings::checkReduction( Node atom, int pol, int effort ) {
         Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) );
         sendLemma( atom, eq, "POS-CTN" );
       }else{
-        // for STRING_SUBSTR, 
+        // for STRING_SUBSTR,
         //     STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL
         std::vector< Node > new_nodes;
         Node res = d_preproc.decompose( atom, new_nodes );
@@ -794,6 +790,7 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
   Trace("strings-pending") << "Assert pending fact : " << atom << " " << polarity << " from " << exp << std::endl;
   Assert(atom.getKind() != kind::OR, "Infer error: a split.");
   if( atom.getKind()==kind::EQUAL ){
+    Trace("strings-pending-debug") << "  Register term" << std::endl;
     //AJR : is this necessary?
     for( unsigned j=0; j<2; j++ ) {
       if( !d_equalityEngine.hasTerm( atom[j] ) && atom[j].getType().isString() ) {
@@ -801,7 +798,11 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
         registerTerm( atom[j] );
       }
     }
+    Trace("strings-pending-debug") << "  Now assert equality" << std::endl;
+    Trace("strings-pending-debug") << atom << std::endl;
+    Trace("strings-pending-debug") << Rewriter::rewrite( atom ) << std::endl;
     d_equalityEngine.assertEquality( atom, polarity, exp );
+    Trace("strings-pending-debug") << "  Finished assert equality" << std::endl;
   } else {
     if( atom.getKind()==kind::STRING_IN_REGEXP ) {
       if( d_ext_func_terms.find( atom )==d_ext_func_terms.end() ){
@@ -811,9 +812,11 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
     }
     d_equalityEngine.assertPredicate( atom, polarity, exp );
   }
+  Trace("strings-pending-debug") << "  Now collect terms" << std::endl;
   //collect extended function terms in the atom
   std::map< Node, bool > visited;
   collectExtendedFuncTerms( atom, visited );
+  Trace("strings-pending-debug") << "  Finished collect terms" << std::endl;
 }
 
 void TheoryStrings::doPendingFacts() {
@@ -1310,13 +1313,12 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
             //we're done
             //addNormalFormPair( normal_form_src[i], normal_form_src[j] );
           } else {
-            Node length_term_i = getLength( normal_forms[i][index_i] );
-            Node length_term_j = getLength( normal_forms[j][index_j] );
+            std::vector< Node > lexp;
+            Node length_term_i = getLength( normal_forms[i][index_i], lexp );
+            Node length_term_j = getLength( normal_forms[j][index_j], lexp );
             //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 ) {
+            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 );
               Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl;
@@ -1329,8 +1331,8 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
               Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl;
               int loop_in_i = -1;
               int loop_in_j = -1;
-              if(detectLoop(normal_forms, i, j, index_i, index_j, loop_in_i, loop_in_j)) {
-                if(!flag_lb) {
+              if( detectLoop(normal_forms, i, j, index_i, index_j, loop_in_i, loop_in_j) ){
+                if( !flag_lb ){
                   c_i = i;
                   c_j = j;
                   c_loop_n_index = loop_in_i!=-1 ? i : j;
@@ -1354,8 +1356,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                 Node conc;
                 std::vector< Node > antec;
                 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) {
+                if( normal_forms[i][index_i].getKind() == kind::CONST_STRING || normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
                   unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j;
                   unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j;
                   unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i;
@@ -1508,29 +1509,21 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
         index_i++;
         success = true;
       } else {
-        Node length_term_i = getLength( normal_forms[i][index_i] );
-        Node length_term_j = getLength( normal_forms[j][index_j] );
+        std::vector< Node > temp_exp;
+        Node length_term_i = getLength( normal_forms[i][index_i], temp_exp );
+        Node length_term_j = getLength( normal_forms[j][index_j], temp_exp );
         //check  length(normal_forms[i][index]) == length(normal_forms[j][index])
-        if( areEqual(length_term_i, length_term_j) ) {
+        if( areEqual( length_term_i, length_term_j ) ){
           Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl;
           Node eq = normal_forms[i][index_i].eqNode( normal_forms[j][index_j] );
           //eq = Rewriter::rewrite( eq );
           Node length_eq = length_term_i.eqNode( 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);
-          //must add explanation for length terms
-          if( !normal_forms[i][index_i].isConst() && !length_term_i.isConst() && length_term_i[0]!=normal_forms[i][index_i] ){
-            temp_exp.push_back( length_term_i[0].eqNode( normal_forms[i][index_i] ) );
-          }
-          if( !normal_forms[j][index_j].isConst() && !length_term_j.isConst() && length_term_j[0]!=normal_forms[j][index_j] ){
-            temp_exp.push_back( length_term_j[0].eqNode( normal_forms[j][index_j] ) );
-          }
-          Node eq_exp = mkAnd( temp_exp );
-          sendInfer( eq_exp, eq, "LengthEq" );
+          sendInfer( mkAnd( temp_exp ), eq, "LengthEq" );
           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 ) ) {
+        }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") << "Simple Case 3 : at endpoint" << std::endl;
           Node conc;
           std::vector< Node > antec;
@@ -1716,8 +1709,9 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
         Trace("strings-solve-debug")  << "...Processing(DEQ) " << i << " " << j << std::endl;
         if( !areEqual( i, j ) ) {
           Assert( i.getKind()!=kind::CONST_STRING || j.getKind()!=kind::CONST_STRING );
-          Node li = getLength( i );
-          Node lj = getLength( j );
+          std::vector< Node > lexp;
+          Node li = getLength( i, lexp );
+          Node lj = getLength( j, lexp );
           if( areDisequal(li, lj) ){
             //if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
 
@@ -1740,9 +1734,9 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
             Node sk3 = mkSkolemCached( i, j, sk_id_deq_z, "z_dsplit", 1 );
             //Node nemp = sk3.eqNode(d_emptyString).negate();
             //conc.push_back(nemp);
-            Node lsk1 = getLength( sk1 );
+            Node lsk1 = mkLength( sk1 );
             conc.push_back( lsk1.eqNode( li ) );
-            Node lsk2 = getLength( sk2 );
+            Node lsk2 = mkLength( sk2 );
             conc.push_back( lsk2.eqNode( lj ) );
             conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
             sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" );
@@ -1794,11 +1788,9 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
       Trace("strings-solve-debug") << "Disequality normalize empty" << std::endl;
       std::vector< Node > ant;
       //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
-      Node lni = getLength( ni );
-      Node lnj = getLength( nj );
+      Node lni = getLengthExp( ni, ant, d_normal_forms_base[ni] );
+      Node lnj = getLengthExp( nj, ant, d_normal_forms_base[nj] );
       ant.push_back( lni.eqNode( lnj ) );
-      ant.push_back( getLengthTerm( ni ).eqNode( d_normal_forms_base[ni] ) );
-      ant.push_back( getLengthTerm( nj ).eqNode( d_normal_forms_base[nj] ) );
       ant.insert( ant.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
       ant.insert( ant.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
       std::vector< Node > cc;
@@ -1844,8 +1836,9 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
             return 1;
           }
         } else {
-          Node li = getLength( i );
-          Node lj = getLength( j );
+          std::vector< Node > lexp;
+          Node li = getLength( i, lexp );
+          Node lj = getLength( j, lexp );
           if( areEqual( li, lj ) && areDisequal( i, j ) ) {
             Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i << " " << j << std::endl;
             //we are done: D-Remove
@@ -2117,6 +2110,10 @@ Node TheoryStrings::mkConcat( const std::vector< Node >& c ) {
   return Rewriter::rewrite( c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ) );
 }
 
+Node TheoryStrings::mkLength( Node t ) {
+  return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t ) );
+}
+
 //isLenSplit: 0-yes, 1-no, 2-ignore
 Node TheoryStrings::mkSkolemS( const char *c, int isLenSplit ) {
   Node n = NodeManager::currentNM()->mkSkolem( c, NodeManager::currentNM()->stringType(), "string sko" );
@@ -2338,7 +2335,8 @@ void TheoryStrings::checkFlatForms() {
               }else{
                 Node curr = d_flat_form[a][count];
                 Node curr_c = d_eqc_to_const[curr];
-                Node lcurr = getLength( curr );
+                std::vector< Node > lexp;
+                Node lcurr = getLength( curr, lexp );
                 for( unsigned i=1; i<it->second.size(); i++ ){
                   b = it->second[i];
                   if( std::find( inelig.begin(), inelig.end(), b )==inelig.end() ){
@@ -2382,16 +2380,12 @@ void TheoryStrings::checkFlatForms() {
                           break;
                         }else{
                           //if lengths are the same, apply LengthEq
-                          Node lcc = getLength( cc );
+                          Node lcc = getLength( cc, lexp );
                           if( areEqual( lcurr, lcc ) ){
+                            Trace("strings-ff-debug") << "Infer " << ac << " == " << bc << " since " << lcurr << " == " << lcc << std::endl;
                             //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) );
+                            exp.insert( exp.end(), lexp.begin(), lexp.end() );
                             addToExplanation( lcurr, lcc, exp );
-                            if( !lcc.isConst() ){
-                              addToExplanation( bc, lcc[0], exp );
-                            }
-                            if( !lcurr.isConst() ){
-                              addToExplanation( ac, lcurr[0], exp );
-                            }
                             conc = ac.eqNode( bc );
                             inf_type = 1;
                             break;
@@ -2485,12 +2479,8 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto
               Node ncy = checkCycles( nr, curr, exp );
               if( !ncy.isNull() ){
                 Trace("strings-cycle") << eqc << " cycle: " << ncy << " at " << n << "[" << i << "] : " << n[i] << std::endl;
-                if( n!=eqc ){
-                  exp.push_back( n.eqNode( eqc ) );
-                }
-                if( nr!=n[i] ){
-                  exp.push_back( nr.eqNode( n[i] ) );
-                }
+                addToExplanation( n, eqc, exp );
+                addToExplanation( nr, n[i], exp );
                 if( ncy==eqc ){
                   //can infer all other components must be empty
                   for( unsigned j=0; j<n.getNumChildren(); j++ ){
@@ -2529,8 +2519,10 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto
 
 void TheoryStrings::checkNormalForms() {
   // simple extended func reduction
+  Trace("strings-process") << "Check extended function reduction effort=1..." << std::endl;
   checkExtfReduction( 1 );
-  if( !hasProcessed() ){  
+  Trace("strings-process") << "Done check extended function reduction" << std::endl;
+  if( !hasProcessed() ){
     Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
     //calculate normal forms for each equivalence class, possibly adding splitting lemmas
     d_normal_forms.clear();
@@ -2658,7 +2650,7 @@ void TheoryStrings::checkLengthsEqc() {
                 Node pv = (*it).second;
                 Assert( d_proxy_var_to_length.find( pv )!=d_proxy_var_to_length.end() );
                 Node pvl = d_proxy_var_to_length[pv];
-                Node ceq = Rewriter::rewrite( getLength( pv, true ).eqNode( pvl ) );
+                Node ceq = Rewriter::rewrite( mkLength( pv ).eqNode( pvl ) );
                 sendLemma( d_true, ceq, "LEN-NORM-I" );
               }
             }
@@ -3911,10 +3903,10 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) {
         to_reduce = n;
       }
       if( !to_reduce.isNull() ){
-        checkExtfInference( n, to_reduce, effort );
         if( effort==1 ){
           Trace("strings-extf") << "  cannot rewrite extf : " << to_reduce << std::endl;
         }
+        checkExtfInference( n, to_reduce, effort );
         if( Trace.isOn("strings-extf-list") ){
           Trace("strings-extf-list") << "  * " << to_reduce;
           if( d_extf_pol[n]!=0 ){
@@ -3957,7 +3949,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, int effort ){
         }
       }else{
         //store this (reduced) assertion
-        Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) );
+        //Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) );
         bool pol = n_pol==1;
         if( std::find( d_extf_info[nr[0]].d_ctn[pol].begin(), d_extf_info[nr[0]].d_ctn[pol].end(), nr[1] )==d_extf_info[nr[0]].d_ctn[pol].end() ){
           Trace("strings-extf-debug") << "  store contains info : " << nr[0] << " " << pol << " " << nr[1] << std::endl;
@@ -4089,22 +4081,23 @@ void TheoryStrings::checkNegContains( std::vector< Node >& negContains ) {
       Node atom = negContains[i];
       Node x = atom[0];
       Node s = atom[1];
-      Node lenx = getLength(x);
-      Node lens = getLength(s);
+      std::vector< Node > lexp;
+      Node lenx = getLength( x, lexp );
+      Node lens = getLength( s, lexp );
       if( areEqual(lenx, lens) ){
         if(d_neg_ctn_eqlen.find(atom) == d_neg_ctn_eqlen.end()) {
-          Node eq = lenx.eqNode(lens);
-          Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), eq ) );
+          lexp.push_back( lenx.eqNode(lens) );
+          lexp.push_back( atom.negate() );
           Node xneqs = x.eqNode(s).negate();
           d_neg_ctn_eqlen.insert( atom );
-          sendLemma( antc, xneqs, "NEG-CTN-EQL" );
+          sendLemma( mkExplain( lexp ), xneqs, "NEG-CTN-EQL" );
         }
-      }else if( !areDisequal(lenx, lens) ){
+      }else if( !areDisequal( lenx, lens ) ){
         if(d_neg_ctn_ulen.find(atom) == d_neg_ctn_ulen.end()) {
           lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
           lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
           d_neg_ctn_ulen.insert( atom );
-          sendSplit(lenx, lens, "NEG-CTN-SP");
+          sendSplit( lenx, lens, "NEG-CTN-SP" );
         }
       }else{
         if(d_neg_ctn_cached.find(atom) == d_neg_ctn_cached.end()) {
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 52bc37cb8..721ba864e 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -133,8 +133,9 @@ private:
   bool hasTerm( Node a );
   bool areEqual( Node a, Node b );
   bool areDisequal( Node a, Node b );
-  Node getLengthTerm( Node t );
-  Node getLength( Node t, bool use_t = false );
+  // t is representative, te = t, add lt = te to explanation exp
+  Node getLengthExp( Node t, std::vector< Node >& exp, Node te );
+  Node getLength( Node t, std::vector< Node >& exp );
 
 private:
   /** The notify class */
@@ -300,7 +301,7 @@ private:
   void checkLengthsEqc();
   //cardinality check
   void checkCardinality();
-  
+
 public:
   /** preregister term */
   void preRegisterTerm(TNode n);
@@ -323,7 +324,7 @@ public:
 protected:
   /** compute care graph */
   void computeCareGraph();
-  
+
   //do pending merges
   void assertPendingFact(Node atom, bool polarity, Node exp);
   void doPendingFacts();
@@ -331,7 +332,7 @@ protected:
   bool hasProcessed();
   void addToExplanation( Node a, Node b, std::vector< Node >& exp );
   void addToExplanation( Node lit, std::vector< Node >& exp );
-  
+
   //register term
   bool registerTerm( Node n );
   //send lemma
@@ -343,6 +344,7 @@ protected:
   inline Node mkConcat( Node n1, Node n2 );
   inline Node mkConcat( Node n1, Node n2, Node n3 );
   inline Node mkConcat( const std::vector< Node >& c );
+  inline Node mkLength( Node n );
   //mkSkolem
   inline Node mkSkolemS(const char * c, int isLenSplit = 0);
   //inline Node mkSkolemI(const char * c);
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index ccce5a86d..80eb89cc3 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -113,20 +113,20 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     //length is positive
     Node c3 = NodeManager::currentNM()->mkNode( kind::GT, t[2], d_zero );
     Node cond = NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3 );
-    
+
     Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for substr" );
     Node sk2 = NodeManager::currentNM()->mkSkolem( "ss2", NodeManager::currentNM()->stringType(), "created for substr" );
     Node b11 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk2 ) );
     //length of first skolem is second argument
     Node b12 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ).eqNode( t[1] );
     //length of second skolem is abs difference between end point and end of string
-    Node b13 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ).eqNode( 
-                 NodeManager::currentNM()->mkNode( kind::ITE, NodeManager::currentNM()->mkNode( kind::GEQ, lt0, t12 ), 
+    Node b13 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ).eqNode(
+                 NodeManager::currentNM()->mkNode( kind::ITE, NodeManager::currentNM()->mkNode( kind::GEQ, lt0, t12 ),
                     NodeManager::currentNM()->mkNode( kind::MINUS, lt0, t12 ), d_zero ) );
-    
+
     Node b1 = NodeManager::currentNM()->mkNode( kind::AND, b11, b12, b13 );
     Node b2 = t.eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );
-    
+
     Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, b1, b2 ) );
     new_nodes.push_back( lemma );
     d_cache[t] = t;
@@ -488,7 +488,7 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
   unsigned num = t.getNumChildren();
   if(num == 0) {
     return simplify(t, new_nodes);
-  } else {
+  }else{
     bool changed = false;
     std::vector< Node > cc;
     if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 168606462..6d84ace90 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1025,8 +1025,6 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
   } else if(node.getKind() == kind::STRING_LENGTH) {
     if(node[0].isConst()) {
       retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) );
-    } else if(node[0].getKind() == kind::STRING_SUBSTR) {
-      //retNode = node[0][2];
     } else if(node[0].getKind() == kind::STRING_CONCAT) {
       Node tmpNode = rewriteConcatString(node[0]);
       if(tmpNode.isConst()) {
@@ -1054,6 +1052,8 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
         }
       }
     }
+    //else if(node[0].getKind() == kind::STRING_SUBSTR) {
+    //retNode = node[0][2];
   }else if( node.getKind() == kind::STRING_CHARAT ){
     Node one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
     retNode = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[0], node[1], one);
@@ -1080,7 +1080,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                 retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
               }else{
                 children.erase( children.begin(), children.begin()+1 );
-                retNode = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, mkConcat( kind::STRING_CONCAT, children ), 
+                retNode = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, mkConcat( kind::STRING_CONCAT, children ),
                                                             NodeManager::currentNM()->mkNode( kind::MINUS, node[1], NodeManager::currentNM()->mkConst( size ) ),
                                                             node[2] );
               }
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 4d1da2efb..f5c6048e6 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -73,7 +73,8 @@ TESTS = \
   bug686dd.smt2 \
   idof-handg.smt2 \
   fmf001.smt2 \
-  type002.smt2
+  type002.smt2 \
+  crash-1019.smt2
 
 FAILING_TESTS =
 
diff --git a/test/regress/regress0/strings/crash-1019.smt2 b/test/regress/regress0/strings/crash-1019.smt2
new file mode 100755
index 000000000..1a41ba715
--- /dev/null
+++ b/test/regress/regress0/strings/crash-1019.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL_SUPPORTED)

+(set-option :strings-exp true)

+(set-option :rewrite-divk true)

+(set-info :status unsat)

+ 

+(declare-fun s () String)

+ 

+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (= (str.++ (str.replace (str.substr s 0 (- (+ (str.indexof s "o" 0) 1) 0)) "o" "a") (str.++ (str.replace (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) 0 (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) "o" "a") (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))))) "faa") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) "o") 1 0) 0)))) (not (= (ite (str.contains (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o") 1 0) 0))) (not (= (ite (str.contains s "o") 1 0) 0))) (>= 0 0)) (> (- (+ (str.indexof s "o" 0) 1) 0) 0)) (> (str.len s) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= 0 0)) (> (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))))

+ 

+(check-sat)