diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index dc7307741..caf8bd5cb 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -144,6 +144,9 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
     if (length() < src.length()) {
         return zstring(*this);
     }
+    if (src.length() == 0) {
+        return zstring(*this);
+    }
     bool found = false;
     for (unsigned i = 0; i < length(); ++i) {
         bool eq = !found && i + src.length() <= length();
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 15122d7b6..6a2208ad4 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2903,10 +2903,12 @@ void theory_seq::add_replace_axiom(expr* r) {
     expr_ref xsy = mk_concat(x, s, y);
     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(cnt,  mk_seq_eq(r, a));
-    add_axiom(~cnt, a_emp, mk_seq_eq(a, xsy));
-    add_axiom(~cnt, a_emp, mk_seq_eq(r, xty));
+    add_axiom(~s_emp, mk_seq_eq(r, 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);
 }