diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 814b2168f..d36f61a85 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -637,6 +637,14 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
         result = a;
         return BR_DONE;
     }
+    if (m_util.str.is_string(b, s1) && s2.length() == 0) {
+        result = m_util.str.mk_concat(a, c);
+        return BR_REWRITE1;
+    }
+    if (m_util.str.is_string(a, s1) && s1.length() == 0) {
+        result = a;
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
 
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 5b862b2d1..3f9369f14 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2925,12 +2925,12 @@ void theory_seq::add_replace_axiom(expr* r) {
     expr_ref y  = mk_skolem(m_indexof_right, a, s);
     expr_ref xty = mk_concat(x, t, y);
     expr_ref xsy = mk_concat(x, s, y);
-    literal cnt = mk_literal(m_util.str.mk_contains(a ,s));
+    literal cnt = mk_literal(m_util.str.mk_contains(a, s));
     literal a_emp = mk_eq_empty(a);
     literal s_emp = mk_eq_empty(s);
-    add_axiom(~a_emp, mk_seq_eq(r, a));
+    add_axiom(~a_emp, s_emp, mk_seq_eq(r, a));
     add_axiom(cnt,  mk_seq_eq(r, a));
-    add_axiom(~s_emp, mk_seq_eq(r, a));
+    add_axiom(~s_emp, mk_seq_eq(r, mk_concat(t, a)));
     add_axiom(~cnt, a_emp, s_emp, mk_seq_eq(a, xsy));
     add_axiom(~cnt, a_emp, s_emp, mk_seq_eq(r, xty));
     tightest_prefix(s, x);