diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt
index 23d4383b0..d2b80ea9c 100644
--- a/src/ast/rewriter/CMakeLists.txt
+++ b/src/ast/rewriter/CMakeLists.txt
@@ -33,6 +33,7 @@ z3_add_component(rewriter
     recfun_rewriter.cpp
     rewriter.cpp
     seq_axioms.cpp
+    seq_eq_solver.cpp
     seq_rewriter.cpp
     seq_skolem.cpp
     th_rewriter.cpp
diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h
index f5d1df68a..1b3101e15 100644
--- a/src/ast/rewriter/seq_axioms.h
+++ b/src/ast/rewriter/seq_axioms.h
@@ -48,11 +48,6 @@ namespace seq {
         expr_ref mk_seq_eq(expr* a, expr* b);
         expr_ref mk_eq_empty(expr* e);
 
-        expr_ref mk_ge(expr* x, int n) { return mk_ge_e(x, a.mk_int(n)); }
-        expr_ref mk_le(expr* x, int n) { return mk_le_e(x, a.mk_int(n)); }
-        expr_ref mk_ge(expr* x, rational const& n) { return mk_ge_e(x, a.mk_int(n)); }
-        expr_ref mk_le(expr* x, rational const& n) { return mk_le_e(x, a.mk_int(n)); }
-
         expr_ref mk_ge_e(expr* x, expr* y);
         expr_ref mk_le_e(expr* x, expr* y);
 
@@ -111,6 +106,11 @@ namespace seq {
         expr_ref length_limit(expr* s, unsigned k);
         expr_ref is_digit(expr* ch);
 
+        expr_ref mk_ge(expr* x, int n) { return mk_ge_e(x, a.mk_int(n)); }
+        expr_ref mk_le(expr* x, int n) { return mk_le_e(x, a.mk_int(n)); }
+        expr_ref mk_ge(expr* x, rational const& n) { return mk_ge_e(x, a.mk_int(n)); }
+        expr_ref mk_le(expr* x, rational const& n) { return mk_le_e(x, a.mk_int(n)); }
+
     };
 
 };
diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h
index 0a53dcd85..dc2548b85 100644
--- a/src/smt/seq_axioms.h
+++ b/src/smt/seq_axioms.h
@@ -97,6 +97,8 @@ namespace smt {
         literal mk_ge(expr* e, rational const& k) { return mk_ge_e(e, a.mk_int(k)); }
         literal mk_le(expr* e, rational const& k) { return mk_le_e(e, a.mk_int(k)); }
 
+        seq::axioms& ax() { return m_ax; }
+
     };
 
 };
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index 735306d04..3eb0d6812 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -41,18 +41,18 @@ bool theory_seq::solve_eqs(unsigned i) {
 }
 
 bool theory_seq::solve_eq(unsigned idx) {
-    const eq& e = m_eqs[idx];
+    const depeq& e = m_eqs[idx];
     expr_ref_vector& ls = m_ls;
     expr_ref_vector& rs = m_rs;
     m_ls.reset();
     m_rs.reset();
     dependency* dep2 = nullptr;
     bool change = false;
-    if (!canonize(e.ls(), ls, dep2, change)) return false;
-    if (!canonize(e.rs(), rs, dep2, change)) return false;
+    if (!canonize(e.ls, ls, dep2, change)) return false;
+    if (!canonize(e.rs, rs, dep2, change)) return false;
     dependency* deps = m_dm.mk_join(dep2, e.dep());
     TRACE("seq_verbose", 
-          tout << e.ls() << " = " << e.rs() << " ==> ";
+          tout << e.ls << " = " << e.rs << " ==> ";
           tout << ls << " = " << rs << "\n";
           display_deps(tout, deps););
 
@@ -81,6 +81,14 @@ bool theory_seq::solve_eq(unsigned idx) {
     if (!ctx.inconsistent() && solve_nth_eq1(rs, ls, deps)) {
         return true;
     }
+    seq::eq_ptr r;
+    m_eq_deps = deps;
+    if (!ctx.inconsistent() && m_eq.solve(e, r)) {
+        if (!r) 
+            return true;
+        m_eqs.set(idx, depeq(m_eq_id++, r->ls, r->rs, deps));
+        return false;
+    }
     if (!ctx.inconsistent() && solve_itos(rs, ls, deps)) {
         return true;
     }
@@ -90,16 +98,34 @@ bool theory_seq::solve_eq(unsigned idx) {
         expr_ref_vector new_ls(m);
         if (!m_offset_eq.empty() && find_better_rep(ls, rs, idx, deps, new_ls)) {
             // Find a better equivalent term for lhs of an equation based on length constraints            
-            m_eqs.push_back(eq(m_eq_id++, new_ls, rs, deps));
+            m_eqs.push_back(depeq(m_eq_id++, new_ls, rs, deps));
             return true;
         }
         else {
-            m_eqs.set(idx, eq(m_eq_id++, ls, rs, deps)); 
+            m_eqs.set(idx, depeq(m_eq_id++, ls, rs, deps));
         }
     }
     return false;
 }
 
+void theory_seq::add_consequence(bool uses_eq, expr_ref_vector const& clause) {
+    dependency* dep = uses_eq ? m_eq_deps : nullptr;
+    if (clause.size() == 1) {
+        propagate_lit(dep, 0, nullptr, mk_literal(clause[0]));
+        return;
+    }
+    enode_pair_vector eqs;
+    literal_vector lits;
+    linearize(dep, eqs, lits);
+    for (auto& lit : lits)
+        lit.neg();
+    for (auto eq : eqs)
+        lits.push_back(~mk_eq(eq.first->get_expr(), eq.second->get_expr(), false));
+    for (auto f : clause)
+        lits.push_back(mk_literal(f));    
+    add_axiom(lits);
+}
+
 bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) {
     if (l == r) {
         return true;
@@ -169,7 +195,6 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons
         case l_true:
             break;
         case l_undef: 
-            ctx.mark_as_relevant(eq);
             propagate_lit(dep, 0, nullptr, eq);
             m_new_propagation = true;
             break;
@@ -277,14 +302,14 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons
     // Offset = 0, Changed
 
     for (unsigned i = 0; i < idx; ++i) {
-        eq const& e = m_eqs[i];
-        if (e.ls() != ls) continue;
+        depeq const& e = m_eqs[i];
+        if (e.ls != ls) continue;
         expr* nl_fst = nullptr;
-        if (e.rs().size() > 1 && is_var(e.rs().get(0)))
-            nl_fst = e.rs().get(0);
+        if (e.rs.size() > 1 && is_var(e.rs.get(0)))
+            nl_fst = e.rs.get(0);
         if (nl_fst && nl_fst != r_fst && root2 == get_root(mk_len(nl_fst))) {
             res.reset();
-            res.append(e.rs());
+            res.append(e.rs);
             deps = m_dm.mk_join(e.dep(), deps);
             return true;
         }
@@ -300,18 +325,18 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons
     // Offset != 0, Changed
     if (m_offset_eq.contains(root2)) {
         for (unsigned i = 0; i < idx; ++i) {
-            eq const& e = m_eqs[i];
-            if (e.ls() != ls) continue;
+            depeq const& e = m_eqs[i];
+            if (e.ls != ls) continue;
             expr* nl_fst = nullptr;
-            if (e.rs().size() > 1 && is_var(e.rs().get(0)))
-                nl_fst = e.rs().get(0);
+            if (e.rs.size() > 1 && is_var(e.rs.get(0)))
+                nl_fst = e.rs.get(0);
             if (nl_fst && nl_fst != r_fst) {
                 expr_ref len_nl_fst = mk_len(nl_fst);
                 if (ctx.e_internalized(len_nl_fst)) {
                     enode * root1 = get_root(len_nl_fst);
                     if (m_offset_eq.contains(root2, root1)) {
                         res.reset();
-                        res.append(e.rs());
+                        res.append(e.rs);
                         deps = m_dm.mk_join(e.dep(), deps);
                         return true;
                     }
@@ -363,9 +388,9 @@ bool theory_seq::len_based_split() {
             eq const& e = m_eqs[i];
             expr_ref_vector new_ls(m);
             dependency *deps = e.dep();
-            if (find_better_rep(e.ls(), e.rs(), i, deps, new_ls)) {
+            if (find_better_rep(e.ls, e.rs, i, deps, new_ls)) {
                 expr_ref_vector rs(m);
-                rs.append(e.rs());
+                rs.append(e.rs);
                 m_eqs.set(i, eq(m_eq_id++, new_ls, rs, deps));
                 TRACE("seq", display_equation(tout, m_eqs[i]););
             }
@@ -400,9 +425,9 @@ bool theory_seq::len_based_split() {
    
 */
 
-bool theory_seq::len_based_split(eq const& e) {
-    expr_ref_vector const& ls = e.ls();
-    expr_ref_vector const& rs = e.rs();
+bool theory_seq::len_based_split(depeq const& e) {
+    expr_ref_vector const& ls = e.ls;
+    expr_ref_vector const& rs = e.rs;
     
     int offset = 0;
     if (!has_len_offset(ls, rs, offset))
@@ -487,17 +512,17 @@ bool theory_seq::branch_variable_mb() {
     int start = ctx.get_random_value();
     for (unsigned i = 0; i < sz; ++i) {
         unsigned k = (i + start) % sz;
-        eq const& e = m_eqs[k];
+        depeq const& e = m_eqs[k];
         vector<rational> len1, len2;
         if (!is_complex(e)) {
             continue;
         }
-        if (e.ls().empty() || e.rs().empty() || 
-            (!is_var(e.ls()[0]) && !is_var(e.rs()[0]))) {
+        if (e.ls.empty() || e.rs.empty() || 
+            (!is_var(e.ls[0]) && !is_var(e.rs[0]))) {
             continue;
         }
 
-        if (!enforce_length(e.ls(), len1) || !enforce_length(e.rs(), len2)) {
+        if (!enforce_length(e.ls, len1) || !enforce_length(e.rs, len2)) {
             // change = true;
             continue;
         }
@@ -505,15 +530,15 @@ bool theory_seq::branch_variable_mb() {
         for (const auto& elem : len1) l1 += elem;
         for (const auto& elem : len2) l2 += elem;
         if (l1 != l2) {
-            expr_ref l = mk_concat(e.ls());
-            expr_ref r = mk_concat(e.rs());
+            expr_ref l = mk_concat(e.ls);
+            expr_ref r = mk_concat(e.rs);
             expr_ref lnl = mk_len(l), lnr = mk_len(r);
             if (propagate_eq(e.dep(), lnl, lnr, false)) {
                 change = true;
             }
             continue;
         }
-        if (split_lengths(e.dep(), e.ls(), e.rs(), len1, len2)) {
+        if (split_lengths(e.dep(), e.ls, e.rs, len1, len2)) {
             TRACE("seq", tout << "split lengths\n";);
             change = true;
             break;
@@ -523,12 +548,12 @@ bool theory_seq::branch_variable_mb() {
 }
 
 
-bool theory_seq::is_complex(eq const& e) {
+bool theory_seq::is_complex(depeq const& e) {
     unsigned num_vars1 = 0, num_vars2 = 0;
-    for (auto const& elem : e.ls()) {
+    for (auto const& elem : e.ls) {
         if (is_var(elem)) ++num_vars1;
     }
-    for (auto const& elem : e.rs()) {
+    for (auto const& elem : e.rs) {
         if (is_var(elem)) ++num_vars2;
     }
     return num_vars1 > 0 && num_vars2 > 0 && num_vars1 + num_vars2 > 2;
@@ -639,14 +664,14 @@ bool theory_seq::branch_binary_variable() {
     return false;
 }
 
-bool theory_seq::branch_binary_variable(eq const& e) {
+bool theory_seq::branch_binary_variable(depeq const& e) {
     if (is_complex(e)) {
         return false;
     }
     ptr_vector<expr> xs, ys;
     expr_ref x(m), y(m);
-    if (!is_binary_eq(e.ls(), e.rs(), x, xs, ys, y) &&
-        !is_binary_eq(e.rs(), e.ls(), x, xs, ys, y))
+    if (!is_binary_eq(e.ls, e.rs, x, xs, ys, y) &&
+        !is_binary_eq(e.rs, e.ls, x, xs, ys, y))
         return false;
     if (x == y) {
         return false;
@@ -706,13 +731,13 @@ bool theory_seq::branch_binary_variable(eq const& e) {
 bool theory_seq::branch_unit_variable() {
     bool result = false;
     for (auto const& e : m_eqs) {
-        if (is_unit_eq(e.ls(), e.rs()) && 
-            branch_unit_variable(e.dep(), e.ls()[0], e.rs())) {
+        if (is_unit_eq(e.ls, e.rs) && 
+            branch_unit_variable(e.dep(), e.ls[0], e.rs)) {
             result = true;
             break;
         }
-        if (is_unit_eq(e.rs(), e.ls()) && 
-            branch_unit_variable(e.dep(), e.rs()[0], e.ls())) {
+        if (is_unit_eq(e.rs, e.ls) && 
+            branch_unit_variable(e.dep(), e.rs[0], e.ls)) {
             result = true;
             break;
         }
@@ -861,11 +886,11 @@ bool theory_seq::can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector c
 // Equation is of the form x ++ xs = y1 ++ ys ++ y2 where xs, ys are units.
 // If xs and ys cannot align then
 //     x ++ xs = y1 ++ ys ++ y2 => x = y1 ++ ys ++ z, z ++ xs = y2
-bool theory_seq::branch_ternary_variable_rhs(eq const& e) {
+bool theory_seq::branch_ternary_variable_rhs(depeq const& e) {
     expr_ref_vector xs(m), ys(m);
     expr_ref x(m), y1(m), y2(m);
-    if (!is_ternary_eq_rhs(e.ls(), e.rs(), x, xs, y1, ys, y2) &&
-        !is_ternary_eq_rhs(e.rs(), e.ls(), x, xs, y1, ys, y2)) {
+    if (!is_ternary_eq_rhs(e.ls, e.rs, x, xs, y1, ys, y2) &&
+        !is_ternary_eq_rhs(e.rs, e.ls, x, xs, y1, ys, y2)) {
         return false;
     }
     if (m_sk.is_align_l(y1) || m_sk.is_align_r(y1))
@@ -905,11 +930,11 @@ bool theory_seq::branch_ternary_variable_rhs(eq const& e) {
 // Equation is of the form xs ++ x = y1 ++ ys ++ y2 where xs, ys are units.
 // If xs and ys cannot align then
 //      xs ++ x = y1 ++ ys ++ y2 => xs ++ z = y1, x = z ++ ys ++ y2
-bool theory_seq::branch_ternary_variable_lhs(eq const& e) {
+bool theory_seq::branch_ternary_variable_lhs(depeq const& e) {
     expr_ref_vector xs(m), ys(m);
     expr_ref x(m), y1(m), y2(m);
-    if (!is_ternary_eq_lhs(e.ls(), e.rs(), xs, x, y1, ys, y2) &&
-        !is_ternary_eq_lhs(e.rs(), e.ls(), xs, x, y1, ys, y2))
+    if (!is_ternary_eq_lhs(e.ls, e.rs, xs, x, y1, ys, y2) &&
+        !is_ternary_eq_lhs(e.rs, e.ls, xs, x, y1, ys, y2))
         return false;
     if (m_sk.is_align_l(y1) || m_sk.is_align_r(y1))
         return false;
@@ -970,10 +995,10 @@ literal theory_seq::mk_alignment(expr* e1, expr* e2) {
 // Equation is of the form x1 ++ xs ++ x2 = y1 ++ ys ++ y2 where xs, ys are units.
 // If xs and ys cannot align then
 //      x1 ++ xs ++ x2 = y1 ++ ys ++ y2 =>    |x1| >= |y1 ++ ys|  V  |x1 ++ xs| <= |y1|
-bool theory_seq::branch_quat_variable(eq const& e) {
+bool theory_seq::branch_quat_variable(depeq const& e) {
     expr_ref_vector xs(m), ys(m);
     expr_ref x1(m), x2(m), y1(m), y2(m);
-    if (!is_quat_eq(e.ls(), e.rs(), x1, xs, x2, y1, ys, y2))
+    if (!is_quat_eq(e.ls, e.rs, x1, xs, x2, y1, ys, y2))
         return false;
     dependency* dep = e.dep();
 
@@ -1132,7 +1157,7 @@ bool theory_seq::branch_variable_eq() {
 
     for (unsigned i = 0; i < sz; ++i) {
         unsigned k = (i + start) % sz;
-        eq const& e = m_eqs[k];
+        depeq const& e = m_eqs[k];
 
         if (branch_variable_eq(e)) {
             TRACE("seq", tout << "branch variable\n";);
@@ -1142,15 +1167,15 @@ bool theory_seq::branch_variable_eq() {
     return ctx.inconsistent();
 }
 
-bool theory_seq::branch_variable_eq(eq const& e) {
+bool theory_seq::branch_variable_eq(depeq const& e) {
     unsigned id = e.id();
     unsigned s = find_branch_start(2*id);
-    TRACE("seq", tout << s << " " << id << ": " << e.ls() << " = " << e.rs() << "\n";);
-    bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs());
+    TRACE("seq", tout << s << " " << id << ": " << e.ls << " = " << e.rs << "\n";);
+    bool found = find_branch_candidate(s, e.dep(), e.ls, e.rs);
     insert_branch_start(2*id, s);
     if (!found) {
         s = find_branch_start(2*id + 1);
-        found = find_branch_candidate(s, e.dep(), e.rs(), e.ls());
+        found = find_branch_candidate(s, e.dep(), e.rs, e.ls);
         insert_branch_start(2*id + 1, s);
     }
     return found;
@@ -1428,8 +1453,8 @@ bool theory_seq::reduce_length_eq() {
     int start = ctx.get_random_value();
 
     for (unsigned i = 0; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
-        eq const& e = m_eqs[(i + start) % m_eqs.size()];
-        if (reduce_length_eq(e.ls(), e.rs(), e.dep())) {
+        depeq const& e = m_eqs[(i + start) % m_eqs.size()];
+        if (reduce_length_eq(e.ls, e.rs, e.dep())) {
             TRACE("seq", tout << "reduce length eq\n";);
             return true;
         }
@@ -1631,7 +1656,7 @@ bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const&
         rs1.push_back(m_util.str.mk_unit(rhs)); 
         rs1.push_back(m_sk.mk_post(s, idx1));
         TRACE("seq", tout << ls1 << "\n"; tout << rs1 << "\n";);
-        m_eqs.push_back(eq(m_eq_id++, ls1, rs1, deps));        
+        m_eqs.push_back(depeq(m_eq_id++, ls1, rs1, deps));
         return true;
     }   
     return false;
diff --git a/src/smt/tactic/CMakeLists.txt b/src/smt/tactic/CMakeLists.txt
index 6187f9c18..3b7a719de 100644
--- a/src/smt/tactic/CMakeLists.txt
+++ b/src/smt/tactic/CMakeLists.txt
@@ -1,12 +1,12 @@
 z3_add_component(smt_tactic
   SOURCES
     ctx_solver_simplify_tactic.cpp
-    smt_tactic.cpp
+    smt_tactic_core.cpp
     unit_subsumption_tactic.cpp
   COMPONENT_DEPENDENCIES
     smt
   TACTIC_HEADERS
     ctx_solver_simplify_tactic.h
-    smt_tactic.h
+    smt_tactic_core.h
     unit_subsumption_tactic.h
 )
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic_core.cpp
similarity index 98%
rename from src/smt/tactic/smt_tactic.cpp
rename to src/smt/tactic/smt_tactic_core.cpp
index 4bd8445b8..705f2751d 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic_core.cpp
@@ -317,12 +317,12 @@ tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) {
     return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p);
 }
 
-tactic * mk_smt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) {
+tactic * mk_smt_tactic_core(ast_manager& m, params_ref const& p, symbol const& logic) {
     parallel_params pp(p);
     return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_seq_smt_tactic(p);
 }
 
-tactic * mk_smt_tactic_using(ast_manager& m, bool auto_config, params_ref const& _p) {
+tactic * mk_smt_tactic_core_using(ast_manager& m, bool auto_config, params_ref const& _p) {
     parallel_params pp(_p);
     params_ref p = _p;
     p.set_bool("auto_config", auto_config);
diff --git a/src/smt/tactic/smt_tactic.h b/src/smt/tactic/smt_tactic_core.h
similarity index 67%
rename from src/smt/tactic/smt_tactic.h
rename to src/smt/tactic/smt_tactic_core.h
index bb9a1b69a..f89b3c649 100644
--- a/src/smt/tactic/smt_tactic.h
+++ b/src/smt/tactic/smt_tactic_core.h
@@ -26,14 +26,13 @@ Notes:
 class tactic;
 class filter_model_converter;
 
-tactic * mk_smt_tactic(ast_manager& m, params_ref const & p = params_ref(), symbol const& logic = symbol::null);
+tactic * mk_smt_tactic_core(ast_manager& m, params_ref const & p = params_ref(), symbol const& logic = symbol::null);
 // syntax sugar for using_params(mk_smt_tactic(), p) where p = (:auto_config, auto_config)
-tactic * mk_smt_tactic_using(ast_manager& m, bool auto_config = true, params_ref const & p = params_ref());
+tactic * mk_smt_tactic_core_using(ast_manager& m, bool auto_config = true, params_ref const & p = params_ref());
 
 tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p);
 
 
 /*
-  ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(m, p)") 
   ADD_TACTIC("psmt", "builtin strategy for SMT tactic in parallel.", "mk_parallel_smt_tactic(m, p)")
 */
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 80f7cf0e5..04852a8a8 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -272,6 +272,7 @@ theory_seq::theory_seq(context& ctx):
     m_autil(m),
     m_sk(m, m_rewrite),
     m_ax(*this, m_rewrite),
+    m_eq(m, m_ax.ax()),
     m_regex(*this),
     m_arith_value(m),
     m_trail_stack(*this),
@@ -285,6 +286,12 @@ theory_seq::theory_seq(context& ctx):
     m_new_solution(false),
     m_new_propagation(false) {
 
+    std::function<void(bool, expr_ref_vector const&)> _add_consequence = 
+        [&](bool uses_eq, expr_ref_vector const& clause) { 
+        add_consequence(uses_eq, clause);
+    };
+
+    m_eq.set_add_consequence(_add_consequence);
 }
 
 theory_seq::~theory_seq() {
@@ -674,8 +681,8 @@ bool theory_seq::check_lts() {
 
 bool theory_seq::is_solved() {
     if (!m_eqs.empty()) {
-        TRACE("seq", tout << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";);
-        IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";);
+        TRACE("seq", tout << "(seq.giveup " << m_eqs[0].ls << " = " << m_eqs[0].rs << " is unsolved)\n";);
+        IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls << " = " << m_eqs[0].rs << " is unsolved)\n";);
         return false;
     }
     if (!m_ncs.empty()) {
@@ -1053,7 +1060,7 @@ bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector con
         rhs.append(rs.size()-1, rs.c_ptr() + 1);
         SASSERT(!lhs.empty() || !rhs.empty());
         deps = mk_join(deps, lits);
-        m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps));
+        m_eqs.push_back(depeq(m_eq_id++, lhs, rhs, deps));
         TRACE("seq", tout << "Propagate equal lengths " << l << " " << r << "\n";);
         propagate_eq(deps, lits, l, r, true);
         return true;
@@ -1067,7 +1074,7 @@ bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector con
         SASSERT(!lhs.empty() || !rhs.empty());
         deps = mk_join(deps, lits);
         TRACE("seq", tout << "Propagate equal lengths " << l << " " << r << "\n" << "ls: " << ls << "\nrs: " << rs << "\n";);
-        m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps));
+        m_eqs.push_back(depeq(m_eq_id++, lhs, rhs, deps));
         propagate_eq(deps, lits, l, r, true);
         return true;
     }
@@ -1145,12 +1152,12 @@ bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vect
         lhs.append(l2, ls2);
         rhs.append(r2, rs2);
         for (auto const& e : m_eqs) {
-            if (e.ls() == lhs && e.rs() == rhs) {
+            if (e.ls == lhs && e.rs == rhs) {
                 return false;
             }
         }
         deps = mk_join(deps, lit);                
-        m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps));
+        m_eqs.push_back(depeq(m_eq_id++, lhs, rhs, deps));
         propagate_eq(deps, l, r, true);
         TRACE("seq", tout << "propagate eq\n" << m_eqs.size() << "\nlhs: " << lhs << "\nrhs: " << rhs << "\n";);
         return true;
@@ -1653,11 +1660,11 @@ std::ostream& theory_seq::display_equations(std::ostream& out) const {
     return out;
 }
 
-std::ostream& theory_seq::display_equation(std::ostream& out, eq const& e) const {
+std::ostream& theory_seq::display_equation(std::ostream& out, depeq const& e) const {
     bool first = true;
-    for (expr* a : e.ls()) { if (first) first = false; else out << "\n"; out << mk_bounded_pp(a, m, 2); }
+    for (expr* a : e.ls) { if (first) first = false; else out << "\n"; out << mk_bounded_pp(a, m, 2); }
     out << " = ";
-    for (expr* a : e.rs()) { if (first) first = false; else out << "\n"; out << mk_bounded_pp(a, m, 2); }
+    for (expr* a : e.rs) { if (first) first = false; else out << "\n"; out << mk_bounded_pp(a, m, 2); }
     out << " <- \n";
     return display_deps(out, e.dep());    
 }
@@ -2017,11 +2024,9 @@ app* theory_seq::mk_value(app* e) {
 void theory_seq::validate_model(model& mdl) {
     return;
     for (auto const& eq : m_eqs) {
-        expr_ref_vector ls = eq.ls();
-        expr_ref_vector rs = eq.rs();
-        sort* srt = ls[0]->get_sort();
-        expr_ref l(m_util.str.mk_concat(ls, srt), m);
-        expr_ref r(m_util.str.mk_concat(rs, srt), m);
+        sort* srt = eq.ls[0]->get_sort();
+        expr_ref l(m_util.str.mk_concat(eq.ls, srt), m);
+        expr_ref r(m_util.str.mk_concat(eq.rs, srt), m);
         if (!mdl.are_equal(l, r)) {
             IF_VERBOSE(0, verbose_stream() << "equality failed: " << l << " = " << r << "\nbut\n" << mdl(l) << " != " << mdl(r) << "\n");
         }
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 94fe410c0..9b202cebd 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -21,6 +21,7 @@ Revision History:
 #include "ast/seq_decl_plugin.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/rewriter/seq_skolem.h"
+#include "ast/rewriter/seq_eq_solver.h"
 #include "ast/ast_trail.h"
 #include "util/scoped_vector.h"
 #include "util/scoped_ptr_vector.h"
@@ -146,26 +147,21 @@ namespace smt {
         };
 
         // Asserted or derived equality with dependencies
-        class eq {
+        class depeq : public seq::eq {
             unsigned         m_id;
-            expr_ref_vector  m_lhs;
-            expr_ref_vector  m_rhs;
             dependency*      m_dep;
-        public:
-            
-            eq(unsigned id, expr_ref_vector& l, expr_ref_vector& r, dependency* d):
-                m_id(id), m_lhs(l), m_rhs(r), m_dep(d) {}
-            expr_ref_vector const& ls() const { return m_lhs; }
-            expr_ref_vector const& rs() const { return m_rhs; }
+        public:            
+            depeq(unsigned id, expr_ref_vector& l, expr_ref_vector& r, dependency* d):
+                eq(l, r), m_id(id), m_dep(d) {}
             dependency* dep() const { return m_dep; }
             unsigned id() const { return m_id; }
         };
 
-        eq mk_eqdep(expr* l, expr* r, dependency* dep) {
+        depeq mk_eqdep(expr* l, expr* r, dependency* dep) {
             expr_ref_vector ls(m), rs(m);
             m_util.str.get_concat_units(l, ls);
             m_util.str.get_concat_units(r, rs);
-            return eq(m_eq_id++, ls, rs, dep);
+            return depeq(m_eq_id++, ls, rs, dep);
         }        
 
         // equalities that are decomposed by conacatenations
@@ -324,7 +320,7 @@ namespace smt {
 
         dependency_manager         m_dm;
         solution_map               m_rep;        // unification representative.
-        scoped_vector<eq>          m_eqs;        // set of current equations.
+        scoped_vector<depeq>       m_eqs;        // set of current equations.
         scoped_vector<ne>          m_nqs;        // set of current disequalities.
         scoped_vector<nc>          m_ncs;        // set of non-contains constraints.
         scoped_vector<expr*>       m_lts;        // set of asserted str.<, str.<= literals
@@ -357,6 +353,7 @@ namespace smt {
         arith_util       m_autil;
         seq::skolem      m_sk;
         seq_axioms       m_ax;
+        seq::eq_solver   m_eq;
         seq_regex        m_regex;
         arith_value      m_arith_value;
         th_trail_stack   m_trail_stack;
@@ -432,28 +429,29 @@ namespace smt {
         bool fixed_length(bool is_zero = false);
         bool fixed_length(expr* e, bool is_zero);
         bool branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units);
-        bool branch_variable_eq(eq const& e);
-        bool branch_binary_variable(eq const& e);
+        bool branch_variable_eq(depeq const& e);
+        bool branch_binary_variable(depeq const& e);
         bool can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs);
         bool can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector const& rs);
-        bool branch_ternary_variable_rhs(eq const& e);
-        bool branch_ternary_variable_lhs(eq const& e);
+        bool branch_ternary_variable_rhs(depeq const& e);
+        bool branch_ternary_variable_lhs(depeq const& e);
         literal mk_alignment(expr* e1, expr* e2);
-        bool branch_quat_variable(eq const& e);
-        bool len_based_split(eq const& e);
+        bool branch_quat_variable(depeq const& e);
+        bool len_based_split(depeq const& e);
         bool is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs);
         bool propagate_length_coherence(expr* e);  
         bool split_lengths(dependency* dep,
                            expr_ref_vector const& ls, expr_ref_vector const& rs, 
                            vector<rational> const& ll, vector<rational> const& rl);
         bool set_empty(expr* x);
-        bool is_complex(eq const& e);
+        bool is_complex(depeq const& e);
         lbool regex_are_equal(expr* r1, expr* r2);
         void add_unhandled_expr(expr* e);
 
         bool check_extensionality();
         bool check_contains();
         bool check_lts();
+        dependency* m_eq_deps { nullptr };
         bool solve_eqs(unsigned start);
         bool solve_eq(unsigned idx);
         bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);
@@ -560,6 +558,7 @@ namespace smt {
         void deque_axiom(expr* e);
         void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal);        
         void add_axiom(literal_vector& lits);
+        void add_consequence(bool uses_eq, expr_ref_vector const& clause);
         
         bool has_length(expr *e) const { return m_has_length.contains(e); }
         void add_length(expr* e, expr* l);
@@ -613,7 +612,7 @@ namespace smt {
 
         // diagnostics
         std::ostream& display_equations(std::ostream& out) const;
-        std::ostream& display_equation(std::ostream& out, eq const& e) const;
+        std::ostream& display_equation(std::ostream& out, depeq const& e) const;
         std::ostream& display_disequations(std::ostream& out) const;
         std::ostream& display_disequation(std::ostream& out, ne const& e) const;
         std::ostream& display_deps(std::ostream& out, dependency* deps) const;
diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp
index f2702e245..a9294471e 100644
--- a/src/tactic/fpa/qffp_tactic.cpp
+++ b/src/tactic/fpa/qffp_tactic.cpp
@@ -25,7 +25,7 @@ Notes:
 #include "tactic/smtlogics/qfnra_tactic.h"
 #include "sat/tactic/sat_tactic.h"
 #include "sat/sat_solver/inc_sat_solver.h"
-#include "smt/tactic/smt_tactic.h"
+#include "tactic/smtlogics/smt_tactic.h"
 #include "ackermannization/ackermannize_bv_tactic.h"
 
 #include "tactic/fpa/qffp_tactic.h"
diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp
index 394aa63b0..7f145b614 100644
--- a/src/tactic/portfolio/default_tactic.cpp
+++ b/src/tactic/portfolio/default_tactic.cpp
@@ -19,7 +19,6 @@ Notes:
 #include "tactic/portfolio/default_tactic.h"
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/smtlogics/qfbv_tactic.h"
-#include "smt/tactic/smt_tactic.h"
 #include "tactic/smtlogics/qflia_tactic.h"
 #include "tactic/smtlogics/qflra_tactic.h"
 #include "tactic/smtlogics/qfnia_tactic.h"
@@ -32,6 +31,7 @@ Notes:
 #include "tactic/smtlogics/qfaufbv_tactic.h"
 #include "tactic/smtlogics/qfauflia_tactic.h"
 #include "tactic/fd_solver/fd_solver.h"
+#include "tactic/smtlogics/smt_tactic.h"
 
 tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = using_params(and_then(mk_simplify_tactic(m),
diff --git a/src/tactic/smtlogics/CMakeLists.txt b/src/tactic/smtlogics/CMakeLists.txt
index a99fef0b5..393f903fd 100644
--- a/src/tactic/smtlogics/CMakeLists.txt
+++ b/src/tactic/smtlogics/CMakeLists.txt
@@ -13,7 +13,7 @@ z3_add_component(smtlogic_tactics
     qfufbv_tactic.cpp
     qfuf_tactic.cpp
     quant_tactics.cpp
-    smt_tactic_select.cpp
+    smt_tactic.cpp
   COMPONENT_DEPENDENCIES
     ackermannization
     aig_tactic
@@ -28,6 +28,7 @@ z3_add_component(smtlogic_tactics
   PYG_FILES
     qfufbv_tactic_params.pyg
   TACTIC_HEADERS
+    smt_tactic.h
     nra_tactic.h
     qfaufbv_tactic.h
     qfauflia_tactic.h
diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp
index 7d3a170ed..c139321f9 100644
--- a/src/tactic/smtlogics/nra_tactic.cpp
+++ b/src/tactic/smtlogics/nra_tactic.cpp
@@ -21,7 +21,7 @@ Notes:
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/nnf_tactic.h"
 #include "tactic/arith/probe_arith.h"
-#include "smt/tactic/smt_tactic.h"
+#include "tactic/smtlogics/smt_tactic.h"
 #include "qe/qe_tactic.h"
 #include "qe/nlqsat.h"
 #include "qe/qe_lite.h"
diff --git a/src/tactic/smtlogics/qfaufbv_tactic.cpp b/src/tactic/smtlogics/qfaufbv_tactic.cpp
index fa346b857..acad15fd6 100644
--- a/src/tactic/smtlogics/qfaufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfaufbv_tactic.cpp
@@ -25,9 +25,8 @@ Notes:
 #include "tactic/bv/bv_size_reduction_tactic.h"
 #include "tactic/core/ctx_simplify_tactic.h"
 #include "tactic/smtlogics/qfbv_tactic.h"
-#include "tactic/smtlogics/smt_tactic_select.h"
+#include "tactic/smtlogics/smt_tactic.h"
 #include "ackermannization/ackermannize_bv_tactic.h"
-#include "smt/tactic/smt_tactic.h"
 
 static tactic * mk_qfaufbv_preamble(ast_manager & m, params_ref const & p) {
 
@@ -60,7 +59,7 @@ tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) {
 
     tactic * st = using_params(
         and_then(preamble_st, 
-                 cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic_select(m, p))), main_p);
+                 cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic(m, p))), main_p);
     
     st->updt_params(p);
     return st;
diff --git a/src/tactic/smtlogics/qfauflia_tactic.cpp b/src/tactic/smtlogics/qfauflia_tactic.cpp
index 20f4791f3..2f1879d58 100644
--- a/src/tactic/smtlogics/qfauflia_tactic.cpp
+++ b/src/tactic/smtlogics/qfauflia_tactic.cpp
@@ -22,7 +22,8 @@ Notes:
 #include "tactic/arith/propagate_ineqs_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
-#include "smt/tactic/smt_tactic.h"
+#include "tactic/smtlogics/smt_tactic.h"
+
 
 tactic * mk_qfauflia_tactic(ast_manager & m, params_ref const & p) {
     params_ref main_p;
diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp
index 1ef40c5e9..af20eae3e 100644
--- a/src/tactic/smtlogics/qfbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfbv_tactic.cpp
@@ -26,11 +26,10 @@ Notes:
 #include "tactic/bv/max_bv_sharing_tactic.h"
 #include "tactic/bv/bv_size_reduction_tactic.h"
 #include "tactic/aig/aig_tactic.h"
-#include "smt/tactic/smt_tactic.h"
 #include "sat/tactic/sat_tactic.h"
 #include "sat/sat_solver/inc_sat_solver.h"
 #include "ackermannization/ackermannize_bv_tactic.h"
-#include "tactic/smtlogics/smt_tactic_select.h"
+#include "tactic/smtlogics/smt_tactic.h"
 
 #define MEMLIMIT 300
 
@@ -123,8 +122,8 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
 
 tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
     tactic * new_sat = cond(mk_produce_proofs_probe(),
-                            and_then(mk_simplify_tactic(m), mk_smt_tactic_select(m, p)),
+                            and_then(mk_simplify_tactic(m), mk_smt_tactic(m, p)),
                             mk_psat_tactic(m, p));
-    return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic_select(m, p));
+    return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic(m, p));
 
 }
diff --git a/src/tactic/smtlogics/qfidl_tactic.cpp b/src/tactic/smtlogics/qfidl_tactic.cpp
index 109089c2e..c86789ed0 100644
--- a/src/tactic/smtlogics/qfidl_tactic.cpp
+++ b/src/tactic/smtlogics/qfidl_tactic.cpp
@@ -24,7 +24,7 @@ Notes:
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/arith/normalize_bounds_tactic.h"
 #include "tactic/arith/fix_dl_var_tactic.h"
-#include "smt/tactic/smt_tactic.h"
+#include "tactic/smtlogics/smt_tactic.h"
 #include "tactic/arith/lia2pb_tactic.h"
 #include "tactic/arith/pb2bv_tactic.h"
 #include "tactic/arith/diff_neq_tactic.h"
diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp
index 0899d6a3e..8673b6380 100644
--- a/src/tactic/smtlogics/qflia_tactic.cpp
+++ b/src/tactic/smtlogics/qflia_tactic.cpp
@@ -23,7 +23,6 @@ Notes:
 #include "tactic/arith/normalize_bounds_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
-#include "smt/tactic/smt_tactic.h"
 #include "tactic/arith/add_bounds_tactic.h"
 #include "tactic/arith/pb2bv_tactic.h"
 #include "tactic/arith/lia2pb_tactic.h"
@@ -31,6 +30,7 @@ Notes:
 #include "tactic/bv/bit_blaster_tactic.h"
 #include "tactic/bv/max_bv_sharing_tactic.h"
 #include "tactic/aig/aig_tactic.h"
+#include "tactic/smtlogics/smt_tactic.h"
 #include "sat/tactic/sat_tactic.h"
 #include "tactic/arith/bound_manager.h"
 #include "tactic/arith/probe_arith.h"
diff --git a/src/tactic/smtlogics/qflra_tactic.cpp b/src/tactic/smtlogics/qflra_tactic.cpp
index 90532cef6..3d8911686 100644
--- a/src/tactic/smtlogics/qflra_tactic.cpp
+++ b/src/tactic/smtlogics/qflra_tactic.cpp
@@ -21,10 +21,10 @@ Notes:
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
-#include "smt/tactic/smt_tactic.h"
 #include "tactic/arith/recover_01_tactic.h"
 #include "tactic/core/ctx_simplify_tactic.h"
 #include "tactic/arith/probe_arith.h"
+#include "tactic/smtlogics/smt_tactic.h"
 
 tactic * mk_qflra_tactic(ast_manager & m, params_ref const & p) {
     params_ref pivot_p;
diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index f8335a279..cf56cced2 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -21,7 +21,6 @@ Notes:
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
-#include "smt/tactic/smt_tactic.h"
 #include "tactic/bv/bit_blaster_tactic.h"
 #include "tactic/bv/max_bv_sharing_tactic.h"
 #include "sat/tactic/sat_tactic.h"
@@ -30,6 +29,7 @@ Notes:
 #include "tactic/arith/card2bv_tactic.h"
 #include "tactic/core/ctx_simplify_tactic.h"
 #include "tactic/core/cofactor_term_ite_tactic.h"
+#include "tactic/smtlogics/smt_tactic.h"
 #include "nlsat/tactic/qfnra_nlsat_tactic.h"
 
 static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp
index 7d93abe25..b9fec4366 100644
--- a/src/tactic/smtlogics/qfnra_tactic.cpp
+++ b/src/tactic/smtlogics/qfnra_tactic.cpp
@@ -20,8 +20,8 @@ Notes:
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/arith/nla2bv_tactic.h"
-#include "smt/tactic/smt_tactic.h"
 #include "nlsat/tactic/qfnra_nlsat_tactic.h"
+#include "tactic/smtlogics/smt_tactic.h"
 
 static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigned bv_size) {
     params_ref nra2sat_p = p;
diff --git a/src/tactic/smtlogics/qfuf_tactic.cpp b/src/tactic/smtlogics/qfuf_tactic.cpp
index b92eea80a..609107a48 100644
--- a/src/tactic/smtlogics/qfuf_tactic.cpp
+++ b/src/tactic/smtlogics/qfuf_tactic.cpp
@@ -22,8 +22,7 @@ Notes:
 #include "tactic/core/symmetry_reduce_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
-#include "smt/tactic/smt_tactic.h"
-#include "tactic/smtlogics/smt_tactic_select.h"
+#include "tactic/smtlogics/smt_tactic.h"
 
 tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p) {
     params_ref s2_p;
@@ -35,7 +34,7 @@ tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p) {
                     mk_solve_eqs_tactic(m, p),
                     using_params(mk_simplify_tactic(m, p), s2_p),
                     if_no_proofs(if_no_unsat_cores(mk_symmetry_reduce_tactic(m, p))),
-                    mk_smt_tactic_select(m, p));
+                    mk_smt_tactic(m, p));
 }
 
                     
diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp
index acbfcac69..ad9e8b46f 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfufbv_tactic.cpp
@@ -22,7 +22,6 @@ Notes:
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
-#include "smt/tactic/smt_tactic.h"
 #include "tactic/bv/max_bv_sharing_tactic.h"
 #include "tactic/bv/bv_size_reduction_tactic.h"
 #include "tactic/core/reduce_args_tactic.h"
@@ -37,7 +36,7 @@ Notes:
 #include "sat/sat_solver/inc_sat_solver.h"
 #include "tactic/smtlogics/qfaufbv_tactic.h"
 #include "tactic/smtlogics/qfbv_tactic.h"
-#include "tactic/smtlogics/smt_tactic_select.h"
+#include "tactic/smtlogics/smt_tactic.h"
 #include "solver/tactic2solver.h"
 #include "tactic/bv/bv_bound_chk_tactic.h"
 #include "ackermannization/ackermannize_bv_tactic.h"
@@ -186,7 +185,7 @@ tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
         and_then(preamble_st,
                  cond(mk_is_qfbv_probe(), 
                       mk_qfbv_tactic(m), 
-                      mk_smt_tactic_select(m, p))),
+                      mk_smt_tactic(m, p))),
         main_p);
 
     st->updt_params(p);
@@ -198,5 +197,5 @@ tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) {
 
     tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p);
     return and_then(preamble_t,
-                    cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic_select(m, p)));
+                    cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic(m, p)));
 }
diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index 72fc2c40b..6a844a594 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -24,9 +24,9 @@ Revision History:
 #include "qe/qe_lite.h"
 #include "qe/qsat.h"
 #include "tactic/core/ctx_simplify_tactic.h"
-#include "smt/tactic/smt_tactic.h"
 #include "tactic/core/elim_term_ite_tactic.h"
 #include "tactic/arith/probe_arith.h"
+#include "tactic/smtlogics/smt_tactic.h"
 
 static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = false) {
     params_ref pull_ite_p;
diff --git a/src/tactic/smtlogics/smt_tactic.cpp b/src/tactic/smtlogics/smt_tactic.cpp
new file mode 100644
index 000000000..0b78761ca
--- /dev/null
+++ b/src/tactic/smtlogics/smt_tactic.cpp
@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    smt_tactic.cpp
+
+Abstract:
+
+    Tactic that selects SMT backend.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-14
+
+
+--*/
+#include "smt/tactic/smt_tactic_core.h"
+#include "sat/tactic/sat_tactic.h"
+#include "sat/sat_params.hpp"
+
+tactic * mk_smt_tactic(ast_manager & m, params_ref const & p) {
+    sat_params sp(p);
+    return sp.euf() ? mk_sat_tactic(m, p) : mk_smt_tactic_core(m, p);
+}
+
+tactic * mk_smt_tactic_using(ast_manager& m, bool auto_config, params_ref const& p) {
+    sat_params sp(p);
+    return sp.euf() ? mk_sat_tactic(m, p) : mk_smt_tactic_core_using(m, auto_config, p);
+}
diff --git a/src/tactic/smtlogics/smt_tactic.h b/src/tactic/smtlogics/smt_tactic.h
new file mode 100644
index 000000000..d4263afb5
--- /dev/null
+++ b/src/tactic/smtlogics/smt_tactic.h
@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    smt_tactic.h
+
+Abstract:
+
+    Tactic that selects SMT backend.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-14
+
+
+--*/
+#pragma once
+
+#include "util/params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_smt_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+tactic * mk_smt_tactic_using(ast_manager& m, bool auto_config = true, params_ref const& p = params_ref());
+
+/*
+  ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(m, p)") 
+*/
+
+
diff --git a/src/tactic/smtlogics/smt_tactic_select.cpp b/src/tactic/smtlogics/smt_tactic_select.cpp
deleted file mode 100644
index af9cf6a8a..000000000
--- a/src/tactic/smtlogics/smt_tactic_select.cpp
+++ /dev/null
@@ -1,26 +0,0 @@
-/*++
-Copyright (c) 2020 Microsoft Corporation
-
-Module Name:
-
-    smt_tactic_select.cpp
-
-Abstract:
-
-    Tactic that selects SMT backend.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2020-09-14
-
-
---*/
-#include "smt/tactic/smt_tactic.h"
-#include "sat/tactic/sat_tactic.h"
-#include "sat/sat_params.hpp"
-
-tactic * mk_smt_tactic_select(ast_manager & m, params_ref const & p) {
-    sat_params sp(p);
-    return sp.euf() ? mk_sat_tactic(m, p) : mk_smt_tactic(m, p);
-}
-
diff --git a/src/tactic/smtlogics/smt_tactic_select.h b/src/tactic/smtlogics/smt_tactic_select.h
deleted file mode 100644
index 900949040..000000000
--- a/src/tactic/smtlogics/smt_tactic_select.h
+++ /dev/null
@@ -1,25 +0,0 @@
-/*++
-Copyright (c) 2020 Microsoft Corporation
-
-Module Name:
-
-    smt_tactic_select.h
-
-Abstract:
-
-    Tactic that selects SMT backend.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2020-09-14
-
-
---*/
-#pragma once
-
-#include "util/params.h"
-class ast_manager;
-class tactic;
-
-tactic * mk_smt_tactic_select(ast_manager & m, params_ref const & p);
-
diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp
index c79834518..e8495c013 100644
--- a/src/tactic/ufbv/ufbv_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_tactic.cpp
@@ -23,7 +23,7 @@ Notes:
 #include "tactic/core/distribute_forall_tactic.h"
 #include "tactic/core/der_tactic.h"
 #include "tactic/core/reduce_args_tactic.h"
-#include "smt/tactic/smt_tactic.h"
+#include "tactic/smtlogics/smt_tactic.h"
 #include "tactic/core/nnf_tactic.h"
 #include "tactic/ufbv/macro_finder_tactic.h"
 #include "tactic/ufbv/ufbv_rewriter_tactic.h"