From 9f10a95e26e9e790a19a6f9e68a658ec2ab6d304 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 27 Jul 2015 20:16:41 -0500 Subject: [PATCH] Hotfix for substr function. --- src/theory/strings/theory_strings_rewriter.cpp | 10 +++++----- 1 file 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().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().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_vec; for(unsigned int i=0; i