diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 9481057eb..1d2977e5c 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -543,6 +543,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 2);
         st = mk_re_range(args[0], args[1], result);
         break;
+    case OP_RE_DIFF: 
+        if (num_args == 2)
+            st = mk_re_diff(args[0], args[1], result);
+        break;
     case OP_RE_INTERSECT:
         if (num_args == 1) {
             result = args[0];
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index db486b473..6ba2b5130 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -311,7 +311,7 @@ namespace smt {
      *
      */
     void seq_regex::propagate_is_non_empty(literal lit) {
-        expr* e = ctx.bool_var2expr(lit.var()), *r, *u;
+        expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr;
         VERIFY(sk().is_is_non_empty(e, r, u));
         expr_ref is_nullable = seq_rw().is_nullable(r);
         rewrite(is_nullable);
@@ -350,7 +350,7 @@ namespace smt {
       is_empty(r, u) is true if r is a member of u
      */
     void seq_regex::propagate_is_empty(literal lit) {
-        expr* e = ctx.bool_var2expr(lit.var()), *r, *u;
+        expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr;
         VERIFY(sk().is_is_empty(e, r, u));
         expr_ref is_nullable = seq_rw().is_nullable(r);
         rewrite(is_nullable);
@@ -382,7 +382,7 @@ namespace smt {
             if (!m.is_true(cond)) {
                 lits.push_back(th.mk_literal(mk_forall(m, hd, mk_not(m, cond))));
             }
-            expr_ref is_empty1 = sk().mk_is_non_empty(p.second, re().mk_union(u, r));    
+            expr_ref is_empty1 = sk().mk_is_empty(p.second, re().mk_union(u, r));    
             lits.push_back(th.mk_literal(is_empty1)); 
             th.add_axiom(lits);
         }