From b80720f15170b02cbc93a53095ec2dd96bb8029c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 22 Mar 2019 03:48:56 +0000 Subject: Fix stripConstantEndpoints in strings rewriter (#2883) `TheoryStringsRewriter::stripConstantEndpoints()` returns the stripped endpoints in the vectors `nb` and `ne`. These endpoints were not computed correctly if string literal had to be split. For example: ``` stripConstantEndpoints({ "ABC" }, { "C" }, {}, {}, 1) ``` returned `true` and only "A" for `nb` (instead of "AB") because we mistakenly used the amount of overlap between "ABC" and "C" (which is one) for the length of the stripped prefix. This commit fixes the issue and adds several unit tests. --- src/theory/strings/theory_strings_rewriter.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/theory') diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 79667b9aa..0763fa7d5 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -3613,6 +3613,8 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector& n1, { Assert(nb.empty()); Assert(ne.empty()); + + NodeManager* nm = NodeManager::currentNM(); bool changed = false; // for ( forwards, backwards ) direction for (unsigned r = 0; r < 2; r++) @@ -3693,15 +3695,13 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector& n1, // component if (r == 0) { - nb.push_back( - NodeManager::currentNM()->mkConst(s.prefix(overlap))); - n1[index0] = NodeManager::currentNM()->mkConst(s.suffix(overlap)); + nb.push_back(nm->mkConst(s.prefix(s.size() - overlap))); + n1[index0] = nm->mkConst(s.suffix(overlap)); } else { - ne.push_back( - NodeManager::currentNM()->mkConst(s.suffix(overlap))); - n1[index0] = NodeManager::currentNM()->mkConst(s.prefix(overlap)); + ne.push_back(nm->mkConst(s.suffix(s.size() - overlap))); + n1[index0] = nm->mkConst(s.prefix(overlap)); } } } -- cgit v1.2.3