diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-22 09:55:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-22 09:55:31 -0500 |
| commit | b58bdc9c5672430cf15914c64129136b24050152 (patch) | |
| tree | 5c58e1834c49feafa46602634bf4e838acee7e67 /test/regress | |
| parent | b967cc5c8d84023c1b821c59b7bca736ffda6bed (diff) | |
Local substitutions for context-depdendent simplification in strings (#3204)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress2/strings/issue3203.smt2 | 17 |
2 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5579885c3..8fa0c2791 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1814,6 +1814,7 @@ set(regress_2_tests regress2/strings/cmu-disagree-0707-dd.smt2 regress2/strings/cmu-prereg-fmf.smt2 regress2/strings/cmu-repl-len-nterm.smt2 + regress2/strings/issue3203.smt2 regress2/strings/issue918.smt2 regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/norn-dis-0707-3.smt2 diff --git a/test/regress/regress2/strings/issue3203.smt2 b/test/regress/regress2/strings/issue3203.smt2 new file mode 100644 index 000000000..89c203889 --- /dev/null +++ b/test/regress/regress2/strings/issue3203.smt2 @@ -0,0 +1,17 @@ +(set-logic ALL_SUPPORTED) +(set-option :strings-exp true) +(set-info :status unsat) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun d () String) +(declare-fun e () String) +(declare-fun f () Int) +(declare-fun g () String) +(declare-fun h () String) +(assert (or + (not (= ( str.replace "B" ( str.at "A" f) "") "B")) + (not (= ( str.replace "B" ( str.replace "B" g "") "") + ( str.at ( str.replace ( str.replace a d "") "C" "") ( str.indexof "B" ( str.replace ( str.replace a d "") "C" "") 0)))))) +(assert (= a (str.++ (str.++ d "C") g))) +(assert (= b (str.++ e g))) +(check-sat) |