diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-03 17:41:40 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-04 00:41:40 +0000 |
| commit | adf497af7a3fc8b06b875eaf9feca2568d0ba9d8 (patch) | |
| tree | f544a1e6207bf76e998e1ba17bee44f5d46b87db /test/regress/CMakeLists.txt | |
| parent | b68e0636fb839142f1515fc8551ade09d3ed1a5d (diff) | |
Fix handling of start index in `str.indexof_re` (#6674)
Fixes #6636, fixes #6637. When the start index was non-zero, the result of
str.indexof_re was not properly restricted to be greater or equal to
the start index. This commit fixes the issue by making the eager
reduction lemma more precise. Additionally, the commit fixes an issue
with the lower bound of the length of the match in str.indexof_re.
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 860d1854a..6036b021b 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1120,6 +1120,7 @@ set(regress_0_tests regress0/strings/ilc-like.smt2 regress0/strings/indexof-sym-simp.smt2 regress0/strings/indexof_re.smt2 + regress0/strings/indexof_re-start-index.smt2 regress0/strings/is_digit_simple.smt2 regress0/strings/issue1189.smt2 regress0/strings/issue2958.smt2 @@ -2456,6 +2457,8 @@ set(regress_2_tests regress2/strings/issue6483.smt2 regress2/strings/issue6057-replace-re-all.smt2 regress2/strings/issue6057-replace-re-all-simplified.smt2 + regress2/strings/issue6636-replace-re-all.smt2 + regress2/strings/issue6637-replace-re-all.smt2 regress2/strings/issue918.smt2 regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/range-perf.smt2 |