diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-03 13:21:55 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-03 13:21:55 -0500 |
| commit | 69b463e1b1150715b2f4179786ddab8ba0c43b37 (patch) | |
| tree | e3c1dcb7d32dc0dbb3dd159cc37ab92371bc9ce3 /test/regress/regress1/strings | |
| parent | fba1437c772b6733ce678b93b5ef7d95e366c82d (diff) | |
Disable substring component contains in strip endpoints (#6266)
Fixes the first benchmark from #6203.
Diffstat (limited to 'test/regress/regress1/strings')
| -rw-r--r-- | test/regress/regress1/strings/issue6203-1-substr-ctn-strip.smt2 | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/issue6203-1-substr-ctn-strip.smt2 b/test/regress/regress1/strings/issue6203-1-substr-ctn-strip.smt2 new file mode 100644 index 000000000..dde9c8210 --- /dev/null +++ b/test/regress/regress1/strings/issue6203-1-substr-ctn-strip.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --strings-exp -q +; EXPECT: sat +(set-logic ALL) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun c () String) +(declare-fun d () String) +(declare-fun e () String) +(assert (or (= (str.++ c (str.substr e (* (mod 0 0) (str.len b)) (str.len d))) "ab") (= (str.++ c (str.substr e (* (mod 0 0) (str.len b)) (str.len d))) ""))) +(assert (= (str.len c) (+ (str.len e) (* (str.indexof a "a" 0) (str.len b))) 1 (str.len b))) +(check-sat) |