diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 36310fd3c3..fcc0d7d094 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -826,18 +826,6 @@ app* seq_util::mk_char_bit(expr* e, unsigned i) {
     return m.mk_app(f, 1, &e);
 }
 
-unsigned seq_util::max_plus(unsigned x, unsigned y) const {
-    if (x + y < x || x + y < y)
-        return UINT_MAX;
-    return x + y;
-}
-
-unsigned seq_util::max_mul(unsigned x, unsigned y) const {
-    uint64_t r = ((uint64_t)x)*((uint64_t)y);
-    return (r > UINT_MAX) ? UINT_MAX : (unsigned)r;
-}
-
-
 bool seq_util::is_const_char(expr* e, unsigned& c) const {
     return ch.is_const_char(e, c);
 }
@@ -1076,12 +1064,12 @@ unsigned seq_util::str::max_length(expr* s) const {
     };
     while (is_concat(s, s1, s2)) {
         if (is_concat(s1))
-            result = u.max_plus(max_length(s1), result);
+            result = add_truncate(max_length(s1), result);
         else
-            result = u.max_plus(get_length(s1), result);
+            result = add_truncate(get_length(s1), result);
         s = s2;
     }
-    result = u.max_plus(get_length(s), result);
+    result = add_truncate(get_length(s), result);
     return result;
 }
 
