diff --git a/CMakeLists.txt b/CMakeLists.txt
index 1ae3bce9a..7cf4eec58 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -315,6 +315,7 @@ endif()
 ################################################################################
 # Threading support
 ################################################################################
+set(THREADS_PREFER_PTHREAD_FLAG TRUE)
 find_package(Threads)
 list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT})
 
diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp
index 942448a7f..e740a21c3 100644
--- a/src/api/api_log.cpp
+++ b/src/api/api_log.cpp
@@ -54,7 +54,7 @@ extern "C" {
             res = false;
         }
         else {
-            *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n";
+            *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << "\"\n";
             g_z3_log->flush();
             g_z3_log_enabled = true;
         }
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 2d5a016e6..e1237fcda 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -416,6 +416,9 @@ br_status seq_rewriter::mk_bool_app(func_decl* f, unsigned n, expr* const* args,
         return mk_bool_app_helper(true, n, args, result);
     case OP_OR:
         return mk_bool_app_helper(false, n, args, result);
+    case OP_EQ:
+        SASSERT(n == 2);
+        // return mk_eq_helper(args[0], args[1], result);
     default:
         return BR_FAILED;
     }
@@ -492,7 +495,27 @@ br_status seq_rewriter::mk_bool_app_helper(bool is_and, unsigned n, expr* const*
         }
     }
     
-    result = is_and ? m().mk_and(new_args.size(), new_args.c_ptr()) : m().mk_or(new_args.size(), new_args.c_ptr());
+    result = is_and ? m().mk_and(new_args) : m().mk_or(new_args);
+    return BR_REWRITE_FULL;
+}
+
+br_status seq_rewriter::mk_eq_helper(expr* a, expr* b, expr_ref& result) {
+    expr* sa = nullptr, *ra = nullptr, *sb = nullptr, *rb = nullptr;
+    if (str().is_in_re(b))
+        std::swap(a, b);
+    if (!str().is_in_re(a, sa, ra))
+        return BR_FAILED;
+    bool is_not = m().is_not(b, b);
+    if (!str().is_in_re(b, sb, rb))
+        return BR_FAILED;
+    if (sa != sb)
+        return BR_FAILED;
+    // sa in ra = sb in rb;
+    // sa in (ra n rb) u (C(ra) n C(rb))
+    if (is_not)
+        rb = re().mk_complement(rb);
+    expr* r = re().mk_union(re().mk_inter(ra, rb), re().mk_inter(re().mk_complement(ra), re().mk_complement(rb)));
+    result = re().mk_in_re(sa, r);
     return BR_REWRITE_FULL;
 }
 
@@ -703,9 +726,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case _OP_STRING_STRIDOF:
         UNREACHABLE();
     }
-    // if (st == BR_FAILED) {
-    //     st = lift_ites_throttled(f, num_args, args, result);
-    // }
+    if (st == BR_FAILED) {
+        st = lift_ites_throttled(f, num_args, args, result);
+    }
     CTRACE("seq_verbose", st != BR_FAILED, tout << expr_ref(m().mk_app(f, num_args, args), m()) << " -> " << result << "\n";);
     SASSERT(st == BR_FAILED || m().get_sort(result) == f->get_range());
     return st;
@@ -2137,7 +2160,7 @@ expr_ref seq_rewriter::is_nullable_rec(expr* r) {
     if (!result) {
         std::cout << "(m) ";
         result = is_nullable(r);
-        m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, nullptr, result);        
+        m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, nullptr, result);
     } else {
         std::cout << "(h) ";
     }
@@ -2288,119 +2311,226 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
     Symbolic derivative: seq -> regex -> regex
     seq should be single char
 */
+
 br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
-    sort *seq_sort = nullptr, *ele_sort = nullptr;
+    result = mk_derivative(ele, r);
+    // TBD: we may even declare BR_DONE here and potentially miss some simplifications
+    return re().is_derivative(result) ? BR_DONE : BR_REWRITE_FULL;
+}
+
+/*
+    Recursive implementation of the symbolic derivative such that
+    the result is in an optimized BDD form.
+
+    Definition of BDD form:
+        if-then-elses are pushed outwards
+        and sorted by condition ID (cond->get_id()), from largest on
+        the outside to smallest on the inside.
+        Duplicate nested conditions are eliminated.
+
+*/
+expr_ref seq_rewriter::mk_derivative(expr* ele, expr* r) {
+    expr_ref result(m_op_cache.find(OP_RE_DERIVATIVE, ele, r, nullptr), m());
+    if (!result) {
+        result = mk_derivative_rec(ele, r);
+        m_op_cache.insert(OP_RE_DERIVATIVE, ele, r, nullptr, result);
+    }
+    return result;
+}
+
+expr_ref seq_rewriter::mk_der_union(expr* r1, expr* r2) {
+    return mk_der_op(OP_RE_UNION, r1, r2);
+}
+
+expr_ref seq_rewriter::mk_der_inter(expr* r1, expr* r2) {
+    return mk_der_op(OP_RE_INTERSECT, r1, r2);
+}
+
+expr_ref seq_rewriter::mk_der_concat(expr* r1, expr* r2) {
+    return mk_der_op(OP_RE_CONCAT, r1, r2);
+}
+
+/*
+    Form a derivative by combining two if-then-else expressions in BDD form.
+
+    Preconditions:
+        - k is a binary op code on REs (re.union, re.inter, etc.)
+        - a and b are in BDD form
+
+    Postcondition:
+        - result is in BDD form
+*/
+expr_ref seq_rewriter::mk_der_op_rec(decl_kind k, expr* a, expr* b) {
+    expr* ca = nullptr, *a1 = nullptr, *a2 = nullptr;
+    expr* cb = nullptr, *b1 = nullptr, *b2 = nullptr;
+    expr_ref result(m());
+    auto mk_ite = [&](expr* c, expr* a, expr* b) {
+        return (a == b) ? a : m().mk_ite(c, a, b);
+    };
+    if (m().is_ite(a, ca, a1, a2)) {
+        if (m().is_ite(b, cb, b1, b2)) {
+            if (ca == cb) {
+                expr_ref r1 = mk_der_op(k, a1, b1);
+                expr_ref r2 = mk_der_op(k, a2, b2);
+                result = mk_ite(ca, r1, r2);
+                return result;
+            }
+            else if (ca->get_id() < cb->get_id()) {
+                expr_ref r1 = mk_der_op(k, a, b1);
+                expr_ref r2 = mk_der_op(k, a, b2);
+                result = mk_ite(cb, r1, r2);
+                return result;
+            }
+        }
+        expr_ref r1 = mk_der_op(k, a1, b);
+        expr_ref r2 = mk_der_op(k, a2, b);
+        result = mk_ite(ca, r1, r2);
+        return result;
+    }
+    if (m().is_ite(b, cb, b1, b2)) {
+        expr_ref r1 = mk_der_op(k, a, b1);
+        expr_ref r2 = mk_der_op(k, a, b2);
+        result = mk_ite(cb, r1, r2);
+        return result;
+    }
+    switch (k) {
+    case OP_RE_INTERSECT:
+        if (BR_FAILED == mk_re_inter(a, b, result))
+            result = re().mk_inter(a, b);
+        break;
+    case OP_RE_UNION:
+        if (BR_FAILED == mk_re_union(a, b, result))
+            result = re().mk_union(a, b);
+        break;
+    case OP_RE_CONCAT:
+        if (BR_FAILED == mk_re_concat(a, b, result))
+            result = re().mk_concat(a, b);
+        break;
+    default:
+        UNREACHABLE();
+        break;
+    }
+    return result;
+}
+
+expr_ref seq_rewriter::mk_der_op(decl_kind k, expr* a, expr* b) {
+    expr_ref _a(a, m()), _b(b, m());
+    expr_ref result(m_op_cache.find(k, a, b, nullptr), m());
+    if (!result) {
+        result = mk_der_op_rec(k, a, b);
+        m_op_cache.insert(k, a, b, nullptr, result);
+    }
+    return result;
+}
+
+expr_ref seq_rewriter::mk_der_compl(expr* r) {
+    expr_ref result(m_op_cache.find(OP_RE_COMPLEMENT, r, nullptr, nullptr), m());
+    if (!result) {
+        expr* c = nullptr, * r1 = nullptr, * r2 = nullptr;
+        if (m().is_ite(r, c, r1, r2)) {
+            result = m().mk_ite(c, mk_der_compl(r1), mk_der_compl(r2));
+        }
+        else if (BR_FAILED == mk_re_complement(r, result))
+            result = re().mk_complement(r);        
+    }
+    m_op_cache.insert(OP_RE_COMPLEMENT, r, nullptr, nullptr, result);
+    return result;
+}
+
+expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
+    expr_ref result(m());
+    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;
+    expr* r1 = nullptr, *r2 = nullptr, *p = nullptr;
+    auto mk_empty = [&]() { return expr_ref(re().mk_empty(m().get_sort(r)), m()); };
     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);
