validLen,
nm->mkNode(STRING_IN_REGEXP, nm->mkNode(STRING_SUBSTR, s, skk, l), r));
// skk != -1 =>
- // exists l. (0 <= l < len(s) - skk) ^ in_re(substr(s, skk, l), r))
- Node match =
- nm->mkNode(OR,
- retNegOne,
- utils::mkForallInternal(bvll, matchBody.negate()).negate());
+ // skk >= n ^ exists l. (0 <= l < len(s) - skk) ^ in_re(substr(s, skk, l),
+ // r))
+ Node match = nm->mkNode(
+ OR,
+ retNegOne,
+ nm->mkNode(AND,
+ nm->mkNode(GEQ, skk, n),
+ utils::mkForallInternal(bvll, matchBody.negate()).negate()));
// assert:
// IF: n > len(s) OR 0 > n
// n <= i < ite(skk = -1, len(s), skk) ^ 0 < l <= len(s) - i =>
// ~in_re(substr(s, i, l), r)) ^
// (skk != -1 =>
- // exists l. 0 <= l <= len(s) - skk ^ in_re(substr(s, skk, l), r))
+ // skk >= n ^ exists l. 0 <= l <= len(s) - skk ^ in_re(substr(s,
+ // skk, l), r))
//
// Note that this reduction relies on eager reduction lemmas being sent to
// properly limit the range of skk.
regress1/strings/issue6653-4-rre.smt2
regress1/strings/issue6653-rre.smt2
regress1/strings/issue6653-rre-small.smt2
+ regress1/strings/issue6654-indexof_re_red.smt2
regress1/strings/issue6766-re-elim-bv.smt2
regress1/strings/issue6777-seq-nth-eval-cm.smt2
regress1/strings/issue6913.smt2
--- /dev/null
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (= b (str.replace_re a (str.to_re "A") "A")))
+(assert (not (str.prefixof (str.++ b b) a)))
+(check-sat)