diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 2b8689264..80d125c32 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -306,14 +306,10 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
         return BR_REWRITE2;
     }
     if (m_util.str.is_empty(a)) {
-        result = a;
-        return BR_DONE;
-    }
-    if (m_util.str.is_empty(b)) {
         result = b;
         return BR_DONE;
     }
-    if (m_util.re.is_full(a) && m_util.re.is_full(b)) {
+    if (m_util.str.is_empty(b)) {
         result = a;
         return BR_DONE;
     }
@@ -860,6 +856,18 @@ br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
+	if (m_util.re.is_full(a) && m_util.re.is_full(b)) {
+		result = a;
+		return BR_DONE;
+	}
+	if (m_util.re.is_empty(a)) {
+		result = a;
+		return BR_DONE;
+	}
+	if (m_util.re.is_empty(b)) {
+		result = b;
+		return BR_DONE;
+	}
     if (is_epsilon(a)) {
         result = b;
         return BR_DONE;
diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h
index 084f3e4f8..a5acc18af 100644
--- a/src/math/automata/automaton.h
+++ b/src/math/automata/automaton.h
@@ -543,8 +543,16 @@ private:
 
 
     void add(move const& mv) {
-        m_delta[mv.src()].push_back(mv);
-        m_delta_inv[mv.dst()].push_back(mv);
+        if (!is_duplicate_cheap(mv)) {
+            m_delta[mv.src()].push_back(mv);
+            m_delta_inv[mv.dst()].push_back(mv);
+        }
+    }
+
+    bool is_duplicate_cheap(move const& mv) const {
+        if (m_delta[mv.src()].empty()) return false;
+        move const& mv0 = m_delta[mv.src()].back();
+        return mv0.src() == mv.src() && mv0.dst() == mv.dst() && mv0.t() == mv.t();
     }