+        expr_ref dr1 = mk_derivative(ele, r1);
+        result = mk_der_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 = m().mk_ite(is_n, re().mk_union(result, dr2), result);
-            return BR_REWRITE3;
+            return result;
         }
+        expr_ref dr2 = mk_derivative(ele, r2);
+        is_n = re_predicate(is_n, seq_sort);
+        return mk_der_union(result, mk_der_concat(is_n, dr2));        
     }
     else if (re().is_star(r, r1)) {
-        result = re().mk_concat(re().mk_derivative(ele, r1), r);
-        return BR_REWRITE2;
+        return mk_der_concat(mk_derivative(ele, r1), r);
     }
     else if (re().is_plus(r, r1)) {
-        result = re().mk_derivative(ele, re().mk_star(r1));
-        return BR_REWRITE1;
+        expr_ref star(re().mk_star(r1), m());
+        return mk_derivative(ele, star);
     }
     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;
+        return mk_der_union(mk_derivative(ele, r1), mk_derivative(ele, r2));
     }
     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;
+        return mk_der_inter(mk_derivative(ele, r1), mk_derivative(ele, r2));
     }
     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;
+        return mk_der_inter(mk_derivative(ele, r1), mk_der_compl(mk_derivative(ele, r2)));
     }
     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;
+        // there is no BDD normalization here
+        result = m().mk_ite(p, mk_derivative(ele, r1), mk_derivative(ele, r2));
+        return result;
     }
     else if (re().is_opt(r, r1)) {
-        result = re().mk_derivative(ele, r1);
-        return BR_REWRITE1;
+        return mk_derivative(ele, r1);
     }
     else if (re().is_complement(r, r1)) {
-        result = re().mk_complement(re().mk_derivative(ele, r1));
-        return BR_REWRITE2;
+        return mk_der_compl(mk_derivative(ele, r1));
     }
     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;
+        return mk_der_concat(mk_derivative(ele, r1), re().mk_loop(r1, lo));
     }
     else if (re().is_loop(r, r1, lo, hi)) {
         if (hi == 0) {
-            result = re().mk_empty(m().get_sort(r));
-            return BR_DONE;
+            return mk_empty();
         }
         hi--;
         if (lo > 0) {
             lo--;
         }
-        result = re().mk_concat(
-            re().mk_derivative(ele, r1),
-            re().mk_loop(r1, lo, hi)
-        );
-        return BR_REWRITE2;
+        return mk_der_concat(mk_derivative(ele, r1), re().mk_loop(r1, lo, hi));
     }
     else if (re().is_full_seq(r) ||
              re().is_empty(r)) {
-        result = r;
-        return BR_DONE;
+        return expr_ref(r, m());
     }
     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;
+            return re_and(m().mk_eq(ele, hd), re().mk_to_re(tl));
         }
         else if (str().is_empty(r1)) {
-            result = re().mk_empty(m().get_sort(r));
-            return BR_DONE;
+            return mk_empty();
         }
         else {
-            return BR_FAILED;
+            return expr_ref(re().mk_derivative(ele, r), m());
+        }
+    }
+    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)) {
+            return re_and(m().mk_eq(ele, tl), re().mk_reverse(re().mk_to_re(hd)));
+        }
+        else if (str().is_empty(r2)) {
+            return mk_empty();
+        }
+        else {
+            return expr_ref(re().mk_derivative(ele, r), m());
         }
     }
     else if (re().is_range(r, r1, r2)) {
@@ -2410,220 +2540,39 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
             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;
+                return mk_der_inter(re_predicate(m_util.mk_le(r1, ele), seq_sort),
+                                    re_predicate(m_util.mk_le(ele, r2), seq_sort));
             }
             else {
-                result = re().mk_empty(m().get_sort(r));
-                return BR_DONE;
+                return mk_empty();
             }
         }
         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;
+            return mk_der_inter(re_predicate(m_util.mk_le(e1, ele), seq_sort),
+                                re_predicate(m_util.mk_le(ele, e2), seq_sort));
         }
     }
     else if (re().is_full_char(r)) {
-        result = re().mk_to_re(str().mk_empty(seq_sort));
-        return BR_DONE;
+        return expr_ref(re().mk_to_re(str().mk_empty(seq_sort)), m());
     }
     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;
+        return re_predicate(result, seq_sort);
     }
     // stuck cases: re().is_derivative, variable, ...
