diff options
Diffstat (limited to 'src/theory/strings/sequences_rewriter.cpp')
| -rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index d8b8765eb..46ed5ac80 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -2992,6 +2992,14 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n) Node retNode = n[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, n[1], val, lens)); + NodeManager* nm = NodeManager::currentNM(); + retNode = + nm->mkNode(AND, + retNode, + nm->mkNode(STRING_LENGTH, + nm->mkNode(kind::STRING_SUBSTR, n[1], val, lens)) + .eqNode(lens)); + return returnRewrite(n, retNode, Rewrite::SUF_PREFIX_ELIM); } |