summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-06-17 01:22:16 -0700
committerAndres Noetzli <andres.noetzli@gmail.com>2018-06-17 01:22:16 -0700
commit9c88dcb765bc94290f9d79221f49ce8fcf670898 (patch)
treece0dfc89ea0a9f9ac0e396b3364968e5f513b50e
parent501fde6c962aa0cb42c5e41695f4cf0952b6a15f (diff)
address commentreplSubst
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 6aad3bacc..4d57ccba1 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2224,9 +2224,9 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
Node lastChild1 = children1[children1.size() - 1];
if (lastChild1.getKind() == kind::STRING_SUBSTR)
{
- // (str.replace x (str.++ ... (str.substr y i j)) z) --->
- // (str.replace x (str.++ ...
- // (str.substr y i (+ (str.len x) 1 (- (str.len ...))))) z)
+ // (str.replace x (str.++ t (str.substr y i j)) z) --->
+ // (str.replace x (str.++ t
+ // (str.substr y i (+ (str.len x) 1 (- (str.len t))))) z)
// if j > len(x)
children1.pop_back();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback