From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 18 Oct 2021 22:59:38 +0000 (-0500)
Subject: Add regression for fixed issue (#7395)
X-Git-Tag: cvc5-1.0.0~1053
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9547f16cd326b71a41e96a42d094170e426561a4;p=cvc5.git

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 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)