3 files changed, 26 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b6fa29e28..eb78c1611 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -865,6 +865,7 @@ set(regress_0_tests
   regress0/strings/strings-native-simple.cvc
   regress0/strings/strip-endpoint-itos.smt2
   regress0/strings/substr-rewrites.smt2
+  regress0/strings/tolower-simple.smt2
   regress0/strings/type001.smt2
   regress0/strings/unsound-0908.smt2
   regress0/strings/unsound-repl-rewrite.smt2
@@ -1607,6 +1608,7 @@ set(regress_1_tests
   regress1/strings/strings-lt-simple.smt2
   regress1/strings/strip-endpt-sound.smt2
   regress1/strings/substr001.smt2
+  regress1/strings/tolower-find.smt2
   regress1/strings/timeout-no-resp.smt2
   regress1/strings/type002.smt2
   regress1/strings/type003.smt2
diff --git a/test/regress/regress0/strings/tolower-simple.smt2 b/test/regress/regress0/strings/tolower-simple.smt2
new file mode 100644
index 000000000..9d2273f8d
--- /dev/null
+++ b/test/regress/regress0/strings/tolower-simple.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL_SUPPORTED)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-const x String)
+(declare-const y String)
+(declare-const z String)
+
+(assert (= (str.tolower "aBCDef") x))
+(assert (= x (str.++ y "c" z)))
+
+(check-sat)
diff --git a/test/regress/regress1/strings/tolower-find.smt2 b/test/regress/regress1/strings/tolower-find.smt2
new file mode 100644
index 000000000..ff27a285a
--- /dev/null
+++ b/test/regress/regress1/strings/tolower-find.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL_SUPPORTED)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-const x String)
+(declare-const y String)
+
+(assert (= (str.tolower x) "abcde"))
+(assert (= (str.tolower y) "abcde"))
+(assert (not (= x "abcde")))
+(assert (not (= y "abcde")))
+(assert (not (= x y)))
+
+(check-sat)