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/regress0/strings | |
| 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/regress0/strings')
| -rw-r--r-- | test/regress/regress0/strings/indexof_re-start-index.smt2 | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/indexof_re-start-index.smt2 b/test/regress/regress0/strings/indexof_re-start-index.smt2 new file mode 100644 index 000000000..9f17c5bef --- /dev/null +++ b/test/regress/regress0/strings/indexof_re-start-index.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-fun i () Int) +(declare-fun a () String) +(assert (= i (str.indexof_re a (str.to_re "abc") 3))) +(assert (and (>= i 0) (< i 3))) +(set-info :status unsat) +(check-sat) |