diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index bcbee627444..0aac9b529fb 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -31,7 +31,8 @@ namespace seq {
         a(m),
         seq(m),
         m_sk(m, r),
-        m_clause(m)
+        m_clause(m),
+        m_trail(m)
     {}
         
     expr_ref axioms::mk_sub(expr* x, expr* y) {
@@ -45,10 +46,34 @@ namespace seq {
             return expr_ref(m);
         if (get_depth(e) == 1)
             return expr_ref(e, m);
-        expr_ref p = expr_ref(m.mk_fresh_const("seq.purify", e->get_sort()), m);
+        if (m.is_value(e))
+            return expr_ref(e, m);
+        expr_ref p(m);
+        expr* r = nullptr;
+        if (m_purified.find(e, r)) 
+            p = r;
+        else {
+            gc_purify();
+            p = expr_ref(m.mk_fresh_const("seq.purify", e->get_sort()), m);
+            m_purified.insert(e, p);
+            m_trail.push_back(e);
+            m_trail.push_back(p);
+        }
         add_clause(mk_eq(p, e));
         return expr_ref(p, m);
     }
+
+    void axioms::gc_purify() {
+        if (m_trail.size() != 4000)
+            return;
+        unsigned new_size = 2000;
+        expr_ref_vector new_trail(m, new_size, m_trail.c_ptr() + new_size);
+        m_purified.reset();
+        for (unsigned i = 0; i < new_size; i += 2) 
+            m_purified.insert(new_trail.get(i), new_trail.get(i + 1));
+        m_trail.reset();
+        m_trail.append(new_trail);
+    }
     
     expr_ref axioms::mk_len(expr* s) {
         expr_ref result(seq.str.mk_length(s), m); 
@@ -135,16 +160,14 @@ namespace seq {
             drop_last_axiom(e, s);
             return;
         }
-        if (is_extract_prefix0(s, _i, _l)) {
+        if (is_extract_prefix(s, _i, _l)) {
             extract_prefix_axiom(e, s, l);
             return;
         }
-#if 0
         if (is_extract_suffix(s, _i, _l)) {
             extract_suffix_axiom(e, s, i);
             return;
         }
-#endif
         TRACE("seq", tout << s << " " << i << " " << l << "\n";);
         expr_ref x = m_sk.mk_pre(s, i);
         expr_ref ls = mk_len(_s);
@@ -226,7 +249,7 @@ namespace seq {
         return l1 == l2;
     }
 
-    bool axioms::is_extract_prefix0(expr* s, expr* i, expr* l) {
+    bool axioms::is_extract_prefix(expr* s, expr* i, expr* l) {
         rational i1;
         return a.is_numeral(i, i1) && i1.is_zero();    
     }
diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h
index 16b166c62e4..e3d7c17a175 100644
--- a/src/ast/rewriter/seq_axioms.h
+++ b/src/ast/rewriter/seq_axioms.h
@@ -33,6 +33,8 @@ namespace seq {
         seq_util        seq;
         skolem          m_sk;
         expr_ref_vector m_clause;
+        expr_ref_vector m_trail;
+        obj_map<expr, expr*> m_purified;
         std::function<void(expr_ref_vector const&)> m_add_clause;
 
         expr_ref mk_len(expr* s);
@@ -49,6 +51,8 @@ namespace seq {
         expr_ref mk_ge(expr* x, rational const& n) { return expr_ref(a.mk_ge(x, a.mk_int(n)), m); }
         expr_ref mk_le(expr* x, rational const& n) { return expr_ref(a.mk_le(x, a.mk_int(n)), m); }
 
+        void gc_purify();
+
         expr_ref is_digit(expr* ch);
         expr_ref purify(expr* e);
         expr_ref mk_digit2int(expr* ch);
@@ -61,7 +65,7 @@ namespace seq {
 
         bool is_drop_last(expr* s, expr* i, expr* l);
         bool is_tail(expr* s, expr* i, expr* l);
-        bool is_extract_prefix0(expr* s, expr* i, expr* l);
+        bool is_extract_prefix(expr* s, expr* i, expr* l);
         bool is_extract_suffix(expr* s, expr* i, expr* l);
 
         void tail_axiom(expr* e, expr* s);
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 9c9e45e6c7b..1449a6bbfe8 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1147,6 +1147,13 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         return BR_REWRITE3;
     }
 
+    // extract(extract(a, 3, 6), 1, len(extract(a, 3, 6)) - 1) -> extract(a, 4, 5)
+    if (str().is_extract(a, a1, b1, c1) && is_suffix(a, b, c) && 
+        m_autil.is_numeral(c1) && m_autil.is_numeral(b1)) {
+        result = str().mk_substr(a1, m_autil.mk_add(b, b1), m_autil.mk_sub(c1, b));
+        return BR_REWRITE2;
+    }
+
     if (!constantPos) 
         return BR_FAILED;
 
@@ -1933,6 +1940,19 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
         return BR_REWRITE3;
     }
 
+    expr* a2 = nullptr, *a3 = nullptr;    
+    if (str().is_replace(a, a1, a2, a3) && a1 == a3 && a2 == b) {
+        // TBD: generalize to when a1 is a prefix of a3?
+        result = str().mk_prefix(a1, b);
+        return BR_DONE;
+    }
+
+    expr* b2 = nullptr, *b3 = nullptr;    
+    if (str().is_replace(b, b1, b2, b3) && b2 == a1 && str().is_empty(b3)) {
+        result = str().mk_prefix(str().mk_concat(a1, a1), b1);
+        return BR_REWRITE2;
+    }
+
     return BR_FAILED;    
 }
 
@@ -1995,6 +2015,14 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
         return BR_REWRITE3;
     }
 
+    expr* a1 = nullptr, *a2 = nullptr, *a3 = nullptr;    
+    if (str().is_replace(a, a1, a2, a3) && a1 == a3 && a2 == b) {
+        // TBD: generalize to when a1 is a prefix of a3?
+        result = str().mk_suffix(a1, b);
+        return BR_DONE;
+    }
+
+
     return BR_FAILED;
 }
 
@@ -2174,6 +2202,14 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
                             result);
         return BR_REWRITE_FULL;
     }
+    if (str().is_unit(as.get(0), u) && m_util.is_const_char(u, ch) && '0' == ch) {
+        result = str().mk_concat(as.size() - 1, as.c_ptr() + 1, as[0]->get_sort());
+        result = str().mk_stoi(result);
+        result = m().mk_ite(m_autil.mk_lt(result, m_autil.mk_int(0)),
+                            m_autil.mk_int(0),
+                            result);
+        return BR_REWRITE_FULL;
+    }
 
     return BR_FAILED;
 }
diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index 6b6d86cb1f4..6d02fcf2183 100644
--- a/src/smt/seq_axioms.cpp
+++ b/src/smt/seq_axioms.cpp
@@ -90,192 +90,6 @@ void seq_axioms::add_clause(expr_ref_vector const& clause) {
 }
 
 
-/***
-
-  let e = extract(s, i, l)
-
-  i is start index, l is length of substring starting at index.
-
-  i < 0 => e = ""
-  i >= |s| => e = ""
-  l <= 0 => e = ""
-  0 <= i < |s| & l > 0 => s = xey, |x| = i, |e| = min(l, |s|-i)
-  l <= 0 => e = ""
-
-this translates to:
-
-  0 <= i <= |s| -> s = xey 
-  0 <= i <= |s| -> len(x) = i
-  0 <= i <= |s| & 0 <= l <= |s| - i -> |e| = l
-  0 <= i <= |s| & |s| < l + i  -> |e| = |s| - i
-  |e| = 0 <=> i < 0 | |s| <= i | l <= 0 | |s| <= 0
-
-  It follows that: 
-  |e| = min(l, |s| - i) for 0 <= i < |s| and 0 < |l|
-
-*/
-
-void seq_axioms::add_extract_axiom(expr* e) {
-    if (m_use_new_axioms) {
-        m_ax.extract_axiom(e);
-        return;
-    }
-    TRACE("seq", tout << mk_pp(e, m) << "\n";);
-    expr* _s = nullptr, *_i = nullptr, *_l = nullptr;
-    VERIFY(seq.str.is_extract(e, _s, _i, _l));
-    expr_ref s(_s, m), i(_i, m), l(_l, m);
-    m_rewrite(s);
-    m_rewrite(i);
-    if (l) m_rewrite(l);
-    if (is_tail(s, i, l)) {
-        add_tail_axiom(e, s);
-        return;
-    }
-    if (is_drop_last(s, i, l)) {
-        add_drop_last_axiom(e, s);
-        return;
-    }
-    if (is_extract_prefix0(s, i, l)) {
-        add_extract_prefix_axiom(e, s, l);
-        return;
-    }
-    if (is_extract_suffix(s, i, l)) {
-        add_extract_suffix_axiom(e, s, i);
-        return;
-    }
-    expr_ref x = m_sk.mk_pre(s, i);
-    expr_ref ls = mk_len(s);
-    expr_ref lx = mk_len(x);
-    expr_ref le = mk_len(e);
-    expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i), l), m);
-    expr_ref y = m_sk.mk_post(s, a.mk_add(i, l));
-    expr_ref xe = mk_concat(x, e);
-    expr_ref xey = mk_concat(x, e, y);
-    expr_ref zero(a.mk_int(0), m);
-
-    literal i_ge_0    = mk_ge(i, 0);
-    literal i_le_ls   = mk_le(mk_sub(i, ls), 0);
-    literal ls_le_i   = mk_le(mk_sub(ls, i), 0);
-    literal ls_ge_li  = mk_ge(ls_minus_i_l, 0);
-    literal l_ge_0    = mk_ge(l, 0);
-    literal l_le_0    = mk_le(l, 0);
-    literal ls_le_0   = mk_le(ls, 0);
-    literal le_is_0   = mk_eq(le, zero);
-
-
-    // 0 <= i & i <= |s| & 0 <= l => xey = s
-    // 0 <= i & i <= |s| => |x| = i
-    // 0 <= i & i <= |s| & l >= 0 & |s| >= l + i => |e| = l
-    // 0 <= i & i <= |s| & |s| < l + i => |e| = |s| - i
-    // i < 0 => |e| = 0
-    // |s| <= i => |e| = 0
-    // |s| <= 0 => |e| = 0
-    // l <= 0 => |e| = 0
-    // |e| = 0 & i >= 0 & |s| > i & |s| > 0 => l <= 0
-    add_axiom(~i_ge_0, ~i_le_ls, ~l_ge_0, mk_seq_eq(xey, s));
-    add_axiom(~i_ge_0, ~i_le_ls, mk_eq(lx, i));
-    add_axiom(~i_ge_0, ~i_le_ls, ~l_ge_0, ~ls_ge_li, mk_eq(le, l));
-    add_axiom(~i_ge_0, ~i_le_ls, ~l_ge_0, ls_ge_li, mk_eq(le, mk_sub(ls, i)));
-    add_axiom(i_ge_0,   le_is_0);
-    add_axiom(~ls_le_i, le_is_0);
-    add_axiom(~ls_le_0, le_is_0);
-    add_axiom(~l_le_0,  le_is_0);
-    add_axiom(~le_is_0, ~i_ge_0, ls_le_i, ls_le_0, l_le_0);
-}
-
-void seq_axioms::add_tail_axiom(expr* e, expr* s) {    
-    expr_ref head(m), tail(m);
-    m_sk.decompose(s, head, tail);
-    TRACE("seq", tout << "tail " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << "\n";);
-    literal emp = mk_eq_empty(s);
-    add_axiom(emp, mk_seq_eq(s, mk_concat(head, e)));
-    add_axiom(~emp, mk_eq_empty(e));
-}
-
-void seq_axioms::add_drop_last_axiom(expr* e, expr* s) {
-    TRACE("seq", tout << "drop last " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << "\n";);
-    literal emp = mk_eq_empty(s);
-    add_axiom(emp, mk_seq_eq(s, mk_concat(e, seq.str.mk_unit(m_sk.mk_last(s)))));
-    add_axiom(~emp, mk_eq_empty(e));
-}
-
-bool seq_axioms::is_drop_last(expr* s, expr* i, expr* l) {
-    rational i1;
-    if (!a.is_numeral(i, i1) || !i1.is_zero()) {
-        return false;
-    }
-    expr_ref l2(m), l1(l, m);
-    l2 = mk_sub(mk_len(s), a.mk_int(1));
-    m_rewrite(l1);
-    m_rewrite(l2);
-    return l1 == l2;
-}
-
-bool seq_axioms::is_tail(expr* s, expr* i, expr* l) {
-    rational i1;
-    if (!a.is_numeral(i, i1) || !i1.is_one()) {
-        return false;
-    }
-    expr_ref l2(m), l1(l, m);
-    l2 = mk_sub(mk_len(s), a.mk_int(1));
-    m_rewrite(l1);
-    m_rewrite(l2);
-    return l1 == l2;
-}
-
-bool seq_axioms::is_extract_prefix0(expr* s, expr* i, expr* l) {
-    rational i1;
-    return a.is_numeral(i, i1) && i1.is_zero();    
-}
-
-bool seq_axioms::is_extract_suffix(expr* s, expr* i, expr* l) {
-    expr_ref len(a.mk_add(l, i), m);
-    m_rewrite(len);
-    return seq.str.is_length(len, l) && l == s;
-}
-
-
-/*
-  s = ey
-  l <= 0 => e = empty
-  0 <= l <= len(s) => len(e) = l
-  len(s) < l => e = s
- */
-void seq_axioms::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
-    TRACE("seq", tout << "prefix " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << " " << mk_bounded_pp(l, m, 2) << "\n";);
-    expr_ref le = mk_len(e);
-    expr_ref ls = mk_len(s);
-    expr_ref ls_minus_l(mk_sub(ls, l), m);
-    expr_ref y = m_sk.mk_post(s, l);
-    expr_ref ey = mk_concat(e, y);
-    literal l_le_s = mk_le(mk_sub(l, ls), 0);
-    add_axiom(mk_seq_eq(s, ey));
-    add_axiom(~mk_le(l, 0), mk_eq_empty(e));
-    add_axiom(~mk_ge(l, 0), ~l_le_s, mk_eq(le, l));
-    add_axiom(l_le_s, mk_eq(e, s));
-}
-
-
-/*
-  s = xe
-  0 <= i <= len(s) => i = len(x)    
-  i < 0 => e = empty
-  i > len(s) => e = empty
-*/
-void seq_axioms::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
-    TRACE("seq", tout << "suffix " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << "\n";);
-    expr_ref x = m_sk.mk_pre(s, i);
-    expr_ref lx = mk_len(x);
-    expr_ref ls = mk_len(s);
-    expr_ref xe = mk_concat(x, e);
-    literal emp = mk_eq_empty(e);
-    literal i_ge_0 = mk_ge(i, 0);
-    literal i_le_s = mk_le(mk_sub(i, ls), 0);
-    add_axiom(mk_eq(s, xe));
-    add_axiom(~i_ge_0, ~i_le_s, mk_eq(i, lx));
-    add_axiom(i_ge_0, emp);
-    add_axiom(i_le_s, emp);
-}        
 
 
 /*
@@ -774,184 +588,6 @@ void seq_axioms::add_is_digit_axiom(expr* n) {
     add_axiom(is_digit, ~ge0, ~le9);
 }
 
-/**
-   len(e) = 1 => 0 <= to_code(e) <= max_code
-   len(e) = 1 => from_code(to_code(e)) = e
-   len(e) != 1 => to_code(e) = -1
- */
-void seq_axioms::add_str_to_code_axiom(expr* n) {
-    if (m_use_new_axioms) {
-        m_ax.str_to_code_axiom(n);
-        return;
-    }
-    expr* e = nullptr;
-    VERIFY(seq.str.is_to_code(n, e)); 
-    literal len_is1 = mk_eq(mk_len(e), a.mk_int(1));
-    add_axiom(~len_is1, mk_ge(n, 0)); 
-    add_axiom(~len_is1, mk_le(n, seq.max_char()));
-    add_axiom(~len_is1, mk_eq(n, seq.mk_char2int(mk_nth(e, 0))));
-    if (!seq.str.is_from_code(e))
-        add_axiom(~len_is1, mk_eq(e, seq.str.mk_from_code(n)));
-    add_axiom(len_is1, mk_eq(n, a.mk_int(-1)));
-}
-
-/**
-   0 <= e <= max_char => len(from_code(e)) = 1
-   0 <= e <= max_char => to_code(from_code(e)) = e
-   e < 0 or e > max_char => len(from_code(e)) = ""
- */
-void seq_axioms::add_str_from_code_axiom(expr* n) {
-    if (m_use_new_axioms) {
-        m_ax.str_from_code_axiom(n);
-        return;
-    }
-    expr* e = nullptr;
-    VERIFY(seq.str.is_from_code(n, e)); 
-    literal ge = mk_ge(e, 0);
-    literal le = mk_le(e, seq.max_char());
-    literal emp = mk_literal(seq.str.mk_is_empty(n));
-    add_axiom(~ge, ~le, mk_eq(mk_len(n), a.mk_int(1)));
-    if (!seq.str.is_to_code(e))
-        add_axiom(~ge, ~le, mk_eq(seq.str.mk_to_code(n), e));
-    add_axiom(ge, emp);
-    add_axiom(le, emp);
-}
-
-
-/**
-
- suffix(s, t) => s = seq.suffix_inv(s, t) + t
-~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)
-
-*/
-
-void seq_axioms::add_suffix_axiom(expr* e) {
-    if (m_use_new_axioms) {
-        m_ax.suffix_axiom(e);
-        return;
-    }
-    expr* _s = nullptr, *_t = nullptr;
-    VERIFY(seq.str.is_suffix(e, _s, _t));
-    expr_ref s(_s, m), t(_t, m);
-    m_rewrite(s);
-    m_rewrite(t);
-    literal lit = mk_literal(e);
-    literal s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1);
-#if 0
-    expr_ref x = m_sk.mk_pre(t, mk_sub(mk_len(t), mk_len(s)));
-    expr_ref y = m_sk.mk_tail(t, mk_sub(mk_len(s), a.mk_int(1)));
-    add_axiom(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, y)));
-    add_axiom(lit, s_gt_t, mk_eq(mk_len(y), mk_len(s)));
-    add_axiom(lit, s_gt_t, ~mk_eq(y, s));    
-#else
-    sort* char_sort = nullptr;
-    VERIFY(seq.is_seq(s->get_sort(), char_sort));
-    expr_ref x = m_sk.mk("seq.suffix.x", s, t);
-    expr_ref y = m_sk.mk("seq.suffix.y", s, t);
-    expr_ref z = m_sk.mk("seq.suffix.z", s, t);
-    expr_ref c = m_sk.mk("seq.suffix.c", s, t, char_sort);
-    expr_ref d = m_sk.mk("seq.suffix.d", s, t, char_sort);
-    add_axiom(lit, s_gt_t, mk_seq_eq(s, mk_concat(y, seq.str.mk_unit(c), x)));
-    add_axiom(lit, s_gt_t, mk_seq_eq(t, mk_concat(z, seq.str.mk_unit(d), x)));
-    add_axiom(lit, s_gt_t, ~mk_eq(c, d));
-#endif
-}
-
-void seq_axioms::add_prefix_axiom(expr* e) {
-    if (m_use_new_axioms) {
-        m_ax.prefix_axiom(e);
-        return;
-    }
-    expr* _s = nullptr, *_t = nullptr;
-    VERIFY(seq.str.is_prefix(e, _s, _t));
-    expr_ref s(_s, m), t(_t, m);
-    m_rewrite(s);
-    m_rewrite(t);
-    literal lit = mk_literal(e);
-    literal s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1);
-#if 0
-    expr_ref x = m_sk.mk_pre(t, mk_len(s));    
-    expr_ref y = m_sk.mk_tail(t, mk_sub(mk_sub(mk_len(t), mk_len(s)), a.mk_int(1)));
-    add_axiom(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, y)));
-    add_axiom(lit, s_gt_t, mk_eq(mk_len(x), mk_len(s)));
-    add_axiom(lit, s_gt_t, ~mk_eq(x, s));
-
-#else
-    sort* char_sort = nullptr;
-    VERIFY(seq.is_seq(s->get_sort(), char_sort));
-    expr_ref x = m_sk.mk("seq.prefix.x", s, t);
-    expr_ref y = m_sk.mk("seq.prefix.y", s, t);
-    expr_ref z = m_sk.mk("seq.prefix.z", s, t);
-    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_axiom(lit, s_gt_t, mk_seq_eq(s, mk_concat(x, seq.str.mk_unit(c), y)));
-    add_axiom(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z)), mk_seq_eq(t, x));
-    add_axiom(lit, s_gt_t, ~mk_eq(c, d));
-#endif
-}
-
-/***
-    let n = len(x)
-    - len(a ++ b) = len(a) + len(b) if x = a ++ b
-    - len(unit(u)) = 1              if x = unit(u)
-    - len(str) = str.length()       if x = str
-    - len(empty) = 0                if x = empty
-    - len(int.to.str(i)) >= 1       if x = int.to.str(i) and more generally if i = 0 then 1 else 1+floor(log(|i|))
-    - len(x) >= 0                   otherwise
- */
-void seq_axioms::add_length_axiom(expr* n) {
-    if (m_use_new_axioms) {
-        m_ax.length_axiom(n);
-        return;
-    }
-
-    expr* x = nullptr;
-    VERIFY(seq.str.is_length(n, x));
-    if (seq.str.is_concat(x) ||
-        seq.str.is_unit(x) ||
-        seq.str.is_empty(x) ||
-        seq.str.is_string(x)) {
-        expr_ref len(n, m);
-        m_rewrite(len);
-        SASSERT(n != len);
-        add_axiom(mk_eq(len, n));
-    }
-    else {
-        add_axiom(mk_ge(n, 0));
-    }
-}
-
-/**
-   ~contains(a, b) => ~prefix(b, a)
-   ~contains(a, b) => ~contains(tail(a), b) or a = empty
-   ~contains(a, b) & a = empty => b != empty
-   ~(a = empty) => a = head + tail 
- */
-void seq_axioms::unroll_not_contains(expr* e) {
-    if (m_use_new_axioms) {
-        m_ax.unroll_not_contains(e);
-        return;
-    }
-    expr_ref head(m), tail(m);
-    expr* a = nullptr, *b = nullptr;
-    VERIFY(seq.str.is_contains(e, a, b));
-    m_sk.decompose(a, head, tail);
-    expr_ref pref(seq.str.mk_prefix(b, a), m);
-    expr_ref postf(seq.str.mk_contains(tail, b), m);
-    m_rewrite(pref);
-    m_rewrite(postf);
-    literal pre = mk_literal(pref);
-    literal cnt = mk_literal(e);
-    literal ctail = mk_literal(postf);
-    literal emp = mk_eq_empty(a, true);
-    add_axiom(cnt, ~pre);
-    add_axiom(cnt, ~ctail);
-    add_axiom(~emp, mk_eq_empty(tail));
-    add_axiom(emp, mk_eq(a, seq.str.mk_concat(head, tail)));
-}
-
 
 expr_ref seq_axioms::add_length_limit(expr* s, unsigned k) {
     expr_ref bound_tracker  = m_sk.mk_length_limit(s, k);
diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h
index d986fccf1c8..1827e54db96 100644
--- a/src/smt/seq_axioms.h
+++ b/src/smt/seq_axioms.h
@@ -37,7 +37,7 @@ namespace smt {
         seq::skolem    m_sk;
         seq::axioms    m_ax;
         bool           m_digits_initialized;
-        bool           m_use_new_axioms { false };
+        bool           m_use_new_axioms { true };
 
         literal mk_eq_empty(expr* e, bool phase = true) { return mk_eq_empty2(e, phase); }
         context& ctx() { return th.get_context(); }
@@ -55,14 +55,6 @@ namespace smt {
         void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, 
                        literal l4 = null_literal, literal l5 = null_literal) { add_axiom5(l1, l2, l3, l4, l5); }
 
-        void add_tail_axiom(expr* e, expr* s);
-        void add_drop_last_axiom(expr* e, expr* s);
-        bool is_drop_last(expr* s, expr* i, expr* l);
-        bool is_tail(expr* s, expr* i, expr* l);
-        bool is_extract_prefix0(expr* s, expr* i, expr* l);
-        bool is_extract_suffix(expr* s, expr* i, expr* l);
-        void add_extract_prefix_axiom(expr* e, expr* s, expr* l);
-        void add_extract_suffix_axiom(expr* e, expr* s, expr* i);
         void tightest_prefix(expr* s, expr* x);
         void ensure_digit_axiom();
         void add_clause(expr_ref_vector const& lits);
@@ -74,9 +66,9 @@ namespace smt {
         std::function<void(literal l1, literal l2, literal l3, literal l4, literal l5)> add_axiom5;
         std::function<literal(expr*,bool)> mk_eq_empty2;
 
-        void add_suffix_axiom(expr* n);
-        void add_prefix_axiom(expr* n);
-        void add_extract_axiom(expr* n);
+        void add_suffix_axiom(expr* n) { m_ax.suffix_axiom(n); }
+        void add_prefix_axiom(expr* n) { m_ax.prefix_axiom(n); }
+        void add_extract_axiom(expr* n) { m_ax.extract_axiom(n); }
         void add_indexof_axiom(expr* n);
         void add_last_indexof_axiom(expr* n);
         void add_replace_axiom(expr* n);
@@ -89,11 +81,11 @@ namespace smt {
         void add_lt_axiom(expr* n) { m_ax.lt_axiom(n); }
         void add_le_axiom(expr* n) { m_ax.le_axiom(n); }
         void add_is_digit_axiom(expr* n);
-        void add_str_to_code_axiom(expr* n);
-        void add_str_from_code_axiom(expr* n);
+        void add_str_to_code_axiom(expr* n) { m_ax.str_to_code_axiom(n); }
+        void add_str_from_code_axiom(expr* n) { m_ax.str_from_code_axiom(n); }
         void add_unit_axiom(expr* n) { m_ax.unit_axiom(n); }
-        void add_length_axiom(expr* n);
-        void unroll_not_contains(expr* n);
+        void add_length_axiom(expr* n) { m_ax.length_axiom(n); }
+        void unroll_not_contains(expr* n) { m_ax.unroll_not_contains(n); }
 
         literal is_digit(expr* ch);
         literal mk_ge(expr* e, int k) { return mk_ge_e(e, a.mk_int(k)); }
diff --git a/src/solver/check_logic.cpp b/src/solver/check_logic.cpp
index f2a8dbf9856..3c8ddf4bf15 100644
--- a/src/solver/check_logic.cpp
+++ b/src/solver/check_logic.cpp
@@ -191,7 +191,7 @@ struct check_logic::imp {
             m_ints        = true;
             m_arrays      = true;
             m_reals       = true;
-            m_quantifiers = false;
+            // m_quantifiers = false; // some QF_SLIA benchmarks are miss-classified
         }
         else if (logic == "QF_FD") {
             m_bvs         = true;