diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index 1f220d639..13e6a3511 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -285,6 +285,7 @@ void OP(unsigned num_args, expr * const * args, expr_ref & result) {    \
     MK_BIN_AC_REDUCE(reduce_add, reduce_bin_add, mk_adder);
     MK_BIN_AC_REDUCE(reduce_mul, reduce_bin_mul, mk_multiplier);
 
+    MK_BIN_AC_REDUCE(reduce_and, reduce_bin_and, mk_and);
     MK_BIN_AC_REDUCE(reduce_or, reduce_bin_or, mk_or);
     MK_BIN_AC_REDUCE(reduce_xor, reduce_bin_xor, mk_xor);
 
@@ -357,8 +358,11 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
         result = mk_mkbv(m_out);
     }
 
-    void throw_unsupported() {
-        throw rewriter_exception("operator is not supported, you must simplify the goal before applying bit-blasting");
+    void throw_unsupported(func_decl * f) {
+        std::string msg = "operator ";
+        msg += f->get_name().str();
+        msg += " is not supported, you must simplify the goal before applying bit-blasting";
+        throw rewriter_exception(std::move(msg));
     }
 
     void blast_bv_term(expr * t, expr_ref & result, proof_ref & result_pr) {
@@ -424,7 +428,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
             case OP_BUREM:
             case OP_BSMOD:
                 if (m_blast_mul)
-                    throw_unsupported(); // must simplify to DIV_I AND DIV0
+                    throw_unsupported(f); // must simplify to DIV_I AND DIV0
                 return BR_FAILED; // keep them
 
             case OP_BSDIV0:
@@ -472,6 +476,9 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
                 SASSERT(num == 2);
                 reduce_sle(args[0], args[1], result);
                 return BR_DONE;
+            case OP_BAND:
+                reduce_and(num, args, result);
+                return BR_DONE;
             case OP_BOR:
                 reduce_or(num, args, result);
                 return BR_DONE;
@@ -545,7 +552,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
             default:
                 TRACE("bit_blaster", tout << "non-supported operator: " << f->get_name() << "\n";
                       for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
-                throw_unsupported();
+                throw_unsupported(f);
             }
         }
 
diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index edc91e21f..bcda71e54 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -1043,12 +1043,19 @@ namespace seq {
     }
 
     /**
+       suffix(s, t):
+       - the sequence s is a suffix of t.
 
-       suffix(s, t) => s = seq.suffix_inv(s, t) + t
+       Positive case is handled by the solver when the atom is asserted
+       suffix(s, t) => t = seq.suffix_inv(s, t) + s
+
+       Negative case is handled by axioms when the negation of the atom is asserted
        ~suffix(s, t) => len(s) > len(t) or s = y(s, t) + unit(c(s, t)) + x(s, t)
        ~suffix(s, t) => len(s) > len(t) or t = z(s, t) + unit(d(s, t)) + x(s, t)
        ~suffix(s, t) => len(s) > len(t) or c(s,t) != d(s,t)
 
+       Symmetric axioms are provided for prefix
+
     */
 
     void axioms::suffix_axiom(expr* e) {
@@ -1101,7 +1108,7 @@ namespace seq {
         expr_ref c = m_sk.mk("seq.prefix.c", s, t, char_sort);
         expr_ref d = m_sk.mk("seq.prefix.d", s, t, char_sort);
         add_clause(lit, s_gt_t, mk_seq_eq(s, mk_concat(x, seq.str.mk_unit(c), y)));
-        add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z)), mk_seq_eq(t, x));
+        add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z)));
         add_clause(lit, s_gt_t, ~mk_eq(c, d));
 #endif
     }
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 6bf44f4ba..63a5044e5 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -14,6 +14,7 @@ Author:
     Nikolaj Bjorner (nbjorner) 2015-12-5
     Murphy Berzish 2017-02-21
     Caleb Stanford 2020-07-07
+    Margus Veanes 2021
 
 --*/
 
@@ -872,6 +873,65 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
     return BR_FAILED;
 }
 
