diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 634eece7d..3699412d3 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -288,8 +288,8 @@ class seq_rewriter {
     void remove_empty_and_concats(expr_ref_vector& es);
     void remove_leading(unsigned n, expr_ref_vector& es);
 
-    class seq_util::re& re() { return u().re; }
-    class seq_util::re const& re() const { return u().re; }
+    class seq_util::rex& re() { return u().re; }
+    class seq_util::rex const& re() const { return u().re; }
     class seq_util::str& str() { return u().str; }
     class seq_util::str const& str() const { return u().str; }
 
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 695a534d3..53e0966fc 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -1312,12 +1312,12 @@ unsigned seq_util::str::max_length(expr* s) const {
     return result;
 }
 
-unsigned seq_util::re::min_length(expr* r) const {
+unsigned seq_util::rex::min_length(expr* r) const {
     SASSERT(u.is_re(r));
     return get_info(r).min_length;
 }
 
-unsigned seq_util::re::max_length(expr* r) const {
+unsigned seq_util::rex::max_length(expr* r) const {
     SASSERT(u.is_re(r));
     expr* r1 = nullptr, *r2 = nullptr, *s = nullptr;
     unsigned lo = 0, hi = 0;
@@ -1341,49 +1341,49 @@ unsigned seq_util::re::max_length(expr* r) const {
     return UINT_MAX;
 }
 
-sort* seq_util::re::to_seq(sort* re) {
+sort* seq_util::rex::to_seq(sort* re) {
     (void)u;
     SASSERT(u.is_re(re));
     return to_sort(re->get_parameter(0).get_ast());
 }
 
-app* seq_util::re::mk_loop(expr* r, unsigned lo) {
+app* seq_util::rex::mk_loop(expr* r, unsigned lo) {
     parameter param(lo);
     return m.mk_app(m_fid, OP_RE_LOOP, 1, &param, 1, &r);
 }
 
-app* seq_util::re::mk_loop(expr* r, unsigned lo, unsigned hi) {
+app* seq_util::rex::mk_loop(expr* r, unsigned lo, unsigned hi) {
     parameter params[2] = { parameter(lo), parameter(hi) };
     return m.mk_app(m_fid, OP_RE_LOOP, 2, params, 1, &r);
 }
 
-app* seq_util::re::mk_loop(expr* r, expr* lo) {
+app* seq_util::rex::mk_loop(expr* r, expr* lo) {
     expr* rs[2] = { r, lo };
     return m.mk_app(m_fid, OP_RE_LOOP, 0, nullptr, 2, rs);
 }
 
-app* seq_util::re::mk_loop(expr* r, expr* lo, expr* hi) {
+app* seq_util::rex::mk_loop(expr* r, expr* lo, expr* hi) {
     expr* rs[3] = { r, lo, hi };
     return m.mk_app(m_fid, OP_RE_LOOP, 0, nullptr, 3, rs);
 }
 
-app* seq_util::re::mk_full_char(sort* s) {
+app* seq_util::rex::mk_full_char(sort* s) {
     return m.mk_app(m_fid, OP_RE_FULL_CHAR_SET, 0, nullptr, 0, nullptr, s);
 }
 
-app* seq_util::re::mk_full_seq(sort* s) {
+app* seq_util::rex::mk_full_seq(sort* s) {
     return m.mk_app(m_fid, OP_RE_FULL_SEQ_SET, 0, nullptr, 0, nullptr, s);
 }
 
-app* seq_util::re::mk_empty(sort* s) {    
+app* seq_util::rex::mk_empty(sort* s) {    
     return m.mk_app(m_fid, OP_RE_EMPTY_SET, 0, nullptr, 0, nullptr, s);
 }
 
-app* seq_util::re::mk_of_pred(expr* p) {
+app* seq_util::rex::mk_of_pred(expr* p) {
     return m.mk_app(m_fid, OP_RE_OF_PRED, 0, nullptr, 1, &p);
 }
 
-bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) const {
+bool seq_util::rex::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) const {
     if (is_loop(n)) {
         app const* a = to_app(n);
         if (a->get_num_args() == 1 && a->get_decl()->get_num_parameters() == 2) {
@@ -1396,7 +1396,7 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& h
     return false;
 }
 
-bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo) const {
+bool seq_util::rex::is_loop(expr const* n, expr*& body, unsigned& lo) const {
     if (is_loop(n)) {
         app const* a = to_app(n);
         if (a->get_num_args() == 1 && a->get_decl()->get_num_parameters() == 1) {
@@ -1408,7 +1408,7 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo) const {
     return false;
 }
 
-bool seq_util::re::is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi) const {
+bool seq_util::rex::is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi) const {
     if (is_loop(n)) {
         app const* a = to_app(n);
         if (a->get_num_args() == 3) {
@@ -1421,7 +1421,7 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi) con
     return false;
 }
 
-bool seq_util::re::is_loop(expr const* n, expr*& body, expr*& lo) const {
+bool seq_util::rex::is_loop(expr const* n, expr*& body, expr*& lo) const {
     if (is_loop(n)) {
         app const* a = to_app(n);
         if (a->get_num_args() == 2) {
@@ -1436,21 +1436,21 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, expr*& lo) const {
 /**
    Returns true iff e is the epsilon regex.
  */
-bool seq_util::re::is_epsilon(expr* r) const {
+bool seq_util::rex::is_epsilon(expr* r) const {
     expr* s;
     return is_to_re(r, s) && u.str.is_empty(s);
 }
 /**
    Makes the epsilon regex for a given sequence sort.
  */
-app* seq_util::re::mk_epsilon(sort* seq_sort) {
+app* seq_util::rex::mk_epsilon(sort* seq_sort) {
     return mk_to_re(u.str.mk_empty(seq_sort));
 }
 
 /*
   Produces compact view of concrete concatenations such as (abcd).
 */
-std::ostream& seq_util::re::pp::compact_helper_seq(std::ostream& out, expr* s) const {
+std::ostream& seq_util::rex::pp::compact_helper_seq(std::ostream& out, expr* s) const {
     SASSERT(re.u.is_seq(s));
     if (re.u.str.is_concat(s)) {
         expr_ref_vector es(re.m);
@@ -1472,7 +1472,7 @@ std::ostream& seq_util::re::pp::compact_helper_seq(std::ostream& out, expr* s) c
 /*
   Produces output such as [a-z] for a range.
 */
-std::ostream& seq_util::re::pp::compact_helper_range(std::ostream& out, expr* s1, expr* s2) const {
+std::ostream& seq_util::rex::pp::compact_helper_range(std::ostream& out, expr* s1, expr* s2) const {
     out << "[";
     seq_unit(out, s1) << "-";
     seq_unit(out, s2) << "]";
@@ -1482,7 +1482,7 @@ std::ostream& seq_util::re::pp::compact_helper_range(std::ostream& out, expr* s1
 /*
   Checks if parenthesis can be omitted in some cases in a loop body or in complement.
 */
-bool seq_util::re::pp::can_skip_parenth(expr* r) const {
+bool seq_util::rex::pp::can_skip_parenth(expr* r) const {
     expr* s;
     return ((re.is_to_re(r, s) && re.u.str.is_unit(s)) || re.is_range(r) || re.is_empty(r) || re.is_epsilon(r));
 }
@@ -1490,7 +1490,7 @@ bool seq_util::re::pp::can_skip_parenth(expr* r) const {
 /*
   Specialize output for a unit sequence converting to visible ASCII characters if possible.
 */
-std::ostream& seq_util::re::pp::seq_unit(std::ostream& out, expr* s) const {
+std::ostream& seq_util::rex::pp::seq_unit(std::ostream& out, expr* s) const {
     expr* e;
     unsigned n = 0;
     if (re.u.str.is_unit(s, e) && re.u.is_const_char(e, n)) {
@@ -1509,7 +1509,7 @@ std::ostream& seq_util::re::pp::seq_unit(std::ostream& out, expr* s) const {
 /*
   Pretty prints the regex r into the out stream
 */
-std::ostream& seq_util::re::pp::display(std::ostream& out) const {
+std::ostream& seq_util::rex::pp::display(std::ostream& out) const {
     expr* r1 = nullptr, * r2 = nullptr, * s = nullptr, * s2 = nullptr;
     unsigned lo = 0, hi = 0;
     if (re.is_full_char(e))
@@ -1580,7 +1580,7 @@ std::ostream& seq_util::re::pp::display(std::ostream& out) const {
 /*
   Pretty prints the regex r into the output string
 */
-std::string seq_util::re::to_str(expr* r) const {
+std::string seq_util::rex::to_str(expr* r) const {
     std::ostringstream out;
     out << pp(u.re, r);
     return out.str();
@@ -1589,14 +1589,14 @@ std::string seq_util::re::to_str(expr* r) const {
 /*
   Returns true iff info has been computed for the regex r
 */
-bool seq_util::re::has_valid_info(expr* r) const {
+bool seq_util::rex::has_valid_info(expr* r) const {
     return r->get_id() < m_infos.size() && m_infos[r->get_id()].is_valid();
 }
 
 /*
   Returns the info in the cache if the info is valid. Returns invalid_info otherwise.
 */
-seq_util::re::info seq_util::re::get_cached_info(expr* e) const {
+seq_util::rex::info seq_util::rex::get_cached_info(expr* e) const {
     if (has_valid_info(e))
         return m_infos[e->get_id()];
     else
@@ -1606,7 +1606,7 @@ seq_util::re::info seq_util::re::get_cached_info(expr* e) const {
 /*
   Get the information value associated with the regular expression e
 */
-seq_util::re::info seq_util::re::get_info(expr* e) const
+seq_util::rex::info seq_util::rex::get_info(expr* e) const
 {
     SASSERT(u.is_re(e));
     auto result = get_cached_info(e);
@@ -1619,7 +1619,7 @@ seq_util::re::info seq_util::re::get_info(expr* e) const
 /*
   Gets the info value for the given regex e, possibly making a new info recursively over the structure of e.
 */
-seq_util::re::info seq_util::re::get_info_rec(expr* e) const {
+seq_util::rex::info seq_util::rex::get_info_rec(expr* e) const {
     auto result = get_cached_info(e);
     if (result.is_valid())
         return result;
@@ -1627,7 +1627,7 @@ seq_util::re::info seq_util::re::get_info_rec(expr* e) const {
         return invalid_info;
     result = mk_info_rec(to_app(e));
     m_infos.setx(e->get_id(), result, invalid_info);
-    STRACE("re_info", tout << "compute_info(" << pp(u.re, e) << "): min_length=" << m_infos[e->get_id()].min_length << std::endl;);
+    STRACE("re_info", tout << "compute_info(" << pp(u.re, e) << ")=" << result << std::endl;);
     return result;
 }
 
@@ -1635,7 +1635,7 @@ seq_util::re::info seq_util::re::get_info_rec(expr* e) const {
   Computes the info value for the given regex e recursively over the structure of e.
   The regex e does not yet have an entry in the cache.
 */
-seq_util::re::info seq_util::re::mk_info_rec(app* e) const {
+seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
     info i1, i2;
     if (e->get_family_id() == u.get_family_id()) {
         switch (e->get_decl()->get_decl_kind())
@@ -1687,3 +1687,17 @@ seq_util::re::info seq_util::re::mk_info_rec(app* e) const {
     }
     return invalid_info;
 }
+
+std::ostream& seq_util::rex::info::display(std::ostream& out) const {
+    if (valid)
+        out << "info(" << "min_length=" << min_length << ")";
+    else
+        out << "invalid_info";
+    return out;
+}
+
+std::string seq_util::rex::info::str() const {
+    std::ostringstream out;
+    display(out);
+    return out.str();
+}
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 5bd1edeeb..1110c06c5 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -408,16 +408,18 @@ public:
         unsigned max_length(expr* s) const;
     };
 
-    class re {
+    class rex {
+    public:
         struct info {
             bool valid;
             unsigned min_length;
             info() : valid(false), min_length(0) {}
             info(unsigned k) : valid(true), min_length(k) {}
-
             bool is_valid() { return valid; }
+            std::ostream& display(std::ostream&) const;
+            std::string str() const;
         };
-
+    private:
         seq_util&    u;
         ast_manager& m;
         family_id    m_fid;
@@ -431,7 +433,7 @@ public:
         info get_cached_info(expr* e) const;
 
     public:
-        re(seq_util& u): u(u), m(u.m), m_fid(u.m_fid), m_info_pinned(u.m) {}
+        rex(seq_util& u): u(u), m(u.m), m_fid(u.m_fid), m_info_pinned(u.m) {}
 
         sort* mk_re(sort* seq) { parameter param(seq); return m.mk_sort(m_fid, RE_SORT, 1, &param); }
         sort* to_seq(sort* re);
@@ -503,7 +505,7 @@ public:
         std::string to_str(expr* r) const;
 
         class pp {
-            seq_util::re& re;
+            seq_util::rex& re;
             expr* e;
             bool can_skip_parenth(expr* r) const;
             std::ostream& seq_unit(std::ostream& out, expr* s) const;
@@ -511,12 +513,12 @@ public:
             std::ostream& compact_helper_range(std::ostream& out, expr* s1, expr* s2) const;
 
         public:
-            pp(seq_util::re& r, expr* e) : re(r), e(e) {}
+            pp(seq_util::rex& r, expr* e) : re(r), e(e) {}
             std::ostream& display(std::ostream&) const;
         };
     };
     str str;
-    re  re;
+    rex  re;
 
     seq_util(ast_manager& m):
         m(m),
@@ -531,8 +533,6 @@ public:
     family_id get_family_id() const { return m_fid; }
 };
 
-inline std::ostream& operator<<(std::ostream& out, seq_util::re::pp const & p) { return p.display(out); }
-
-
-
+inline std::ostream& operator<<(std::ostream& out, seq_util::rex::pp const & p) { return p.display(out); }
 
+inline std::ostream& operator<<(std::ostream& out, seq_util::rex::info const& p) { return p.display(out); }
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index d025c2eee..ff1f57abd 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -29,7 +29,7 @@ namespace smt {
     {}
 
     seq_util& seq_regex::u() { return th.m_util; }
-    class seq_util::re& seq_regex::re() { return th.m_util.re; }
+    class seq_util::rex& seq_regex::re() { return th.m_util.re; }
     class seq_util::str& seq_regex::str() { return th.m_util.str; }
     seq_rewriter& seq_regex::seq_rw() { return th.m_seq_rewrite; }
     seq_skolem& seq_regex::sk() { return th.m_sk; }
@@ -794,7 +794,7 @@ namespace smt {
         STRACE("seq_regex", tout << "Updating state graph for regex "
                                  << mk_pp(r, m) << ") ";);
         if (!m_state_graph.is_seen(r_id))
-            STRACE("state_graph", tout << std::endl << "state(" << r_id << ") = " << seq_util::re::pp(re(), r) << std::endl;);
+            STRACE("state_graph", tout << std::endl << "state(" << r_id << ") = " << seq_util::rex::pp(re(), r) << std::endl;);
         // Add state
         m_state_graph.add_state(r_id);
         STRACE("state_graph", tout << "regex(" << r_id << ") = " << mk_pp(r, m) << std::endl;);
@@ -817,7 +817,7 @@ namespace smt {
                 STRACE("seq_regex_verbose", tout
                     << std::endl << "  traversing deriv: " << dr_id << " ";);
                 if (!m_state_graph.is_seen(dr_id))
-                    STRACE("state_graph", tout << "state(" << dr_id << ") = " << seq_util::re::pp(re(), dr) << std::endl;);
+                    STRACE("state_graph", tout << "state(" << dr_id << ") = " << seq_util::rex::pp(re(), dr) << std::endl;);
                 // Add state
                 m_state_graph.add_state(dr_id);
                 STRACE("state_graph", tout << "regex(" << dr_id << ") = " << mk_pp(dr, m) << std::endl;);
diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h
index e5782a94f..f29d1837b 100644
--- a/src/smt/seq_regex.h
+++ b/src/smt/seq_regex.h
@@ -132,7 +132,7 @@ namespace smt {
             Solvers and utilities
         */
         seq_util& u();
-        class seq_util::re& re();
+        class seq_util::rex& re();
         class seq_util::str& str();
         seq_rewriter& seq_rw();
         seq_skolem& sk();