diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-10 12:32:19 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-10 18:32:19 +0000 |
| commit | 132504c9f255fdb2c31b9a43bb3b9513db41afc1 (patch) | |
| tree | 2cfa7969467b77b911bba8fdbf80bc4e1e5866a8 /test | |
| parent | cdcdd49a79ba03966cbb29c4f380f426c95a7d3a (diff) | |
Fix extended equality rewrite involving replace. (#6104)
Fixes #6075.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6075-repl-len-one-rr.smt2 | 8 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 147019108..30cdf43d9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2033,6 +2033,7 @@ set(regress_1_tests regress1/strings/issue5692-infer-proxy.smt2 regress1/strings/issue5940-skc-len-conc.smt2 regress1/strings/issue5940-2-skc-len-conc.smt2 + regress1/strings/issue6075-repl-len-one-rr.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue6075-repl-len-one-rr.smt2 b/test/regress/regress1/strings/issue6075-repl-len-one-rr.smt2 new file mode 100644 index 000000000..f60fe9168 --- /dev/null +++ b/test/regress/regress1/strings/issue6075-repl-len-one-rr.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(declare-fun x () String) +(declare-fun y () String) +(assert (str.< x (str.replace "" (str.++ (str.replace "B" x "") +(str.replace "B" (str.replace "B" x "") "")) y))) +(check-sat) |