diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index b9ed08cf7..1456676b4 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -599,6 +599,7 @@ void seq_decl_plugin::init() {
     m_sigs[OP_RE_CONCAT]     = alloc(psig, m, "re.++",        1, 2, reAreA, reA);
     m_sigs[OP_RE_UNION]      = alloc(psig, m, "re.union",     1, 2, reAreA, reA);
     m_sigs[OP_RE_INTERSECT]  = alloc(psig, m, "re.inter",     1, 2, reAreA, reA);
+    m_sigs[OP_RE_DIFF]       = alloc(psig, m, "re.diff",      1, 2, reAreA, reA);
     m_sigs[OP_RE_LOOP]           = alloc(psig, m, "re.loop",    1, 1, &reA, reA);
     m_sigs[OP_RE_POWER]          = alloc(psig, m, "re.^", 1, 1, &reA, reA);
     m_sigs[OP_RE_COMPLEMENT]     = alloc(psig, m, "re.comp", 1, 1, &reA, reA);
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index fb15721d4..db486b473 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -280,21 +280,17 @@ namespace smt {
     }
 
     void seq_regex::propagate_eq(expr* r1, expr* r2) {
-        expr_ref r = symmetric_diff(r1, r2);
-        sort* seq_sort = nullptr;        
-        VERIFY(u().is_re(r, seq_sort));
-        expr_ref emp(re().mk_empty(seq_sort), m);
+        expr_ref r = symmetric_diff(r1, r2);       
+        expr_ref emp(re().mk_empty(m.get_sort(r)), m);
         expr_ref is_empty = sk().mk_is_empty(r, emp);
-        th.add_axiom(~th.mk_eq(r, emp, false), th.mk_literal(is_empty));
+        th.add_axiom(~th.mk_eq(r1, r2, false), th.mk_literal(is_empty));
     }
     
     void seq_regex::propagate_ne(expr* r1, expr* r2) {
         expr_ref r = symmetric_diff(r1, r2);
-        sort* seq_sort = nullptr;        
-        VERIFY(u().is_re(r, seq_sort));
-        expr_ref emp(re().mk_empty(seq_sort), m);
+        expr_ref emp(re().mk_empty(m.get_sort(r)), m);
         expr_ref is_non_empty = sk().mk_is_non_empty(r, emp);
-        th.add_axiom(th.mk_eq(r, emp, false), th.mk_literal(is_non_empty));
+        th.add_axiom(th.mk_eq(r1, r2, false), th.mk_literal(is_non_empty));
     }
 
     bool seq_regex::is_member(expr* r, expr* u) {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 52f2401fb..4ee901d10 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1536,6 +1536,7 @@ bool theory_seq::internalize_term(app* term) {
     }
 
     if (ctx.get_fparams().m_seq_use_derivatives && 
+        m.is_bool(term) && 
         (m_util.str.is_in_re(term) || m_sk.is_skolem(term))) {
         bool_var bv = ctx.mk_bool_var(term);
         ctx.set_var_theory(bv, get_id());