diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index 2be078b9f..dd4b05eb3 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -420,7 +420,7 @@ namespace seq {
         expr_ref cnt(seq.str.mk_contains(t, s), m);
         expr_ref i_eq_m1 = mk_eq(i, minus_one);
         expr_ref i_eq_0 = mk_eq(i, zero);
-        expr_ref s_eq_empty = mk_eq_empty(s);
+        expr_ref s_eq_empty = mk_eq(s, seq.str.mk_empty(s->get_sort()));
         expr_ref t_eq_empty = mk_eq_empty(t);
 
         // |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index ce407e243..d36861ea8 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1578,6 +1578,7 @@ br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) {
    indexof(s, b, c) -> -1 if c < 0
    indexof(a, "", 0) -> if a = "" then 0 else -1
    indexof("", b, r) -> if b = "" and r = 0 then 0 else -1
+   indexof(a, "", x) -> if 0 <= x <= len(a) then x else - 1
    indexof(unit(x)+a, b, r+1) -> indexof(a, b, r) 
    indexof(unit(x)+a, unit(y)+b, 0) -> indexof(a,unit(y)+b, 0) if x != y
    indexof(substr(x,y,len1), z, len2) -> -1 if len2 > len1
@@ -1591,11 +1592,11 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
 
     if (isc1 && isc2 && m_autil.is_numeral(c, r) && r.is_unsigned()) {
         int idx = s1.indexofu(s2, r.get_unsigned());
-        result = m_autil.mk_numeral(rational(idx), true);
+        result = m_autil.mk_int(idx);
         return BR_DONE;
     }
     if (m_autil.is_numeral(c, r) && r.is_neg()) {
-        result = m_autil.mk_numeral(rational(-1), true);
+        result = m_autil.mk_int(-1);
         return BR_DONE;
     }
     
@@ -1604,6 +1605,14 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
         return BR_DONE;
     }
 
+    if (str().is_empty(b)) {
+        result = m().mk_ite(m().mk_and(m_autil.mk_le(m_autil.mk_int(0), c),
+                                       m_autil.mk_le(c, str().mk_length(a))),
+                            c,
+                            m_autil.mk_int(-1));
+        return BR_REWRITE2;
+    }
+
     
     if (str().is_empty(a)) {
         expr* emp = str().mk_is_empty(b);