diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-18 17:59:38 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-18 22:59:38 +0000 |
| commit | 9547f16cd326b71a41e96a42d094170e426561a4 (patch) | |
| tree | 9b750734673b684d47a28486670723bf6a73449e /test/regress | |
| parent | 3609bd8a3ef60a0ed61927567f5321eb28365858 (diff) | |
Add regression for fixed issue (#7395)
Fixes #6653.
The third benchmark on that issue is no longer an issue, this adds it as a regression, which is the last open benchmark on the referenced issue.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6653-3-seq.smt2 | 10 |
2 files changed, 11 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 272867d0c..b1d776b21 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2207,6 +2207,7 @@ set(regress_1_tests regress1/strings/issue6604-2.smt2 regress1/strings/issue6635-rre.smt2 regress1/strings/issue6653-2-update-c-len.smt2 + regress1/strings/issue6653-3-seq.smt2 regress1/strings/issue6653-4-rre.smt2 regress1/strings/issue6653-rre.smt2 regress1/strings/issue6653-rre-small.smt2 diff --git a/test/regress/regress1/strings/issue6653-3-seq.smt2 b/test/regress/regress1/strings/issue6653-3-seq.smt2 new file mode 100644 index 000000000..a48fc7664 --- /dev/null +++ b/test/regress/regress1/strings/issue6653-3-seq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic QF_SLIA) +(set-info :status sat) +(set-option :strings-lazy-pp false) +(declare-fun z () Int) +(declare-fun a () (Seq Int)) +(assert (not (= (seq.nth a 1) (seq.nth a z)))) +(assert (= z (- 1))) +(check-sat) |