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 22a2223694e36034389f7169ba142390141dd01e..151e0108887df280c4f62e6c3622b82db23d9911 100644 (file)
--- 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 (file)
index 0000000..2384f82
--- /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)