diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 8b6c5baba..15122d7b6 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2902,9 +2902,11 @@ void theory_seq::add_replace_axiom(expr* r) {
     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 a_emp = mk_eq_empty(a);
+    add_axiom(~a_emp, mk_seq_eq(r, a));
     add_axiom(cnt,  mk_seq_eq(r, a));
-    add_axiom(~cnt, mk_seq_eq(a, xsy));
-    add_axiom(~cnt, mk_seq_eq(r, xty));
+    add_axiom(~cnt, a_emp, mk_seq_eq(a, xsy));
+    add_axiom(~cnt, a_emp, mk_seq_eq(r, xty));
     tightest_prefix(s, x);
 }