diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index 35e2bf397..2e2a0cff2 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -1030,6 +1030,29 @@ namespace seq {
         add_clause(le, emp);
     }
 
+    /**
+     * Assume that r has the property that if r accepts string p
+     * then r does *not* accept any suffix of p. It is conceptually easy to 
+     * convert a deterministic automaton for a regex to a suffix blocking acceptor
+     * by redirecting removing outgoing edges from accepting states and redirecting them
+     * to a sink. Alternative, introduce a different string membership predicate that is 
+     * prefix sensitive. 
+     *
+     * Let e = replace_re(s, r, t)
+     * Then a claim is that the following axioms suffice to encode str.replace_re
+     * 
+     * s = "" => e = t
+     * r = "" => e = s + t
+     * s not in .*r.* => e = t
+     * s = x + y + [z] + u & y + [z] in r & x + y not in .*r.* => e = x + t + u
+     */
+    void axioms::replace_re_axiom(expr* e) {
+        expr* s = nullptr, *r = nullptr, *t = nullptr;
+        VERIFY(seq.str.is_replace_re(e, s, r, t)); 
+        NOT_IMPLEMENTED_YET();
+    }
+
+
 
     /**
        Unit is injective:
@@ -1171,4 +1194,5 @@ namespace seq {
         return bound_tracker;
     }
 
+
 }
diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h
index 6cd83b00f..0a2eb2ed2 100644
--- a/src/ast/rewriter/seq_axioms.h
+++ b/src/ast/rewriter/seq_axioms.h
@@ -106,6 +106,7 @@ namespace seq {
         void unit_axiom(expr* n);
         void length_axiom(expr* n);
         void unroll_not_contains(expr* e);
+        void replace_re_axiom(expr* e);
 
         expr_ref length_limit(expr* s, unsigned k);
         expr_ref is_digit(expr* ch);