diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index c89b59dcb..59f98d93a 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -735,6 +735,12 @@ br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) {
    "" + a = a
    string + (string + a) = string + a
 */
+expr_ref seq_rewriter::mk_seq_concat(expr* a, expr* b) {
+    expr_ref result(m());
+    if (BR_FAILED == mk_seq_concat(a, b, result))
+        result = str().mk_concat(a, b);
+    return result;
+}
 br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
     zstring s1, s2;
     expr* c, *d;
@@ -2074,7 +2080,7 @@ bool seq_rewriter::get_head_tail(expr* s, expr_ref& head, expr_ref& tail) {
         return true;
     }
     if (str().is_concat(s, h, t) && get_head_tail(h, head, tail)) {
-        tail = str().mk_concat(tail, t);
+        tail = mk_seq_concat(tail, t);
         return true;
     }
     return false;
@@ -2097,7 +2103,7 @@ bool seq_rewriter::get_head_tail_reversed(expr* s, expr_ref& head, expr_ref& tai
         return true;
     }
     if (str().is_concat(s, h, t) && get_head_tail_reversed(t, head, tail)) {
-        head = str().mk_concat(h, head);
+        head = mk_seq_concat(h, head);
         return true;
     }
     return false;
@@ -2179,6 +2185,7 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
     sort* seq_sort = nullptr;
     VERIFY(m_util.is_re(r, seq_sort));
     expr* r1 = nullptr, *r2 = nullptr, *p = nullptr, *s = nullptr;
+    expr* s1 = nullptr, *s2 = nullptr;
     zstring zs;
     unsigned lo = 0, hi = 0;
     if (re().is_concat(r, r1, r2)) {
@@ -2241,6 +2248,15 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
         result = re().mk_to_re(str().mk_string(zs.reverse()));
         return BR_DONE;
     }
+    else if (re().is_to_re(r, s) && str().is_unit(s)) {
+        result = r;
+        return BR_DONE;
+    }
+    else if (re().is_to_re(r, s) && str().is_concat(s, s1, s2)) {
+        result = re().mk_concat(re().mk_reverse(re().mk_to_re(s2)), 
+                                re().mk_reverse(re().mk_to_re(s1)));
+        return BR_REWRITE3;
+    }
     else {
         // stuck cases: variable, re().is_to_re, re().is_derivative, ...
         return BR_FAILED;
@@ -2402,6 +2418,12 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
                 return BR_DONE;
             }
         }
+        expr* e1 = nullptr, *e2 = nullptr;
+        if (str().is_unit(r1, e1) && str().is_unit(r2, e2)) {
+            result = m().mk_and(m_util.mk_le(e1, ele), m_util.mk_le(ele, e2));
+            result = re_predicate(result, seq_sort);
+            return BR_REWRITE2;
+        }
     }
     else if (re().is_full_char(r)) {
         result = re().mk_to_re(str().mk_empty(seq_sort));
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 9bf56370d..afa6f5a40 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -138,6 +138,7 @@ class seq_rewriter {
     bool get_head_tail_reversed(expr* e, expr_ref& head, expr_ref& tail);
     expr_ref re_and(expr* cond, expr* r);
     expr_ref re_predicate(expr* cond, sort* seq_sort);
+    expr_ref mk_seq_concat(expr* a, expr* b);    
 
     br_status mk_seq_unit(expr* e, expr_ref& result);
     br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index 4240dbcb5..0a5d5d597 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -1207,7 +1207,7 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
             switch (ctx.get_assignment(lit)) {
             case l_true:  break;
             case l_false: start = 0; return true;
-            case l_undef: ctx.force_phase(~lit); start = 0; return true;
+            case l_undef: ctx.mark_as_relevant(lit); ctx.force_phase(~lit); start = 0; return true;
             }
         }
         set_conflict(dep, lits);