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.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 272867d0caa53482443e2742595b96120956e486..b1d776b21a256524be6c22724af187f2f64392ef 100644 (file)
--- 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 (file)
index 0000000..a48fc76
--- /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)