From 8337f548b12dfb2a9e58942d50f00baae8ca9ad5 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 15 Jun 2018 13:31:04 -0700 Subject: Address comment --- src/theory/strings/theory_strings_rewriter.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index e69222df4..60bfe6ad5 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2029,8 +2029,9 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { // For example: // str.indexof(str.++("ABCD", x), y, 3) ---> // str.indexof(str.++("AAAD", x), y, 3) - Node normNr = lengthPreserveRewrite(mkConcat(kind::STRING_CONCAT, nr)); - if (normNr != mkConcat(kind::STRING_CONCAT, nr)) + Node nodeNr = mkConcat(kind::STRING_CONCAT, nr); + Node normNr = lengthPreserveRewrite(nodeNr); + if (normNr != nodeNr) { std::vector normNrChildren; getConcat(normNr, normNrChildren); -- cgit v1.2.3