From 94943076044eb21793c2cb6d202e8dd9eb9e184e Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 27 Jul 2021 04:57:02 -0700 Subject: [PATCH] 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. --- test/regress/CMakeLists.txt | 1 + test/regress/regress2/strings/issue6639-replace-re-all.smt2 | 6 ++++++ 2 files changed, 7 insertions(+) create mode 100644 test/regress/regress2/strings/issue6639-replace-re-all.smt2 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) -- 2.30.2