diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index f3b82a60c..953519fe6 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -255,6 +255,7 @@ public:
         expr* mk_concat(unsigned n, expr* const* es) const { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); }
         expr* mk_concat(expr_ref_vector const& es) const { return mk_concat(es.size(), es.c_ptr()); }
         app* mk_length(expr* a) const { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); }
+        app* mk_at(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_AT, 2, es); }
         app* mk_nth(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_NTH, 2, es); }
         app* mk_nth(expr* s, unsigned i) const;
 
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 1c4b08371..23b9da9dc 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -272,6 +272,7 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
     m_find(*this),
     m_overlap(m),
     m_overlap2(m),
+    m_internal_nth_es(m),
     m_len_prop_lvl(-1),
     m_factory(nullptr),
     m_exclude(m),
@@ -298,7 +299,6 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
     m_suffix         = "seq.s.prefix";
     m_accept         = "aut.accept";
     m_tail           = "seq.tail";
-    m_nth            = "seq.nth";
     m_seq_first      = "seq.first";
     m_seq_last       = "seq.last";
     m_indexof_left   = "seq.idx.left";
@@ -1985,18 +1985,10 @@ bool theory_seq::is_unit_nth(expr* e) const {
 
 bool theory_seq::is_nth(expr* e) const {
     return m_util.str.is_nth(e);
-//    return is_skolem(m_nth, e);
 }
 
 bool theory_seq::is_nth(expr* e, expr*& e1, expr*& e2) const {
-    if (is_nth(e)) {
-        e1 = to_app(e)->get_arg(0);
-        e2 = to_app(e)->get_arg(1);
-        return true;
-    }
-    else {
-        return false;
-    }
+    return m_util.str.is_nth(e, e1, e2);
 }
 
 bool theory_seq::is_tail(expr* e, expr*& s, unsigned& idx) const {
@@ -2023,7 +2015,12 @@ bool theory_seq::is_post(expr* e, expr*& s, expr*& i) {
 
 
 expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
-    return expr_ref(m_util.str.mk_nth(s, idx), m);
+    expr_ref result(m_util.str.mk_nth(s, idx), m);
+    if (!m_internal_nth_table.contains(result)) {
+        m_internal_nth_table.insert(result);
+        m_internal_nth_es.push_back(result);
+    }
+    return result;
 }
 
 expr_ref theory_seq::mk_sk_ite(expr* c, expr* t, expr* e) {
@@ -5132,6 +5129,10 @@ void theory_seq::add_nth_axiom(expr* e) {
         app_ref ch(m_util.str.mk_char(str[n.get_unsigned()]), m);
         add_axiom(mk_eq(ch, e, false));
     }
+    else if (!m_internal_nth_table.contains(e)) {
+        expr_ref emp(m_util.str.mk_empty(m.get_sort(s)), m);
+        add_axiom(mk_eq(s, emp, false), mk_eq(m_util.str.mk_unit(e), m_util.str.mk_at(s, i), false));
+    }
 }
 
 
@@ -5597,6 +5598,7 @@ void theory_seq::push_scope_eh() {
     m_eqs.push_scope();
     m_nqs.push_scope();
     m_ncs.push_scope();
+    m_internal_nth_lim.push_back(m_internal_nth_es.size());
 }
 
 void theory_seq::pop_scope_eh(unsigned num_scopes) {
@@ -5617,6 +5619,12 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) {
         m_len_prop_lvl = ctx.get_scope_level();
         m_len_offset.reset();
     }
+    unsigned old_sz = m_internal_nth_lim[m_internal_nth_lim.size() - num_scopes];
+    for (unsigned i = m_internal_nth_es.size(); i-- > old_sz; ) {
+        m_internal_nth_table.erase(m_internal_nth_es.get(i));
+    }
+    m_internal_nth_es.shrink(old_sz);
+    m_internal_nth_lim.shrink(m_internal_nth_lim.size() - num_scopes);
 }
 
 void theory_seq::restart_eh() {
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index f0d7fa15b..bb05e0be8 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -336,13 +336,16 @@ namespace smt {
         obj_map<enode, obj_map<enode, int>>   m_len_offset;
         int                                   m_len_prop_lvl;
 
+        obj_hashtable<expr>        m_internal_nth_table;
+        expr_ref_vector            m_internal_nth_es;
+        unsigned_vector            m_internal_nth_lim;
 
         seq_factory*               m_factory;    // value factory
         exclusion_table            m_exclude;    // set of asserted disequalities.
         expr_ref_vector            m_axioms;     // list of axioms to add.
         obj_hashtable<expr>        m_axiom_set;
         unsigned                   m_axioms_head; // index of first axiom to add.
-        bool            m_incomplete;             // is the solver (clearly) incomplete for the fragment.
+        bool                       m_incomplete;             // is the solver (clearly) incomplete for the fragment.
         expr_ref_vector     m_int_string;
         obj_map<expr, rational> m_si_axioms;
         obj_hashtable<expr> m_has_length;          // is length applied
@@ -357,7 +360,7 @@ namespace smt {
         th_trail_stack   m_trail_stack;
         stats            m_stats;
         symbol           m_prefix, m_suffix, m_accept, m_reject;
-        symbol           m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
+        symbol           m_tail, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
         symbol           m_pre, m_post, m_eq, m_seq_align;
         ptr_vector<expr> m_todo;
         expr_ref_vector  m_ls, m_rs, m_lhs, m_rhs;