diff options
| -rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 9 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/issue6681-split-eq-strip-l.smt2 | 8 |
3 files changed, 14 insertions, 4 deletions
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 7ef1242c6..f63b416ff 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -437,7 +437,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) size_t startRhs = 0; for (size_t i = 0, size0 = v0.size(); i <= size0; i++) { - std::vector<Node> pfxv0(v0.begin(), v0.begin() + i); + const std::vector<Node> pfxv0(v0.begin(), v0.begin() + i); Node pfx0 = utils::mkConcat(pfxv0, stype); for (size_t j = startRhs, size1 = v1.size(); j <= size1; j++) { @@ -502,21 +502,22 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) // Example: // (= (str.++ x "AB" z) (str.++ "A" x y)) ---> // (and (= (str.++ x "A") (str.++ "A" x)) (= (str.++ "B" z) y)) + std::vector<Node> sfxv0 = pfxv0; std::vector<Node> rpfxv0; if (StringsEntail::stripSymbolicLength( - pfxv0, rpfxv0, 1, lenPfx1, true)) + sfxv0, rpfxv0, 1, lenPfx1, true)) { // The rewrite requires the full right-hand prefix length to be // stripped (otherwise we would have to keep parts of the // right-hand prefix). if (lenPfx1.isConst() && lenPfx1.getConst<Rational>().isZero()) { - pfxv0.insert(pfxv0.end(), v0.begin() + i, v0.end()); + sfxv0.insert(sfxv0.end(), v0.begin() + i, v0.end()); std::vector<Node> sfxv1(v1.begin() + j, v1.end()); Node ret = nm->mkNode(kind::AND, utils::mkConcat(rpfxv0, stype).eqNode(pfx1), - utils::mkConcat(pfxv0, stype) + utils::mkConcat(sfxv0, stype) .eqNode(utils::mkConcat(sfxv1, stype))); return returnRewrite(node, ret, Rewrite::SPLIT_EQ_STRIP_L); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 707e5e43d..237ca77dd 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1156,6 +1156,7 @@ set(regress_0_tests regress0/strings/issue6560-indexof-reduction.smt2 regress0/strings/issue6604-re-elim.smt2 regress0/strings/issue6643-ctn-decompose-conflict.smt2 + regress0/strings/issue6681-split-eq-strip-l.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue6681-split-eq-strip-l.smt2 b/test/regress/regress0/strings/issue6681-split-eq-strip-l.smt2 new file mode 100644 index 000000000..213d9737b --- /dev/null +++ b/test/regress/regress0/strings/issue6681-split-eq-strip-l.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun c () String) +(declare-fun d () String) +(assert (= (str.++ "A" a "CBA" b "BA" d) (str.++ b "BA" d a "CBA" c))) +(set-info :status sat) +(check-sat) |