diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 8aa37e1b2..e2ee944d7 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -97,7 +97,6 @@ def_module_params(module_name='smt',
                           ('core.validate', BOOL, False, '[internal] validate unsat core produced by SMT context. This option is intended for debugging'),
                           ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'),
                           ('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'),
-                          ('seq.use_derivatives', BOOL, False, 'dev flag (not for users) enable derivative based unfolding of regex'),
 	                  ('seq.use_unicode', BOOL, False, 'dev flag (not for users) enable unicode semantics'),
                           ('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'),
                           ('str.aggressive_length_testing', BOOL, False, 'prioritize testing concrete length values over generating more options'),
diff --git a/src/smt/params/theory_seq_params.cpp b/src/smt/params/theory_seq_params.cpp
index 069a43c47..bd67e2bda 100644
--- a/src/smt/params/theory_seq_params.cpp
+++ b/src/smt/params/theory_seq_params.cpp
@@ -21,6 +21,5 @@ void theory_seq_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);
     m_split_w_len = p.seq_split_w_len();
     m_seq_validate = p.seq_validate();
-    m_seq_use_derivatives = p.seq_use_derivatives();
     m_seq_use_unicode = p.seq_use_unicode();
 }
diff --git a/src/smt/params/theory_seq_params.h b/src/smt/params/theory_seq_params.h
index d75d3bf2c..9d227e5fc 100644
--- a/src/smt/params/theory_seq_params.h
+++ b/src/smt/params/theory_seq_params.h
@@ -24,14 +24,12 @@ struct theory_seq_params {
      */
     bool m_split_w_len;
     bool m_seq_validate;
-    bool m_seq_use_derivatives;
     bool m_seq_use_unicode;
 
 
     theory_seq_params(params_ref const & p = params_ref()):
         m_split_w_len(false),
         m_seq_validate(false),
-        m_seq_use_derivatives(false),
         m_seq_use_unicode(false)
     {
         updt_params(p);
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index a835c4634..25bf344a8 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -305,14 +305,12 @@ theory_seq::theory_seq(context& ctx):
     m_ls(m), m_rs(m),
     m_lhs(m), m_rhs(m),
     m_new_eqs(m),
-    m_res(m),
     m_max_unfolding_depth(1),
     m_max_unfolding_lit(null_literal),
     m_unhandled_expr(nullptr),
     m_has_seq(m_util.has_seq()),
     m_new_solution(false),
-    m_new_propagation(false),
-    m_mk_aut(m) {
+    m_new_propagation(false) {
 
 }
 
@@ -706,13 +704,6 @@ bool theory_seq::is_solved() {
         IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";);
         return false;
     }
-    for (unsigned i = 0; i < m_automata.size(); ++i) {
-        if (!m_automata[i]) {
-            TRACE("seq", tout  << "(seq.giveup regular expression did not compile to automaton)\n";);
-            IF_VERBOSE(10, verbose_stream() << "(seq.giveup regular expression did not compile to automaton)\n";);
-            return false;
-        }
-    }
     if (!m_ncs.empty()) {
         TRACE("seq", display_nc(tout << "(seq.giveup ", m_ncs[0]); tout << " is unsolved)\n";);
         IF_VERBOSE(10, display_nc(verbose_stream() << "(seq.giveup ", m_ncs[0]); verbose_stream() << " is unsolved)\n";);
@@ -1534,8 +1525,7 @@ bool theory_seq::internalize_term(app* term) {
         return true;
     }
 
-    if (ctx.get_fparams().m_seq_use_derivatives && 
-        m.is_bool(term) && 
+    if (m.is_bool(term) && 
         (m_util.str.is_in_re(term) || m_sk.is_skolem(term))) {
         bool_var bv = ctx.mk_bool_var(term);
         ctx.set_var_theory(bv, get_id());
@@ -1670,16 +1660,6 @@ void theory_seq::display(std::ostream & out) const {
     if (!m_nqs.empty()) {
         display_disequations(out);
     }
-    if (!m_re2aut.empty()) {
-        out << "Regex\n";
-        for (auto const& kv : m_re2aut) {
-            out << mk_pp(kv.m_key, m) << "\n";
-            display_expr disp(m);
-            if (kv.m_value) {
-                kv.m_value->display(out, disp);
-            }
-        }
-    }
     if (!m_rep.empty()) {
         out << "Solved equations:\n";
         m_rep.display(out);
@@ -1828,13 +1808,9 @@ void theory_seq::collect_statistics(::statistics & st) const {
     st.update("seq extensionality", m_stats.m_extensionality);
     st.update("seq fixed length", m_stats.m_fixed_length);
     st.update("seq int.to.str", m_stats.m_int_string);
-    st.update("seq automata", m_stats.m_propagate_automata);
 }
 
 void theory_seq::init_search_eh() {
-    m_re2aut.reset();
-    m_res.reset();
-    m_automata.reset();
     auto as = get_fparams().m_arith_mode;
     if (m_has_seq && as != AS_OLD_ARITH && as != AS_NEW_ARITH) {
         throw default_exception("illegal arithmetic solver used with string solver");
@@ -2565,7 +2541,7 @@ void theory_seq::add_dependency(dependency*& dep, enode* a, enode* b) {
 void theory_seq::propagate() {
     if (ctx.get_fparams().m_seq_use_unicode)
         m_unicode.propagate();
-    if (ctx.get_fparams().m_seq_use_derivatives && m_regex.can_propagate())
+    if (m_regex.can_propagate())
         m_regex.propagate();
     while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) {
         expr_ref e(m);
@@ -2672,90 +2648,6 @@ expr_ref theory_seq::add_elim_string_axiom(expr* n) {
     return result;
 }
 
-void theory_seq::propagate_in_re(expr* n, bool is_true) {
-
-    TRACE("seq", tout << mk_pp(n, m) << " <- " << (is_true?"true":"false") << "\n";);
-
-    expr_ref tmp(n, m);
-    m_rewrite(tmp);
-    if (m.is_true(tmp)) {
-        if (!is_true) {
-            literal_vector lits;
-            lits.push_back(mk_literal(n));
-            set_conflict(nullptr, lits);
-        }
-        return;
-    }
-    else if (m.is_false(tmp)) {
-        if (is_true) {
-            literal_vector lits;
-            lits.push_back(~mk_literal(n));
-            set_conflict(nullptr, lits);
-        }
-        return;
-    }
-
-    expr* s = nullptr, *_re = nullptr;
-    VERIFY(m_util.str.is_in_re(n, s, _re));
-    expr_ref re(_re, m);
-    literal lit = ctx.get_literal(n);
-    if (!is_true) {
-        re = m_util.re.mk_complement(re);
-        lit.neg();
-    }
-
-    literal_vector lits;    
-    for (unsigned i = 0; i < m_s_in_re.size(); ++i) {
-        auto const& entry = m_s_in_re[i];
-        if (entry.m_active && get_root(entry.m_s) == get_root(s) && entry.m_re != re) {
-            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 " << re << " " << mk_pp(entry.m_re, m) << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << "\n";);
-            re = m_util.re.mk_inter(entry.m_re, re);
-            m_rewrite(re);
-            lits.push_back(~entry.m_lit);
-            enode* n1 = ensure_enode(entry.m_s);
-            enode* n2 = ensure_enode(s);
-            if (n1 != n2) {
-                lits.push_back(~mk_eq(n1->get_owner(), n2->get_owner(), false));
-            }
-        }
-    }
-
-    IF_VERBOSE(11, verbose_stream() << mk_pp(s, m) << " in " << re << "\n");
-    eautomaton* a = get_automaton(re);
-    if (!a) {
-        std::stringstream strm;
-        strm << "expression " << re << " does not correspond to a supported regular expression";
-        TRACE("seq", tout << strm.str() << "\n";);
-        throw default_exception(strm.str());
-    }
-
-    m_s_in_re.push_back(s_in_re(lit, s, re, a));
-    m_trail_stack.push(push_back_vector<theory_seq, vector<s_in_re>>(m_s_in_re));
-
-    expr_ref len = mk_len(s);
-
-    expr_ref zero(m_autil.mk_int(0), m);
-    unsigned_vector states;
-    a->get_epsilon_closure(a->init(), states);
-    lits.push_back(~lit);
-    
-    for (unsigned st : states) {
-        literal acc = mk_accept(s, zero, re, st);
-        lits.push_back(acc);
-    }
-    if (lits.size() == 2) {
-        propagate_lit(nullptr, 1, &lit, lits[1]);
-    }
-    else {
-        TRACE("seq", ctx.display_literals_verbose(tout, lits) << "\n";);
-        
-        scoped_trace_stream _sts(*this, lits);
-        ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
-    }
-}
-
 expr_ref theory_seq::mk_sub(expr* a, expr* b) {
     expr_ref result(m_autil.mk_sub(a, b), m);
     m_rewrite(result);
@@ -3106,15 +2998,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             m_ncs.push_back(nc(expr_ref(e, m), len_gt, dep));
         }
     }
-    else if (is_accept(e)) {
-        if (is_true) {
-            if (ctx.get_fparams().m_seq_use_derivatives) {
-                m_regex.propagate_accept(lit);
-            }
-            else {
-                propagate_accept(lit, e);
-            }
-        }
+    else if (m_sk.is_accept(e)) {
+        if (is_true) 
+            m_regex.propagate_accept(lit);
     }
     else if (m_sk.is_is_empty(e)) {
         if (is_true)
@@ -3124,23 +3010,13 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
         if (is_true)
             m_regex.propagate_is_non_empty(lit);
     }
-    else if (m_sk.is_step(e)) {
-        if (is_true) {
-            propagate_step(lit, e);
-        }
-    }
     else if (m_sk.is_eq(e, e1, e2)) {
         if (is_true) {
             propagate_eq(lit, e1, e2, true);
         }
     }
     else if (m_util.str.is_in_re(e)) {
-        if (ctx.get_fparams().m_seq_use_derivatives) {
-            m_regex.propagate_in_re(lit);
-        }
-        else {
-            propagate_in_re(e, is_true);
-        }
+        m_regex.propagate_in_re(lit);
     }
     else if (m_sk.is_digit(e)) {
         // no-op
@@ -3191,7 +3067,7 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
     }
     if (!m_util.is_seq(o1) && !m_util.is_re(o1))
         return;
-    if (ctx.get_fparams().m_seq_use_derivatives && m_util.is_re(o1)) {
+    if (m_util.is_re(o1)) {
         m_regex.propagate_eq(o1, o2);
         return;        
     }
@@ -3200,33 +3076,6 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
     new_eq_eh(deps, n1, n2);
 }
 
-lbool theory_seq::regex_are_equal(expr* _r1, expr* _r2) {
-    if (_r1 == _r2) {
-        return l_true;
-    }
-    expr_ref r1(_r1, m);
-    expr_ref r2(_r2, m);
-    m_rewrite(r1);
-    m_rewrite(r2);
-    if (r1 == r2) 
-        return l_true;
-    expr* d1 = m_util.re.mk_inter(r1, m_util.re.mk_complement(r2));
-    expr* d2 = m_util.re.mk_inter(r2, m_util.re.mk_complement(r1));
-    expr_ref diff(m_util.re.mk_union(d1, d2), m);
-    m_rewrite(diff);
-    eautomaton* aut = get_automaton(diff);
-    if (!aut) {
-        return l_undef;
-    }
-    else if (aut->is_empty()) {
-        return l_true;
-    }
-    else {
-        return l_false;
-    }
-}
-
-
 void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
     expr* e1 = n1->get_owner();
     expr* e2 = n2->get_owner();
@@ -3246,22 +3095,7 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
         enforce_length_coherence(n1, n2);
     }
     else if (n1 != n2 && m_util.is_re(e1)) {
-        // create an expression for the symmetric difference and imply it is empty.
-        enode_pair_vector eqs;
-        literal_vector lits;
-        switch (regex_are_equal(e1, e2)) {
-        case l_true:
-            break;
-        case l_false:
-            linearize(deps, eqs, lits);
-            eqs.push_back(enode_pair(n1, n2));
-            set_conflict(eqs, lits);
-            break;
-        default:
-            std::stringstream strm;
-            strm << "could not decide equality over: " << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";
-            throw default_exception(strm.str());
-        }
+        UNREACHABLE();
     }
 }
 
@@ -3271,27 +3105,9 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
     expr_ref e1(n1->get_owner(), m);
     expr_ref e2(n2->get_owner(), m);
     SASSERT(n1->get_root() != n2->get_root());
-    if (m_util.is_re(n1->get_owner())) {
-        
-        if (ctx.get_fparams().m_seq_use_derivatives) {
-            m_regex.propagate_ne(e1, e2);
-            return;
-        }
-
-        enode_pair_vector eqs;
-        literal_vector lits;
-        switch (regex_are_equal(e1, e2)) {
-        case l_false:
-            return;
-        case l_true: {
-            literal lit = mk_eq(e1, e2, false);
-            lits.push_back(~lit);
-            set_conflict(eqs, lits);
-            return;
-        }
-        default:
-            throw default_exception("convert regular expressions into automata");            
-        }
+    if (m_util.is_re(n1->get_owner())) {        
+        m_regex.propagate_ne(e1, e2);
+        return;
     }
     if (ctx.get_fparams().m_seq_use_unicode && m_util.is_char(n1->get_owner())) {
         m_unicode.new_diseq_eh(v1, v2);
@@ -3404,132 +3220,6 @@ void theory_seq::add_unhandled_expr(expr* n) {
 }
 
 
-eautomaton* theory_seq::get_automaton(expr* re) {
-    eautomaton* result = nullptr;
-    if (m_re2aut.find(re, result)) {
-        return result;
-    }
-    if (!m_mk_aut.has_solver()) {
-        m_mk_aut.set_solver(alloc(seq_expr_solver, m, ctx.get_fparams()));
-    }
-    result = m_mk_aut(re);
-    CTRACE("seq", result, { display_expr d(m); result->display(tout, d); });
-    m_automata.push_back(result);
-    m_re2aut.insert(re, result);
-    m_res.push_back(re);
-    return result;
-}
-
-literal theory_seq::mk_accept(expr* s, expr* idx, expr* re, expr* state) {
-    expr_ref_vector args(m);
-    args.push_back(s).push_back(idx).push_back(re).push_back(state);
-    return mk_literal(m_sk.mk_accept(args));
-}
-
-bool theory_seq::is_accept(expr* e, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut) {
-    expr* n = nullptr;
-    if (m_sk.is_accept(e, s, idx, re, n)) {
-        rational r;
-        TRACE("seq", tout << mk_pp(re, m) << "\n";);
-        VERIFY(m_autil.is_numeral(n, r));
-        SASSERT(r.is_unsigned());
-        i = r.get_unsigned();
-        aut = get_automaton(re);        
-        return aut != nullptr;
-    }
-    else {
-        return false;
-    }
-}
-
-/**
-   step(s, idx, re, i, j, t) -> nth(s, idx) == t & len(s) > idx
-   step(s, idx, re, i, j, t) -> accept(s, idx + 1, re, j)
-*/
-void theory_seq::propagate_step(literal lit, expr* step) {
-    SASSERT(ctx.get_assignment(lit) == l_true);
-    expr* re = nullptr, *s = nullptr, *t = nullptr, *idx = nullptr, *i = nullptr, *j = nullptr;
-    VERIFY(m_sk.is_step(step, s, idx, re, i, j, t));
-    
-    TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(t, m) << "\n";);
-    propagate_lit(nullptr, 1, &lit, mk_literal(t));
-
-    expr_ref len_s = mk_len(s);
-    rational lo;
-    rational _idx;
-    VERIFY(m_autil.is_numeral(idx, _idx));
-    if (lower_bound(len_s, lo) && lo.is_unsigned() && lo >= _idx) {
-        // skip
-    }
-    else {
-        propagate_lit(nullptr, 1, &lit, ~m_ax.mk_le(len_s, _idx));
-    }
-    ensure_nth(lit, s, idx);
-
-    expr_ref idx1(m_autil.mk_int(_idx + 1), m);
-    propagate_lit(nullptr, 1, &lit, mk_accept(s, idx1, re, j));
-}
-
-/**
-   acc(s, idx, re, i) ->  \/ step(s, idx, re, i, j, t)                if i is non-final
-   acc(s, idx, re, i) -> len(s) <= idx \/ step(s, idx, re, i, j, t)   if i is final   
-   acc(s, idx, re, i) -> len(s) >= idx    if i is final
-   acc(s, idx, re, i) -> len(s) > idx     if i is non-final
-   acc(s, idx, re, i) -> idx < max_unfolding
- */
-void theory_seq::propagate_accept(literal lit, expr* acc) {
-    ++m_stats.m_propagate_automata;
-    expr *e = nullptr, *idx = nullptr, *re = nullptr;
-    unsigned src = 0;
-    rational _idx;
-    eautomaton* aut = nullptr;
-    if (!is_accept(acc, e, idx, re, src, aut))
-        return;
-    VERIFY(m_autil.is_numeral(idx, _idx));
-    VERIFY(aut);
-    if (aut->is_sink_state(src)) {
-        TRACE("seq", { display_expr d(m); aut->display(tout << "sink " << src << "\n", d); });
-        propagate_lit(nullptr, 1, &lit, false_literal);
-        return;
-    }
-
-    expr_ref len = mk_len(e);
-    literal_vector lits;
-    lits.push_back(~lit);
-    if (aut->is_final_state(src)) {
-        lits.push_back(mk_literal(m_autil.mk_le(len, idx)));
-        propagate_lit(nullptr, 1, &lit, mk_literal(m_autil.mk_ge(len, idx)));
-    }
-    else {
-        propagate_lit(nullptr, 1, &lit, ~mk_literal(m_autil.mk_le(len, idx)));
-    }
-
-    eautomaton::moves mvs;
-    aut->get_moves_from(src, mvs);
-    TRACE("seq", tout << mk_pp(acc, m) << " #moves " << mvs.size() << "\n";);
-    for (auto const& mv : mvs) {
-        expr_ref nth = mk_nth(e, idx);
-        expr_ref t = mv.t()->accept(nth);
-        ctx.get_rewriter()(t);
-        expr_ref step_e(m_sk.mk_step(e, idx, re, src, mv.dst(), t), m);
-        lits.push_back(mk_literal(step_e));
-    }
-    
-    {
-        scoped_trace_stream _sts(*this, lits);        
-        ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
-    }
-
-    // NB. use instead a length tracking assumption on e to limit unfolding.
-    // that is, use add_length_limit when the atomaton is instantiated.
-    // and track the assignment to the length literal (mk_le(len, idx)).
-    // 
-    if (_idx.get_unsigned() > m_max_unfolding_depth && 
-        m_max_unfolding_lit != null_literal && ctx.get_scope_level() > 0) {
-        propagate_lit(nullptr, 1, &lit, ~m_max_unfolding_lit);
-    }
-}
-
 void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) {
     if (m_has_seq) {
         TRACE("seq", tout << "add_theory_assumption\n";);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index ac5f52ac1..afc3a6340 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -23,7 +23,6 @@ Revision History:
 #include "ast/ast_trail.h"
 #include "util/scoped_vector.h"
 #include "util/scoped_ptr_vector.h"
-#include "math/automata/automaton.h"
 #include "ast/rewriter/seq_rewriter.h"
 #include "util/union_find.h"
 #include "util/obj_ref_hashtable.h"
@@ -301,15 +300,6 @@ namespace smt {
             }
         };
 
-        struct s_in_re {
-            literal     m_lit;
-            expr*       m_s;
-            expr*       m_re;
-            eautomaton* m_aut;
-            bool        m_active;
-            s_in_re(literal l, expr*s, expr* re, eautomaton* aut):
-                m_lit(l), m_s(s), m_re(re), m_aut(aut), m_active(true) {}
-        };
 
         void erase_index(unsigned idx, unsigned i);
 
@@ -318,7 +308,6 @@ namespace smt {
             void reset() { memset(this, 0, sizeof(stats)); }
             unsigned m_num_splits;
             unsigned m_num_reductions;
-            unsigned m_propagate_automata;
             unsigned m_check_length_coherence;
             unsigned m_branch_variable;
             unsigned m_branch_nqs;
@@ -376,19 +365,13 @@ namespace smt {
         expr_ref_vector  m_ls, m_rs, m_lhs, m_rhs;
         expr_ref_pair_vector m_new_eqs;
 
-        // maintain automata with regular expressions.
-        scoped_ptr_vector<eautomaton>  m_automata;
-        obj_map<expr, eautomaton*>     m_re2aut;
-        expr_ref_vector                m_res;
         unsigned                       m_max_unfolding_depth;
         literal                        m_max_unfolding_lit;
-        vector<s_in_re>                m_s_in_re;
 
         expr*                          m_unhandled_expr;
         bool                           m_has_seq;
         bool                           m_new_solution;     // new solution added
         bool                           m_new_propagation;  // new propagation to core
-        re2automaton                   m_mk_aut;
 
         obj_hashtable<expr>            m_fixed;            // string variables that are fixed length.
         obj_hashtable<expr>            m_is_digit;         // expressions that have been constrained to be digits
@@ -618,13 +601,6 @@ namespace smt {
 
         void set_incomplete(app* term);
 
-        // automata utilities
-        void propagate_in_re(expr* n, bool is_true);
-        eautomaton* get_automaton(expr* e);
-        literal mk_accept(expr* s, expr* idx, expr* re, expr* state);
-        literal mk_accept(expr* s, expr* idx, expr* re, unsigned i) { return mk_accept(s, idx, re, m_autil.mk_int(i)); }
-        bool is_accept(expr* acc) const {  return m_sk.is_accept(acc); }
-        bool is_accept(expr* acc, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut);
         void propagate_not_prefix(expr* e);
         void propagate_not_suffix(expr* e);
         void ensure_nth(literal lit, expr* s, expr* idx);