diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 27ed95155..f91685d43 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3221,7 +3221,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
     // ~contains(t,s) <=> indexof(t,s,offset) = -1
 
     add_axiom(cnt,  i_eq_m1);
-    add_axiom(~cnt,  ~i_eq_m1);
+//    add_axiom(~cnt,  ~i_eq_m1);
     add_axiom(~t_eq_empty, s_eq_empty, i_eq_m1);
 
     if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) {
@@ -3234,6 +3234,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
         add_axiom(~s_eq_empty, i_eq_0);
         add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy));
         add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx, false));
+        add_axiom(~cnt, mk_literal(m_autil.mk_ge(i, zero)));
         tightest_prefix(s, x);
     }
     else {