diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index 1d00e30bd..2c8b489ab 100644
--- a/src/smt/seq_axioms.cpp
+++ b/src/smt/seq_axioms.cpp
@@ -461,7 +461,7 @@ void seq_axioms::add_at_axiom(expr* e) {
         expr_ref nth(m);
         unsigned k = iv.get_unsigned();
         for (unsigned j = 0; j <= k; ++j) {
-            es.push_back(seq.str.mk_unit(mk_nth(s, a.mk_int(j))));
+            es.push_back(seq.str.mk_unit(mk_nth(s, j)));
         }
         nth = es.back();
         es.push_back(m_sk.mk_tail(s, i));
@@ -562,29 +562,34 @@ void seq_axioms::add_stoi_axiom(expr* e) {
    0 < i, len(s) > i  =>        stoi(s, i) = 10*stoi(s, i - 1) + digit(nth_i(s, i - 1))   
 
 Define auxiliary function with the property:
-   for 0 <= i < len(s)
+   for 0 <= i < k
      stoi(s, i) := stoi(extract(s, 0, i+1)) 
 
-   for 0 < i < len(s):
+   for 0 < i < k:
      len(s) > i  => stoi(s, i) := stoi(extract(s, 0, i))*10 + stoi(extract(s, i, 1))
      len(s) <= i => stoi(s, i) := stoi(extract(s, 0, i-1), i-1)
 
+   for i <= i < k:
+     stoi(s) > = 0, len(s) > i => is_digit(nth(s, i))     
+
  */
 void seq_axioms::add_stoi_axiom(expr* e, unsigned k) {
     SASSERT(k > 0);
     expr* s = nullptr;
     VERIFY (seq.str.is_stoi(e, s));    
     auto stoi2 = [&](unsigned j) { return m_sk.mk("seq.stoi", s, a.mk_int(j), a.mk_int()); }; 
-    auto digit = [&](unsigned j) { return m_sk.mk_digit2int(mk_nth(s, a.mk_int(j))); };
+    auto digit = [&](unsigned j) { return m_sk.mk_digit2int(mk_nth(s, j)); };
     expr_ref len = mk_len(s);
     literal ge0 = mk_ge(e, 0);
     literal lek = mk_le(len, k);
     add_axiom(~ge0, ~mk_eq(len, a.mk_int(0)));
     add_axiom(~ge0, ~lek, mk_eq(e, stoi2(k-1)));
-    add_axiom(mk_eq(len, a.mk_int(0)), mk_eq(stoi2(0), digit(0)));
+    add_axiom(mk_le(len, 0), mk_eq(stoi2(0), digit(0)));
+    add_axiom(~ge0, is_digit(mk_nth(s, 0)));
     for (unsigned i = 1; i < k; ++i) {
         add_axiom(mk_le(len, i),   mk_eq(stoi2(i), a.mk_add(a.mk_mul(a.mk_int(10), stoi2(i-1)), digit(i))));
         add_axiom(~mk_le(len, i),  mk_eq(stoi2(i), stoi2(i-1)));
+        add_axiom(~ge0, mk_le(len, i), is_digit(mk_nth(s, i)));
     }
 }
 
@@ -619,6 +624,32 @@ void seq_axioms::add_itos_axiom(expr* s, unsigned k) {
     }
 }
 
+literal seq_axioms::is_digit(expr* ch) {
+    ensure_digit_axiom();
+    literal isd = mk_literal(m_sk.mk_is_digit(ch));
+    expr_ref d2i = m_sk.mk_digit2int(ch);
+    expr_ref _lo(seq.mk_le(seq.mk_char('0'), ch), m);
+    expr_ref _hi(seq.mk_le(ch, seq.mk_char('9')), m);
+    literal lo = mk_literal(_lo);
+    literal hi = mk_literal(_hi);
+    add_axiom(~lo, ~hi, isd);
+    add_axiom(~isd, lo);
+    add_axiom(~isd, hi);
+    return isd;
+}
+
+void seq_axioms::ensure_digit_axiom() {
+    if (!m_digits_initialized) {
+        for (unsigned i = 0; i < 10; ++i) {
+            expr_ref cnst(seq.mk_char('0'+i), m);
+            add_axiom(mk_eq(m_sk.mk_digit2int(cnst), a.mk_int(i)));
+        }
+        ctx().push_trail(value_trail<context, bool>(m_digits_initialized));
+        m_digits_initialized = true;
+    }
+}
+
+
 /**
    e1 < e2 => prefix(e1, e2) or e1 = xcy e1 < e2 => prefix(e1, e2) or
    c < d e1 < e2 => prefix(e1, e2) or e2 = xdz e1 < e2 => e1 != e2
@@ -711,30 +742,6 @@ void seq_axioms::add_prefix_axiom(expr* e) {
     add_axiom(lit, e1_gt_e2, ~mk_eq(c, d));
 }
 
-literal seq_axioms::is_digit(expr* ch) {
-    literal isd = mk_literal(m_sk.mk_is_digit(ch));
-    expr_ref d2i = m_sk.mk_digit2int(ch);
-    expr_ref _lo(seq.mk_le(seq.mk_char('0'), ch), m);
-    expr_ref _hi(seq.mk_le(ch, seq.mk_char('9')), m);
-    literal lo = mk_literal(_lo);
-    literal hi = mk_literal(_hi);
-    add_axiom(~lo, ~hi, isd);
-    add_axiom(~isd, lo);
-    add_axiom(~isd, hi);
-    return isd;
-}
-
-void seq_axioms::ensure_digit_axiom() {
-    if (!m_digits_initialized) {
-        for (unsigned i = 0; i < 10; ++i) {
-            expr_ref cnst(seq.mk_char('0'+i), m);
-            add_axiom(mk_eq(m_sk.mk_digit2int(cnst), a.mk_int(i)));
-        }
-        ctx().push_trail(value_trail<context, bool>(m_digits_initialized));
-        m_digits_initialized = true;
-    }
-}
-
 
 expr_ref seq_axioms::add_length_limit(expr* s, unsigned k) {
     expr_ref bound_tracker  = m_sk.mk_length_limit(s, k);
diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h
index 63dea963f..712db8ad9 100644
--- a/src/smt/seq_axioms.h
+++ b/src/smt/seq_axioms.h
@@ -46,7 +46,7 @@ namespace smt {
         expr_ref mk_sub(expr* x, expr* y);
         expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(seq.str.mk_concat(e1, e2, e3), m); }
         expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(seq.str.mk_concat(e1, e2), m); }
-        expr_ref mk_nth(expr* e, expr* i) { return expr_ref(seq.str.mk_nth_i(e, i), m); }
+        expr_ref mk_nth(expr* e, unsigned i) { return expr_ref(seq.str.mk_nth_i(e, a.mk_int(i)), m); }
         literal mk_ge(expr* e, int k) { return mk_ge_e(e, a.mk_int(k)); }
         literal mk_le(expr* e, int k) { return mk_le_e(e, a.mk_int(k)); }
         literal mk_ge(expr* e, rational const& k) { return mk_ge_e(e, a.mk_int(k)); }
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 21c7b325a..d2160cc57 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -197,6 +197,7 @@ namespace smt {
             for (auto & kv : sorted_exprs) {
                 expr* e = kv.first;
                 if (!is_app(e) || 
+                    !m.is_bool(e) ||
                     to_app(e)->get_family_id() == null_family_id || 
                     to_app(e)->get_family_id() == m.get_basic_family_id()) 
                     internalize_rec(e, kv.second);