+/*
+*  In general constructs nth(t,0) but if t = substring(s,j,..) then simplifies to nth(s,j)
+*  This method assumes that |t| > 0.
+*/
+expr_ref seq_rewriter::mk_seq_first(expr* t) {
+    expr_ref result(m());
+    expr* s, * j, * k;
+    if (str().is_extract(t, s, j, k))
+        result = str().mk_nth_i(s, j);
+    else
+        result = str().mk_nth_i(t, m_autil.mk_int(0));
+    return result;
+}
+
+/*
+*  In general constructs substring(t,1,|t|-1) but if t = substring(s,j,k) then simplifies to substring(s,j+1,k-1)
+*  This method assumes that |t| > 0.
+*/
+expr_ref seq_rewriter::mk_seq_rest(expr* t) {
+    expr_ref result(m());
+    expr* s, * j, * k; 
+    expr_ref one(m_autil.mk_int(1), m());
+    if (str().is_extract(t, s, j, k))
+        result = str().mk_substr(s, m_autil.mk_add(j, one), m_autil.mk_sub(k, one));
+    else
+        result = str().mk_substr(t, one, m_autil.mk_sub(str().mk_length(t), one));
+    return result;
+}
+
+/*
+*  In general constructs nth(t,|t|-1) but if t = substring(s,j,k) then simplifies to nth(s,j+k-1) 
+*  This method assumes that |t| > 0.
+*/
+expr_ref seq_rewriter::mk_seq_last(expr* t) {
+    expr_ref result(m());
+    expr* s, * j, * k;
+    expr_ref one(m_autil.mk_int(1), m());
+    if (str().is_extract(t, s, j, k))
+        result = str().mk_nth_i(s, m_autil.mk_sub(m_autil.mk_add(j, k), one));
+    else
+        result = str().mk_nth_i(t, m_autil.mk_sub(str().mk_length(t), one));
+    return result;
+}
+
+/*
+*  In general constructs substring(t,0,|t|-1) but if t = substring(s,j,k) then simplifies to substring(s,j,k-1) 
+*  This method assumes that |t| > 0 holds.
+*/
+expr_ref seq_rewriter::mk_seq_butlast(expr* t) {
+    expr_ref result(m());
+    expr* s, * j, * k;
+    expr_ref one(m_autil.mk_int(1), m());
+    if (str().is_extract(t, s, j, k))
+        result = str().mk_substr(s, j, m_autil.mk_sub(k, one));
+    else
+        result = str().mk_substr(t, m_autil.mk_int(0), m_autil.mk_sub(str().mk_length(t), one));
+    return result;
+}
+
 /*
     Lift all ite expressions to the top level, safely
     throttled to not blowup the size of the expression.
@@ -1890,16 +1950,16 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref&
     } 
     if (a == b) {
         result = m().mk_ite(str().mk_is_empty(b), str().mk_empty(a->get_sort()), c);
-        return BR_REWRITE1;
+        return BR_REWRITE2;
     }
     zstring s1, s2;
+    expr_ref_vector strs(m());
     if (str().is_string(a, s1) && str().is_string(b, s2)) {
         SASSERT(s2.length() > 0);
         if (s1.length() < s2.length()) {
             result = a;
             return BR_DONE;
         }
-        expr_ref_vector strs(m());
         for (unsigned i = 0; i < s1.length(); ++i) {
             if (s1.length() >= s2.length() + i && 
                 s2 == s1.extract(i, s2.length())) {
@@ -1912,11 +1972,63 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref&
         result = str().mk_concat(strs, a->get_sort());
         return BR_REWRITE_FULL;
     }
-    // TBD: add case when a, b are concatenation of units that are values.
-    // in this case we can use a similar loop as for strings.
+    expr_ref_vector a_vals(m());
+    expr_ref_vector b_vals(m());
+    if (try_get_unit_values(a, a_vals) && try_get_unit_values(b, b_vals)) {
+        replace_all_subvectors(a_vals, b_vals, c, strs);
+        result = str().mk_concat(strs, a->get_sort());
+        return BR_REWRITE_FULL;
+    }
+
+    //TODO: the case when a is a unit or concatenation of units while b is a string 
+    //or the other way around -- if that situation is possible at all -- is similar to the above
     return BR_FAILED;
 }
 
+/*
+* Returns false if s is not a single unit value or concatenation of unit values.
+* Else extracts the units from s into vals and returns true.
+*/
+bool seq_rewriter::try_get_unit_values(expr* s, expr_ref_vector& vals) {
+    expr* h, * t, * v;
+    t = s;
+    //collect all unit values from s, if not all elements are unit-values then fail
+    while (str().is_concat(t, h, t))
+        if (str().is_unit(h, v) && m().is_value(v))
+            vals.push_back(h);
+        else
+            return false;
+    //add the last element
+    if (str().is_unit(t, v) && m().is_value(v))
+        vals.push_back(t);
+    else
+        return false;
+    return true;
+}
+
+/*
+* Replace all subvectors of b in a by c
+*/
+void seq_rewriter::replace_all_subvectors(expr_ref_vector const& a, expr_ref_vector const& b, expr* c, expr_ref_vector& result) {
+    unsigned int i = 0;
+    unsigned int k = b.size();
+    while (i + k <= a.size()) {
+        //if a[i..i+k-1] equals b then replace it by c and inceremnt i by k
+        unsigned j = 0;
+        while (j < k && b[j] == a[i + j]) 
+            ++j;
+        if (j < k) //the equality failed
+            result.push_back(a[i++]);
+        else { //the equality succeeded
+            result.push_back(c);
+            i += k;
+        }
+    }
+    //add the trailing elements from a 
+    while (i < a.size())
+        result.push_back(a[i++]);
+}
+
 br_status seq_rewriter::mk_seq_replace_re_all(expr* a, expr* b, expr* c, expr_ref& result) {
     return BR_FAILED;
 }
