Add benchmark for 6270 (#6283)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f3f31edbf5fb1512d7a547f44d2cfaf100f87700..c7c311079db14790d358cd13bffacc164769b1d9 100644 (file)
--- 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 (file)
index 0000000..1c073fc
--- /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)