@@ -1092,26 +1080,7 @@ unsigned seq_util::rex::min_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;
-    if (is_empty(r))
-        return 0;
-    if (is_concat(r, r1, r2))
-        return u.max_plus(max_length(r1), max_length(r2));
-    if (is_union(r, r1, r2) || m.is_ite(r, s, r1, r2))
-        return std::max(max_length(r1), max_length(r2));
-    if (is_intersection(r, r1, r2))
-        return std::min(max_length(r1), max_length(r2));
-    if (is_diff(r, r1, r2) || is_reverse(r, r1) || is_opt(r, r1))
-        return max_length(r1);
-    if (is_loop(r, r1, lo, hi))
-        return u.max_mul(hi, max_length(r1));
-    if (is_to_re(r, s))
-        return u.str.max_length(s);
-    if (is_range(r) || is_of_pred(r) || is_full_char(r))
-        return 1;
-    // Else: star, plus, complement, full_seq, loop(r,r1,lo), derivative
-    return UINT_MAX;
+    return get_info(r).max_length;
 }
 
 /**
@@ -1671,9 +1640,9 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
     if (e->get_family_id() == u.get_family_id()) {
         switch (e->get_decl()->get_decl_kind()) {
         case OP_RE_EMPTY_SET:
-            return info(true, l_false, UINT_MAX, false);
+            return info(true, l_false, UINT_MAX, 0, false);
         case OP_RE_FULL_SEQ_SET:
-            return info(true, l_true, 0, true);
+            return info(true, l_true, 0, UINT_MAX, true);
         case OP_RE_STAR:
             i1 = get_info_rec(e->get_arg(0));
             return i1.star();
@@ -1686,14 +1655,14 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
             if (u.str.is_string(e->get_arg(0), slo) && slo.length() == 1 &&
                 u.str.is_string(e->get_arg(1), shi) && shi.length() == 1 &&
                 slo[0] <= shi[0])
-                return info(true, l_false, 1, true);
+                return info(true, l_false, 1, 1, true);
             // Symbolic or unknown: not classical
-            return info(true, l_false, 1, false);
+            return info(true, l_false, 1, 1, false);
         }
         case OP_RE_FULL_CHAR_SET:
         case OP_RE_OF_PRED:
             //TBD: check if the character predicate contains uninterpreted symbols or is nonground or is unsat
-            return info(true, l_false, 1, false);
+            return info(true, l_false, 1, 1, false);
         case OP_RE_CONCAT:
             if (e->get_num_args() == 1)
                 return get_info_rec(e->get_arg(0));            
@@ -1722,7 +1691,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
             min_length = u.str.min_length(e->get_arg(0));
             is_value = m.is_value(e->get_arg(0));
             nullable = (is_value && min_length == 0 ? l_true : (min_length > 0 ? l_false : l_undef));
-            return info(is_value, nullable, min_length, true);
+            return info(is_value, nullable, min_length, u.str.max_length(e->get_arg(0)), true);
         case OP_RE_REVERSE:
             return get_info_rec(e->get_arg(0));
         case OP_RE_PLUS:
@@ -1788,6 +1757,7 @@ std::ostream& seq_util::rex::info::display(std::ostream& out) const {
         out << "info("
             << "nullable=" << (nullable == l_true ? "T" : (nullable == l_false ? "F" : "U")) << ", "
             << "min_length=" << min_length << ", "
+            << "max_length=" << max_length << ", "
             << "classical=" << (classical ? "T" : "F") << ")";
     }
     else if (is_valid())
@@ -1808,13 +1778,13 @@ std::string seq_util::rex::info::str() const {
 
 seq_util::rex::info seq_util::rex::info::star() const {
     //if is_known() is false then all mentioned properties will remain false
-    return seq_util::rex::info(interpreted, l_true, 0, classical);
+    return seq_util::rex::info(interpreted, l_true, 0, max_length == 0 ? 0 : UINT_MAX, classical);
 }
 
 seq_util::rex::info seq_util::rex::info::plus() const {
     if (is_known()) {
         //plus never occurs in a normalized regex
-        return info(interpreted, nullable, min_length, classical);
+        return info(interpreted, nullable, min_length, max_length == 0 ? 0 : UINT_MAX, classical);
     }
     else
         return *this;
@@ -1823,14 +1793,14 @@ seq_util::rex::info seq_util::rex::info::plus() const {
 seq_util::rex::info seq_util::rex::info::opt() const {
     // if is_known() is false then all mentioned properties will remain false
     // optional construct never occurs in a normalized regex
-    return seq_util::rex::info(interpreted, l_true, 0, classical);
+    return seq_util::rex::info(interpreted, l_true, 0, max_length, classical);
 }
 
 seq_util::rex::info seq_util::rex::info::complement() const {
     if (is_known()) {
         lbool compl_nullable = (nullable == l_true ? l_false : (nullable == l_false ? l_true : l_undef));
         unsigned compl_min_length = (compl_nullable == l_false ? 1 : 0);
-        return info(interpreted, compl_nullable, compl_min_length, false);
+        return info(interpreted, compl_nullable, compl_min_length, UINT_MAX, false);
     }
     else
         return *this;
@@ -1839,12 +1809,15 @@ seq_util::rex::info seq_util::rex::info::complement() const {
 seq_util::rex::info seq_util::rex::info::concat(seq_util::rex::info const& rhs, bool lhs_is_concat) const {
     if (is_known()) {
         if (rhs.is_known()) {
-            unsigned m = min_length + rhs.min_length;
-            if (m < min_length || m < rhs.min_length)
-                m = UINT_MAX;
+            lbool is_nullable = l_undef;
+            if (nullable == l_true && rhs.nullable == l_true)
+                is_nullable = l_true;
+            if (nullable == l_false || rhs.nullable == l_false)
+                is_nullable = l_false;
             return info(interpreted && rhs.interpreted,
-                ((nullable == l_false || rhs.nullable == l_false) ? l_false : ((nullable == l_true && rhs.nullable == l_true) ? l_true : l_undef)),
-                m,
+                is_nullable,
+                add_truncate(min_length, rhs.min_length),
+                add_truncate(max_length, rhs.max_length),
                 classical && rhs.classical);
         }
         else
@@ -1860,6 +1833,7 @@ seq_util::rex::info seq_util::rex::info::disj(seq_util::rex::info const& rhs) co
         return info(interpreted && rhs.interpreted,
             ((nullable == l_true || rhs.nullable == l_true) ? l_true : ((nullable == l_false && rhs.nullable == l_false) ? l_false : l_undef)),
             std::min(min_length, rhs.min_length),
+            std::max(max_length, rhs.max_length),
             classical && rhs.classical);
     }
     else
@@ -1872,6 +1846,7 @@ seq_util::rex::info seq_util::rex::info::conj(seq_util::rex::info const& rhs) co
             return info(interpreted && rhs.interpreted,
                 ((nullable == l_true && rhs.nullable == l_true) ? l_true : ((nullable == l_false || rhs.nullable == l_false) ? l_false : l_undef)),
                 std::max(min_length, rhs.min_length),
+                std::min(max_length, rhs.max_length),
                 false);
         }
         else
@@ -1886,7 +1861,8 @@ seq_util::rex::info seq_util::rex::info::diff(seq_util::rex::info const& rhs) co
         if (rhs.is_known()) {
             return info(interpreted & rhs.interpreted,
                 ((nullable == l_true && rhs.nullable == l_false) ? l_true : ((nullable == l_false || rhs.nullable == l_false) ? l_false : l_undef)),
-                std::max(min_length, rhs.min_length),
+                min_length,
+                max_length,
                 false);
         }
         else
@@ -1906,6 +1882,7 @@ seq_util::rex::info seq_util::rex::info::xor_(seq_util::rex::info const& rhs) co
             return info(interpreted & rhs.interpreted,
                 xor_nullable,
                 0,
+                UINT_MAX,
                 false);
         }
         else
@@ -1924,6 +1901,7 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co
             return info(false,
                 ((nullable == l_true && i.nullable == l_true) ? l_true : ((nullable == l_false && i.nullable == l_false) ? l_false : l_undef)),
                 std::min(min_length, i.min_length),
+                std::max(max_length, i.max_length),
                 classical && i.classical);
         }
         else
@@ -1935,12 +1913,10 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co
 
 seq_util::rex::info seq_util::rex::info::loop(unsigned lower, unsigned upper) const {
     if (is_known()) {
-        unsigned m = min_length * lower;
-        // Code review: this is not a complete overflow check. 
-        if (m > 0 && (m < min_length || m < lower))
-            m = UINT_MAX;
+        unsigned m = mul_truncate(min_length, lower);
+        unsigned max_l = mul_truncate(max_length, upper);
         lbool loop_nullable = (nullable == l_true || lower == 0 ? l_true : nullable);
-        return info(interpreted, loop_nullable, m, classical);
+        return info(interpreted, loop_nullable, m, max_l, classical);
     }
     else
         return *this;
@@ -1955,8 +1931,7 @@ seq_util::rex::info& seq_util::rex::info::operator=(info const& other) {
     interpreted = other.interpreted;
     nullable = other.nullable;
     min_length = other.min_length;
+    max_length = other.max_length;
     classical = other.classical;
     return *this;
 }
-
-
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 12995a6f1d..b6fa2dc8ba 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -225,9 +225,6 @@ class seq_util {
 
 public:
 
-    unsigned max_plus(unsigned x, unsigned y) const;
-    unsigned max_mul(unsigned x, unsigned y) const;
-
     ast_manager& get_manager() const { return m; }
     char_decl_plugin &get_char_plugin() const {
         return ch;
@@ -451,6 +448,8 @@ public:
             lbool nullable { l_undef };
             /* Lower bound  on the length of all accepted words. */
             unsigned min_length { 0 };
