diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index e3fbe8ca0..077299a88 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -2995,6 +2995,7 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
         result = re().mk_union(a1, re().mk_union(a2, b));
         return BR_REWRITE2;
     }
+        
     auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); };
     if (re().is_union(b, b1, b2)) {
         if (is_subset(a, b1)) {
@@ -3015,10 +3016,6 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
         }
     }
     else {
-        if (get_id(a) > get_id(b)) {
-            result = re().mk_union(b, a);
-            return BR_DONE;
-        }
         if (is_subset(a, b)) {
             result = b;
             return BR_DONE;
@@ -3027,6 +3024,10 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
             result = a;
             return BR_DONE;
         }
+        if (get_id(a) > get_id(b)) {
+            result = re().mk_union(b, a);
+            return BR_DONE;
+        }
     }
     return BR_FAILED;
 }
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index 6044f0275..e667d0f5b 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -225,8 +225,8 @@ namespace smt {
         d = derivative_wrapper(m.mk_var(0, m.get_sort(head)), r);
         // timer tm;
         // std::cout << d->get_id() << " " << tm.get_seconds() << "\n";
-        // if (tm.get_seconds() > 1) 
-        //     std::cout << d << "\n";
+        //if (tm.get_seconds() > 0.3) 
+        //    std::cout << d << "\n";
         // std::cout.flush();
         literal_vector conds;
         conds.push_back(~lit);