@@ -2521,12 +2633,18 @@ bool seq_rewriter::get_re_head_tail_reversed(expr* r, expr_ref& head, expr_ref&
     if (re().is_concat(r, r1, r2)) {
         unsigned len = re().min_length(r2);
         if (len != UINT_MAX && re().max_length(r2) == len) {
-            head = r1;
-            tail = r2;
+            if (get_re_head_tail_reversed(r1, head, tail))
+                // left associative binding of concat
+                tail = mk_re_append(tail, r2);
+            else {
+                // right associative binding of concat
+                head = r1;
+                tail = r2;
+            }
             return true;
         }
         if (get_re_head_tail_reversed(r2, head, tail)) {
-            head = re().mk_concat(r1, head);
+            head = mk_re_append(r1, head);
             return true;
         }
     }
@@ -3059,7 +3177,8 @@ expr_ref seq_rewriter::mk_der_op_rec(decl_kind k, expr* a, expr* b) {
                 return result;
             }
             // Order with higher IDs on the outside
-            if (get_id(ca) < get_id(cb)) {
+            bool is_symmetric = k == OP_RE_UNION || k == OP_RE_INTERSECT;
+            if (is_symmetric && get_id(ca) < get_id(cb)) {
                 std::swap(a, b);
                 std::swap(ca, cb);
                 std::swap(notca, notcb);
@@ -3348,7 +3467,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
             //while mk_empty() = [], because deriv(epsilon) = [] = nothing
             return mk_empty();
         }
-        else if (str().is_itos(r1, r2)) {
+        else if (str().is_itos(r1)) {
             //
             // here r1 = (str.from_int r2) and r2 is non-ground 
             // or else the expression would have been simplified earlier
@@ -3356,27 +3475,46 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
             // '0' <= elem <= '9'
             // if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else []
             //
-            hd = str().mk_nth_i(r1, m_autil.mk_int(0));
-            m_br.mk_and(u().mk_le(m_util.mk_char('0'), ele), u().mk_le(ele, m_util.mk_char('9')), m().mk_eq(hd, ele), result); 
-            tl = re().mk_to_re(str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1))));            
+            hd = mk_seq_first(r1);
+            m_br.mk_and(u().mk_le(m_util.mk_char('0'), ele), u().mk_le(ele, m_util.mk_char('9')), 
+                m().mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele)), result);
+            tl = re().mk_to_re(mk_seq_rest(r1));            
+            return re_and(result, tl);
+        }
+        else {
+            // recall: [] denotes the empty language (nothing) regex, () denotes epsilon or empty sequence
+            // construct the term (if (r1 != () and (ele = (first r1)) then (to_re (rest r1)) else []))
+            hd = mk_seq_first(r1);
+            m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result);
+            tl = re().mk_to_re(mk_seq_rest(r1));
             return re_and(result, tl);
         }
     }