-    // and re().is_reverse
-    return BR_FAILED;
+    // and re().is_reverse if the reverse is not applied to a string
+    return expr_ref(re().mk_derivative(ele, r), m());
 }
 
 /*
-    Combine two if-then-else expressions in BDD form.
+    Lift all ite expressions to the top level, safely
+    throttled to not blowup the size of the expression.
 
-    Definition of BDD form:
-        if-then-elses are pushed outwards
-        and sorted by condition ID (cond->get_id()), from largest on
-        the outside to smallest on the inside.
-        Duplicate nested conditions are eliminated.
-
-    Preconditions:
-    - EITHER k is a binary op code on REs (re.union, re.inter, etc.)
-      and cond is nullptr,
-      OR k is if-then-else (OP.ITE) and cond is the condition.
-    - a and b are in BDD form.
-
-    Postcondition: result is in BDD form.
-        if-then-elses are pushed outwards
-        and sorted by condition ID (cond->get_id()), from largest on
-        the outside to smallest on the inside.
-
-    Uses op cache (memoization) to avoid duplicating work for the same
-    pair of pointers.
-*/
-expr_ref seq_rewriter::combine_ites(decl_kind k, expr* a, expr* b, expr* cond) {
-    std::cout << "c";
-    expr_ref result(m_op_cache.find(k, a, b, cond), m());
-    if (result) {
-        std::cout << "(h) ";
-        return result;
-    }
-    std::cout << "(m) ";
-    std::cout << std::endl << "combine_ites: "
-                           << k << ", "
-                           << expr_ref(a, m()) << ", "
-                           << expr_ref(b, m()) << ", "
-                           << expr_ref(cond, m()) << std::endl;
-    SASSERT((k == OP_ITE) == (cond != nullptr));
-    expr *acond = nullptr, *a1 = nullptr, *a2 = nullptr,
-         *bcond = nullptr, *b1 = nullptr, *b2 = nullptr;
-    expr_ref result1(m()), result2(m());
-    if (k == OP_ITE) {
-        if (m().is_ite(a, acond, a1, a2) &&
-            cond->get_id() < acond->get_id()) {
-            std::cout << "  case 1a" << std::endl;
-            // Push ITE inwards on first arg
-            result1 = combine_ites(k, a1, b, cond);
-            result2 = combine_ites(k, a2, b, cond);
-            result = combine_ites(k, result1, result2, acond);
-        }
-        else if (m().is_ite(a, acond, a1, a2) &&
-                 cond == acond) {
-            std::cout << "  case 1b" << std::endl;
-            // Collapse ITE on first arg
-            result = combine_ites(k, a1, b, cond);
-        }
-        else if (m().is_ite(b, bcond, b1, b2) &&
-                 cond->get_id() < bcond->get_id()) {
-            // Push ITE inwards on second arg
-            std::cout << "  case 1c" << std::endl;
-            result1 = combine_ites(k, a, b1, cond);
-            result2 = combine_ites(k, a, b2, cond);
-            result = combine_ites(k, result1, result2, bcond);
-        }
-        else if (m().is_ite(b, bcond, b1, b2) &&
-                 cond == bcond) {
-            std::cout << "  case 1d" << std::endl;
-            // Collapse ITE on second arg
-            result = combine_ites(k, a, b2, cond);
-        }
-        else {
-            // Apply ITE -- no simplification required
-            std::cout << "  case 1e" << std::endl;
-            result = m().mk_ite(cond, a, b);
-        }
-    }
-    else if (m().is_ite(a, acond, a1, a2)) {
-        std::cout << "  case 2" << std::endl;
-        // Push binary op inwards on first arg
-        result1 = combine_ites(k, a1, b, nullptr);
-        result2 = combine_ites(k, a2, b, nullptr);
-        result = combine_ites(OP_ITE, result1, result2, acond);
-    }
-    else if (m().is_ite(b, bcond, b1, b2)) {
-        std::cout << "  case 3" << std::endl;
-        // Push binary op inwards on second arg
-        result1 = combine_ites(k, a, b1, nullptr);
-        result2 = combine_ites(k, a, b2, nullptr);
-        result = combine_ites(OP_ITE, result1, result2, bcond);
-    }
-    else {
-        std::cout << "  case 4" << std::endl;
-        // Apply binary op (a and b are free of ITE)
-        result = m().mk_app(get_fid(), k, a, b);
-    }
-    // Save result before returning
-    m_op_cache.insert(k, a, b, cond, result);
-    std::cout << "combine result: " << result << std::endl;
-    return result;
-}
-
-/*
-    Lift if-then-else expressions to the top level, enforcing a BDD form.
-
-    Postcondition: result is in BDD form.
-    - Alternatively, if lift_over_union and/or lift_over_inter is false,
-      then result is a disjunction and/or conjunciton of expressions in
-      BDD form. (Even in this case, ITE is still lifted at lower levels,
-      just not at the top level.)
-    - Note that the result may not be fully simplified (particularly the
-      nested expressions inside if-then-else). Simplification should be
-      called afterwards.
-
-    Cost: Causes potential blowup in the size of an expression (when
-    expanded out), but keeps the representation compact (subexpressions
-    are shared).
-
-    Used by: the regex solver in seq_regex.cpp when dealing with
-    derivatives of a regex by a symbolic character. Enables efficient
-    representation in unfolding string in regex constraints.
-*/
-expr_ref seq_rewriter::lift_ites(expr* r, bool lift_over_union, bool lift_over_inter) {
-    std::cout << "l ";
-    decl_kind k = to_app(r)->get_decl_kind();
-    family_id fid = get_fid();
-    expr *r1 = nullptr, *r2 = nullptr, *cond = nullptr, *ele = nullptr;
-    unsigned lo = 0, hi = 0;
-    expr_ref result(m()), result1(m()), result2(m());
-    if ((re().is_union(r, r1, r2) && !lift_over_union) ||
-        (re().is_intersection(r, r1, r2) && !lift_over_inter)) {
-        // Preserve unions and/or intersections
-        result1 = lift_ites(r1, lift_over_union, lift_over_inter);
-        result2 = lift_ites(r2, lift_over_union, lift_over_inter);
-        result = m().mk_app(fid, k, r1, r2);
-    }
-    else if (m().is_ite(r, cond, r1, r2) ||
-        re().is_concat(r, r1, r2) ||
-        re().is_union(r, r1, r2) ||
-        re().is_intersection(r, r1, r2) ||
-        re().is_diff(r, r1, r2)) {
-        // Use combine_ites on the subresults
-        // Stop preserving unions and intersections
-        result1 = lift_ites(r1, true, true);
-        result2 = lift_ites(r2, true, true);
-        result = combine_ites(k, r1, r2, cond);
-    }
-    else if (re().is_star(r, r1) ||
-             re().is_plus(r, r1) ||
-             re().is_opt(r, r1) ||
-             re().is_complement(r, r1) ||
-             re().is_reverse(r, r1)) {
-        // Stop preserving unions and intersections
-        result1 = lift_ites(r1, true, true);
-        result = m().mk_app(fid, k, r1);
-    }
-    else if (re().is_derivative(r, ele, r1)) {
-        result1 = lift_ites(r1, true, true);
-        result = m().mk_app(fid, k, ele, r1);
-    }
-    else if (re().is_loop(r, r1, lo)) {
-        result1 = lift_ites(r1, true, true);
-        result = re().mk_loop(result1, lo);
-    }
-    else if (re().is_loop(r, r1, lo, hi)) {
-        result1 = lift_ites(r1, true, true);
-        result = re().mk_loop(result1, lo, hi);
-    }
-    else {
-        // is_full_seq, is_empty, is_to_re, is_range, is_full_char, is_of_pred
-        result = r;
-    }
-    std::cout << std::endl << "lift of: " << expr_ref(r, m()) << std::endl;
-    std::cout << "  = " << result << std::endl;
-    return result;
-}
-
-/*
-    Lift all ite expressions to the top level, but
-    a different "safe" version which is throttled to not
-    blowup the size of the expression.
-
-    Note: this function does not ensure the same BDD form that lift_ites
-    ensures.
+    Note: this function does not ensure the same BDD form that is
+    used in the normal form for derivatives in mk_re_derivative.
 */
 br_status seq_rewriter::lift_ites_throttled(func_decl* f, unsigned n, expr* const* args, expr_ref& result) {
     expr* c = nullptr, *t = nullptr, *e = nullptr;
@@ -2644,51 +2593,6 @@ br_status seq_rewriter::lift_ites_throttled(func_decl* f, unsigned n, expr* cons
     return BR_FAILED;
 }
 
-// /*
-//     Rewrite rules for ITEs of regexes.
-//     ite(not c, r1, r2) -> ite(c, r2, r1)
-//     ite(c, ite(c, r1, r2), r3)) -> ite(c, r1, r3)
-//     ite(c, r1, ite(c, r2, r3)) -> ite(c, r1, r3)
-//     ite(c1, ite(c2, r1, r2), r3) where id of c1 < id of c2 ->
-//         ite(c2, ite(c1, r1, r3), ite(c1, r2, r3))
-//     ite(c1, r1, ite(c2, r2, r3)) where id of c1 < id of c2 ->
-//         ite(c2, ite(c1, r1, r2), ite(c1, r1, r3))
-// */
-// br_status seq_rewriter::rewrite_re_ite(expr* cond, expr* r1, expr* r2, expr_ref& result) {
-//     VERIFY(m_util.is_re(r1));
-//     VERIFY(m_util.is_re(r2));
-//     expr *c = nullptr, *ra = nullptr, *rb = nullptr;
-//     if (m().is_not(cond, c)) {
-//         result = m().mk_ite(c, r2, r1);
-//         return BR_REWRITE1;
-//     }
-//     if (m().is_ite(r1, c, ra, rb)) {
-//         if (m().are_equal(c, cond)) {
-//             result = m().mk_ite(cond, ra, r2);
-//             return BR_REWRITE1;
-//         }
-//         if (cond->get_id() < c->get_id()) {
-//             expr *result1 = m().mk_ite(cond, ra, r2);
-//             expr *result2 = m().mk_ite(cond, rb, r2);
-//             result = m().mk_ite(c, result1, result2);
-//             return BR_REWRITE2;
-//         }
-//     }
-//     if (m().is_ite(r2, c, ra, rb)) {
-//         if (m().are_equal(c, cond)) {
-//             result = m().mk_ite(cond, r1, rb);
-//             return BR_REWRITE1;
-//         }
-//         if (cond->get_id() < c->get_id()) {
-//             expr *result1 = m().mk_ite(cond, r1, ra);
-//             expr* result2 = m().mk_ite(cond, r1, rb);
-//             result = m().mk_ite(c, result1, result2);
-//             return BR_REWRITE2;
-//         }
-//     }
-//     return BR_DONE;
-// }
-
 /*
  * pattern match against all ++ "abc" ++ all ++ "def" ++ all regexes.
 */
@@ -2885,7 +2789,6 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
         return BR_REWRITE_FULL;
     }
 
