diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 8c501d531..00145970a 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -982,7 +982,9 @@ bool theory_seq::solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep)
     }
     expr* u = nullptr;
     for (expr* r : rs) {
-        if (m_util.str.is_unit(r, u)) {
+        if (m_util.str.is_unit(r, u) && !m_is_digit.contains(u)) {
+            m_is_digit.insert(u);
+            m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_is_digit, u));
             literal is_digit = m_ax.is_digit(u);
             if (get_context().get_assignment(is_digit) != l_true) {
                 propagate_lit(dep, 0, nullptr, is_digit);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index f09d6b89a..47f64564e 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -425,6 +425,7 @@ namespace smt {
         re2automaton                   m_mk_aut;
 
         obj_hashtable<expr>            m_fixed;            // string variables that are fixed length.
+        obj_hashtable<expr>            m_is_digit;         // expressions that have been constrained to be digits
 
         void init(context* ctx) override;
         final_check_status final_check_eh() override;