6 files changed, 74 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d112bdf1d..4ee8e513e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -737,6 +737,7 @@ set(regress_0_tests
   regress0/options/ast-and-sexpr.smt2
   regress0/options/invalid_dump.smt2
   regress0/options/set-and-get-options.smt2
+  regress0/options/statistics.smt2
   regress0/parallel-let.smt2
   regress0/parser/as.smt2
   regress0/parser/bv_arity_smt2.6.smt2
@@ -2125,7 +2126,11 @@ set(regress_1_tests
   regress1/strings/issue6337-replace-re.smt2
   regress1/strings/issue6567-empty-re-range.smt2
   regress1/strings/issue6604-2.smt2
+  regress1/strings/issue6635-rre.smt2
   regress1/strings/issue6653-2-update-c-len.smt2
+  regress1/strings/issue6653-4-rre.smt2
+  regress1/strings/issue6653-rre.smt2
+  regress1/strings/issue6653-rre-small.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
diff --git a/test/regress/regress0/options/statistics.smt2 b/test/regress/regress0/options/statistics.smt2
new file mode 100644
index 000000000..ae9d93b6f
--- /dev/null
+++ b/test/regress/regress0/options/statistics.smt2
@@ -0,0 +1,43 @@
+; REQUIRES: statistics
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: true
+; EXPECT: true
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: true
+; EXPECT: false
+; EXPECT: false
+; EXPECT: true
+(set-logic QF_UF)
+(get-option :stats)
+(get-option :stats-all)
+(get-option :stats-every-query)
+(get-option :stats-expert)
+
+(set-option :stats-all true)
+
+(get-option :stats)
+(get-option :stats-all)
+(get-option :stats-every-query)
+(get-option :stats-expert)
+
+(set-option :stats false)
+
+(get-option :stats)
+(get-option :stats-all)
+(get-option :stats-every-query)
+(get-option :stats-expert)
+
+(set-option :stats-expert true)
+
+(get-option :stats)
+(get-option :stats-all)
+(get-option :stats-every-query)
+(get-option :stats-expert)
+\ No newline at end of file
diff --git a/test/regress/regress1/strings/issue6635-rre.smt2 b/test/regress/regress1/strings/issue6635-rre.smt2
new file mode 100644
index 000000000..cbca77783
--- /dev/null
+++ b/test/regress/regress1/strings/issue6635-rre.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () String)
+(assert (str.in_re (str.replace_re a (re.++ (str.to_re "A") (re.union (str.to_re "") (str.to_re (str.from_code (str.len a))))) "AB") (re.+ (str.to_re "A"))))
+(check-sat)
diff --git a/test/regress/regress1/strings/issue6653-4-rre.smt2 b/test/regress/regress1/strings/issue6653-4-rre.smt2
new file mode 100644
index 000000000..8de99a334
--- /dev/null
+++ b/test/regress/regress1/strings/issue6653-4-rre.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun x () String)
+(assert (str.in_re (str.replace_re x (str.to_re "A") x) (re.++ (re.comp (str.to_re "A")) (str.to_re "A") re.allchar)))
+(check-sat)
diff --git a/test/regress/regress1/strings/issue6653-rre-small.smt2 b/test/regress/regress1/strings/issue6653-rre-small.smt2
new file mode 100644
index 000000000..c4b6a497b
--- /dev/null
+++ b/test/regress/regress1/strings/issue6653-rre-small.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --strings-exp --strings-fmf --re-elim --re-elim-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(assert (str.in_re a (re.+ (str.to_re (str.replace_re a (str.to_re a) "A")))))
+(check-sat)
diff --git a/test/regress/regress1/strings/issue6653-rre.smt2 b/test/regress/regress1/strings/issue6653-rre.smt2
new file mode 100644
index 000000000..66b7dd64e
--- /dev/null
+++ b/test/regress/regress1/strings/issue6653-rre.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (str.in_re (str.replace_re b (str.to_re (str.replace_all a (str.++ b "a") b)) (str.++ b "a")) (re.+ (str.to_re "b"))))
+(assert (str.in_re a (re.* (re.range "a" "b"))))
+(check-sat)