Fix stripConstantEndpoints in strings rewriter (#2883)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 22 Mar 2019 03:48:56 +0000 (03:48 +0000)
committerGitHub <noreply@github.com>
Fri, 22 Mar 2019 03:48:56 +0000 (03:48 +0000)
commitb80720f15170b02cbc93a53095ec2dd96bb8029c
tree3dc2245110cf7f9e149a59e9250bc6ff1f4b66c7
parenta20702bcbb04422ddfcda5a241fd0cc0ec32edc8
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
test/unit/theory/theory_strings_rewriter_white.h