diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 955d6f34b..c17ba3d92 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -2207,7 +2207,7 @@ expr_ref seq_rewriter::is_nullable(expr* r) {
 }
 
 /*
-    Push reverse inwards (gets stuck at variables and strings).
+    Push reverse inwards (whenever possible).
 */
 br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
     sort* seq_sort = nullptr;
@@ -2286,7 +2286,7 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
         return BR_REWRITE3;
     }
     else {
-        // stuck cases: variable, re().is_to_re, re().is_derivative, ...
+        // stuck cases: variable, re().is_derivative, ...
         return BR_FAILED;
     }
 }
@@ -2410,26 +2410,6 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
             return BR_FAILED;
         }
     }
-    else if (re().is_reverse(r, r1) && re().is_to_re(r1, r2)) {
-        // Reverses are rewritten so that the only derivative case is
-        // derivative of a reverse of a string. (All other cases stuck)
-        // This is analagous to the previous is_to_re case.
-        expr_ref hd(m()), tl(m());
-        if (get_head_tail_reversed(r2, hd, tl)) {
-            result = re_and(
-                m().mk_eq(ele, tl),
-                re().mk_reverse(re().mk_to_re(hd))
-            );
-            return BR_REWRITE3;
-        }
-        else if (str().is_empty(r2)) {
-            result = re().mk_empty(m().get_sort(r));
-            return BR_DONE;
-        }
-        else {
-            return BR_FAILED;
-        }
-    }
     else if (re().is_range(r, r1, r2)) {
         // r1, r2 are sequences.
         zstring s1, s2;
@@ -2465,10 +2445,171 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
         return BR_REWRITE2;
     }
     // stuck cases: re().is_derivative, variable, ...
-    // and re().is_reverse if the reverse is not applied to a string
+    // and re().is_reverse
     return BR_FAILED;
 }
 