-#if 0
     if (get_re_head_tail(b, hd, tl)) {
         SASSERT(re().min_length(hd) == re().max_length(hd));
         expr_ref len_hd(m_autil.mk_int(re().min_length(hd)), m()); 
@@ -2906,7 +2809,6 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
                             re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl));
         return BR_REWRITE_FULL;
     }
-#endif
     if (false && rewrite_contains_pattern(a, b, result))
         return BR_REWRITE_FULL;
 
@@ -2998,6 +2900,50 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
     }
     return BR_FAILED;
 }
+
+bool seq_rewriter::are_complements(expr* r1, expr* r2) const {
+    expr* r = nullptr;
+    if (re().is_complement(r1, r) && r == r2)
+        return true;
+    if (re().is_complement(r2, r) && r == r1)
+        return true;
+    return false;
+}
+
+/*
+ * basic subset checker.
+ */
+bool seq_rewriter::is_subset(expr* r1, expr* r2) const {
+    // return false;
+    expr* ra1 = nullptr, *ra2 = nullptr, *ra3 = nullptr;
+    expr* rb1 = nullptr, *rb2 = nullptr, *rb3 = nullptr;
+    if (re().is_complement(r1, ra1) && 
+        re().is_complement(r2, rb1)) {
+        return is_subset(rb1, ra1);
+    }
+    auto is_concat = [&](expr* r, expr*& a, expr*& b, expr*& c) {
+        return re().is_concat(r, a, b) && re().is_concat(b, b, c);
+    };
+    while (true) {
+        if (r1 == r2)
+            return true;
+        if (re().is_full_seq(r2))
+            return true;
+        if (is_concat(r1, ra1, ra2, ra3) &&
+            is_concat(r2, rb1, rb2, rb3) && ra1 == rb1 && ra2 == rb2) {
+            r1 = ra3;
+            r2 = rb3;
+            continue;
+        }
+        if (re().is_concat(r1, ra1, ra2) && 
+            re().is_concat(r2, rb1, rb2) && re().is_full_seq(rb1)) {
+            r1 = ra2;
+            continue;
+        }
+        return false;
+    }
+}
+
 /*
     (a + a) = a
     (a + eps) = a
@@ -3032,18 +2978,66 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
         result = b;
         return BR_DONE;
     }
+    auto mk_full = [&]() { return re().mk_full_seq(m().get_sort(a)); };
+    if (are_complements(a, b)) {
+        result = mk_full();
+        return BR_DONE;
+    }
+        
+    expr* a1 = nullptr, *a2 = nullptr;
+    expr* b1 = nullptr, *b2 = nullptr;
+    // ensure union is right-associative
+    // and swap-sort entries 
+    if (re().is_union(a, a1, a2)) {
+        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)) {
+            result = b;
+            return BR_DONE;
+        }
+        if (is_subset(b1, a)) {
+            result = re().mk_union(a, b2);
+            return BR_REWRITE1;
+        }
+        if (are_complements(a, b1)) {
+            result = mk_full();
+            return BR_DONE;
+        }
+        if (get_id(a) > get_id(b1)) {
+            result = re().mk_union(b1, re().mk_union(a, b2));
+            return BR_REWRITE2;
+        }
+    }
+    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;
+        }
+        if (is_subset(b, a)) {
+            result = a;
+            return BR_DONE;
+        }
+    }
     return BR_FAILED;
 }
 
 /*
     comp(intersect e1 e2) -> union comp(e1) comp(e2)
     comp(union e1 e2) -> intersect comp(e1) comp(e2)
-    comp(none) = all
-    comp(all) = none
+    comp(none) -> all
+    comp(all) -> none
+    comp(comp(e1)) -> e1
     comp(ite p e1 e2) -> ite p comp(e1) comp(e2)
 */
 br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
-    expr* e1, *e2;
+    expr *cond = nullptr, *e1 = nullptr, *e2 = nullptr;
     if (re().is_intersection(a, e1, e2)) {
         result = re().mk_union(re().mk_complement(e1), re().mk_complement(e2));
         return BR_REWRITE2;
@@ -3060,10 +3054,13 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
         result = re().mk_empty(m().get_sort(a));
         return BR_DONE;
     }