+            /* Upper bound on the length of all accepted words, or UINT_MAX if unknown. */
+            unsigned max_length { UINT_MAX };
             /* Classical regular expression: does not use complement, intersection, diff, or the empty language (fail). */
             bool classical { true };
 
@@ -471,11 +470,13 @@ public:
             info(bool is_interpreted,
                 lbool is_nullable,
                 unsigned min_l,
+                unsigned max_l,
                 bool is_classical) :
                 known(l_true), 
                 interpreted(is_interpreted),
                 nullable(is_nullable),
                 min_length(min_l),
+                max_length(max_l),
                 classical(is_classical) {}
 
             /*
@@ -664,4 +665,3 @@ public:
 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 0eec49165c..448bde4399 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -493,7 +493,7 @@ namespace smt {
 
         // Rule 1: use min_length to prune search
         unsigned min_len = re().min_length(r);
-        unsigned min_len_plus_i = u().max_plus(min_len, idx);
+        unsigned min_len_plus_i = add_truncate(min_len, idx);
         literal len_s_ge_min = th.m_ax.mk_ge(th.mk_len(s), min_len_plus_i);
         // Acc(s,i,r) ==> |s| >= i + minlength(r)
         th.propagate_lit(nullptr, 1, &lit, len_s_ge_min);
diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp
index ebfdb09e11..13f5110bcd 100644
--- a/src/test/seq_rewriter.cpp
+++ b/src/test/seq_rewriter.cpp
@@ -18,6 +18,7 @@ Tests:
  20. Solver: contradictory constant lexical bounds are unsatisfiable
  22. re.loop with bounds as arguments agrees with the indexed form
  23. (Σ*·S)* is flattened to () | Σ*·S
+ 24. Regex info tracks inferred maximal lengths
 --*/
 
 #include "ast/arith_decl_plugin.h"
