Add regressions for issue 6214 (#6305)

Adds 3 of the 6 benchmarks from issue 6214, the 1st and 5th benchmarks timeout.
Fixes #6214.

These benchmarks were fixed by 3c98bb2.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 38748b75704abbe24f0f09c158be17bc1670d6c1..dc0a4c980f6ecb0f2cee361e5f65ade6ee2a6ede 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2054,6 +2054,9 @@ 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/issue6214-2-sym-re-inc.smt2
+  regress1/strings/issue6214-3-sym-re-inc.smt2
+  regress1/strings/issue6214-4-sym-re-inc.smt2
   regress1/strings/issue6270.smt2
   regress1/strings/issue6271-rnf.smt2
   regress1/strings/issue6271-2-rnf.smt2

diff --git a/test/regress/regress1/strings/issue6214-2-sym-re-inc.smt2 b/test/regress/regress1/strings/issue6214-2-sym-re-inc.smt2
new file mode 100644 (file)
index 0000000..0e74394
--- /dev/null
+++ b/test/regress/regress1/strings/issue6214-2-sym-re-inc.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (str.in_re a (re.range "a" "c")))
+(assert
+ (str.in_re a
+  (re.*
+   (re.union
+    (re.++ (re.union (str.to_re "a") (str.to_re "b")) (str.to_re "a"))
+    (str.to_re (str.from_int (str.len b)))))))
+(check-sat)

diff --git a/test/regress/regress1/strings/issue6214-3-sym-re-inc.smt2 b/test/regress/regress1/strings/issue6214-3-sym-re-inc.smt2
new file mode 100644 (file)
index 0000000..c203c25
--- /dev/null
+++ b/test/regress/regress1/strings/issue6214-3-sym-re-inc.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert
+ (str.in_re
+  (str.++ (ite (str.in_re b (re.* (re.range "a" "u"))) a "") b)
+  (re.++ (re.range "a" "u")
+   (re.diff (str.to_re "")
+    (str.to_re (ite (str.in_re b (re.* (re.range "a" "u"))) "" b))))))
+(assert (str.<= b "a"))
+(check-sat)

diff --git a/test/regress/regress1/strings/issue6214-4-sym-re-inc.smt2 b/test/regress/regress1/strings/issue6214-4-sym-re-inc.smt2
new file mode 100644 (file)
index 0000000..c203c25
--- /dev/null
+++ b/test/regress/regress1/strings/issue6214-4-sym-re-inc.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert
+ (str.in_re
+  (str.++ (ite (str.in_re b (re.* (re.range "a" "u"))) a "") b)
+  (re.++ (re.range "a" "u")
+   (re.diff (str.to_re "")
+    (str.to_re (ite (str.in_re b (re.* (re.range "a" "u"))) "" b))))))
+(assert (str.<= b "a"))
+(check-sat)