diff options
| -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); |