From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 7 Apr 2021 22:13:14 +0000 (-0500)
Subject: Add benchmark for 6270 (#6283)
X-Git-Tag: cvc5-1.0.0~1947
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4c2347c1cded72e3a7c71f3ed349148e5ef9bfd3;p=cvc5.git

Add benchmark for 6270 (#6283)
---

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f3f31edbf..c7c311079 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2052,6 +2052,7 @@ set(regress_1_tests
   regress1/strings/issue6191-replace-all.smt2
   regress1/strings/issue6203-1-substr-ctn-strip.smt2
   regress1/strings/issue6203-2-re-ccache.smt2
+  regress1/strings/issue6270.smt2
   regress1/strings/issue6271-rnf.smt2
   regress1/strings/issue6271-2-rnf.smt2
   regress1/strings/kaluza-fl.smt2
diff --git a/test/regress/regress1/strings/issue6270.smt2 b/test/regress/regress1/strings/issue6270.smt2
new file mode 100644
index 000000000..1c073fc12
--- /dev/null
+++ b/test/regress/regress1/strings/issue6270.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp --nl-ext-tplanes
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun i9 () Int)
+(declare-fun str0 () String)
+(declare-fun str9 () String)
+(assert (and (= 0 (str.indexof str9 str9 (abs (str.len str0)))) (= (abs (str.len str0)) (+ (- 5) (* i9 i9)))))
+(check-sat)