diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 17c3b1b88..9c70f5999 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -980,10 +980,6 @@ namespace smt {
 
         void push_eq(enode * lhs, enode * rhs, eq_justification const & js) {
             SASSERT(lhs != rhs);
-            {
-                seq_util u(get_manager());
-                SASSERT(!u.is_re(lhs->get_owner()));
-            }
             m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js));
         }
 
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index da275de24..ec22e8520 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3927,8 +3927,6 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
     }
     else if (n1 != n2 && m_util.is_re(n1->get_owner())) {
         // ignore
-        UNREACHABLE();
-
         // eautomaton* a1 = get_automaton(n1->get_owner());
         // eautomaton* a2 = get_automaton(n2->get_owner());
         // eautomaton* b1 = mk_difference(*a1, *a2);