From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Tue, 28 Jul 2015 01:16:41 +0000 (-0500)
Subject: Hotfix for substr function.
X-Git-Tag: cvc5-1.0.0~6268
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9f10a95e26e9e790a19a6f9e68a658ec2ab6d304;p=cvc5.git

Hotfix for substr function.
---

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 5bf44dce8..b5e741edd 100644
--- 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) {