-    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)) {
-            // Use mk_der_cond to normalize
-            STRACE("seq_verbose", tout << "deriv reverse to_re" << std::endl;);
-            result = m().mk_eq(ele, tl);
-            result = mk_der_cond(result, ele, seq_sort);
-            result = mk_der_concat(result, re().mk_reverse(re().mk_to_re(hd)));
-            return result;
-        }
-        else if (str().is_empty(r2)) {
-            return mk_empty();
+    else if (re().is_reverse(r, r1)) {
+        if (re().is_to_re(r1, r2)) {
+            // First try to exctract hd and tl such that r = hd ++ tl and |tl|=1
+            expr_ref hd(m()), tl(m());
+            if (get_head_tail_reversed(r2, hd, tl)) {
+                // Use mk_der_cond to normalize
+                STRACE("seq_verbose", tout << "deriv reverse to_re" << std::endl;);
+                result = m().mk_eq(ele, tl);
+                result = mk_der_cond(result, ele, seq_sort);
+                result = mk_der_concat(result, re().mk_reverse(re().mk_to_re(hd)));
+                return result;
+            }
+            else if (str().is_empty(r2)) {
+                return mk_empty();
+            }
+            else {
+                // construct the term (if (r2 != () and (ele = (last r2)) then reverse(to_re (butlast r2)) else []))
+                // hd = first of reverse(r2) i.e. last of r2
+                // tl = rest of reverse(r2) i.e. butlast of r2
+                //hd = str().mk_nth_i(r2, m_autil.mk_sub(str().mk_length(r2), m_autil.mk_int(1)));
+                hd = mk_seq_last(r2);
+                m_br.mk_and(m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result);
+                tl = re().mk_to_re(mk_seq_butlast(r2));
+                return re_and(result, re().mk_reverse(tl));
+            }
         }
     }
     else if (re().is_range(r, r1, r2)) {
@@ -3423,10 +3561,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
         STRACE("seq_verbose", tout << "deriv of_pred" << std::endl;);
         return mk_der_cond(result, ele, seq_sort);
     }
-    // stuck cases: re.derivative, variable,
-    // str.to_re if the head of the string can't be obtained,
-    // and re.reverse if not applied to a string or if the tail char
-    // of the string can't be obtained
+    // stuck cases: re.derivative, re variable,
     return expr_ref(re().mk_derivative(ele, r), m());
 }
 
@@ -3662,12 +3797,14 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
     }
     if (get_re_head_tail_reversed(b, hd, tl)) {
         SASSERT(re().min_length(tl) == re().max_length(tl));
-        expr_ref len_tl(m_autil.mk_int(re().min_length(tl)), m()); 
+        expr_ref len_tl(m_autil.mk_int(re().min_length(tl)), m());
         expr_ref len_a(str().mk_length(a), m());
         expr_ref len_hd(m_autil.mk_sub(len_a, len_tl), m());
+        expr* s = nullptr;
         result = m().mk_and(m_autil.mk_ge(len_a, len_tl),
-                            re().mk_in_re(str().mk_substr(a, m_autil.mk_int(0), len_hd), hd),
-                            re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl));
+            re().mk_in_re(str().mk_substr(a, m_autil.mk_int(0), len_hd), hd),
+            (re().is_to_re(tl, s) ? m().mk_eq(s, str().mk_substr(a, len_hd, len_tl)) :
+                re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl)));
         return BR_REWRITE_FULL;
     }
 
