7 files changed, 74 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/rev-conv1.smt2 b/test/regress/regress1/strings/rev-conv1.smt2
new file mode 100644
index 000000000..ca20076cb
--- /dev/null
+++ b/test/regress/regress1/strings/rev-conv1.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(assert (= (str.rev (str.toupper x)) "CBA"))
+(assert (not (= x "ABC")))
+(assert (not (= x "abc")))
+(check-sat)
diff --git a/test/regress/regress1/strings/rev-ex1.smt2 b/test/regress/regress1/strings/rev-ex1.smt2
new file mode 100644
index 000000000..36d40fcdd
--- /dev/null
+++ b/test/regress/regress1/strings/rev-ex1.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(assert (not (= (str.rev (str.++ x y)) (str.rev (str.++ x z)))))
+(check-sat)
diff --git a/test/regress/regress1/strings/rev-ex2.smt2 b/test/regress/regress1/strings/rev-ex2.smt2
new file mode 100644
index 000000000..163785bdc
--- /dev/null
+++ b/test/regress/regress1/strings/rev-ex2.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(assert (= x (str.rev (str.++ y "A"))))
+(assert (> (str.len x) (+ (str.len y) 1)))
+(check-sat)
diff --git a/test/regress/regress1/strings/rev-ex3.smt2 b/test/regress/regress1/strings/rev-ex3.smt2
new file mode 100644
index 000000000..e317191ad
--- /dev/null
+++ b/test/regress/regress1/strings/rev-ex3.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(assert (= x (str.rev (str.++ y "A"))))
+(assert (= x (str.rev (str.++ "B" z))))
+(assert (= z (str.++ w "C")))
+(check-sat)
diff --git a/test/regress/regress1/strings/rev-ex4.smt2 b/test/regress/regress1/strings/rev-ex4.smt2
new file mode 100644
index 000000000..a3eed8e35
--- /dev/null
+++ b/test/regress/regress1/strings/rev-ex4.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --strings-exp --strings-fmf
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(assert (= x (str.rev y)))
+(assert (= y (str.rev z)))
+(assert (distinct x z w))
+(assert (< (str.len x) 2))
+(check-sat)
diff --git a/test/regress/regress1/strings/rev-ex5.smt2 b/test/regress/regress1/strings/rev-ex5.smt2
new file mode 100644
index 000000000..74a374962
--- /dev/null
+++ b/test/regress/regress1/strings/rev-ex5.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(assert (= x (str.rev x)))
+(assert (> (str.len x) 1))
+(check-sat)
diff --git a/test/regress/regress1/strings/str-rev-simple-s.smt2 b/test/regress/regress1/strings/str-rev-simple-s.smt2
new file mode 100644
index 000000000..5445a19ea
--- /dev/null
+++ b/test/regress/regress1/strings/str-rev-simple-s.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(assert (= (str.rev "ABC") "CBA"))
+(assert (= (str.rev "") ""))
+(assert (= (str.rev "A") x))
+(assert (= (str.rev (str.++ x y)) "BCA"))
+(assert (= (str.rev y) "BC"))
+(check-sat)