-    expr *a1 = nullptr, *a2 = nullptr, *cond = nullptr;
-    if (m().is_ite(a, cond, a1, a2)) {
-        result = m().mk_ite(cond, re().mk_complement(a1),
-                                  re().mk_complement(a2));
+    if (re().is_complement(a, e1)) {
+        result = e1;
+        return BR_DONE;
+    }
+    if (m().is_ite(a, cond, e1, e2)) {
+        result = m().mk_ite(cond, re().mk_complement(e1),
+                                  re().mk_complement(e2));
         return BR_REWRITE2;
     }
     return BR_FAILED;
@@ -3101,12 +3098,53 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) {
         result = a;
         return BR_DONE;
     }
-    expr* ac = nullptr, *bc = nullptr;
-    if ((re().is_complement(a, ac) && ac == b) ||
-        (re().is_complement(b, bc) && bc == a)) {
-        result = re().mk_empty(m().get_sort(a));
+    auto mk_empty = [&]() { return re().mk_empty(m().get_sort(a)); };
+    if (are_complements(a, b)) {
+        result = mk_empty();
         return BR_DONE;
     }
+    expr* a1 = nullptr, *a2 = nullptr;
+    expr* b1 = nullptr, *b2 = nullptr;
+
+    // ensure intersection is right-associative
+    // and swap-sort entries 
+    if (re().is_intersection(a, a1, a2)) {
+        result = re().mk_inter(a1, re().mk_inter(a2, b));
+        return BR_REWRITE2;
+    }
+    auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); };
+    if (re().is_intersection(b, b1, b2)) {
+        if (is_subset(b1, a)) {
+            result = b;
+            return BR_DONE;
+        }
+        if (is_subset(a, b1)) {
+            result = re().mk_inter(a, b2);
+            return BR_REWRITE1;
+        }
+        if (are_complements(a, b1)) {
+            result = mk_empty();
+            return BR_DONE;
+        }
+        if (get_id(a) > get_id(b1)) {
+            result = re().mk_inter(b1, re().mk_inter(a, b2));
+            return BR_REWRITE2;
+        }
+    }
+    else {
+        if (get_id(a) > get_id(b)) {
+            result = re().mk_inter(b, a);
+            return BR_DONE;
+        }
+        if (is_subset(a, b)) {
+            result = a;
+            return BR_DONE;
+        }
+        if (is_subset(b, a)) {
+            result = b;
+            return BR_DONE;
+        }
+    }
     if (re().is_to_re(b)) 
         std::swap(a, b);
     expr* s = nullptr;
@@ -3388,7 +3426,6 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
                 else                 
                     intersect(0, ch-1, ranges);
             }
-            // TBD: case for negation of range (not (and (<= lo e) (<= e hi)))
             else {
                 all_ranges = false;
                 break;
@@ -3429,124 +3466,6 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
     }    
 }
 
-void seq_rewriter::get_cofactors(expr* r, expr_ref_vector& conds, expr_ref_pair_vector& result) {
-    expr_ref cond(m()), th(m()), el(m());
-    if (has_cofactor(r, cond, th, el)) {
-        conds.push_back(cond);
-        get_cofactors(th, conds, result);
-        conds.pop_back();
-        conds.push_back(mk_not(m(), cond));
-        get_cofactors(el, conds, result);
-        conds.pop_back();
-    }
-    else {
-        cond = mk_and(conds);
-        result.push_back(cond, r);
-    }
-}
-
-bool seq_rewriter::has_cofactor(expr* r, expr_ref& cond, expr_ref& th, expr_ref& el) {
-    if (m().is_ite(r)) {
-        cond = to_app(r)->get_arg(0);
-        th = to_app(r)->get_arg(1);
-        el = to_app(r)->get_arg(2);
-        return true;
-    }
-    expr_ref_vector trail(m()), args_th(m()), args_el(m());
-    expr* c = nullptr, *tt = nullptr, *ee = nullptr;
-    cond = nullptr;
-    obj_map<expr,expr*> cache_th, cache_el;
-    expr_mark no_cofactor, visited;
-    ptr_vector<expr> todo;
-    todo.push_back(r);
-    while (!todo.empty()) {
-        expr* e = todo.back();
-        if (visited.is_marked(e) || !is_app(e)) {
-            todo.pop_back();
-            continue;
-        }        
-        app* a = to_app(e);
-        if (m().is_ite(e, c, tt, ee)) {
-            if (!cond) {
-                cond = c;
-                cache_th.insert(a, tt);
-                cache_el.insert(a, ee);
-            }
-            else if (cond == c) {
-                cache_th.insert(a, tt);
-                cache_el.insert(a, ee);
-            }
-            else {
-                no_cofactor.mark(a);
-            }
-            visited.mark(e, true);
-            todo.pop_back();
-            continue;
-        }
-
-        if (a->get_family_id() != u().get_family_id()) {
-            visited.mark(e, true);
-            no_cofactor.mark(e, true);
-            todo.pop_back();
-            continue;
-        }
-        switch (a->get_decl_kind()) {
-        case OP_RE_CONCAT:
-        case OP_RE_UNION:
-        case OP_RE_INTERSECT:
-        case OP_RE_COMPLEMENT:
-            break;
-        case OP_RE_STAR:
-        case OP_RE_LOOP:
-        default:
-            visited.mark(e, true);
-            no_cofactor.mark(e, true);
-            continue;
-        }
-        args_th.reset(); 
-        args_el.reset();
-        bool has_cof = false;
-        for (expr* arg : *a) {
-            if (no_cofactor.is_marked(arg)) {
-                args_th.push_back(arg);
-                args_el.push_back(arg);
-            }
-            else if (cache_th.contains(arg)) {
-                args_th.push_back(cache_th[arg]);
-                args_el.push_back(cache_el[arg]);
-                has_cof = true;
-            }
-            else {
-                todo.push_back(arg);
-            }
-        }
-        if (args_th.size() == a->get_num_args()) {
-            if (has_cof) {
-                th = mk_app(a->get_decl(), args_th);
-                el = mk_app(a->get_decl(), args_el);
-                trail.push_back(th);
-                trail.push_back(el);
-                cache_th.insert(a, th);
-                cache_el.insert(a, el);
-            }
-            else {
-                no_cofactor.mark(a, true);
-            }
-            visited.mark(e, true);
-            todo.pop_back();
-        }
-    }
-    SASSERT(cond == !no_cofactor.is_marked(r));
-    if (cond) {
-        th = cache_th[r];
-        el = cache_el[r];
-        return true;
-    }
-    else {
-        return false;
-    }
-}
-
 br_status seq_rewriter::reduce_re_is_empty(expr* r, expr_ref& result) {
     expr* r1, *r2, *r3, *r4;
     zstring s1, s2;
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 21ab76d07..208261474 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -182,6 +182,18 @@ class seq_rewriter {
 
     expr_ref mk_seq_concat(expr* a, expr* b);    
 
+    expr_ref mk_der_op(decl_kind k, expr* a, expr* b);
+    expr_ref mk_der_op_rec(decl_kind k, expr* a, expr* b);
+    expr_ref mk_der_concat(expr* a, expr* b);
+    expr_ref mk_der_union(expr* a, expr* b);
+    expr_ref mk_der_inter(expr* a, expr* b);
+    expr_ref mk_der_compl(expr* a);
+    expr_ref mk_derivative(expr* ele, expr* r);
+    expr_ref mk_derivative_rec(expr* ele, expr* r);
+
+    bool are_complements(expr* r1, expr* r2) const;
+    bool is_subset(expr* r1, expr* r2) const;
+
     br_status mk_seq_unit(expr* e, expr_ref& result);
     br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
     br_status mk_seq_length(expr* a, expr_ref& result);
@@ -230,6 +242,7 @@ class seq_rewriter {
     bool rewrite_contains_pattern(expr* a, expr* b, expr_ref& result);
 
     br_status mk_bool_app_helper(bool is_and, unsigned n, expr* const* args, expr_ref& result);
+    br_status mk_eq_helper(expr* a, expr* b, expr_ref& result);
 
     bool cannot_contain_prefix(expr* a, expr* b);
     bool cannot_contain_suffix(expr* a, expr* b);
@@ -265,15 +278,15 @@ class seq_rewriter {
     class seq_util::str& str() { return u().str; }
     class seq_util::str const& str() const { return u().str; }
 
-    void get_cofactors(expr* r, expr_ref_vector& conds, expr_ref_pair_vector& result);
+    expr_ref is_nullable_rec(expr* r);
     void intersect(unsigned lo, unsigned hi, svector<std::pair<unsigned, unsigned>>& ranges);
 
-    expr_ref combine_ites(decl_kind k, expr* a, expr* b, expr* cond);
     br_status lift_ites_throttled(func_decl* f, unsigned n, expr* const* args, expr_ref& result);
 
 public:
     seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
-        m_util(m), m_autil(m), m_re2aut(m), m_op_cache(m), m_es(m), m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
+        m_util(m), m_autil(m), m_re2aut(m), m_op_cache(m), m_es(m), 
+        m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
     }
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }
@@ -314,23 +327,12 @@ public:
 
     void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_pair_vector& new_eqs);
 
-    // Memoized checking for acceptance of the empty string
+    // Check for acceptance of the empty string
     expr_ref is_nullable(expr* r);
-    expr_ref is_nullable_rec(expr* r);
-
-    // utilities for cofactors of if-then-else expressions
-    bool has_cofactor(expr* r, expr_ref& cond, expr_ref& th, expr_ref& el);
-    void get_cofactors(expr* r, expr_ref_pair_vector& result) {
-        expr_ref_vector conds(m());
-        get_cofactors(r, conds, result);
-    }
 
     // heuristic elimination of element from condition that comes form a derivative.
     // special case optimization for conjunctions of equalities, disequalities and ranges.
     void elim_condition(expr* elem, expr_ref& cond);
-
-    // if-then-else rewriting support (for REs)
-    expr_ref lift_ites(expr* r, bool lift_over_union = true, bool lift_over_inter = true);
 };
 
 #endif
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 6ba8bc481..340c76805 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -203,7 +203,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 if (st != BR_FAILED)
                     return st;
             }
