From: Andres Noetzli Date: Tue, 27 Jul 2021 11:57:02 +0000 (-0700) Subject: Add regression for fixed `str.indexof_re` issue (#6938) X-Git-Tag: cvc5-1.0.0~1446 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=94943076044eb21793c2cb6d202e8dd9eb9e184e;p=cvc5.git Add regression for fixed `str.indexof_re` issue (#6938) Fixes #6639. The issue cannot be reproduced on current master and git bisect suggests that commit adf497a fixed the issue. --- diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 22a222369..151e01088 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2506,6 +2506,7 @@ set(regress_2_tests regress2/strings/issue6057-replace-re-all-simplified.smt2 regress2/strings/issue6636-replace-re-all.smt2 regress2/strings/issue6637-replace-re-all.smt2 + regress2/strings/issue6639-replace-re-all.smt2 regress2/strings/issue918.smt2 regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/range-perf.smt2 diff --git a/test/regress/regress2/strings/issue6639-replace-re-all.smt2 b/test/regress/regress2/strings/issue6639-replace-re-all.smt2 new file mode 100644 index 000000000..2384f82ef --- /dev/null +++ b/test/regress/regress2/strings/issue6639-replace-re-all.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_SLIA) +(declare-fun a () String) +(assert (= a "")) +(assert (not (str.in_re (str.replace_re_all "b" (re.comp (str.to_re a)) "a") (str.to_re "a")))) +(set-info :status unsat) +(check-sat)