From 52b39dfc1f3abef991d9c309c3e92d454330f274 Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 21 Oct 2013 09:55:34 -0500
Subject: [PATCH] add a string test case

---
 test/regress/regress0/strings/Makefile.am  | 3 ++-
 test/regress/regress0/strings/loop009.smt2 | 9 +++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/strings/loop009.smt2

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)
-- 
2.30.2