diff options
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
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) { |