Hotfix for substr function.

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 5bf44dce8d8623c2426a8306ce291a1e22a2c65a..b5e741edd1ed882cc28b9248fa77a44f878d00c5 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -866,15 +866,15 @@ 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_TOTAL) {
+    } else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) {
         retNode = node[0][2];
-    }*/ else if(node[0].getKind() == kind::STRING_CONCAT) {
+    } else if(node[0].getKind() == kind::STRING_CONCAT) {
       Node tmpNode = rewriteConcatString(node[0]);
       if(tmpNode.isConst()) {
         retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) );
-      } /*else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) {
-      retNode = tmpNode[2];
-      }*/ else {
+      } else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) {
+        retNode = tmpNode[2];
+      } else {
         // it has to be string concat
         std::vector<Node> node_vec;
         for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) {