@@ -4974,6 +5111,12 @@ bool seq_rewriter::reduce_itos(expr_ref_vector& ls, expr_ref_vector& rs,
         str().is_itos(ls.get(0), n) &&
         is_string(rs.size(), rs.data(), s)) {
         std::string s1 = s.encode();
+        for (auto c : s1) {
+            if (!('0' <= c && c <= '9'))
+                return false;
+        }
+        if (s1.size() > 1 && s1[0] == '0')
+            return false;
         try {
             rational r(s1.c_str());
             if (s1 == r.to_string()) {
@@ -5015,6 +5158,10 @@ bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) {
         result = m().mk_or(fmls);
         return true;
     }
+    if (str().is_itos(r, s)) {
+        result = m_autil.mk_lt(s, m_autil.mk_int(0));
+        return true;
+    }
     return false;
 }
 
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index c779a5f73..f726a4673 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -180,6 +180,16 @@ class seq_rewriter {
 
     expr_ref mk_seq_concat(expr* a, expr* b);    
 
+    // Construct the expressions for taking the first element, the last element, the rest, and the butlast element
+    expr_ref mk_seq_first(expr* s);
+    expr_ref mk_seq_rest(expr* s);
+    expr_ref mk_seq_last(expr* s);
+    expr_ref mk_seq_butlast(expr* s);
+
+    bool try_get_unit_values(expr* s, expr_ref_vector& result);
+    //replace b in a by c into result
+    void replace_all_subvectors(expr_ref_vector const& as, expr_ref_vector const& bs, expr* c, expr_ref_vector& result);
+
     // Calculate derivative, memoized and enforcing a normal form
     expr_ref is_nullable_rec(expr* r);
     expr_ref mk_derivative_rec(expr* ele, expr* r);
@@ -344,6 +354,16 @@ public:
         return result;
     }
 
+    /*
+    * makes concat and simplifies
+    */
+    expr_ref mk_re_append(expr* r1, expr* r2) {
+        expr_ref result(m());
+        if (mk_re_concat(r1, r2, result) == BR_FAILED)
+            result = re().mk_concat(r1, r2);
+        return result;
+    }
+
     /**
      * check if regular expression is of the form all ++ s ++ all ++ t + u ++ all, where, s, t, u are sequences
      */
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 6695d9497..82ab83681 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -911,7 +911,7 @@ unsigned seq_util::str::max_length(expr* s) const {
             return UINT_MAX;
     };
     while (is_concat(s, s1, s2)) {
-        result = u.max_plus(get_length(s), result);
+        result = u.max_plus(get_length(s1), result);
         s = s2;
     }
     result = u.max_plus(get_length(s), result);
@@ -1058,6 +1058,7 @@ app* seq_util::rex::mk_epsilon(sort* seq_sort) {
 */
 std::ostream& seq_util::rex::pp::compact_helper_seq(std::ostream& out, expr* s) const {
     SASSERT(re.u.is_seq(s));
+    zstring z;
     if (re.u.str.is_empty(s))
         out << "()";
     else if (re.u.str.is_unit(s))
@@ -1068,6 +1069,10 @@ std::ostream& seq_util::rex::pp::compact_helper_seq(std::ostream& out, expr* s)
         for (expr* e : es)
             compact_helper_seq(out, e);
     }
+    else if (re.u.str.is_string(s, z)) {
+        for (unsigned i = 0; i < z.length(); i++)
+            out << (char)z[i];
+    }
     //using braces to indicate 'full' output
     //for example an uninterpreted constant X will be printed as {X}
     //while a unit sequence "X" will be printed as X
@@ -1100,7 +1105,7 @@ bool seq_util::rex::pp::can_skip_parenth(expr* r) const {
 std::ostream& seq_util::rex::pp::seq_unit(std::ostream& out, expr* s) const {
     expr* e;
     unsigned n = 0;
-    if (re.u.str.is_unit(s, e) && re.u.is_const_char(e, n)) {
+    if ((re.u.str.is_unit(s, e) && re.u.is_const_char(e, n)) || re.u.is_const_char(s, n)) {
         char c = (char)n;
         if (c == '\n')
             out << "\\n";
@@ -1148,7 +1153,11 @@ std::ostream& seq_util::rex::pp::seq_unit(std::ostream& out, expr* s) const {
 std::ostream& seq_util::rex::pp::display(std::ostream& out) const {
     expr* r1 = nullptr, * r2 = nullptr, * s = nullptr, * s2 = nullptr;
     unsigned lo = 0, hi = 0;
-    if (re.is_full_char(e))
+    if (re.u.is_char(e))
+        return seq_unit(out, e);
+    else if (re.u.is_seq(e))
+        return compact_helper_seq(out, e);
+    else if (re.is_full_char(e))
         return out << ".";
     else if (re.is_full_seq(e))
         return out << ".*";
@@ -1163,9 +1172,9 @@ std::ostream& seq_util::rex::pp::display(std::ostream& out) const {
     else if (re.is_concat(e, r1, r2)) 
         return out << pp(re, r1) << pp(re, r2);
     else if (re.is_union(e, r1, r2)) 
-        return out << pp(re, r1) << "|" << pp(re, r2);
+        return out << "(" << pp(re, r1) << "|" << pp(re, r2) << ")";
     else if (re.is_intersection(e, r1, r2)) 
-        return out << "(" << pp(re, r1) << (html_encode ? ")&amp;(": ")&(" ) << pp(re, r2) << ")";
+        return out << "(" << pp(re, r1) << "&amp;" /*(html_encode ? ")&amp;(" : ")&(")*/ << pp(re, r2) << ")";
     else if (re.is_complement(e, r1)) {
         if (can_skip_parenth(r1))
             return out << "~" << pp(re, r1);
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 7a6957467..a9910852e 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -2022,10 +2022,14 @@ namespace sat {
         }
         remove_bin_clauses(pos_l);
         remove_bin_clauses(neg_l);
-        remove_clauses(pos_occs, pos_l);
-        remove_clauses(neg_occs, neg_l);
-        pos_occs.reset();
-        neg_occs.reset();
+        {
+            clause_use_list& pos_occs = m_use_list.get(pos_l);
+            clause_use_list& neg_occs = m_use_list.get(neg_l);
+            remove_clauses(pos_occs, pos_l);
+            remove_clauses(neg_occs, neg_l);
+            pos_occs.reset();
+            neg_occs.reset();
+        }
         return true;
     }
 
diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index 7e41aeb46..b1398c836 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -418,6 +418,7 @@ namespace arith {
             expr* p = nullptr, * q = nullptr;
             VERIFY(a.is_idiv(n, p, q));
             theory_var v1 = internalize_def(p);
+            ensure_column(v1);
             lp::impq r1 = get_ivalue(v1);
             rational r2;
 
diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp
index b4e7d3cab..74594e5a0 100644
--- a/src/sat/smt/array_model.cpp
+++ b/src/sat/smt/array_model.cpp
@@ -73,7 +73,7 @@ namespace array {
             obj_map<expr, unsigned> num_occ;
             for (euf::enode* p : euf::enode_parents(n->get_root())) {
                 if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n->get_root()) {
-                    expr* v = values.get(p->get_root_id());
+                    expr* v = values.get(p->get_root_id(), nullptr);
                     if (!v)
                         continue;
                     unsigned no = 0;
@@ -92,7 +92,7 @@ namespace array {
 
         for (euf::enode* p : euf::enode_parents(n)) {
             if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n) {
-                expr* value = values.get(p->get_root_id());
+                expr* value = values.get(p->get_root_id(), nullptr);
                 if (!value || value == fi->get_else())
                     continue;
                 args.reset();
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index c83680f72..a2c27fd60 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -490,6 +490,10 @@ namespace q {
         TRACE("q", tout << "add " << mk_pp(_q, m) << "\n";);
         clause* c = clausify(_q);
         quantifier* q = c->q();
+        if (m_q2clauses.contains(q)) {
+            dealloc(c);
+            return;
+        }
         ensure_ground_enodes(*c);
         m_clauses.push_back(c);
         m_q2clauses.insert(q, c->index());
diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp
index 000f76879..8b75e87ea 100644
--- a/src/sat/smt/q_mam.cpp
+++ b/src/sat/smt/q_mam.cpp
@@ -414,7 +414,7 @@ namespace q {
         enode_vector               m_candidates;
 #ifdef Z3DEBUG
         egraph *                   m_egraph;
-        ptr_vector<app>            m_patterns;
+        svector<std::pair<quantifier*, app*>>            m_patterns;
 #endif
 #ifdef _PROFILE_MAM
         stopwatch                  m_watch;
@@ -568,7 +568,7 @@ namespace q {
             m_egraph = ctx;
         }
 
-        ptr_vector<app> & get_patterns() {
+        svector<std::pair<quantifier*, app*>> & get_patterns() {
             return m_patterns;
         }
 #endif
@@ -578,8 +578,8 @@ namespace q {
             if (m_egraph) {
                 ast_manager & m = m_egraph->get_manager();
                 out << "patterns:\n";
-                for (app* a : m_patterns) 
-                    out << mk_pp(a, m) << "\n";
+                for (auto [q, a] : m_patterns) 
+                    out << mk_pp(q, m) << " " << mk_pp(a, m) << "\n";
             }
 #endif
             out << "function: " << m_root_lbl->get_name();
@@ -2862,12 +2862,11 @@ namespace q {
                 // The E-matching engine that was built when all + and * applications were binary.
                 // We ignore the pattern if it does not have the expected number of arguments.
                 // This is not the ideal solution, but it avoids possible crashes.
-                if (tree->expected_num_args() == p->get_num_args()) {
+                if (tree->expected_num_args() == p->get_num_args()) 
                     m_compiler.insert(tree, qa, mp, first_idx, false);
-                }
             }
-            DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(mp);
-                       ctx.push(push_back_trail<app*, false>(m_trees[lbl_id]->get_patterns())););
+            DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(std::make_pair(qa, mp));
+                       ctx.push(push_back_trail<std::pair<quantifier*,app*>, false>(m_trees[lbl_id]->get_patterns())););
             TRACE("trigger_bug", tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout););
         }
 
diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp
index c9ee5d532..1d4805c67 100644
--- a/src/tactic/core/pb_preprocess_tactic.cpp
+++ b/src/tactic/core/pb_preprocess_tactic.cpp
@@ -44,6 +44,7 @@ class pb_preprocess_tactic : public tactic {
     struct rec { unsigned_vector pos, neg; rec() { } };
     typedef obj_map<app, rec> var_map;
     ast_manager&     m;
+    expr_ref_vector  m_trail;
     pb_util          pb;
     var_map          m_vars;    
     unsigned_vector  m_ge;
@@ -99,7 +100,7 @@ class pb_preprocess_tactic : public tactic {
 
 public:
     pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()): 
-        m(m), pb(m), m_r(m) {}
+        m(m), m_trail(m), pb(m), m_r(m) {}
 
     ~pb_preprocess_tactic() override {}
 
@@ -157,7 +158,7 @@ public:
         m_progress = false;
         // first eliminate variables
         var_map::iterator it = next_resolvent(m_vars.begin()); 
-        while (it != m_vars.end()) {            
+        while (it != m_vars.end()) {  
             app * e = it->m_key;
             rec const& r = it->m_value;
             TRACE("pb", tout << mk_pp(e, m) << " " << r.pos.size() << " " << r.neg.size() << "\n";);
@@ -235,6 +236,7 @@ private:
         m_ge.reset();
         m_other.reset();
         m_vars.reset();
+        m_trail.reset();
     }
 
     expr* negate(expr* e) {
@@ -410,6 +412,7 @@ private:
     void insert(unsigned i, app* e, bool pos) {
         SASSERT(is_uninterp_const(e));
         if (!m_vars.contains(e)) {
+            m_trail.push_back(e);
             m_vars.insert(e, rec());
         }
         if (pos) {
@@ -504,10 +507,7 @@ private:
             bool found = false;
             for (unsigned j = 0; j < args2.size(); ++j) {
                 if (is_complement(args1.get(i), args2.get(j))) {
-                    if (i == 0) {
-                        min_coeff = coeffs2[j];
-                    }
-                    else if (min_coeff > coeffs2[j]) {
+                    if (i == 0 || min_coeff > coeffs2[j]) {
                         min_coeff = coeffs2[j];
                         min_index = j;
                     }
diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index 85062b03b..57df65e83 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -93,10 +93,11 @@ public:
                 g->update(idx, f_new, new_pr, g->dep(idx));
             }  
             if (mc) g->add(mc.get());
-            g->inc_depth();
+	    TRACE("invertible_tactic", g->display(tout););
+	    g->inc_depth();
         }        
         result.push_back(g.get());
-        CTRACE("invertible_tactic", g->mc(), g->mc()->display(tout););
+	CTRACE("invertible_tactic", g->mc(), g->mc()->display(tout););
     }
 
     void cleanup() override {}
@@ -223,28 +224,46 @@ private:
         rational r;
         app* a = to_app(v);
         expr* fst_arg = a->get_arg(0);
-        bool fst_is_var = is_var(fst_arg);
 
-        for (unsigned i = 0, n = a->get_num_args(); i != n; ++i) {
-            auto arg = a->get_arg(i);
-            if (!m_parents[arg->get_id()].get() || is_var(arg) != fst_is_var)
+        for (expr* arg : *a) 
+            if (!m_parents[arg->get_id()].get())
                 return false;
 
-            if (fst_is_var && to_var(arg)->get_idx() >= max_var)
-                return false;
-
-            if (m_bv.is_numeral(arg, r) && r != mdl)
-                return false;
-
-            if (i > 0 && !is_var(arg) && (!is_app(arg) || to_app(arg)->get_num_args() > 0))
+        if (is_var(fst_arg)) {
+            for (expr* arg : *a) {
+                if (!is_var(arg))
+                    return false;
+                if (to_var(arg)->get_idx() >= max_var)
+                    return false;
+            }
+        }
+        else {            
+            bool first = true;
+            for (expr* arg : *a) {
+                if (!is_app(arg))
+                    return false;
+                if (is_uninterp_const(arg))
+                    continue;
+                if (m_bv.is_numeral(arg, r) && r == mdl) {
+                    if (first || mdl.is_zero()) {
+                        first = false;
+                        continue;
+                    }
+                    else
+                        return false;
+                }
                 return false;
+            }
         }
 
         if (mc) {
             ensure_mc(mc);
             expr_ref num(m_bv.mk_numeral(mdl, fst_arg->get_sort()), m);
             for (unsigned i = 1, n = a->get_num_args(); i != n; ++i) {
-                (*mc)->add(a->get_arg(i), num);
+                expr* arg = a->get_arg(i);
+                if (m_bv.is_numeral(arg))
+                    continue;
+                (*mc)->add(arg, num);
             }
         }
         new_v = fst_arg;
@@ -327,7 +346,6 @@ private:
             // 
             unsigned sz = m_bv.get_bv_size(p);
             expr_ref bit1(m_bv.mk_numeral(1, 1), m);
-            new_v = m_bv.mk_numeral(0, sz);
 
             
             unsigned sh = 0;
@@ -335,9 +353,10 @@ private:
                 r /= rational(2);
                 ++sh;
             }
-            if (r.is_pos() && sh > 0) {
+            if (r.is_pos() && sh > 0) 
                 new_v = m_bv.mk_concat(m_bv.mk_extract(sz-sh-1, 0, v), m_bv.mk_numeral(0, sh));
-            }
+            else
+                new_v = v;
             if (mc && !r.is_zero()) {
                 ensure_mc(mc);
                 expr_ref def(m);
@@ -414,6 +433,38 @@ private:
                 return true;
             }
         }
+
+        //
+        // v <= u
+        // => u + 1 == 0 or delta
+        // v := delta ? u : u + 1
+        //
+        if (m_bv.is_bv_ule(p, e1, e2) && e1 == v && mc) {
+            ensure_mc(mc);
+            unsigned sz = m_bv.get_bv_size(e2);
+            expr_ref delta(m.mk_fresh_const("ule", m.mk_bool_sort()), m);
+            expr_ref succ_e2(m_bv.mk_bv_add(e2, m_bv.mk_numeral(1, sz)), m);
+            new_v = m.mk_or(delta, m.mk_eq(succ_e2, m_bv.mk_numeral(0, sz)));
+            (*mc)->hide(delta);
+            (*mc)->add(v, m.mk_ite(delta, e2, succ_e2));
+            return true;
+        }
+
+        //
+        // u <= v
+        // => u == 0 or delta
+        // v := delta ? u : u - 1
+        //
+        if (m_bv.is_bv_ule(p, e1, e2) && e2 == v && mc) {
+            ensure_mc(mc);
+            unsigned sz = m_bv.get_bv_size(e1);
+            expr_ref delta(m.mk_fresh_const("ule", m.mk_bool_sort()), m);
+            expr_ref pred_e1(m_bv.mk_bv_sub(e1, m_bv.mk_numeral(1, sz)), m);
+            new_v = m.mk_or(delta, m.mk_eq(e1, m_bv.mk_numeral(0, sz)));
+            (*mc)->hide(delta);
+            (*mc)->add(v, m.mk_ite(delta, e1, pred_e1));
+            return true;
+        }
         return false;
     }
 
diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp
index ac6cdede2..3a23f5984 100644
--- a/src/tactic/portfolio/solver_subsumption_tactic.cpp
+++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp
@@ -41,31 +41,41 @@ class solver_subsumption_tactic : public tactic {
 
     /**
     * Check subsumption (a \/ b \/ c)
-    * if (a \/ b) is already implied
-    * Use a naive algorithm (not binary disection here)
+    *
+    * If 
+    *   F |= (a \/ ~b \/ c)
+    * Then replace (a \/ b \/ c) by (a \/ c)
+    * 
+    * If
+    *   F |= (a \/ b \/ c)
+    * Then replace (a \/ b \/ c) by true
+    * 
     */
 
     bool simplify(expr_ref& f) {
+        expr_ref_vector fmls(m), ors(m), nors(m), prefix(m);
+        expr_ref nf(m.mk_not(f), m);
+        fmls.push_back(nf);
+        lbool is_sat = m_solver->check_sat(fmls);
+        if (is_sat == l_false) {
+            f = m.mk_true();
+            return true;
+        }
         if (!m.is_or(f))
             return false;
-        expr_ref_vector ors(m);
         ors.append(to_app(f)->get_num_args(), to_app(f)->get_args());
-        expr_ref_vector prefix(m);
+        for (expr* arg : ors)
+            nors.push_back(mk_not(m, arg));
         for (unsigned i = 0; i < ors.size(); ++i) {
-            expr_ref_vector fmls(m);
-            fmls.append(prefix);
-            for (unsigned k = i + 1; k < ors.size(); ++k)
-                fmls.push_back(m.mk_not(ors.get(k)));
-            lbool is_sat = m_solver->check_sat(fmls);
-            if (is_sat == l_false)
-                continue;
-            fmls.reset();
-            fmls.push_back(ors.get(i));
-            
-            is_sat = m_solver->check_sat(fmls);
-            if (is_sat == l_false)
-                continue;
-            prefix.push_back(ors.get(i));                
+            expr* arg = ors.get(i);
+            expr_ref save(nors.get(i), m);
+            nors[i] = arg;
+            is_sat = m_solver->check_sat(nors);
+            nors[i] = save;
+            if (is_sat == l_false) 
+                nors[i] = m.mk_true();
+            else 
+                prefix.push_back(arg);            
         }
         if (ors.size() != prefix.size()) {
             ors.reset();
@@ -131,7 +141,7 @@ public:
     }
 
     void collect_param_descrs(param_descrs& r) override { 
-        r.insert("max_conflicts", CPK_UINT, "(default: 10) maximal number of conflicts allowed per solver call.");
+        r.insert("max_conflicts", CPK_UINT, "(default: 2) maximal number of conflicts allowed per solver call.");
     }
 
     void operator()(goal_ref const& g, goal_ref_buffer& result) override {
diff --git a/src/util/state_graph.cpp b/src/util/state_graph.cpp
index 400d1f586..2cc4158c7 100644
--- a/src/util/state_graph.cpp
+++ b/src/util/state_graph.cpp
@@ -13,7 +13,7 @@ Abstract:
 Author:
 
     Caleb Stanford (calebstanford-msr / cdstanford) 2020-7
-
+    Margus Veanes 2020-8
 --*/
 
 #include "state_graph.h"