diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-02 00:36:42 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-02-02 00:36:42 -0800 |
commit | e374c7fbde3b3a5148b6e8fc302277b6e786965e (patch) | |
tree | bf1084d0080949b4352a5fa58221d02839519556 /src | |
parent | 546bf68640875107739011cff1f704f0d3e38f82 (diff) |
Fix corner case in stripConstantEndpoints (#2824)
`stripConstantEndpoints()` was returning `true` when the first argument
was a list only containing an empty string, which could lead to rewrite
loops. This commit checks for that case and adds a unit test for it.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 0c8d6ac8d..f90d5bcfd 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -3583,6 +3583,12 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1, unsigned index1 = r == 0 ? 0 : n2.size() - 1; bool removeComponent = false; Node n1cmp = n1[index0]; + + if (n1cmp.isConst() && n1cmp.getConst<String>().size() == 0) + { + return false; + } + std::vector<Node> sss; std::vector<Node> sls; n1cmp = decomposeSubstrChain(n1cmp, sss, sls); |