diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-02 10:01:07 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-02 10:01:07 -0700 |
| commit | adb0ca274a1294e251fa5bca030ad54406fe26df (patch) | |
| tree | ae4df4998a18e1d22b7cd371b243b809a4eaffdf /test/regress/regress0/strings/issue6643-ctn-decompose-conflict.smt2 | |
| parent | 5f827e53d2dcd80a3cc679454de0b40108f01d93 (diff) | |
| parent | 338982182dbdabecf6f3b06e659621cf43bed916 (diff) | |
Merge branch 'master' into issue6661
Diffstat (limited to 'test/regress/regress0/strings/issue6643-ctn-decompose-conflict.smt2')
| -rw-r--r-- | test/regress/regress0/strings/issue6643-ctn-decompose-conflict.smt2 | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/issue6643-ctn-decompose-conflict.smt2 b/test/regress/regress0/strings/issue6643-ctn-decompose-conflict.smt2 new file mode 100644 index 000000000..41a515640 --- /dev/null +++ b/test/regress/regress0/strings/issue6643-ctn-decompose-conflict.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-fun y () String) +(declare-fun z () String) +(assert (not (= (str.contains y (str.replace "A" "" z)) (str.contains y "A")))) +(set-info :status sat) +(check-sat) |