diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 68ddad07d..cb915d86b 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -459,9 +459,11 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_SEQ_AT:
         SASSERT(num_args == 2);
         return mk_seq_at(args[0], args[1], result); 
+#if 0
     case OP_SEQ_NTH:
         SASSERT(num_args == 2);
         return mk_seq_nth(args[0], args[1], result); 
+#endif
     case OP_SEQ_PREFIX: 
         SASSERT(num_args == 2);
         return mk_seq_prefix(args[0], args[1], result);
@@ -896,15 +898,9 @@ br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) {
         if (m_util.str.is_unit(a, u)) {
             if (len == i) {
                 result = u;
-                return BR_REWRITE1;
+                return BR_DONE;
             }            
         }
-        else if (i > 0) {
-            SASSERT(len >= i);
-            result = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i);
-            result = m().mk_app(m_util.get_family_id(), OP_SEQ_NTH, result, m_autil.mk_int(len - i));
-            return BR_REWRITE2;
-        }
         else {
             return BR_FAILED;
         }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 71d448960..936953d0a 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -4261,6 +4261,9 @@ void theory_seq::deque_axiom(expr* n) {
     else if (m_util.str.is_at(n)) {
         add_at_axiom(n);
     }
+    else if (m_util.str.is_nth(n)) {
+        add_nth_axiom(n);
+    }
     else if (m_util.str.is_string(n)) {
         add_elim_string_axiom(n);
     }
@@ -4965,6 +4968,17 @@ void theory_seq::add_at_axiom(expr* e) {
     add_axiom(~i_ge_len_s, mk_eq(e, emp, false));
 }
 
+void theory_seq::add_nth_axiom(expr* e) {
+    expr* s = nullptr, *i = nullptr;
+    rational n;
+    zstring str;
+    VERIFY(m_util.str.is_nth(e, s, i));
+    if (m_util.str.is_string(s, str) && m_autil.is_numeral(i, n) && n.is_unsigned() && n.get_unsigned() < str.length()) {
+        app_ref ch(m_util.str.mk_char(str[n.get_unsigned()]), m);
+        add_axiom(mk_eq(ch, e, false));
+    }
+}
+
 
 /*
     lit => s = (nth s 0) ++ (nth s 1) ++ ... ++ (nth s idx) ++ (tail s idx)
@@ -5431,6 +5445,7 @@ void theory_seq::relevant_eh(app* n) {
         m_util.str.is_replace(n) ||
         m_util.str.is_extract(n) ||
         m_util.str.is_at(n) ||
+        m_util.str.is_nth(n) ||
         m_util.str.is_empty(n) ||
         m_util.str.is_string(n) ||
         m_util.str.is_itos(n) || 
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 9925188b6..242d24e4f 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -575,6 +575,7 @@ namespace smt {
 
         expr_ref add_elim_string_axiom(expr* n);
         void add_at_axiom(expr* n);
+        void add_nth_axiom(expr* n);
         void add_in_re_axiom(expr* n);
         void add_itos_axiom(expr* n);
         void add_stoi_axiom(expr* n);