@@ -349,5 +350,32 @@ void tst_seq_rewriter() {
         ENSURE(i2.nullable == l_false && i2.min_length == 2);
     }
 
+    // -----------------------------------------------------------------------
+    // 24. Regex info tracks inferred maximal lengths.
+    // -----------------------------------------------------------------------
+    {
+        expr_ref empty(su.re.mk_empty(re_sort), m);
+        expr_ref epsilon(su.re.mk_to_re(su.str.mk_empty(str_sort)), m);
+        expr_ref ab(su.re.mk_to_re(su.str.mk_string("ab")), m);
+        expr_ref abc(su.re.mk_to_re(su.str.mk_string("abc")), m);
+        expr_ref intersection(su.re.mk_inter(ab, abc), m);
+        expr_ref union_(su.re.mk_union(ab, abc), m);
+        expr_ref complement(su.re.mk_complement(ab), m);
+        expr_ref loop(su.re.mk_loop_proper(abc, 2, 4), m);
+
+        ENSURE(su.re.get_info(empty).max_length == 0);
+        ENSURE(su.re.get_info(epsilon).max_length == 0);
+        ENSURE(su.re.get_info(intersection).max_length == 2);
+        ENSURE(su.re.get_info(union_).max_length == 3);
+        ENSURE(su.re.get_info(complement).max_length == UINT_MAX);
+        ENSURE(su.re.get_info(loop).max_length == 12);
+
+        seq_util::rex::info large(true, l_false, 1, UINT_MAX / 2 + 1, true);
+        ENSURE(large.loop(1, 2).max_length == UINT_MAX);
+        seq_util::rex::info almost_max(true, l_false, 1, UINT_MAX - 1, true);
+        seq_util::rex::info two(true, l_false, 1, 2, true);
+        ENSURE(almost_max.concat(two, false).max_length == UINT_MAX);
+    }
+
     std::cout << "tst_seq_rewriter: all tests passed\n";
 }
diff --git a/src/util/util.cpp b/src/util/util.cpp
index fbc13c6e0d..a011c4c3f9 100644
--- a/src/util/util.cpp
+++ b/src/util/util.cpp
@@ -119,6 +119,16 @@ unsigned uint64_log2(uint64_t v) {
     return r;
 }
 
+unsigned mul_truncate(unsigned a, unsigned b) {
+    auto r = (uint64_t)a * (uint64_t)b;
+    return r > UINT_MAX ? UINT_MAX : (unsigned)r;
+}
+
+unsigned add_truncate(unsigned a, unsigned b) {
+    auto r = (uint64_t)a + (uint64_t)b;
+    return r > UINT_MAX ? UINT_MAX : (unsigned)r;
+}
+
 bool product_iterator_next(unsigned n, unsigned const * sz, unsigned * it) {
     for (unsigned i = 0; i < n; ++i) {
         it[i]++;
@@ -160,4 +170,3 @@ void escaped::display(std::ostream & out) const {
         }
     }
 }
-
diff --git a/src/util/util.h b/src/util/util.h
index b1415671d2..7fb9471120 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -109,6 +109,8 @@ static inline unsigned next_power_of_two(unsigned v) {
 */
 unsigned log2(unsigned v);
 unsigned uint64_log2(uint64_t v);
+unsigned mul_truncate(unsigned a, unsigned b);
+unsigned add_truncate(unsigned a, unsigned b);
 
 static_assert(sizeof(unsigned) == 4, "unsigned are 32 bits");