+/*
+    Generalized "lifted" symbolic derivative
+    lifted in the sense of having the following type:
+    regex -> (List (pred * regex))
+    The list [(p1, r1), (p2, r2), ...] represents
+    a regex disjunction: if(p1, r1, none) or if(p2, r2, none) or ...
+*/
+// br_status seq_rewriter::gen_derivative(expr* r, expr_ref& result) {
+//     sort* seq_sort = nullptr, *ele_sort = nullptr;
+//     VERIFY(m_util.is_re(r, seq_sort));
+//     VERIFY(m_util.is_seq(seq_sort, ele_sort));
+//     SASSERT(ele_sort == m().get_sort(ele));
+//     expr* r1 = nullptr, *r2 = nullptr, *p = nullptr;
+//     unsigned lo = 0, hi = 0;
+//     if (re().is_concat(r, r1, r2)) {
+//         expr_ref is_n = is_nullable(r1);
+//         expr_ref dr1(re().mk_derivative(ele, r1), m());
+//         expr_ref dr2(re().mk_derivative(ele, r2), m());
+//         result = re().mk_concat(dr1, r2);
+//         if (m().is_false(is_n)) {
+//             return BR_REWRITE2;
+//         }
+//         else if (m().is_true(is_n)) {
+//             result = re().mk_union(result, dr2);
+//             return BR_REWRITE3;
+//         }
+//         else {
+//             result = re().mk_union(result, re_and(is_n, dr2));
+//             return BR_REWRITE3;
+//         }
+//     }
+//     else if (re().is_star(r, r1)) {
+//         result = re().mk_concat(re().mk_derivative(ele, r1), r);
+//         return BR_REWRITE2;
+//     }
+//     else if (re().is_plus(r, r1)) {
+//         result = re().mk_derivative(ele, re().mk_star(r1));
+//         return BR_REWRITE1;
+//     }
+//     else if (re().is_union(r, r1, r2)) {
+//         result = re().mk_union(
+//             re().mk_derivative(ele, r1),
+//             re().mk_derivative(ele, r2)
+//         );
+//         return BR_REWRITE2;
+//     }
+//     else if (re().is_intersection(r, r1, r2)) {
+//         result = re().mk_inter(
+//             re().mk_derivative(ele, r1),
+//             re().mk_derivative(ele, r2)
+//         );
+//         return BR_REWRITE2;
+//     }
+//     else if (re().is_diff(r, r1, r2)) {
+//         result = re().mk_diff(
+//             re().mk_derivative(ele, r1),
+//             re().mk_derivative(ele, r2)
+//         );
+//         return BR_REWRITE2;
+//     }
+//     else if (m().is_ite(r, p, r1, r2)) {
+//         result = m().mk_ite(
+//             p,
+//             re().mk_derivative(ele, r1),
+//             re().mk_derivative(ele, r2)
+//         );
+//         return BR_REWRITE2;
+//     }
+//     else if (re().is_opt(r, r1)) {
+//         result = re().mk_derivative(ele, r1);
+//         return BR_REWRITE1;
+//     }
+//     else if (re().is_complement(r, r1)) {
+//         result = re().mk_complement(re().mk_derivative(ele, r1));
+//         return BR_REWRITE2;
+//     }
+//     else if (re().is_loop(r, r1, lo)) {
+//         if (lo > 0) {
+//             lo--;
+//         }
+//         result = re().mk_concat(
+//             re().mk_derivative(ele, r1),
+//             re().mk_loop(r1, lo)
+//         );
+//         return BR_REWRITE2;
+//     }
+//     else if (re().is_loop(r, r1, lo, hi)) {
+//         if (hi == 0) {
+//             result = re().mk_empty(m().get_sort(r));
+//             return BR_DONE;
+//         }
+//         hi--;
+//         if (lo > 0) {
+//             lo--;
+//         }
+//         result = re().mk_concat(
+//             re().mk_derivative(ele, r1),
+//             re().mk_loop(r1, lo, hi)
+//         );
+//         return BR_REWRITE2;
+//     }
+//     else if (re().is_full_seq(r) ||
+//              re().is_empty(r)) {
+//         result = r;
+//         return BR_DONE;
+//     }
+//     else if (re().is_to_re(r, r1)) {
+//         // r1 is a string here (not a regexp)
+//         expr_ref hd(m()), tl(m());
+//         if (get_head_tail(r1, hd, tl)) {
+//             // head must be equal; if so, derivative is tail
+//             result = re_and(m().mk_eq(ele, hd),re().mk_to_re(tl));
+//             return BR_REWRITE2;
+//         }
+//         else if (str().is_empty(r1)) {
+//             result = re().mk_empty(m().get_sort(r));
+//             return BR_DONE;
+//         }
+//         else {
+//             return BR_FAILED;
+//         }
+//     }
+//     else if (re().is_range(r, r1, r2)) {
+//         // r1, r2 are sequences.
+//         zstring s1, s2;
+//         if (str().is_string(r1, s1) && str().is_string(r2, s2)) {
+//             if (s1.length() == 1 && s2.length() == 1) {
+//                 r1 = m_util.mk_char(s1[0]);
+//                 r2 = m_util.mk_char(s2[0]);
+//                 result = m().mk_and(m_util.mk_le(r1, ele), m_util.mk_le(ele, r2));
+//                 result = re_predicate(result, seq_sort);
+//                 return BR_REWRITE3;
+//             }
+//             else {
+//                 result = re().mk_empty(m().get_sort(r));
+//                 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));
+//         return BR_DONE;
+//     }
+//     else if (re().is_of_pred(r, p)) {
+//         array_util array(m());
+//         expr* args[2] = { p, ele };
+//         result = array.mk_select(2, args);
+//         result = re_predicate(result, seq_sort);
+//         return BR_REWRITE2;
+//     }
+//     // stuck cases: re().is_derivative, variable, ...
+//     // and re().is_reverse
+//     return BR_FAILED;
+// }
+
 /*
  * pattern match against all ++ "abc" ++ all ++ "def" ++ all regexes.
 */