diff options
Diffstat (limited to 'test/regress/regress1/strings/issue6203-1-substr-ctn-strip.smt2')
| -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) |