-            if ((k == OP_AND || k == OP_OR) && m_seq_rw.u().has_re()) {
+            if ((k == OP_AND || k == OP_OR /*|| k == OP_EQ*/) && m_seq_rw.u().has_re()) {
                 st = m_seq_rw.mk_bool_app(f, num, args, result); 
                 if (st != BR_FAILED)
                     return st;
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 8423bb1b9..d86893199 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -367,6 +367,7 @@ namespace opt {
     void context::fix_model(model_ref& mdl) {
         if (mdl && !m_model_fixed.contains(mdl.get())) {
             TRACE("opt", m_fm->display(tout << "fix-model\n");
+                  tout << *mdl << "\n";
                   if (m_model_converter) m_model_converter->display(tout););
             (*m_fm)(mdl);
             apply(m_model_converter, mdl);
@@ -482,6 +483,7 @@ namespace opt {
     lbool context::execute_box() {
         if (m_box_index < m_box_models.size()) {
             m_model = m_box_models[m_box_index];
+            CTRACE("opt", m_model, tout << *m_model << "\n";);
             ++m_box_index;           
             return l_true;
         }
@@ -505,12 +507,15 @@ namespace opt {
                 m_box_models.push_back(m_model.get());
             }
             else {
-                m_box_models.push_back(m_optsmt.get_model(j));
+                model* mdl = m_optsmt.get_model(j);
+                if (!mdl) mdl = m_model.get();
+                m_box_models.push_back(mdl);
                 ++j;
             }
         }
         if (r == l_true && !m_box_models.empty()) {
             m_model = m_box_models[0];
+            CTRACE("opt", m_model, tout << *m_model << "\n";);
         }
         return r;
     }
@@ -787,6 +792,7 @@ namespace opt {
 
     void context::normalize(expr_ref_vector const& asms) {
         expr_ref_vector fmls(m);
+        m_model_converter = nullptr;
         to_fmls(fmls);
         simplify_fmls(fmls, asms);
         from_fmls(fmls);
@@ -1248,7 +1254,7 @@ namespace opt {
             case O_MAXSMT: {
                 maxsmt& ms = *m_maxsmts.find(obj.m_id);
                 for (unsigned j = 0; j < obj.m_terms.size(); ++j) {
-                    ms.add(obj.m_terms[j].get(), obj.m_weights[j]);        
+                    ms.add(obj.m_terms.get(j), obj.m_weights[j]);        
                 }
                 break;
             }
@@ -1468,6 +1474,7 @@ namespace opt {
     void context::clear_state() {
         m_pareto = nullptr;
         m_box_index = UINT_MAX;
+        m_box_models.reset();
         m_model.reset();
         m_model_fixed.reset();
         m_core.reset();
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 8dff3f924..c8c254179 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -469,6 +469,7 @@ namespace opt {
         return l_true;
     }
 
+
     void optsmt::setup(opt_solver& solver) {
         m_s = &solver;
         solver.reset_objectives();
@@ -577,7 +578,9 @@ namespace opt {
         m_upper.reset();
         m_objs.reset();
         m_vars.reset();
-        m_model.reset();
+        m_model.reset();       
+        m_best_model = nullptr; 
+        m_models.reset();
         m_lower_fmls.reset();
         m_s = nullptr;
     }
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 2905d334c..ee74e90a2 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -330,7 +330,7 @@ namespace sat {
         m_stats.m_num_conflicts++;
         TRACE("ba", display(tout, c, true); );
         if (!validate_conflict(c)) {
-            display(std::cout, c, true);
+            IF_VERBOSE(0, display(verbose_stream(), c, true));
             UNREACHABLE();
         }
         SASSERT(validate_conflict(c));
@@ -2941,6 +2941,8 @@ namespace sat {
 
     void ba_solver::pre_simplify() {
         VERIFY(s().at_base_lvl());
+        if (s().inconsistent())
+            return;
         m_constraint_removed = false;
         xor_finder xf(s());
         for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) pre_simplify(xf, *m_constraints[i]);
@@ -2983,6 +2985,8 @@ namespace sat {
 
     void ba_solver::simplify() {        
         if (!s().at_base_lvl()) s().pop_to_base_level();
+        if (s().inconsistent())
+            return;
         unsigned trail_sz, count = 0;
         do {
             trail_sz = s().init_trail_size();
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index 1f9b1705a..b87beeeb2 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -118,11 +118,9 @@ namespace smt {
         if (coallesce_in_re(lit))
             return;
 
-#if 1
-        // Enable/disable to test effect
         if (is_string_equality(lit))
             return;
-#endif        
+
         //
         // TBD s in R => R != {}
         // non-emptiness enforcement could instead of here, 
@@ -151,32 +149,6 @@ namespace smt {
             m_to_propagate.push_back(lit);
     }
 
-    // s in R[if(p,R1,R2)] & p => s in R[R1]
-    // s in R[if(p,R1,R2)] & ~p => s in R[R2]
-
-    bool seq_regex::unfold_cofactors(expr_ref& r, literal_vector& conds) {
-        expr_ref cond(m), tt(m), el(m);
-        while (seq_rw().has_cofactor(r, cond, tt, el)) {
-            rewrite(cond);
-            literal lcond = th.mk_literal(cond);
-            switch (ctx.get_assignment(lcond)) {
-            case l_true: 
-                conds.push_back(~lcond);
-                r = tt;
-                break;
-            case l_false:
-                conds.push_back(lcond);
-                r = el;
-                break;
-            case l_undef:
-                ctx.mark_as_relevant(lcond);
-                return false;
-            }
-            rewrite(r);
-        }
-        return true;
-    }
-
     /**
      * Propagate the atom (accept s i r)
      * 
@@ -184,6 +156,8 @@ namespace smt {
      *
      * (accept s i r[if(c,r1,r2)]) & c => (accept s i r[r1])
      * (accept s i r[if(c,r1,r2)]) & ~c => (accept s i r[r2])
+     * (accept s i r) & nullable(r) => len(s) >= i
+     * (accept s i r) & ~nullable(r) => len(s) >= i + 1
      * (accept s i r) & len(s) <= i => nullable(r)
      * (accept s i r) & len(s) > i => (accept s (+ i 1) D(nth(s,i), r))
      */
@@ -195,53 +169,121 @@ namespace smt {
         expr* e = ctx.bool_var2expr(lit.var());
         unsigned idx = 0;
         VERIFY(sk().is_accept(e, s, i, idx, r));
-        expr_ref is_nullable(m), d(r, m);
-
 
         TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
 
         std::cout << "P ";
-        // << mk_pp(e, m) << std::endl;
+
+        if (re().is_empty(r)) {
+            th.add_axiom(~lit);
+            return true;
+        }
 
         if (block_unfolding(lit, idx))
             return true;
 
+        propagate_nullable(lit, e, s, idx, r);
+
+        return propagate_derivative(lit, e, s, i, idx, r);
+    }
+
+    /**
+       Implement the two axioms as propagations:
+
+       (accept s i r) => len(s) >= i
+       (accept s i r) & ~nullable(r) => len(s) >= i + 1
+     */
+
+    void seq_regex::propagate_nullable(literal lit, expr* e, expr* s, unsigned idx, expr* r) {
+        expr_ref is_nullable = seq_rw().is_nullable(r);
+        rewrite(is_nullable);
+        literal len_s_ge_i = th.m_ax.mk_ge(th.mk_len(s), idx);
+        if (m.is_true(is_nullable)) {
+            th.propagate_lit(nullptr, 1,&lit, len_s_ge_i);
+        }
+        else if (m.is_false(is_nullable)) {
+            th.propagate_lit(nullptr, 1, &lit, th.m_ax.mk_ge(th.mk_len(s), idx + 1));
+        }
+        else {
+            literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx);
+            switch (ctx.get_assignment(len_s_le_i)) {
+            case l_undef:
+                th.add_axiom(~lit, ~len_s_le_i, th.mk_literal(is_nullable));
+                break;
+            case l_true: {
+                literal lits[2] = { lit, len_s_le_i };
+                th.propagate_lit(nullptr, 2, lits, th.mk_literal(is_nullable));
+                break;
+            }
+            case l_false:
+                break;
+            }
+            th.propagate_lit(nullptr, 1, &lit, len_s_ge_i);
+        }
+    }
+    
+    bool seq_regex::propagate_derivative(literal lit, expr* e, expr* s, expr* i, unsigned idx, expr* r) {
+        // (accept s i R) & len(s) > i => (accept s (+ i 1) D(nth(s, i), R)) or conds
+        expr_ref d(m);
+        expr_ref head = th.mk_nth(s, i);
+
+        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";
+        // std::cout.flush();
         literal_vector conds;
         conds.push_back(~lit);
-        if (!unfold_cofactors(d, conds)) 
-            return false;
-
-        if (re().is_empty(d)) {
-            th.add_axiom(conds);
-            return true;
+        conds.push_back(th.m_ax.mk_le(th.mk_len(s), idx));
+        expr* cond = nullptr, *tt = nullptr, *el = nullptr;
+        var_subst subst(m);
+        expr_ref_vector sub(m);
+        sub.push_back(head);       
+        // s in R[if(p,R1,R2)] & p => s in R[R1]
+        // s in R[if(p,R1,R2)] & ~p => s in R[R2]
+        while (m.is_ite(d, cond, tt, el)) {
+            literal lcond = th.mk_literal(subst(cond, sub));
+            switch (ctx.get_assignment(lcond)) {
+            case l_true:
+                conds.push_back(~lcond);
+                d = tt;
+                break;
+            case l_false:
+                conds.push_back(lcond);
+                d = el;
+                break;
+            case l_undef: 
+#if 1
+                ctx.mark_as_relevant(lcond);
+                return false;
+#else
+                if (re().is_empty(tt)) {
+                    literal_vector ensure_false(conds);
+                    ensure_false.push_back(~lcond);
+                    th.add_axiom(ensure_false);
+                    conds.push_back(lcond);
+                    d = el;
+                }
+                else if (re().is_empty(el)) {
+                    literal_vector ensure_true(conds);
+                    ensure_true.push_back(lcond);
+                    th.add_axiom(ensure_true);
+                    conds.push_back(~lcond);
+                    d = tt;
+                }
+                else {
+                    ctx.mark_as_relevant(lcond);
+                    return false;
+                }
+                break;
+#endif
+            }
         }
-
-        // s in R & len(s) <= i => nullable(R)
-        literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx);
-        switch (ctx.get_assignment(len_s_le_i)) {
-        case l_undef:
-            ctx.mark_as_relevant(len_s_le_i);
-            return false;
-        case l_true:
-            is_nullable = seq_rw().is_nullable(d);
-            rewrite(is_nullable);
-            conds.push_back(~len_s_le_i);
-            conds.push_back(th.mk_literal(is_nullable));            
-            th.add_axiom(conds);
-            return true;
-        case l_false:
-            break;
-        }
-
-        // (accept s i R) & len(s) > i => (accept s (+ i 1) D(nth(s, i), R)) or conds
-        expr_ref head = th.mk_nth(s, i);
-        d = derivative_wrapper(head, r);
-
-        literal acc_next = th.mk_literal(sk().mk_accept(s, a().mk_int(idx + 1), d));
-        conds.push_back(len_s_le_i);
-        conds.push_back(acc_next);
-        th.add_axiom(conds);
-        
+        // at this point there should be no free variables as the ites are at top-level.
+        if (!re().is_empty(d)) 
+            conds.push_back(th.mk_literal(sk().mk_accept(s, a().mk_int(idx + 1), d)));
+        th.add_axiom(conds);        
         TRACE("seq", tout << "unfold " << head << "\n" << mk_pp(r, m) << "\n";);
         return true;
     }
@@ -264,7 +306,6 @@ namespace smt {
      * within the same Regex.
      */
     bool seq_regex::coallesce_in_re(literal lit) {
-        // initially disable this
         return false;
         expr* s = nullptr, *r = nullptr;
         expr* e = ctx.bool_var2expr(lit.var());
@@ -273,10 +314,10 @@ namespace smt {
         literal_vector lits;    
         for (unsigned i = 0; i < m_s_in_re.size(); ++i) {
             auto const& entry = m_s_in_re[i];
-            enode* n1 = th.ensure_enode(entry.m_s);
-            enode* n2 = th.ensure_enode(s);
             if (!entry.m_active)
                 continue;
+            enode* n1 = th.ensure_enode(entry.m_s);
+            enode* n2 = th.ensure_enode(s);
             if (n1->get_root() != n2->get_root())
                 continue;
             if (entry.m_re == regex) 
@@ -284,7 +325,7 @@ namespace smt {
 
             th.m_trail_stack.push(vector_value_trail<theory_seq, s_in_re, true>(m_s_in_re, i));
             m_s_in_re[i].m_active = false;
-            IF_VERBOSE(11, verbose_stream() << "intersect " << regex << " " << 
+            IF_VERBOSE(11, verbose_stream() << "Intersect " << regex << " " << 
                        mk_pp(entry.m_re, m) << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << "\n";);
             regex = re().mk_inter(entry.m_re, regex);
             rewrite(regex);
@@ -315,17 +356,14 @@ namespace smt {
     }
 
     /*
-        Memoized(TODO) wrapper around the regex symbolic derivative.
-        Also ensures that the derivative is written in a normalized form
+        Wrapper around the regex symbolic derivative from the rewriter.
+        Ensures that the derivative is written in a normalized BDD form
         with optimizations for if-then-else expressions involving the head.
     */
     expr_ref seq_regex::derivative_wrapper(expr* hd, expr* r) {
         std::cout << "D ";
         expr_ref result = expr_ref(re().mk_derivative(hd, r), m);
         rewrite(result);
-        // don't lift over unions
-        result = seq_rw().lift_ites(result); // false, true);
-        rewrite(result);
         std::cout << std::endl << "Derivative result: " << result << std::endl;
         return result;
     }
@@ -378,7 +416,7 @@ namespace smt {
         if (null_lit != false_literal) 
             lits.push_back(null_lit);
         expr_ref_pair_vector cofactors(m);
-        seq_rw().get_cofactors(d, cofactors);
+        get_cofactors(d, cofactors);
         for (auto const& p : cofactors) {
             if (is_member(p.second, u))
                 continue;
@@ -395,6 +433,21 @@ namespace smt {
         th.add_axiom(lits);
     }
 
+    void seq_regex::get_cofactors(expr* r, expr_ref_vector& conds, expr_ref_pair_vector& result) {
+        expr* cond = nullptr, *th = nullptr, *el = nullptr;
+        if (m.is_ite(r, cond, th, el)) {
+            conds.push_back(cond);
+            get_cofactors(th, conds, result);
+            conds.pop_back();
+            conds.push_back(mk_not(m, cond));
+            get_cofactors(el, conds, result);
+            conds.pop_back();
+        }
+        else {
+            cond = mk_and(conds);
+            result.push_back(cond, r);
+        }
+    }
 
     /*
       is_empty(r, u) => ~is_nullable(r)
@@ -418,10 +471,7 @@ namespace smt {
         d = derivative_wrapper(hd, r);
         literal_vector lits;
         expr_ref_pair_vector cofactors(m);
-        seq_rw().get_cofactors(d, cofactors);
-
-        // is_empty(r, u) => forall hd . cond => is_empty(r1, u union r)
-        
+        get_cofactors(d, cofactors);        
         for (auto const& p : cofactors) {
             if (is_member(p.second, u))
                 continue;
diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h
index 77f845447..56d3bab6b 100644
--- a/src/smt/seq_regex.h
+++ b/src/smt/seq_regex.h
@@ -59,18 +59,27 @@ namespace smt {
 
         bool block_unfolding(literal lit, unsigned i);
 
+        void propagate_nullable(literal lit, expr* e, expr* s, unsigned idx, expr* r);
+
+        bool propagate_derivative(literal lit, expr* e, expr* s, expr* i, unsigned idx, expr* r);
+
         expr_ref mk_first(expr* r);
 
         expr_ref unroll_non_empty(expr* r, expr_mark& seen, unsigned depth);
 
-        bool unfold_cofactors(expr_ref& r, literal_vector& conds);
-
         bool is_member(expr* r, expr* u);
 
         expr_ref symmetric_diff(expr* r1, expr* r2);
 
         expr_ref derivative_wrapper(expr* hd, expr* r);
 
+        void get_cofactors(expr* r, expr_ref_vector& conds, expr_ref_pair_vector& result);
+
+        void get_cofactors(expr* r, expr_ref_pair_vector& result) {
+            expr_ref_vector conds(m);
+            get_cofactors(r, conds, result);
+        }
+
     public:
 
         seq_regex(theory_seq& th);
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index d3793b707..21cce643a 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -436,7 +436,8 @@ namespace smt {
 
         ctx.internalize(term->get_args(), term->get_num_args(), false);
 
-        enode * e = ctx.mk_enode(term, false, false, true);
+        enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) :
+                                                 ctx.mk_enode(term, false, false, true);
 
         if (!is_attached_to_var(e)) {
             attach_new_th_var(e);
@@ -503,16 +504,14 @@ namespace smt {
 
         fpa_util & fu = m_fpa_util;
 
-        expr_ref xe(m), ye(m);
-        xe = e_x->get_owner();
-        ye = e_y->get_owner();
+        expr * xe = e_x->get_owner();
+        expr * ye = e_y->get_owner();
 
         if (m_fpa_util.is_bvwrap(xe) || m_fpa_util.is_bvwrap(ye))
             return;
 
-        expr_ref xc(m), yc(m);
-        xc = convert(xe);
-        yc = convert(ye);
+        expr_ref xc = convert(xe);
+        expr_ref yc = convert(ye);
 
         TRACE("t_fpa_detail", tout << "xc = " << mk_ismt2_pp(xc, m) << std::endl <<
                                       "yc = " << mk_ismt2_pp(yc, m) << std::endl;);
@@ -546,16 +545,14 @@ namespace smt {
 
         fpa_util & fu = m_fpa_util;
 
-        expr_ref xe(m), ye(m);
-        xe = e_x->get_owner();
-        ye = e_y->get_owner();
+        expr * xe = e_x->get_owner();
+        expr * ye = e_y->get_owner();
 
         if (m_fpa_util.is_bvwrap(xe) || m_fpa_util.is_bvwrap(ye))
             return;
 
-        expr_ref xc(m), yc(m);
-        xc = convert(xe);
-        yc = convert(ye);
+        expr_ref xc = convert(xe);
+        expr_ref yc = convert(ye);
 
         expr_ref c(m);