diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-15 13:31:04 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-15 13:31:04 -0700 |
commit | 8337f548b12dfb2a9e58942d50f00baae8ca9ad5 (patch) | |
tree | da7a3ebbbc31cc74405c8757128a4e5e9e5fe1c9 | |
parent | 74dc5dafba5f4b316944c12371836102accc904d (diff) |
Address commentlengthPreserve
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
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<Node> normNrChildren; getConcat(normNr, normNrChildren); |