From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 21 Oct 2013 14:55:34 +0000 (-0500)
Subject: add a string test case
X-Git-Tag: cvc5-1.0.0~7275^2~7^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=88779ec5966b142364424c06136dde004a55ff7c;p=cvc5.git

add a string test case
---

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index cd3116eac..c98f37958 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -39,7 +39,8 @@ TESTS =	\
   loop005.smt2 \
   loop006.smt2 \
   loop007.smt2 \
-  loop008.smt2
+  loop008.smt2 \
+  loop009.smt2
 
 FAILING_TESTS =
 
diff --git a/test/regress/regress0/strings/loop009.smt2 b/test/regress/regress0/strings/loop009.smt2
new file mode 100644
index 000000000..41eab0f35
--- /dev/null
+++ b/test/regress/regress0/strings/loop009.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+
+(assert (= (str.++ x "aa") (str.++ "aa" x)))
+(assert (= (str.len x) 7))
+
+(check-sat)