From 9547f16cd326b71a41e96a42d094170e426561a4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 18 Oct 2021 17:59:38 -0500 Subject: [PATCH] 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. --- test/regress/CMakeLists.txt | 1 + test/regress/regress1/strings/issue6653-3-seq.smt2 | 10 ++++++++++ 2 files changed, 11 insertions(+) create mode 100644 test/regress/regress1/strings/issue6653-3-seq.smt2 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) -- 2.30.2