From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 9 Apr 2021 19:11:31 +0000 (-0500)
Subject: Add regressions for issue 6214 (#6305)
X-Git-Tag: cvc5-1.0.0~1933
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e5358e498db6d934d0b8704cfd023b0f67b6fbc0;p=cvc5.git

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 38748b757..dc0a4c980 100644
--- 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
index 000000000..0e74394ee
--- /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
index 000000000..c203c256f
--- /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
index 000000000..c203c256f
--- /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)