diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 0d99dbc39..8a74e7310 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -61,7 +61,8 @@ def init_project_def():
     add_lib('fuzzing', ['ast'], 'test/fuzzing')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')
     add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
-    add_lib('qe', ['smt', 'sat', 'nlsat', 'tactic', 'nlsat_tactic'], 'qe')
+    add_lib('mbp', ['model', 'simplex'], 'qe/mbp')
+    add_lib('qe', ['smt', 'mbp', 'nlsat', 'tactic', 'nlsat_tactic'], 'qe')
     add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver')
     add_lib('fd_solver', ['core_tactics', 'arith_tactics', 'sat_solver', 'smt'], 'tactic/fd_solver') 
     add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base')
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 736bfbdad..bd3ee4cf0 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -79,6 +79,7 @@ add_subdirectory(smt)
 add_subdirectory(tactic/bv)
 add_subdirectory(smt/tactic)
 add_subdirectory(tactic/sls)
+add_subdirectory(qe/mbp)
 add_subdirectory(qe)
 add_subdirectory(muz/base)
 add_subdirectory(muz/dataflow)
diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp
index 64c085def..e3c51c7b5 100644
--- a/src/api/api_qe.cpp
+++ b/src/api/api_qe.cpp
@@ -18,6 +18,7 @@ Notes:
 --*/
 
 #include <iostream>
+#include "ast/expr_map.h"
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
@@ -25,10 +26,8 @@ Notes:
 #include "api/api_model.h"
 #include "api/api_ast_map.h"
 #include "api/api_ast_vector.h"
-#include "qe/qe_vartest.h"
 #include "qe/qe_lite.h"
 #include "muz/spacer/spacer_util.h"
-#include "ast/expr_map.h"
 
 extern "C"
 {
diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index bf6b53077..dcae49e46 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -896,6 +896,34 @@ bool arith_util::is_extended_numeral(expr* term, rational& r) const {
         if (is_to_real(term, term)) {
             continue;
         }
+        if (is_mul(term)) {
+            rational r(mul), n(0);
+            for (expr* arg : *to_app(term)) {
+                if (!is_extended_numeral(arg, n))
+                    return false;
+                r *= n;
+            }
+            return true;
+        }
+        if (is_add(term)) {
+            rational r(0), n(0);
+            for (expr* arg : *to_app(term)) {
+                if (!is_extended_numeral(arg, n))
+                    return false;
+                r += n;
+            }
+            r *= mul;
+            return true;
+        }
+        rational k1, k2;
+        expr* t1, *t2;
+        if (is_sub(term, t1, t2) && 
+            is_extended_numeral(t1, k1) &&
+            is_extended_numeral(t2, k2)) {
+            r = k1 - k2;
+            r *= mul;
+            return true;
+        }
         return false;
     } while (false);
     return false;
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index 4e6983ced..b06141365 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -348,7 +348,7 @@ namespace datatype {
         MATCH_UNARY(is_recognizer);
         bool is_accessor(expr const* e) const { return is_app(e) && is_app_of(to_app(e), fid(), OP_DT_ACCESSOR); }
         MATCH_UNARY(is_accessor);
-        bool is_update_field(app * f) const { return is_app_of(f, fid(), OP_DT_UPDATE_FIELD); }
+        bool is_update_field(expr * f) const { return is_app(f) && is_app_of(to_app(f), fid(), OP_DT_UPDATE_FIELD); }
         app* mk_is(func_decl * c, expr *f);
         ptr_vector<func_decl> const * get_datatype_constructors(sort * ty);
         unsigned get_datatype_num_constructors(sort * ty);
diff --git a/src/qe/qe_vartest.h b/src/ast/is_variable_test.h
similarity index 97%
rename from src/qe/qe_vartest.h
rename to src/ast/is_variable_test.h
index 403856b56..1b8fa5fdb 100644
--- a/src/qe/qe_vartest.h
+++ b/src/ast/is_variable_test.h
@@ -21,7 +21,6 @@ Revision History:
 #include "ast/ast.h"
 #include "util/uint_set.h"
 
-// TBD: move under qe namespace
 class is_variable_proc : public std::unary_function<expr*,bool> {
 public:
     virtual bool operator()(const expr* e) const = 0;
diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp
index 3b6b2224c..6f63a5aee 100644
--- a/src/cmd_context/extra_cmds/dbg_cmds.cpp
+++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp
@@ -33,7 +33,7 @@ Notes:
 #include "util/gparams.h"
 #include "qe/qe_mbp.h"
 #include "qe/qe_mbi.h"
-#include "qe/qe_term_graph.h"
+#include "qe/mbp/mbp_term_graph.h"
 
 
 BINARY_SYM_CMD(get_quantifier_body_cmd,
@@ -369,7 +369,7 @@ public:
             }
             vars.push_back(to_app(v));
         }
-        qe::mbp mbp(m);
+        qe::mbproj mbp(m);
         expr_ref fml(m_fml, m);
         mbp.spacer(vars, *mdl.get(), fml);
         ctx.regular_stream() << fml << "\n";
diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp
index 9d2c00c33..09e438142 100644
--- a/src/muz/spacer/spacer_generalizers.cpp
+++ b/src/muz/spacer/spacer_generalizers.cpp
@@ -30,7 +30,7 @@ Revision History:
 #include "ast/substitution/matcher.h"
 #include "ast/expr_functors.h"
 #include "smt/smt_solver.h"
-#include "qe/qe_term_graph.h"
+#include "qe/mbp/mbp_term_graph.h"
 
 namespace spacer {
 void lemma_sanity_checker::operator()(lemma_ref &lemma) {
@@ -309,14 +309,13 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma)
     {TRACE("core_array_eq", tout << "Not-Inductive!\n";);}
 }
 
-void lemma_eq_generalizer::operator() (lemma_ref &lemma)
-{
+void lemma_eq_generalizer::operator() (lemma_ref &lemma) {
     TRACE("core_eq", tout << "Transforming equivalence classes\n";);
 
     if (lemma->get_cube().empty()) return;
 
     ast_manager &m = m_ctx.get_ast_manager();
-    qe::term_graph egraph(m);
+    mbp::term_graph egraph(m);
     egraph.add_lits(lemma->get_cube());
 
     // -- expand the cube with all derived equalities
diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp
index e6abfdbf1..18c8ba1bf 100644
--- a/src/muz/spacer/spacer_qe_project.cpp
+++ b/src/muz/spacer/spacer_qe_project.cpp
@@ -26,6 +26,7 @@ Revision History:
 #include "ast/expr_functors.h"
 #include "ast/expr_substitution.h"
 #include "ast/ast_util.h"
+#include "ast/is_variable_test.h"
 
 #include "ast/rewriter/expr_replacer.h"
 #include "ast/rewriter/expr_safe_replace.h"
@@ -35,7 +36,6 @@ Revision History:
 #include "model/model_pp.h"
 
 #include "qe/qe.h"
-#include "qe/qe_vartest.h"
 #include "qe/qe_lite.h"
 
 #include "muz/spacer/spacer_mev_array.h"
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 09d712dff..c3d1be6d7 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -54,7 +54,8 @@ Notes:
 
 #include "qe/qe_lite.h"
 #include "qe/qe_mbp.h"
-#include "qe/qe_term_graph.h"
+#include "qe/mbp/mbp_term_graph.h"
+#include "qe/mbp/mbp_plugin.h"
 
 #include "tactic/tactical.h"
 #include "tactic/core/propagate_values_tactic.h"
@@ -69,54 +70,54 @@ Notes:
 
 namespace spacer {
 
-    bool is_clause(ast_manager &m, expr *n) {
-      if (spacer::is_literal(m, n))
-        return true;
-      if (m.is_or(n)) {
-        for (expr *arg : *to_app(n)){
-          if (!spacer::is_literal(m, arg))
-            return false;
-          return true;
+    bool is_clause(ast_manager& m, expr* n) {
+        if (spacer::is_literal(m, n))
+            return true;
+        if (m.is_or(n)) {
+            for (expr* arg : *to_app(n)) {
+                if (!spacer::is_literal(m, arg))
+                    return false;
+                return true;
+            }
         }
-      }
-      return false;
-    }
-
-    bool is_literal(ast_manager &m, expr *n) {
-      return spacer::is_atom(m, n) || (m.is_not(n) && spacer::is_atom(m, to_app(n)->get_arg(0)));
-    }
-
-    bool is_atom(ast_manager &m, expr *n) {
-      if (is_quantifier(n) || !m.is_bool(n))
         return false;
-      if (is_var(n))
-        return true;
-      SASSERT(is_app(n));
-      if (to_app(n)->get_family_id() != m.get_basic_family_id()) {
-        return true;
-      }
+    }
 
-      if ((m.is_eq(n) && !m.is_bool(to_app(n)->get_arg(0))) ||
-          m.is_true(n) || m.is_false(n))
-        return true;
+    bool is_literal(ast_manager& m, expr* n) {
+        return spacer::is_atom(m, n) || (m.is_not(n) && spacer::is_atom(m, to_app(n)->get_arg(0)));
+    }
 
-      // x=y is atomic if x and y are Bool and atomic
-      expr *e1, *e2;
-      if (m.is_eq(n, e1, e2) && spacer::is_atom(m, e1) && spacer::is_atom(m, e2))
-        return true;
-      return false;
+    bool is_atom(ast_manager& m, expr* n) {
+        if (is_quantifier(n) || !m.is_bool(n))
+            return false;
+        if (is_var(n))
+            return true;
+        SASSERT(is_app(n));
+        if (to_app(n)->get_family_id() != m.get_basic_family_id()) {
+            return true;
+        }
+
+        if ((m.is_eq(n) && !m.is_bool(to_app(n)->get_arg(0))) ||
+            m.is_true(n) || m.is_false(n))
+            return true;
+
+        // x=y is atomic if x and y are Bool and atomic
+        expr* e1, * e2;
+        if (m.is_eq(n, e1, e2) && spacer::is_atom(m, e1) && spacer::is_atom(m, e2))
+            return true;
+        return false;
     }
 
     void subst_vars(ast_manager& m,
-                    app_ref_vector const& vars, model& mdl, expr_ref& fml) {
+        app_ref_vector const& vars, model& mdl, expr_ref& fml) {
         model::scoped_model_completion _sc_(mdl, true);
         expr_safe_replace sub(m);
-        for (app * v : vars) sub.insert (v, mdl(v));
+        for (app* v : vars) sub.insert(v, mdl(v));
         sub(fml);
     }
 
-    void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars) {
-        ast_manager &m = vars.m();
+    void to_mbp_benchmark(std::ostream& out, expr* fml, const app_ref_vector& vars) {
+        ast_manager& m = vars.m();
         ast_pp_util pp(m);
         pp.collect(fml);
         pp.display_decls(out);
@@ -128,20 +129,20 @@ namespace spacer {
             << "(assert mbp_benchmark_fml)\n"
             << "(check-sat)\n"
             << "(mbp mbp_benchmark_fml (";
-        for (auto v : vars) {out << mk_pp(v, m) << " ";}
+        for (auto v : vars) { out << mk_pp(v, m) << " "; }
         out << "))\n"
             << "(pop 1)\n"
             << "(exit)\n";
     }
 
-    void qe_project_z3 (ast_manager& m, app_ref_vector& vars, expr_ref& fml,
-                        model & mdl, bool reduce_all_selects, bool use_native_mbp,
-                        bool dont_sub) {
+    void qe_project_z3(ast_manager& m, app_ref_vector& vars, expr_ref& fml,
+        model& mdl, bool reduce_all_selects, bool use_native_mbp,
+        bool dont_sub) {
         params_ref p;
         p.set_bool("reduce_all_selects", reduce_all_selects);
         p.set_bool("dont_sub", dont_sub);
 
-        qe::mbp mbp(m, p);
+        qe::mbproj mbp(m, p);
         mbp.spacer(vars, mdl, fml);
     }
 
@@ -149,19 +150,19 @@ namespace spacer {
      * eliminate simple equalities using qe_lite
      * then, MBP for Booleans (substitute), reals (based on LW), ints (based on Cooper), and arrays
      */
-    void qe_project_spacer (ast_manager& m, app_ref_vector& vars, expr_ref& fml,
-                            model& mdl, bool reduce_all_selects, bool use_native_mbp,
-                            bool dont_sub) {
-        th_rewriter rw (m);
-        TRACE ("spacer_mbp",
-               tout << "Before projection:\n";
-               tout << fml << "\n";
-               tout << "Vars:\n" << vars;);
+    void qe_project_spacer(ast_manager& m, app_ref_vector& vars, expr_ref& fml,
+        model& mdl, bool reduce_all_selects, bool use_native_mbp,
+        bool dont_sub) {
+        th_rewriter rw(m);
+        TRACE("spacer_mbp",
+            tout << "Before projection:\n";
+        tout << fml << "\n";
+        tout << "Vars:\n" << vars;);
 
         {
             // Ensure that top-level AND of fml is flat
             expr_ref_vector flat(m);
-            flatten_and (fml, flat);
+            flatten_and(fml, flat);
             fml = mk_and(flat);
         }
 
@@ -169,38 +170,40 @@ namespace spacer {
         // uncomment for benchmarks
         //to_mbp_benchmark(verbose_stream(), fml, vars);
 
-        app_ref_vector arith_vars (m);
-        app_ref_vector array_vars (m);
-        array_util arr_u (m);
-        arith_util ari_u (m);
-        expr_safe_replace bool_sub (m);
-        expr_ref bval (m);
+        app_ref_vector arith_vars(m);
+        app_ref_vector array_vars(m);
+        array_util arr_u(m);
+        arith_util ari_u(m);
+        expr_safe_replace bool_sub(m);
+        expr_ref bval(m);
 
         while (true) {
             params_ref p;
             qe_lite qe(m, p, false);
-            qe (vars, fml);
-            rw (fml);
+            qe(vars, fml);
+            rw(fml);
 
-            TRACE ("spacer_mbp",
-                   tout << "After qe_lite:\n";
-                   tout << mk_pp (fml, m) << "\n";
-                   tout << "Vars:\n" << vars;);
+            TRACE("spacer_mbp",
+                tout << "After qe_lite:\n";
+            tout << mk_pp(fml, m) << "\n";
+            tout << "Vars:\n" << vars;);
 
-            SASSERT (!m.is_false (fml));
+            SASSERT(!m.is_false(fml));
 
 
             // sort out vars into bools, arith (int/real), and arrays
             for (app* v : vars) {
-                if (m.is_bool (v)) {
+                if (m.is_bool(v)) {
                     // obtain the interpretation of the ith var
                     // using model completion
                     model::scoped_model_completion _sc_(mdl, true);
-                    bool_sub.insert (v, mdl(v));
-                } else if (arr_u.is_array(v)) {
+                    bool_sub.insert(v, mdl(v));
+                }
+                else if (arr_u.is_array(v)) {
                     array_vars.push_back(v);
-                } else {
-                    SASSERT (ari_u.is_int(v) || ari_u.is_real(v));
+                }
+                else {
+                    SASSERT(ari_u.is_int(v) || ari_u.is_real(v));
                     arith_vars.push_back(v);
                 }
             }
@@ -209,117 +212,119 @@ namespace spacer {
             if (!bool_sub.empty()) {
                 bool_sub(fml);
                 // -- bool_sub is not simplifying
-                rw (fml);
-                SASSERT(!m.is_false (fml));
+                rw(fml);
+                SASSERT(!m.is_false(fml));
                 TRACE("spacer_mbp", tout << "Projected Booleans:\n" << fml << "\n"; );
                 bool_sub.reset();
             }
 
-            TRACE ("spacer_mbp", tout << "Array vars:\n"; tout << array_vars;);
+            TRACE("spacer_mbp", tout << "Array vars:\n"; tout << array_vars;);
 
-            vars.reset ();
+            vars.reset();
 
             // project arrays
             {
-                scoped_no_proof _sp (m);
+                scoped_no_proof _sp(m);
                 // -- local rewriter that is aware of current proof mode
                 th_rewriter srw(m);
-                spacer_qe::array_project (mdl, array_vars, fml, vars, reduce_all_selects);
-                SASSERT (array_vars.empty ());
-                srw (fml);
-                SASSERT (!m.is_false (fml));
+                spacer_qe::array_project(mdl, array_vars, fml, vars, reduce_all_selects);
+                SASSERT(array_vars.empty());
+                srw(fml);
+                SASSERT(!m.is_false(fml));
             }
 
-            TRACE ("spacer_mbp",
-                   tout << "extended model:\n";
-                   model_pp (tout, mdl);
-                   tout << "Auxiliary variables of index and value sorts:\n";
-                   tout << vars;);
+            TRACE("spacer_mbp",
+                tout << "extended model:\n";
+            model_pp(tout, mdl);
+            tout << "Auxiliary variables of index and value sorts:\n";
+            tout << vars;);
 
             if (vars.empty()) { break; }
         }
 
         // project reals and ints
-        if (!arith_vars.empty ()) {
-            TRACE ("spacer_mbp", tout << "Arith vars:\n" << arith_vars;);
+        if (!arith_vars.empty()) {
+            TRACE("spacer_mbp", tout << "Arith vars:\n" << arith_vars;);
 
-        if (use_native_mbp) {
-              qe::mbp mbp (m);
-              expr_ref_vector fmls(m);
-              flatten_and (fml, fmls);
+            if (use_native_mbp) {
+                qe::mbproj mbp(m);
+                expr_ref_vector fmls(m);
+                flatten_and(fml, fmls);
 
-              mbp (true, arith_vars, mdl, fmls);
-              fml = mk_and(fmls);
-              SASSERT(arith_vars.empty ());
-        } else {
-                scoped_no_proof _sp (m);
-                spacer_qe::arith_project (mdl, arith_vars, fml);
+                mbp(true, arith_vars, mdl, fmls);
+                fml = mk_and(fmls);
+                SASSERT(arith_vars.empty());
+            }
+            else {
+                scoped_no_proof _sp(m);
+                spacer_qe::arith_project(mdl, arith_vars, fml);
+            }
+
+            TRACE("spacer_mbp",
+                tout << "Projected arith vars:\n" << fml << "\n";
+            tout << "Remaining arith vars:\n" << arith_vars << "\n";);
+            SASSERT(!m.is_false(fml));
         }
 
-            TRACE ("spacer_mbp",
-                   tout << "Projected arith vars:\n" << fml << "\n";
-                   tout << "Remaining arith vars:\n" << arith_vars << "\n";);
-            SASSERT (!m.is_false (fml));
-        }
-
-        if (!arith_vars.empty ()) {
-            mbqi_project (mdl, arith_vars, fml);
+        if (!arith_vars.empty()) {
+            mbqi_project(mdl, arith_vars, fml);
         }
 
         // substitute any remaining arith vars
-        if (!dont_sub && !arith_vars.empty ()) {
-            subst_vars (m, arith_vars, mdl, fml);
-            TRACE ("spacer_mbp",
-                    tout << "After substituting remaining arith vars:\n";
-                    tout << mk_pp (fml, m) << "\n";
-                  );
+        if (!dont_sub && !arith_vars.empty()) {
+            subst_vars(m, arith_vars, mdl, fml);
+            TRACE("spacer_mbp",
+                tout << "After substituting remaining arith vars:\n";
+            tout << mk_pp(fml, m) << "\n";
+            );
             // an extra round of simplification because subst_vars is not simplifying
             rw(fml);
         }
 
-        DEBUG_CODE (
+        DEBUG_CODE(
             model_evaluator mev(mdl);
             mev.set_model_completion(false);
             SASSERT(mev.is_true(fml));
         );
 
-        vars.reset ();
-        if (dont_sub && !arith_vars.empty ()) {
+        vars.reset();
+        if (dont_sub && !arith_vars.empty()) {
             vars.append(arith_vars);
         }
     }
 
 
-    static expr* apply_accessor(ast_manager &m,
-                                ptr_vector<func_decl> const& acc,
-                                unsigned j,
-                                func_decl* f,
-                                expr* c)
-    {
+    static expr* apply_accessor(ast_manager& m,
+        ptr_vector<func_decl> const& acc,
+        unsigned j,
+        func_decl* f,
+        expr* c) {
         if (is_app(c) && to_app(c)->get_decl() == f) {
             return to_app(c)->get_arg(j);
-        } else {
+        }
+        else {
             return m.mk_app(acc[j], c);
         }
     }
 
-    void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml,
-                     model &mdl, bool reduce_all_selects, bool use_native_mbp,
-                     bool dont_sub) {
+    void qe_project(ast_manager& m, app_ref_vector& vars, expr_ref& fml,
+        model& mdl, bool reduce_all_selects, bool use_native_mbp,
+        bool dont_sub) {
         if (use_native_mbp)
             qe_project_z3(m, vars, fml, mdl,
-                          reduce_all_selects, use_native_mbp, dont_sub);
+                reduce_all_selects, use_native_mbp, dont_sub);
         else
             qe_project_spacer(m, vars, fml, mdl,
-                              reduce_all_selects, use_native_mbp, dont_sub);
+                reduce_all_selects, use_native_mbp, dont_sub);
     }
 
-    void expand_literals(ast_manager &m, expr_ref_vector& conjs) {
-        if (conjs.empty()) { return; }
+    void expand_literals(ast_manager& m, expr_ref_vector& conjs) {
+        if (conjs.empty()) 
+            return; 
         arith_util arith(m);
         datatype_util dt(m);
         bv_util       bv(m);
-        expr* e1, *e2, *c, *val;
+        expr* e1, * e2, * c, * val;
         rational r;
         unsigned bv_size;
 
@@ -328,16 +333,18 @@ namespace spacer {
         for (unsigned i = 0; i < conjs.size(); ++i) {
             expr* e = conjs[i].get();
             if (m.is_eq(e, e1, e2) && arith.is_int_real(e1)) {
-                conjs[i] = arith.mk_le(e1,e2);
-                if (i+1 == conjs.size()) {
+                conjs[i] = arith.mk_le(e1, e2);
+                if (i + 1 == conjs.size()) {
                     conjs.push_back(arith.mk_ge(e1, e2));
-                } else {
-                    conjs.push_back(conjs[i+1].get());
-                    conjs[i+1] = arith.mk_ge(e1, e2);
+                }
+                else {
+                    conjs.push_back(conjs[i + 1].get());
+                    conjs[i + 1] = arith.mk_ge(e1, e2);
                 }
                 ++i;
-            } else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) ||
-                       (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))) {
+            }
+            else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) ||
+                (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))) {
                 func_decl* f = to_app(val)->get_decl();
                 func_decl* r = dt.get_constructor_is(f);
                 conjs[i] = m.mk_app(r, c);
@@ -345,8 +352,9 @@ namespace spacer {
                 for (unsigned j = 0; j < acc.size(); ++j) {
                     conjs.push_back(m.mk_eq(apply_accessor(m, acc, j, f, c), to_app(val)->get_arg(j)));
                 }
-            } else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) ||
-                       (m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) {
+            }
+            else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) ||
+                (m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) {
                 rational two(2);
                 for (unsigned j = 0; j < bv_size; ++j) {
                     parameter p(j);
@@ -357,7 +365,8 @@ namespace spacer {
                     r = div(r, two);
                     if (j == 0) {
                         conjs[i] = e;
-                    } else {
+                    }
+                    else {
                         conjs.push_back(e);
                     }
                 }
@@ -366,219 +375,219 @@ namespace spacer {
         TRACE("spacer_expand", tout << "end expand\n" << conjs << "\n";);
     }
 
-namespace {
-    class implicant_picker {
-        model &m_model;
-        ast_manager &m;
-        arith_util m_arith;
+    namespace {
+        class implicant_picker {
+            model& m_model;
+            ast_manager& m;
+            arith_util m_arith;
 
-        expr_ref_vector m_todo;
-        expr_mark m_visited;
+            expr_ref_vector m_todo;
+            expr_mark m_visited;
 
-        // add literal to the implicant
-        // applies lightweight normalization
-        void add_literal(expr *e, expr_ref_vector &out) {
-            SASSERT(m.is_bool(e));
+            // add literal to the implicant
+            // applies lightweight normalization
+            void add_literal(expr* e, expr_ref_vector& out) {
+                SASSERT(m.is_bool(e));
 
-            expr_ref res(m), v(m);
-            v = m_model(e);
-            // the literal must have a value
-            SASSERT(m.limit().is_canceled() || m.is_true(v) || m.is_false(v));
+                expr_ref res(m), v(m);
+                v = m_model(e);
+                // the literal must have a value
+                SASSERT(m.limit().is_canceled() || m.is_true(v) || m.is_false(v));
 
-            res = m.is_false(v) ? m.mk_not(e) : e;
+                res = m.is_false(v) ? m.mk_not(e) : e;
 
-            if (m.is_distinct(res)) {
-                // --(distinct a b) == (not (= a b))
-                if (to_app(res)->get_num_args() == 2) {
-                    res = m.mk_eq(to_app(res)->get_arg(0),
-                                  to_app(res)->get_arg(1));
-                    res = m.mk_not(res);
+                if (m.is_distinct(res)) {
+                    // --(distinct a b) == (not (= a b))
+                    if (to_app(res)->get_num_args() == 2) {
+                        res = m.mk_eq(to_app(res)->get_arg(0),
+                            to_app(res)->get_arg(1));
+                        res = m.mk_not(res);
+                    }
                 }
-            }
 
-            expr *nres = nullptr, *f1 = nullptr, *f2 = nullptr;
-            if (m.is_not(res, nres)) {
-                // --(not (xor a b)) == (= a b)
-                if (m.is_xor(nres, f1, f2))
-                    res = m.mk_eq(f1, f2);
-                // -- split arithmetic inequality
-                else if (m.is_eq(nres, f1, f2) && m_arith.is_int_real(f1)) {
-                    res = m_arith.mk_lt(f1, f2);
-                    if (!m_model.is_true(res))
-                        res = m_arith.mk_lt(f2, f1);
+                expr* nres = nullptr, * f1 = nullptr, * f2 = nullptr;
+                if (m.is_not(res, nres)) {
+                    // --(not (xor a b)) == (= a b)
+                    if (m.is_xor(nres, f1, f2))
+                        res = m.mk_eq(f1, f2);
+                    // -- split arithmetic inequality
+                    else if (m.is_eq(nres, f1, f2) && m_arith.is_int_real(f1)) {
+                        res = m_arith.mk_lt(f1, f2);
+                        if (!m_model.is_true(res))
+                            res = m_arith.mk_lt(f2, f1);
+                    }
                 }
-            }
 
-            
-            if (!m_model.is_true(res)) {
-                IF_VERBOSE(2, verbose_stream() 
-                           << "(spacer-model-anomaly: " << res << ")\n");
-            }
-            out.push_back(res);
-        }
 
-        void process_app(app *a, expr_ref_vector &out)  {
-            if (m_visited.is_marked(a)) return;
-            SASSERT(m.is_bool(a));
-            expr_ref v(m);
-            v = m_model(a);
-            bool is_true = m.is_true(v);
-
-            if (!is_true && !m.is_false(v)) return;
-
-            expr* na = nullptr, * f1 = nullptr, * f2 = nullptr, * f3 = nullptr;
-
-            SASSERT(!m.is_false(a));
-            if (m.is_true(a)) {
-                // noop
-            }
-            else if (a->get_family_id() != m.get_basic_family_id()) {
-                add_literal(a, out);
-            }
-            else if (is_uninterp_const(a)) {
-                add_literal(a, out);
-            }
-            else if (m.is_not(a, na)) {
-                m_todo.push_back(na);
-            }
-            else if (m.is_distinct(a)) {
-                if (!is_true) {
-                    expr_ref tmp = qe::project_plugin::pick_equality(m, m_model, a);
-                    m_todo.push_back(tmp);
+                if (!m_model.is_true(res)) {
+                    IF_VERBOSE(2, verbose_stream()
+                        << "(spacer-model-anomaly: " << res << ")\n");
                 }
-                else if (a->get_num_args() == 2) {
+                out.push_back(res);
+            }
+
+            void process_app(app* a, expr_ref_vector& out) {
+                if (m_visited.is_marked(a)) return;
+                SASSERT(m.is_bool(a));
+                expr_ref v(m);
+                v = m_model(a);
+                bool is_true = m.is_true(v);
+
+                if (!is_true && !m.is_false(v)) return;
+
+                expr* na = nullptr, * f1 = nullptr, * f2 = nullptr, * f3 = nullptr;
+
+                SASSERT(!m.is_false(a));
+                if (m.is_true(a)) {
+                    // noop
+                }
+                else if (a->get_family_id() != m.get_basic_family_id()) {
                     add_literal(a, out);
                 }
-                else {
-                    m_todo.push_back(m.mk_distinct_expanded(a->get_num_args(),
-                                                            a->get_args()));
+                else if (is_uninterp_const(a)) {
+                    add_literal(a, out);
                 }
-            }
-            else if (m.is_and(a)) {
-                if (is_true) {
-                    m_todo.append(a->get_num_args(), a->get_args());
+                else if (m.is_not(a, na)) {
+                    m_todo.push_back(na);
                 }
-                else {
-                    for (expr* e : *a) {
-                        if (m_model.is_false(e)) {
-                            m_todo.push_back(e);
-                            break;
-                        }
+                else if (m.is_distinct(a)) {
+                    if (!is_true) {
+                        expr_ref tmp = mbp::project_plugin::pick_equality(m, m_model, a);
+                        m_todo.push_back(tmp);
                     }
-                }
-            }
-            else if (m.is_or(a)) {
-                if (!is_true)
-                    m_todo.append(a->get_num_args(), a->get_args());
-                else {
-                    for (expr * e : *a) {
-                        if (m_model.is_true(e)) {
-                            m_todo.push_back(e);
-                            break;
-                        }
-                    }
-                }
-            }
-            else if (m.is_eq(a, f1, f2) ||
-                     (is_true && m.is_not(a, na) && m.is_xor(na, f1, f2))) {
-                if (!m.are_equal(f1, f2) && !m.are_distinct(f1, f2)) {
-                    if (m.is_bool(f1) &&
-                        (!is_uninterp_const(f1) || !is_uninterp_const(f2)))
-                        m_todo.append(a->get_num_args(), a->get_args());
-                    else
+                    else if (a->get_num_args() == 2) {
                         add_literal(a, out);
+                    }
+                    else {
+                        m_todo.push_back(m.mk_distinct_expanded(a->get_num_args(),
+                            a->get_args()));
+                    }
                 }
-            }
-            else if (m.is_ite(a, f1, f2, f3)) {
-                if (m.are_equal(f2, f3)) {
-                    m_todo.push_back(f2);
+                else if (m.is_and(a)) {
+                    if (is_true) {
+                        m_todo.append(a->get_num_args(), a->get_args());
+                    }
+                    else {
+                        for (expr* e : *a) {
+                            if (m_model.is_false(e)) {
+                                m_todo.push_back(e);
+                                break;
+                            }
+                        }
+                    }
                 }
-                else if (m_model.is_true(f2) && m_model.is_true(f3)) {
-                    m_todo.push_back(f2);
-                    m_todo.push_back(f3);
+                else if (m.is_or(a)) {
+                    if (!is_true)
+                        m_todo.append(a->get_num_args(), a->get_args());
+                    else {
+                        for (expr* e : *a) {
+                            if (m_model.is_true(e)) {
+                                m_todo.push_back(e);
+                                break;
+                            }
+                        }
+                    }
                 }
-                else if (m_model.is_false(f2) && m_model.is_false(f3)) {
-                    m_todo.push_back(f2);
-                    m_todo.push_back(f3);
+                else if (m.is_eq(a, f1, f2) ||
+                    (is_true && m.is_not(a, na) && m.is_xor(na, f1, f2))) {
+                    if (!m.are_equal(f1, f2) && !m.are_distinct(f1, f2)) {
+                        if (m.is_bool(f1) &&
+                            (!is_uninterp_const(f1) || !is_uninterp_const(f2)))
+                            m_todo.append(a->get_num_args(), a->get_args());
+                        else
+                            add_literal(a, out);
+                    }
                 }
-                else if (m_model.is_true(f1)) {
-                    m_todo.push_back(f1);
-                    m_todo.push_back(f2);
-                }
-                else if (m_model.is_false(f1)) {
-                    m_todo.push_back(f1);
-                    m_todo.push_back(f3);
-                }
-            }
-            else if (m.is_xor(a, f1, f2)) {
-                m_todo.append(a->get_num_args(), a->get_args());
-            }
-            else if (m.is_implies(a, f1, f2)) {
-                if (is_true) {
-                    if (m_model.is_true(f2))
+                else if (m.is_ite(a, f1, f2, f3)) {
+                    if (m.are_equal(f2, f3)) {
                         m_todo.push_back(f2);
-                    else if (m_model.is_false(f1))
+                    }
+                    else if (m_model.is_true(f2) && m_model.is_true(f3)) {
+                        m_todo.push_back(f2);
+                        m_todo.push_back(f3);
+                    }
+                    else if (m_model.is_false(f2) && m_model.is_false(f3)) {
+                        m_todo.push_back(f2);
+                        m_todo.push_back(f3);
+                    }
+                    else if (m_model.is_true(f1)) {
                         m_todo.push_back(f1);
+                        m_todo.push_back(f2);
+                    }
+                    else if (m_model.is_false(f1)) {
+                        m_todo.push_back(f1);
+                        m_todo.push_back(f3);
+                    }
                 }
-                else
+                else if (m.is_xor(a, f1, f2)) {
                     m_todo.append(a->get_num_args(), a->get_args());
-            }
-            else {
-                IF_VERBOSE(0,
-                           verbose_stream() << "Unexpected expression: "
-                           << mk_pp(a, m) << "\n");
-                UNREACHABLE();
-            }
-        }
-
-        void pick_literals(expr *e, expr_ref_vector &out)  {
-            SASSERT(m_todo.empty());
-            if (m_visited.is_marked(e) || !is_app(e)) return;
-
-            // -- keep track of all created expressions to
-            // -- make sure that expression ids are stable
-            expr_ref_vector pinned(m);
-
-            m_todo.reset();
-            m_todo.push_back(e);
-            while(!m_todo.empty()) {
-                pinned.push_back(m_todo.back());
-                m_todo.pop_back();
-                if (!is_app(pinned.back())) continue;
-                app* a = to_app(pinned.back());
-                process_app(a, out);
-                m_visited.mark(a, true);
-            }
-            m_todo.reset();
-        }
-
-        bool pick_implicant(const expr_ref_vector &in, expr_ref_vector &out) {
-            m_visited.reset();
-            bool is_true = m_model.is_true(in);
-
-            for (expr* e : in) {
-                if (is_true || m_model.is_true(e)) {
-                    pick_literals(e, out);
+                }
+                else if (m.is_implies(a, f1, f2)) {
+                    if (is_true) {
+                        if (m_model.is_true(f2))
+                            m_todo.push_back(f2);
+                        else if (m_model.is_false(f1))
+                            m_todo.push_back(f1);
+                    }
+                    else
+                        m_todo.append(a->get_num_args(), a->get_args());
+                }
+                else {
+                    IF_VERBOSE(0,
+                        verbose_stream() << "Unexpected expression: "
+                        << mk_pp(a, m) << "\n");
+                    UNREACHABLE();
                 }
             }
-            m_visited.reset();
-            return is_true;
-        }
 
-    public:
+            void pick_literals(expr* e, expr_ref_vector& out) {
+                SASSERT(m_todo.empty());
+                if (m_visited.is_marked(e) || !is_app(e)) return;
 
-        implicant_picker(model &mdl) :
-            m_model(mdl), m(m_model.get_manager()), m_arith(m), m_todo(m) {}
+                // -- keep track of all created expressions to
+                // -- make sure that expression ids are stable
+                expr_ref_vector pinned(m);
 
-        void operator()(expr_ref_vector &in, expr_ref_vector& out) {
-            model::scoped_model_completion _sc_(m_model, false);
-            pick_implicant(in, out);
-        }
-    };
-}
+                m_todo.reset();
+                m_todo.push_back(e);
+                while (!m_todo.empty()) {
+                    pinned.push_back(m_todo.back());
+                    m_todo.pop_back();
+                    if (!is_app(pinned.back())) continue;
+                    app* a = to_app(pinned.back());
+                    process_app(a, out);
+                    m_visited.mark(a, true);
+                }
+                m_todo.reset();
+            }
 
-    expr_ref_vector compute_implicant_literals(model &mdl,
-                                     expr_ref_vector &formula) {
+            bool pick_implicant(const expr_ref_vector& in, expr_ref_vector& out) {
+                m_visited.reset();
+                bool is_true = m_model.is_true(in);
+
+                for (expr* e : in) {
+                    if (is_true || m_model.is_true(e)) {
+                        pick_literals(e, out);
+                    }
+                }
+                m_visited.reset();
+                return is_true;
+            }
+
+        public:
+
+            implicant_picker(model& mdl) :
+                m_model(mdl), m(m_model.get_manager()), m_arith(m), m_todo(m) {}
+
+            void operator()(expr_ref_vector& in, expr_ref_vector& out) {
+                model::scoped_model_completion _sc_(m_model, false);
+                pick_implicant(in, out);
+            }
+        };
+    }
+
+    expr_ref_vector compute_implicant_literals(model& mdl,
+        expr_ref_vector& formula) {
         // flatten the formula and remove all trivial literals
 
         // TBD: not clear why there is a dependence on it(other than
@@ -602,7 +611,7 @@ namespace {
 
         goal_ref_buffer result;
         tactic_ref simplifier = mk_arith_bounds_tactic(m);
-       (*simplifier)(g, result);
+        (*simplifier)(g, result);
         SASSERT(result.size() == 1);
         goal* r = result[0];
         cube.reset();
@@ -611,8 +620,8 @@ namespace {
         }
     }
 
-    void simplify_bounds_new(expr_ref_vector &cube) {
-        ast_manager &m = cube.m();
+    void simplify_bounds_new(expr_ref_vector& cube) {
+        ast_manager& m = cube.m();
         scoped_no_proof _no_pf_(m);
         goal_ref g(alloc(goal, m, false, false, false));
         for (expr* c : cube)
@@ -623,7 +632,7 @@ namespace {
         tactic_ref prop_bounds = mk_propagate_ineqs_tactic(m);
         tactic_ref t = and_then(prop_values.get(), prop_bounds.get());
 
-       (*t)(g, goals);
+        (*t)(g, goals);
         SASSERT(goals.size() == 1);
 
         g = goals[0];
@@ -633,23 +642,23 @@ namespace {
         }
     }
 
-    void simplify_bounds(expr_ref_vector &cube) {
+    void simplify_bounds(expr_ref_vector& cube) {
         simplify_bounds_new(cube);
     }
 
     /// Adhoc rewriting of arithmetic expressions
     struct adhoc_rewriter_cfg : public default_rewriter_cfg {
-        ast_manager &m;
+        ast_manager& m;
         arith_util m_util;
 
-        adhoc_rewriter_cfg(ast_manager &manager) : m(manager), m_util(m) {}
+        adhoc_rewriter_cfg(ast_manager& manager) : m(manager), m_util(m) {}
 
-        bool is_le(func_decl const * n) const { return m_util.is_le(n); }
-        bool is_ge(func_decl const * n) const { return m_util.is_ge(n); }
+        bool is_le(func_decl const* n) const { return m_util.is_le(n); }
+        bool is_ge(func_decl const* n) const { return m_util.is_ge(n); }
 
-        br_status reduce_app(func_decl * f, unsigned num, expr * const * args,
-                              expr_ref & result, proof_ref & result_pr) {
-            expr * e;
+        br_status reduce_app(func_decl* f, unsigned num, expr* const* args,
+            expr_ref& result, proof_ref& result_pr) {
+            expr* e;
             if (is_le(f))
                 return mk_le_core(args[0], args[1], result);
             if (is_ge(f))
@@ -661,7 +670,7 @@ namespace {
             return BR_FAILED;
         }
 
-        br_status mk_le_core(expr *arg1, expr * arg2, expr_ref & result) {
+        br_status mk_le_core(expr* arg1, expr* arg2, expr_ref& result) {
             // t <= -1  ==> t < 0 ==> !(t >= 0)
             if (m_util.is_int(arg1) && m_util.is_minus_one(arg2)) {
                 result = m.mk_not(m_util.mk_ge(arg1, mk_zero()));
@@ -669,7 +678,7 @@ namespace {
             }
             return BR_FAILED;
         }
-        br_status mk_ge_core(expr * arg1, expr * arg2, expr_ref & result) {
+        br_status mk_ge_core(expr* arg1, expr* arg2, expr_ref& result) {
             // t >= 1 ==> t > 0 ==> !(t <= 0)
             if (m_util.is_int(arg1) && is_one(arg2)) {
 
@@ -678,15 +687,15 @@ namespace {
             }
             return BR_FAILED;
         }
-        expr * mk_zero() {return m_util.mk_numeral(rational(0), true);}
-        bool is_one(expr const * n) const {
+        expr* mk_zero() { return m_util.mk_numeral(rational(0), true); }
+        bool is_one(expr const* n) const {
             rational val; return m_util.is_numeral(n, val) && val.is_one();
         }
     };
 
-    void normalize(expr *e, expr_ref &out,
-                    bool use_simplify_bounds,
-                    bool use_factor_eqs)
+    void normalize(expr* e, expr_ref& out,
+        bool use_simplify_bounds,
+        bool use_factor_eqs)
     {
 
         params_ref params;
@@ -717,7 +726,7 @@ namespace {
                 }
                 if (use_factor_eqs) {
                     // -- refactor equivalence classes and choose a representative
-                    qe::term_graph egraph(out.m());
+                    mbp::term_graph egraph(out.m());
                     egraph.add_lits(v);
                     v.reset();
                     egraph.to_lits(v);
@@ -726,15 +735,15 @@ namespace {
                 std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc());
 
                 TRACE("spacer_normalize",
-                      tout << "Normalized:\n"
-                      << out << "\n"
-                      << "to\n"
-                      << mk_and(v) << "\n";);
+                    tout << "Normalized:\n"
+                    << out << "\n"
+                    << "to\n"
+                    << mk_and(v) << "\n";);
                 TRACE("spacer_normalize",
-                      qe::term_graph egraph(out.m());
-                      for (expr* e : v) egraph.add_lit(to_app(e));
-                      tout << "Reduced app:\n"
-                      << mk_pp(egraph.to_expr(), out.m()) << "\n";);
+                    mbp::term_graph egraph(out.m());
+                for (expr* e : v) egraph.add_lit(to_app(e));
+                tout << "Reduced app:\n"
+                    << mk_pp(egraph.to_expr(), out.m()) << "\n";);
                 out = mk_and(v);
             }
         }
@@ -742,25 +751,25 @@ namespace {
 
     // rewrite term such that the pretty printing is easier to read
     struct adhoc_rewriter_rpp : public default_rewriter_cfg {
-        ast_manager &m;
+        ast_manager& m;
         arith_util m_arith;
 
-        adhoc_rewriter_rpp(ast_manager &manager) : m(manager), m_arith(m) {}
+        adhoc_rewriter_rpp(ast_manager& manager) : m(manager), m_arith(m) {}
 
-        bool is_le(func_decl const * n) const { return m_arith.is_le(n); }
-        bool is_ge(func_decl const * n) const { return m_arith.is_ge(n); }
-        bool is_lt(func_decl const * n) const { return m_arith.is_lt(n); }
-        bool is_gt(func_decl const * n) const { return m_arith.is_gt(n); }
-        bool is_zero(expr const * n) const {rational val; return m_arith.is_numeral(n, val) && val.is_zero();}
+        bool is_le(func_decl const* n) const { return m_arith.is_le(n); }
+        bool is_ge(func_decl const* n) const { return m_arith.is_ge(n); }
+        bool is_lt(func_decl const* n) const { return m_arith.is_lt(n); }
+        bool is_gt(func_decl const* n) const { return m_arith.is_gt(n); }
+        bool is_zero(expr const* n) const { rational val; return m_arith.is_numeral(n, val) && val.is_zero(); }
 
-        br_status reduce_app(func_decl * f, unsigned num, expr * const * args,
-                              expr_ref & result, proof_ref & result_pr)
+        br_status reduce_app(func_decl* f, unsigned num, expr* const* args,
+            expr_ref& result, proof_ref& result_pr)
         {
             br_status st = BR_FAILED;
-            expr *e1, *e2, *e3, *e4;
+            expr* e1, * e2, * e3, * e4;
 
             // rewrites(=(+ A(* -1 B)) 0) into(= A B)
-            if (m.is_eq(f) && is_zero(args [1]) &&
+            if (m.is_eq(f) && is_zero(args[1]) &&
                 m_arith.is_add(args[0], e1, e2) &&
                 m_arith.is_mul(e2, e3, e4) && m_arith.is_minus_one(e3)) {
                 result = m.mk_eq(e1, e4);
@@ -769,38 +778,47 @@ namespace {
             // simplify normalized leq, where right side is different from 0
             // rewrites(<=(+ A(* -1 B)) C) into(<= A B+C)
             else if ((is_le(f) || is_lt(f) || is_ge(f) || is_gt(f)) &&
-                     m_arith.is_add(args[0], e1, e2) &&
-                     m_arith.is_mul(e2, e3, e4) && m_arith.is_minus_one(e3)) {
+                m_arith.is_add(args[0], e1, e2) &&
+                m_arith.is_mul(e2, e3, e4) && m_arith.is_minus_one(e3)) {
                 expr_ref rhs(m);
                 rhs = is_zero(args[1]) ? e4 : m_arith.mk_add(e4, args[1]);
 
                 if (is_le(f)) {
                     result = m_arith.mk_le(e1, rhs);
                     st = BR_DONE;
-                } else if (is_lt(f)) {
+                }
+                else if (is_lt(f)) {
                     result = m_arith.mk_lt(e1, rhs);
                     st = BR_DONE;
-                } else if (is_ge(f)) {
+                }
+                else if (is_ge(f)) {
                     result = m_arith.mk_ge(e1, rhs);
                     st = BR_DONE;
-                } else if (is_gt(f)) {
+                }
+                else if (is_gt(f)) {
                     result = m_arith.mk_gt(e1, rhs);
                     st = BR_DONE;
-                } else
-                { UNREACHABLE(); }
+                }
+                else
+                {
+                    UNREACHABLE();
+                }
             }
             // simplify negation of ordering predicate
             else if (m.is_not(f)) {
                 if (m_arith.is_lt(args[0], e1, e2)) {
                     result = m_arith.mk_ge(e1, e2);
                     st = BR_DONE;
-                } else if (m_arith.is_le(args[0], e1, e2)) {
+                }
+                else if (m_arith.is_le(args[0], e1, e2)) {
                     result = m_arith.mk_gt(e1, e2);
                     st = BR_DONE;
-                } else if (m_arith.is_gt(args[0], e1, e2)) {
+                }
+                else if (m_arith.is_gt(args[0], e1, e2)) {
                     result = m_arith.mk_le(e1, e2);
                     st = BR_DONE;
-                } else if (m_arith.is_ge(args[0], e1, e2)) {
+                }
+                else if (m_arith.is_ge(args[0], e1, e2)) {
                     result = m_arith.mk_lt(e1, e2);
                     st = BR_DONE;
                 }
@@ -809,8 +827,8 @@ namespace {
         }
     };
 
-    mk_epp::mk_epp(ast *t, ast_manager &m, unsigned indent,
-                   unsigned num_vars, char const * var_prefix) :
+    mk_epp::mk_epp(ast* t, ast_manager& m, unsigned indent,
+        unsigned num_vars, char const* var_prefix) :
         mk_pp(t, m, m_epp_params, indent, num_vars, var_prefix), m_epp_expr(m) {
         m_epp_params.set_uint("min_alias_size", UINT_MAX);
         m_epp_params.set_uint("max_depth", UINT_MAX);
@@ -821,41 +839,41 @@ namespace {
         }
     }
 
-    void mk_epp::rw(expr *e, expr_ref &out) {
+    void mk_epp::rw(expr* e, expr_ref& out) {
         adhoc_rewriter_rpp cfg(out.m());
         rewriter_tpl<adhoc_rewriter_rpp> arw(out.m(), false, cfg);
         arw(e, out);
     }
 
-    void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) {
+    void ground_expr(expr* e, expr_ref& out, app_ref_vector& vars) {
         expr_free_vars fv;
-        ast_manager &m = out.m();
+        ast_manager& m = out.m();
 
         fv(e);
         if (vars.size() < fv.size()) {
             vars.resize(fv.size());
         }
         for (unsigned i = 0, sz = fv.size(); i < sz; ++i) {
-            sort *s = fv[i] ? fv[i] : m.mk_bool_sort();
+            sort* s = fv[i] ? fv[i] : m.mk_bool_sort();
             vars[i] = mk_zk_const(m, i, s);
             var_subst vs(m, false);
-            out = vs(e, vars.size(),(expr * *) vars.c_ptr());
+            out = vs(e, vars.size(), (expr**)vars.c_ptr());
         }
     }
 
     struct index_term_finder {
-        ast_manager     &m;
+        ast_manager& m;
         array_util       m_array;
         app_ref          m_var;
-        expr_ref_vector &m_res;
+        expr_ref_vector& m_res;
 
-        index_term_finder(ast_manager &mgr, app* v, expr_ref_vector &res) : m(mgr), m_array(m), m_var(v, m), m_res(res) {}
-        void operator()(var *n) {}
-        void operator()(quantifier *n) {}
-        void operator()(app *n) {
+        index_term_finder(ast_manager& mgr, app* v, expr_ref_vector& res) : m(mgr), m_array(m), m_var(v, m), m_res(res) {}
+        void operator()(var* n) {}
+        void operator()(quantifier* n) {}
+        void operator()(app* n) {
             if (m_array.is_select(n) || m.is_eq(n)) {
                 unsigned i = 0;
-                for (expr * arg : *n) {
+                for (expr* arg : *n) {
                     if ((m.is_eq(n) || i > 0) && m_var != arg) m_res.push_back(arg);
                     ++i;
                 }
@@ -863,36 +881,36 @@ namespace {
         }
     };
 
-    bool mbqi_project_var(model &mdl, app* var, expr_ref &fml) {
-        ast_manager &m = fml.get_manager();
+    bool mbqi_project_var(model& mdl, app* var, expr_ref& fml) {
+        ast_manager& m = fml.get_manager();
         model::scoped_model_completion _sc_(mdl, false);
 
         expr_ref val(m);
         val = mdl(var);
 
         TRACE("mbqi_project_verbose",
-              tout << "MBQI: var: " << mk_pp(var, m) << "\n"
-              << "fml: " << fml << "\n";);
+            tout << "MBQI: var: " << mk_pp(var, m) << "\n"
+            << "fml: " << fml << "\n";);
         expr_ref_vector terms(m);
         index_term_finder finder(m, var, terms);
         for_each_expr(finder, fml);
 
         TRACE("mbqi_project_verbose", tout << "terms:\n" << terms << "\n";);
 
-        for (expr * term : terms) {
+        for (expr* term : terms) {
             expr_ref tval(m);
             tval = mdl(term);
 
             TRACE("mbqi_project_verbose",
-                   tout << "term: " << mk_pp(term, m)
-                   << " tval: " << tval << " val: " << val << "\n";);
+                tout << "term: " << mk_pp(term, m)
+                << " tval: " << tval << " val: " << val << "\n";);
 
             // -- if the term does not contain an occurrence of var
             // -- and is in the same equivalence class in the model
             if (tval == val && !occurs(var, term)) {
                 TRACE("mbqi_project",
-                       tout << "MBQI: replacing " << mk_pp(var, m)
-                      << " with " << mk_pp(term, m) << "\n";);
+                    tout << "MBQI: replacing " << mk_pp(var, m)
+                    << " with " << mk_pp(term, m) << "\n";);
                 expr_safe_replace sub(m);
                 sub.insert(var, term);
                 sub(fml);
@@ -901,14 +919,14 @@ namespace {
         }
 
         TRACE("mbqi_project",
-               tout << "MBQI: failed to eliminate " << mk_pp(var, m)
-              << " from " << fml << "\n";);
+            tout << "MBQI: failed to eliminate " << mk_pp(var, m)
+            << " from " << fml << "\n";);
 
         return false;
     }
 
-    void mbqi_project(model &mdl, app_ref_vector &vars, expr_ref &fml) {
-        ast_manager &m = fml.get_manager();
+    void mbqi_project(model& mdl, app_ref_vector& vars, expr_ref& fml) {
+        ast_manager& m = fml.get_manager();
         expr_ref tmp(m);
         model::scoped_model_completion _sc_(mdl, false);
         // -- evaluate to initialize mev cache
@@ -925,7 +943,7 @@ namespace {
     struct found {};
     struct check_select {
         array_util a;
-        check_select(ast_manager& m): a(m) {}
+        check_select(ast_manager& m) : a(m) {}
         void operator()(expr* n) {}
         void operator()(app* n) { if (a.is_select(n)) throw found(); }
     };
@@ -936,7 +954,7 @@ namespace {
             for_each_expr(cs, fml);
             return false;
         }
-        catch(const found &) {
+        catch (const found&) {
             return true;
         }
     }
@@ -944,14 +962,14 @@ namespace {
     struct collect_indices {
         app_ref_vector& m_indices;
         array_util      a;
-        collect_indices(app_ref_vector& indices): m_indices(indices),
-                                                  a(indices.get_manager()) {}
+        collect_indices(app_ref_vector& indices) : m_indices(indices),
+            a(indices.get_manager()) {}
         void operator()(expr* n) {}
         void operator()(app* n) {
             if (a.is_select(n)) {
                 // for all but first argument
                 for (unsigned i = 1; i < n->get_num_args(); ++i) {
-                    expr *arg = n->get_arg(i);
+                    expr* arg = n->get_arg(i);
                     if (is_app(arg))
                         m_indices.push_back(to_app(arg));
                 }
@@ -959,15 +977,15 @@ namespace {
         }
     };
 
-    void get_select_indices(expr* fml, app_ref_vector &indices) {
+    void get_select_indices(expr* fml, app_ref_vector& indices) {
         collect_indices ci(indices);
         for_each_expr(ci, fml);
     }
 
     struct collect_decls {
         app_ref_vector& m_decls;
-        std::string&    prefix;
-        collect_decls(app_ref_vector& decls, std::string& p): m_decls(decls), prefix(p) {}
+        std::string& prefix;
+        collect_decls(app_ref_vector& decls, std::string& p) : m_decls(decls), prefix(p) {}
         void operator()(expr* n) {}
         void operator()(app* n) {
             if (n->get_decl()->get_name().str().find(prefix) != std::string::npos)
@@ -981,7 +999,7 @@ namespace {
     }
 
     // set the value of a boolean function to true in model
-    void set_true_in_mdl(model &model, func_decl *f) {
+    void set_true_in_mdl(model& model, func_decl* f) {
         SASSERT(f->get_arity() == 0);
         model.unregister_decl(f);
         model.register_decl(f, model.get_manager().mk_true());
diff --git a/src/qe/CMakeLists.txt b/src/qe/CMakeLists.txt
index 3c87298ed..49a9f73b4 100644
--- a/src/qe/CMakeLists.txt
+++ b/src/qe/CMakeLists.txt
@@ -2,30 +2,25 @@ z3_add_component(qe
   SOURCES
     nlarith_util.cpp
     nlqsat.cpp
-    qe_arith.cpp
     qe_arith_plugin.cpp
     qe_array_plugin.cpp
-    qe_arrays.cpp
     qe_bool_plugin.cpp
     qe_bv_plugin.cpp
     qe_cmd.cpp
     qe.cpp
     qe_datatype_plugin.cpp
-    qe_datatypes.cpp
     qe_dl_plugin.cpp
     qe_lite.cpp
-    qe_mbp.cpp
     qe_mbi.cpp
-    qe_solve_plugin.cpp
+    qe_mbp.cpp
     qe_tactic.cpp
-    qe_term_graph.cpp
     qsat.cpp
   COMPONENT_DEPENDENCIES
     nlsat_tactic
     nlsat
-    sat
     smt
     tactic
+    mbp
   TACTIC_HEADERS
     nlqsat.h
     qe_lite.h
diff --git a/src/qe/mbp/CMakeLists.txt b/src/qe/mbp/CMakeLists.txt
new file mode 100644
index 000000000..69d5dfd20
--- /dev/null
+++ b/src/qe/mbp/CMakeLists.txt
@@ -0,0 +1,12 @@
+z3_add_component(mbp
+  SOURCES
+    mbp_arith.cpp    
+    mbp_arrays.cpp
+    mbp_datatypes.cpp
+    mbp_plugin.cpp
+    mbp_solve_plugin.cpp
+    mbp_term_graph.cpp
+  COMPONENT_DEPENDENCIES
+    model   
+    simplex
+)
diff --git a/src/qe/qe_arith.cpp b/src/qe/mbp/mbp_arith.cpp
similarity index 82%
rename from src/qe/qe_arith.cpp
rename to src/qe/mbp/mbp_arith.cpp
index e0b7eaac4..42b20cfe3 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/mbp/mbp_arith.cpp
@@ -19,20 +19,19 @@ Revision History:
 
 --*/
 
-#include "qe/qe_arith.h"
-#include "qe/qe_mbp.h"
+#include "qe/mbp/mbp_arith.h"
 #include "ast/ast_util.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/ast_pp.h"
-#include "model/model_v2_pp.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/expr_functors.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "math/simplex/model_based_opt.h"
 #include "model/model_evaluator.h"
 #include "model/model_smt2_pp.h"
+#include "model/model_v2_pp.h"
 
-namespace qe {
+namespace mbp {
     
     struct arith_project_plugin::imp {
 
@@ -43,14 +42,13 @@ namespace qe {
         void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts) {
             // TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << " " << v << "\n";);
             rational w;
-            if (ts.find(x, w)) {
-                ts.insert(x, w + v);
-            }
-            else {
-                ts.insert(x, v); 
-            }
+            if (ts.find(x, w)) 
+                ts.insert(x, w + v);            
+            else 
+                ts.insert(x, v);             
         }
 
+
         //
         // extract linear inequalities from literal 'lit' into the model-based optimization manager 'mbo'.
         // It uses the current model to choose values for conditionals and it primes mbo with the current
@@ -227,37 +225,7 @@ namespace qe {
         }
 
         bool is_numeral(expr* t, rational& r) {
-            expr* t1, *t2;
-            rational r1, r2;
-            if (a.is_numeral(t, r)) {
-                // no-op
-            }
-            else if (a.is_uminus(t, t1) && is_numeral(t1, r)) {
-                r.neg();
-            }         
-            else if (a.is_mul(t)) {
-                app* ap = to_app(t);
-                r = rational(1);
-                for (expr * arg : *ap) {
-                    if (!is_numeral(arg, r1)) return false;
-                    r *= r1;
-                }
-            }
-            else if (a.is_add(t)) {
-                app* ap = to_app(t);
-                r = rational(0);
-                for (expr * arg : *ap) {
-                    if (!is_numeral(arg, r1)) return false;
-                    r += r1;
-                }
-            }
-            else if (a.is_sub(t, t1, t2) && is_numeral(t1, r1) && is_numeral(t2, r2)) {
-                r = r1 - r2;
-            }
-            else {
-                return false;
-            }
-            return true;
+            return a.is_extended_numeral(t, r);
         }
 
         struct compare_second {
@@ -280,10 +248,6 @@ namespace qe {
 
         ~imp() {}
 
-        bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
-            return false;
-        }
-
         bool operator()(model& model, app* v, app_ref_vector& vars, expr_ref_vector& lits) {
             app_ref_vector vs(m);
             vs.push_back(v);
@@ -308,9 +272,8 @@ namespace qe {
             for (expr* v : vars) {
                 has_arith |= is_arith(v);
             }
-            if (!has_arith) {
-                return vector<def>();
-            }
+            if (!has_arith) 
+                return vector<def>();            
             model_evaluator eval(model);
             TRACE("qe", tout << model;);
             eval.set_model_completion(true);
@@ -356,9 +319,8 @@ namespace qe {
                 }
             }
             if (m_check_purified) {
-                for (expr* fml : fmls) {
-                    mark_rec(fmls_mark, fml);
-                }
+                for (expr* fml : fmls) 
+                    mark_rec(fmls_mark, fml);                
                 for (auto& kv : tids) {
                     expr* e = kv.m_key;
                     if (!var_mark.is_marked(e)) {
@@ -368,36 +330,57 @@ namespace qe {
             }
 
             ptr_vector<expr> index2expr;
-            for (auto& kv : tids) {
-                index2expr.setx(kv.m_value, kv.m_key, nullptr);
-            }
+            for (auto& kv : tids) 
+                index2expr.setx(kv.m_value, kv.m_key, nullptr);            
 
             j = 0;
             unsigned_vector real_vars;
             for (app* v : vars) {
-                if (is_arith(v) && !fmls_mark.is_marked(v)) {
-                    real_vars.push_back(tids.find(v));
-                }
-                else {
-                    vars[j++] = v;
-                }
+                if (is_arith(v) && !fmls_mark.is_marked(v)) 
+                    real_vars.push_back(tids.find(v));                
+                else 
+                    vars[j++] = v;                
             }
             vars.shrink(j);
             
             TRACE("qe", tout << "remaining vars: " << vars << "\n"; 
-                  for (unsigned v : real_vars) {
-                      tout << "v" << v << " " << mk_pp(index2expr[v], m) << "\n";
-                  }
+                  for (unsigned v : real_vars) tout << "v" << v << " " << mk_pp(index2expr[v], m) << "\n";
                   mbo.display(tout););
             vector<opt::model_based_opt::def> defs = mbo.project(real_vars.size(), real_vars.c_ptr(), compute_def);
             TRACE("qe", mbo.display(tout << "mbo result\n");
-                  for (auto const& d : defs) {
-                      tout << "def: " << d << "\n";
-                  }
-                  );
+                  for (auto const& d : defs) tout << "def: " << d << "\n";);
             vector<row> rows;
             mbo.get_live_rows(rows);
+            rows2fmls(rows, index2expr, fmls);
             
+            vector<def> result;
+            if (compute_def) 
+                optdefs2mbpdef(defs, index2expr, real_vars, result);            
+            return result;
+        }        
+
+        void optdefs2mbpdef(vector<opt::model_based_opt::def> const& defs, ptr_vector<expr> const& index2expr, unsigned_vector const& real_vars, vector<def>& result) {
+            SASSERT(defs.size() == real_vars.size());
+            for (unsigned i = 0; i < defs.size(); ++i) {
+                auto const& d = defs[i];
+                expr* x = index2expr[real_vars[i]];
+                bool is_int = a.is_int(x);
+                expr_ref_vector ts(m);
+                expr_ref t(m);
+                for (var const& v : d.m_vars) 
+                    ts.push_back(var2expr(index2expr, v));                
+                if (!d.m_coeff.is_zero())
+                    ts.push_back(a.mk_numeral(d.m_coeff, is_int));
+                t = mk_add(ts);
+                if (!d.m_div.is_one() && is_int) 
+                    t = a.mk_idiv(t, a.mk_numeral(d.m_div, is_int));                
+                else if (!d.m_div.is_one() && !is_int) 
+                    t = a.mk_div(t, a.mk_numeral(d.m_div, is_int));                
+                result.push_back(def(expr_ref(x, m), t));
+            }
+        }
+
+        void rows2fmls(vector<row> const& rows, ptr_vector<expr> const& index2expr, expr_ref_vector& fmls) {
             for (row const& r : rows) {
                 expr_ref_vector ts(m);
                 expr_ref t(m), s(m), val(m);
@@ -418,8 +401,6 @@ namespace qe {
                     default: UNREACHABLE();
                     }
                     fmls.push_back(t);
-                    val = eval(t);
-                    CTRACE("qe", !m.is_true(val), tout << "Evaluated unit " << t << " to " << val << "\n";);
                     continue;
                 }
                 for (var const& v : r.m_vars) {
@@ -435,7 +416,7 @@ namespace qe {
                 case opt::t_lt: t = a.mk_lt(t, s); break;
                 case opt::t_le: t = a.mk_le(t, s); break;
                 case opt::t_eq: t = a.mk_eq(t, s); break;
-                case opt::t_mod: 
+                case opt::t_mod:
                     if (!r.m_coeff.is_zero()) {
                         t = a.mk_sub(t, s);
                     }
@@ -443,46 +424,11 @@ namespace qe {
                     break;
                 }
                 fmls.push_back(t);
-                val = eval(t);
-                CTRACE("qe", !m.is_true(val), tout << "Evaluated " << t << " to " << val << "\n";);
             }
-            vector<def> result;
-            if (compute_def) {
-                SASSERT(defs.size() == real_vars.size());
-                for (unsigned i = 0; i < defs.size(); ++i) {
-                    auto const& d = defs[i];
-                    expr* x = index2expr[real_vars[i]];
-                    bool is_int = a.is_int(x);
-                    expr_ref_vector ts(m);
-                    expr_ref t(m);
-                    for (var const& v : d.m_vars) {
-                        ts.push_back(var2expr(index2expr, v));
-                    }
-                    if (!d.m_coeff.is_zero()) 
-                        ts.push_back(a.mk_numeral(d.m_coeff, is_int));
-                    t = mk_add(ts);
-                    if (!d.m_div.is_one() && is_int) {
-                        t = a.mk_idiv(t, a.mk_numeral(d.m_div, is_int));
-                    }
-                    else if (!d.m_div.is_one() && !is_int) {
-                        t = a.mk_div(t, a.mk_numeral(d.m_div, is_int));
-                    }
-                    
-                    result.push_back(def(expr_ref(x, m), t));
-                }
-            }
-            return result;
-        }        
+        }
 
         expr_ref mk_add(expr_ref_vector const& ts) {
-            switch (ts.size()) {
-            case 0:
-                return expr_ref(a.mk_int(0), m);
-            case 1:
-                return expr_ref(ts.get(0), m);
-            default:
-                return expr_ref(a.mk_add(ts.size(), ts.c_ptr()), m);
-            }
+            return a.mk_add_simplify(ts);
         }
 
         opt::inf_eps maximize(expr_ref_vector const& fmls0, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
@@ -550,11 +496,11 @@ namespace qe {
 
         bool validate_model(model_evaluator& eval, expr_ref_vector const& fmls) {
             bool valid = true;
-            for (unsigned i = 0; i < fmls.size(); ++i) {
-                expr_ref val = eval(fmls[i]);
+            for (expr* fml : fmls) {
+                expr_ref val = eval(fml);
                 if (!m.is_true(val)) {
                     valid = false;
-                    TRACE("qe", tout << mk_pp(fmls[i], m) << " := " << val << "\n";);
+                    TRACE("qe", tout << mk_pp(fml, m) << " := " << val << "\n";);
                 }
             }
             return valid;
@@ -586,7 +532,7 @@ namespace qe {
 
     };
 
-    arith_project_plugin::arith_project_plugin(ast_manager& m) {
+    arith_project_plugin::arith_project_plugin(ast_manager& m):project_plugin(m) {
         m_imp = alloc(imp, m);
     }
 
@@ -610,10 +556,6 @@ namespace qe {
         m_imp->m_check_purified = check_purified;
     }
 
-    bool arith_project_plugin::solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
-        return m_imp->solve(model, vars, lits);
-    }
-
     family_id arith_project_plugin::get_family_id() {
         return m_imp->a.get_family_id();
     }
@@ -622,11 +564,6 @@ namespace qe {
         return m_imp->maximize(fmls, mdl, t, ge, gt);
     }
 
-    void arith_project_plugin::saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) {
-        UNREACHABLE();
-    }
-
-
     bool arith_project(model& model, app* var, expr_ref_vector& lits) {
         ast_manager& m = lits.get_manager();
         arith_project_plugin ap(m);
diff --git a/src/qe/qe_arith.h b/src/qe/mbp/mbp_arith.h
similarity index 90%
rename from src/qe/qe_arith.h
rename to src/qe/mbp/mbp_arith.h
index fdcb2296a..2a66e0abc 100644
--- a/src/qe/qe_arith.h
+++ b/src/qe/mbp/mbp_arith.h
@@ -7,11 +7,11 @@ Copyright (c) 2015 Microsoft Corporation
 
 #pragma once
 
-#include "model/model.h"
 #include "ast/arith_decl_plugin.h"
-#include "qe/qe_mbp.h"
+#include "model/model.h"
+#include "qe/mbp/mbp_plugin.h"
 
-namespace qe {
+namespace mbp {
 
     /**
        Loos-Weispfenning model-based projection for a basic conjunction.
@@ -25,12 +25,13 @@ namespace qe {
     public:
         arith_project_plugin(ast_manager& m);
         ~arith_project_plugin() override;
+        
         bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
-        bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override { return false; }
         family_id get_family_id() override;
         void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
         vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
-        void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override;
+        void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override { UNREACHABLE(); }
 
         opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt);
 
@@ -39,6 +40,7 @@ namespace qe {
          * arithmetic variables nested under foreign functions are handled properly.
          */
         void set_check_purified(bool check_purified);
+
     };
 
     bool arith_project(model& model, app* var, expr_ref_vector& lits);
diff --git a/src/qe/qe_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp
similarity index 99%
rename from src/qe/qe_arrays.cpp
rename to src/qe/mbp/mbp_arrays.cpp
index 949b4c504..772a62869 100644
--- a/src/qe/qe_arrays.cpp
+++ b/src/qe/mbp/mbp_arrays.cpp
@@ -3,7 +3,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 Module Name:
 
-    qe_arrays.cpp
+    mbp_arrays.cpp
 
 Abstract:
 
@@ -27,8 +27,8 @@ Revision History:
 #include "ast/ast_util.h"
 #include "ast/ast_pp.h"
 #include "model/model_evaluator.h"
-#include "qe/qe_arrays.h"
-#include "qe/qe_term_graph.h"
+#include "qe/mbp/mbp_arrays.h"
+#include "qe/mbp/mbp_term_graph.h"
 
 
 namespace {
@@ -154,7 +154,7 @@ namespace {
     }
 }
 
-namespace qe {
+namespace mbp {
 
 
     static bool is_eq(expr_ref_vector const& xs, expr_ref_vector const& ys) {
@@ -1571,7 +1571,7 @@ namespace qe {
     };
 
 
-    array_project_plugin::array_project_plugin(ast_manager& m) {
+    array_project_plugin::array_project_plugin(ast_manager& m):project_plugin(m) {
         m_imp = alloc(imp, m);
     }
 
diff --git a/src/qe/qe_arrays.h b/src/qe/mbp/mbp_arrays.h
similarity index 94%
rename from src/qe/qe_arrays.h
rename to src/qe/mbp/mbp_arrays.h
index 3b1e304d2..bb18cde11 100644
--- a/src/qe/qe_arrays.h
+++ b/src/qe/mbp/mbp_arrays.h
@@ -3,7 +3,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 Module Name:
 
-    qe_arrays.h
+    mbp_arrays.h
 
 Abstract:
 
@@ -21,9 +21,9 @@ Revision History:
 #pragma once
 
 #include "ast/array_decl_plugin.h"
-#include "qe/qe_mbp.h"
+#include "qe/mbp/mbp_plugin.h"
 
-namespace qe {
+namespace mbp {
 
     class array_project_plugin : public project_plugin {
         struct imp;
diff --git a/src/qe/qe_datatypes.cpp b/src/qe/mbp/mbp_datatypes.cpp
similarity index 99%
rename from src/qe/qe_datatypes.cpp
rename to src/qe/mbp/mbp_datatypes.cpp
index fb1afc4c2..7c5d43afb 100644
--- a/src/qe/qe_datatypes.cpp
+++ b/src/qe/mbp/mbp_datatypes.cpp
@@ -17,16 +17,15 @@ Revision History:
 
 --*/
 
-#include "qe/qe_arith.h"
 #include "ast/ast_pp.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/expr_functors.h"
 #include "model/model_v2_pp.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "util/obj_pair_hashtable.h"
-#include "qe/qe_datatypes.h"
+#include "qe/mbp/mbp_datatypes.h"
 
-namespace qe {
+namespace mbp {
     
     struct datatype_project_plugin::imp  {
         ast_manager&              m;
@@ -285,7 +284,8 @@ namespace qe {
         
     };
     
-    datatype_project_plugin::datatype_project_plugin(ast_manager& m) {
+    datatype_project_plugin::datatype_project_plugin(ast_manager& m):
+        project_plugin(m) {
         m_imp = alloc(imp, m);
     }
     
diff --git a/src/qe/qe_datatypes.h b/src/qe/mbp/mbp_datatypes.h
similarity index 95%
rename from src/qe/qe_datatypes.h
rename to src/qe/mbp/mbp_datatypes.h
index 5ecf042e9..345260970 100644
--- a/src/qe/qe_datatypes.h
+++ b/src/qe/mbp/mbp_datatypes.h
@@ -21,9 +21,9 @@ Revision History:
 #pragma once
 
 #include "ast/datatype_decl_plugin.h"
-#include "qe/qe_mbp.h"
+#include "qe/mbp/mbp_plugin.h"
 
-namespace qe {
+namespace mbp {
 
     class datatype_project_plugin : public project_plugin {
         struct imp;
diff --git a/src/qe/mbp/mbp_plugin.cpp b/src/qe/mbp/mbp_plugin.cpp
new file mode 100644
index 000000000..ed4ab5252
--- /dev/null
+++ b/src/qe/mbp/mbp_plugin.cpp
@@ -0,0 +1,262 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    qe_mbp.cpp
+
+Abstract:
+
+    Model-based projection utilities
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-5-29
+
+Revision History:
+
+
+--*/
+
+#include "ast/rewriter/expr_safe_replace.h"
+#include "ast/ast_pp.h"
+#include "ast/ast_util.h"
+#include "ast/occurs.h"
+#include "ast/rewriter/th_rewriter.h"
+#include "ast/expr_functors.h"
+#include "ast/for_each_expr.h"
+#include "ast/scoped_proof.h"
+#include "qe/mbp/mbp_plugin.h"
+#include "model/model_pp.h"
+#include "model/model_evaluator.h"
+
+
+namespace mbp {
+
+    struct noop_op_proc {
+        void operator()(expr*) {}
+    };
+
+    void project_plugin::mark_rec(expr_mark& visited, expr* e) {
+        for_each_expr_proc<noop_op_proc> fe;
+        for_each_expr(fe, visited, e);
+    }
+
+    void project_plugin::mark_rec(expr_mark& visited, expr_ref_vector const& es) {
+        for (expr* e : es)
+            mark_rec(visited, e);
+    }
+
+    /**
+       \brief return two terms that are equal in the model.
+       The distinct term t is false in model, so there
+       are at least two arguments of t that are equal in the model.
+    */
+    expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) {
+        SASSERT(m.is_distinct(t));
+        expr_ref val(m);
+        expr_ref_vector vals(m);
+        obj_map<expr, expr*> val2expr;
+        app* alit = to_app(t);
+        if (alit->get_num_args() == 2) {
+            return expr_ref(m.mk_eq(alit->get_arg(0), alit->get_arg(1)), m);
+        }
+        for (expr* e1 : *alit) {
+            expr* e2;
+            val = model(e1);
+            TRACE("qe", tout << mk_pp(e1, m) << " |-> " << val << "\n";);
+            if (val2expr.find(val, e2)) {
+                return expr_ref(m.mk_eq(e1, e2), m);
+            }
+            val2expr.insert(val, e1);
+            vals.push_back(val);
+        }
+        for (unsigned i = 0; i < alit->get_num_args(); ++i) {
+            for (unsigned j = i + 1; j < alit->get_num_args(); ++j) {
+                expr* e1 = alit->get_arg(i);
+                expr* e2 = alit->get_arg(j);
+                val = m.mk_eq(e1, e2);
+                if (!model.is_false(val))
+                    return expr_ref(m.mk_eq(e1, e2), m);
+            }
+        }
+        UNREACHABLE();
+        return expr_ref(nullptr, m);
+    }
+
+
+    void project_plugin::erase(expr_ref_vector& lits, unsigned& i) {
+        lits[i] = lits.back();
+        lits.pop_back();
+        --i;
+    }
+
+    void project_plugin::push_back(expr_ref_vector& lits, expr* e) {
+        if (!m.is_true(e))
+            lits.push_back(e);
+    }
+
+    void project_plugin::extract_literals(model& model, app_ref_vector const& vars, expr_ref_vector& fmls) {
+        m_bool_visited.reset();
+        expr_ref val(m);
+        model_evaluator eval(model);
+        eval.set_expand_array_equalities(true);
+        TRACE("qe", tout << fmls << "\n";);
+        for (unsigned i = 0; i < fmls.size(); ++i) {
+            expr* fml = fmls.get(i), * nfml, * f1, * f2, * f3;
+            SASSERT(m.is_bool(fml));
+            if (m.is_not(fml, nfml) && m.is_distinct(nfml))
+                fmls[i--] = mbp::project_plugin::pick_equality(m, model, nfml);
+            else if (m.is_or(fml)) {
+                for (expr* arg : *to_app(fml)) {
+                    val = eval(arg);
+                    if (m.is_true(val)) {
+                        fmls[i] = arg;
+                        --i;
+                        break;
+                    }
+                }
+            }
+            else if (m.is_and(fml)) {
+                fmls.append(to_app(fml)->get_num_args(), to_app(fml)->get_args());
+                mbp::project_plugin::erase(fmls, i);
+            }
+            else if (m.is_iff(fml, f1, f2) || (m.is_not(fml, nfml) && m.is_xor(nfml, f1, f2))) {
+                val = eval(f1);
+                if (m.is_false(val)) {
+                    f1 = mk_not(m, f1);
+                    f2 = mk_not(m, f2);
+                }
+                fmls[i--] = f1;
+                push_back(fmls, f2);
+            }
+            else if (m.is_implies(fml, f1, f2)) {
+                val = eval(f2);
+                if (m.is_true(val)) {
+                    fmls[i] = f2;
+                }
+                else {
+                    fmls[i] = mk_not(m, f1);
+                }
+                --i;
+            }
+            else if (m.is_ite(fml, f1, f2, f3)) {
+                val = eval(f1);
+                if (m.is_true(val)) {
+                    push_back(fmls, f1);
+                    push_back(fmls, f2);
+                }
+                else {
+                    push_back(fmls, mk_not(m, f1));
+                    push_back(fmls, f3);
+                }
+                mbp::project_plugin::erase(fmls, i);
+            }
+            else if (m.is_not(fml, nfml) && m.is_not(nfml, nfml)) {
+                push_back(fmls, nfml);
+                mbp::project_plugin::erase(fmls, i);
+            }
+            else if (m.is_not(fml, nfml) && m.is_and(nfml)) {
+                for (expr* arg : *to_app(nfml)) {
+                    val = eval(arg);
+                    if (m.is_false(val)) {
+                        fmls[i--] = mk_not(m, arg);
+                        break;
+                    }
+                }
+            }
+            else if (m.is_not(fml, nfml) && m.is_or(nfml)) {
+                for (expr* arg : *to_app(nfml))
+                    push_back(fmls, mk_not(m, arg));
+                mbp::project_plugin::erase(fmls, i);
+            }
+            else if ((m.is_not(fml, nfml) && m.is_iff(nfml, f1, f2)) || m.is_xor(fml, f1, f2)) {
+                val = eval(f1);
+                if (m.is_true(val)) {
+                    f2 = mk_not(m, f2);
+                }
+                else {
+                    f1 = mk_not(m, f1);
+                }
+                push_back(fmls, f1);
+                push_back(fmls, f2);
+                mbp::project_plugin::erase(fmls, i);
+            }
+            else if (m.is_not(fml, nfml) && m.is_implies(nfml, f1, f2)) {
+                push_back(fmls, f1);
+                push_back(fmls, mk_not(m, f2));
+                mbp::project_plugin::erase(fmls, i);
+            }
+            else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) {
+                val = eval(f1);
+                if (m.is_true(val)) {
+                    push_back(fmls, f1);
+                    push_back(fmls, mk_not(m, f2));
+                }
+                else {
+                    push_back(fmls, mk_not(m, f1));
+                    push_back(fmls, mk_not(m, f3));
+                }
+                mbp::project_plugin::erase(fmls, i);
+            }
+            else if (m.is_not(fml, nfml)) {
+                if (extract_bools(eval, fmls, nfml)) {
+                    mbp::project_plugin::erase(fmls, i);
+                }
+            }
+            else if (extract_bools(eval, fmls, fml))
+                mbp::project_plugin::erase(fmls, i);
+        }
+        TRACE("qe", tout << fmls << "\n";);
+    }
+
+    bool project_plugin::extract_bools(model_evaluator& eval, expr_ref_vector& fmls, expr* fml) {
+        TRACE("qe", tout << "extract bools: " << mk_pp(fml, m) << "\n";);
+        ptr_vector<expr> todo;
+        expr_safe_replace sub(m);
+        m_visited.reset();
+        bool found_bool = false;
+        if (is_app(fml)) {
+            todo.append(to_app(fml)->get_num_args(), to_app(fml)->get_args());
+        }
+        while (!todo.empty() && m.inc()) {
+            expr* e = todo.back();
+            todo.pop_back();
+            if (m_visited.is_marked(e)) {
+                continue;
+            }
+            m_visited.mark(e);
+            if (m.is_bool(e) && !m.is_true(e) && !m.is_false(e)) {
+                expr_ref val = eval(e);
+                TRACE("qe", tout << "found: " << mk_pp(e, m) << " " << val << "\n";);
+                if (!m.inc())
+                    continue;
+                if (!m.is_true(val) && !m.is_false(val) && contains_uninterpreted(val)) 
+                    throw default_exception("could not evaluate Boolean in model");
+                SASSERT(m.is_true(val) || m.is_false(val));
+
+                if (!m_bool_visited.is_marked(e)) 
+                    fmls.push_back(m.is_true(val) ? e : mk_not(m, e));
+                sub.insert(e, val);
+                m_bool_visited.mark(e);
+                found_bool = true;
+            }
+            else if (is_app(e)) {
+                todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+            }
+            else {
+                TRACE("qe", tout << "expression not handled " << mk_pp(e, m) << "\n";);
+            }
+        }
+        if (found_bool) {
+            expr_ref tmp(m);
+            sub(fml, tmp);
+            expr_ref val = eval(tmp);
+            if (!m.is_true(val) && !m.is_false(val))
+                return false;
+            fmls.push_back(m.is_true(val) ? tmp : mk_not(m, tmp));
+        }
+        return found_bool;
+    }
+
+}
diff --git a/src/qe/mbp/mbp_plugin.h b/src/qe/mbp/mbp_plugin.h
new file mode 100644
index 000000000..efb8728f0
--- /dev/null
+++ b/src/qe/mbp/mbp_plugin.h
@@ -0,0 +1,93 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    mbp_plugin.h
+
+Abstract:
+
+    Model-based projection utilities
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-5-28
+
+Revision History:
+
+
+--*/
+
+#pragma once
+
+#include "ast/ast.h"
+#include "util/params.h"
+#include "model/model.h"
+#include "math/simplex/model_based_opt.h"
+
+
+namespace mbp {
+
+    struct cant_project {};
+
+    struct def {
+        expr_ref var, term;
+        def(const expr_ref& v, expr_ref& t): var(v), term(t) {}
+    };
+
+    class project_plugin {
+        ast_manager& m;
+        expr_mark m_visited;
+        expr_mark m_bool_visited;
+
+        bool extract_bools(model_evaluator& eval, expr_ref_vector& fmls, expr* fml);
+        // over-approximation
+        bool contains_uninterpreted(expr* v) { return true; }
+
+        void push_back(expr_ref_vector& lits, expr* lit);
+    public:
+        project_plugin(ast_manager& m) :m(m) {}
+        virtual ~project_plugin() {}
+        virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { return false; }
+        /**
+           \brief partial solver.
+        */
+        virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; }
+        virtual family_id get_family_id() { return null_family_id; }
+
+        virtual void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { };
+
+        /**
+           \brief project vars modulo model, return set of definitions for eliminated variables.
+           - vars in/out: returns variables that were not eliminated
+           - lits in/out: returns projected literals
+           - returns set of definitions
+             (TBD: in triangular form, the last definition can be substituted into definitions that come before)
+        */
+        virtual vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return vector<def>(); }
+
+        /**
+           \brief model based saturation. Saturates theory axioms to equi-satisfiable literals over EUF,
+           such that 'shared' are not retained for EUF.
+         */
+        virtual void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) {}
+
+
+        /*
+        * extract top-level literals
+        */
+        void extract_literals(model& model, app_ref_vector const& vars, expr_ref_vector& fmls);
+
+        /*
+        * Purify literals into linear inequalities or constraints without arithmetic variables.
+        */
+        void purify(model& model, app_ref_vector const& vars, expr_ref_vector& fmls);
+
+        static expr_ref pick_equality(ast_manager& m, model& model, expr* t);
+        static void erase(expr_ref_vector& lits, unsigned& i);
+
+        static void mark_rec(expr_mark& visited, expr* e);
+        static void mark_rec(expr_mark& visited, expr_ref_vector const& es);
+    };
+}
+
diff --git a/src/qe/qe_solve_plugin.cpp b/src/qe/mbp/mbp_solve_plugin.cpp
similarity index 99%
rename from src/qe/qe_solve_plugin.cpp
rename to src/qe/mbp/mbp_solve_plugin.cpp
index 8b63402fa..c43fa402f 100644
--- a/src/qe/qe_solve_plugin.cpp
+++ b/src/qe/mbp/mbp_solve_plugin.cpp
@@ -23,9 +23,9 @@ Revision History:
 #include "ast/datatype_decl_plugin.h"
 #include "ast/ast_util.h"
 #include "ast/ast_pp.h"
-#include "qe/qe_solve_plugin.h"
+#include "qe/mbp/mbp_solve_plugin.h"
 
-namespace qe {
+namespace mbp {
 
     expr_ref solve_plugin::operator()(expr* lit) {
         if (m.is_not(lit, lit))
diff --git a/src/qe/qe_solve_plugin.h b/src/qe/mbp/mbp_solve_plugin.h
similarity index 94%
rename from src/qe/qe_solve_plugin.h
rename to src/qe/mbp/mbp_solve_plugin.h
index 38be6deaf..27e7f85a8 100644
--- a/src/qe/qe_solve_plugin.h
+++ b/src/qe/mbp/mbp_solve_plugin.h
@@ -3,7 +3,7 @@ Copyright (c) 2018 Microsoft Corporation
 
 Module Name:
 
-    qe_solve.h
+    mbp_solve_plugin.h
 
 Abstract:
 
@@ -21,10 +21,10 @@ Revision History:
 #pragma once
 
 #include "ast/ast.h"
+#include "ast/is_variable_test.h"
 #include "util/plugin_manager.h"
-#include "qe/qe_vartest.h"
 
-namespace qe {
+namespace mbp {
 
     class solve_plugin {
     protected:
diff --git a/src/qe/qe_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp
similarity index 99%
rename from src/qe/qe_term_graph.cpp
rename to src/qe/mbp/mbp_term_graph.cpp
index a0793025c..3916da38b 100644
--- a/src/qe/qe_term_graph.cpp
+++ b/src/qe/mbp/mbp_term_graph.cpp
@@ -24,10 +24,10 @@ Notes:
 #include "ast/ast_util.h"
 #include "ast/for_each_expr.h"
 #include "ast/occurs.h"
-#include "qe/qe_term_graph.h"
 #include "model/model_evaluator.h"
+#include "qe/mbp/mbp_term_graph.h"
 
-namespace qe {
+namespace mbp {
 
     static expr_ref mk_neq(ast_manager &m, expr *e1, expr *e2) {
         expr *t = nullptr;
@@ -245,8 +245,8 @@ namespace qe {
     bool term_graph::term_eq::operator()(term const* a, term const* b) const { return term::cg_eq(a, b); }
 
     term_graph::term_graph(ast_manager &man) : m(man), m_lits(m), m_pinned(m), m_projector(nullptr) {
-        m_plugins.register_plugin(mk_basic_solve_plugin(m, m_is_var));
-        m_plugins.register_plugin(mk_arith_solve_plugin(m, m_is_var));
+        m_plugins.register_plugin(mbp::mk_basic_solve_plugin(m, m_is_var));
+        m_plugins.register_plugin(mbp::mk_arith_solve_plugin(m, m_is_var));
     }
 
     term_graph::~term_graph() {
@@ -283,7 +283,7 @@ namespace qe {
         for (unsigned i = 0; i < lits.size(); ++i) {
             l = lits.get(i);
             family_id fid = get_family_id(m, l);
-            qe::solve_plugin *pin = m_plugins.get_plugin(fid);
+            mbp::solve_plugin *pin = m_plugins.get_plugin(fid);
             lit = pin ? (*pin)(l) : l;
             if (m.is_and(lit)) {
                 lits.append(::to_app(lit)->get_num_args(), ::to_app(lit)->get_args());
diff --git a/src/qe/qe_term_graph.h b/src/qe/mbp/mbp_term_graph.h
similarity index 96%
rename from src/qe/qe_term_graph.h
rename to src/qe/mbp/mbp_term_graph.h
index 4f443350e..37d1e7b8d 100644
--- a/src/qe/qe_term_graph.h
+++ b/src/qe/mbp/mbp_term_graph.h
@@ -3,7 +3,7 @@ Copyright (c) Arie Gurfinkel
 
 Module Name:
 
-    qe_term_graph.h
+    mbp_term_graph.h
 
 Abstract:
 
@@ -19,12 +19,12 @@ Notes:
 #pragma once
 
 #include "ast/ast.h"
+#include "ast/is_variable_test.h"
 #include "util/plugin_manager.h"
-#include "qe/qe_solve_plugin.h"
-#include "qe/qe_vartest.h"
+#include "qe/mbp/mbp_solve_plugin.h"
 #include "model/model.h"
 
-namespace qe {
+namespace mbp {
 
     class term;
 
@@ -53,7 +53,7 @@ namespace qe {
         ast_ref_vector    m_pinned;
         projector*        m_projector;
         u_map<expr*>      m_term2app;
-        plugin_manager<qe::solve_plugin> m_plugins;
+        plugin_manager<solve_plugin> m_plugins;
         ptr_hashtable<term, term_hash, term_eq> m_cg_table;
         vector<std::pair<term*,term*>> m_merge;
 
diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp
index 30b09a381..52c5647eb 100644
--- a/src/qe/qe_arith_plugin.cpp
+++ b/src/qe/qe_arith_plugin.cpp
@@ -32,7 +32,7 @@ Revision History:
 #include "qe/nlarith_util.h"
 #include "model/model_evaluator.h"
 #include "smt/smt_kernel.h"
-#include "qe/qe_arith.h"
+#include "qe/mbp/mbp_arith.h"
 
 namespace qe {
 
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index 1d158ca94..bc2b5339a 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -17,25 +17,24 @@ Revision History:
 
 
 --*/
-#include "qe/qe_lite.h"
+#include "util/uint_set.h"
 #include "ast/expr_abstract.h"
 #include "ast/used_vars.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_smt2_pp.h"
-#include "tactic/tactical.h"
+#include "ast/is_variable_test.h"
 #include "ast/rewriter/bool_rewriter.h"
 #include "ast/rewriter/var_subst.h"
-#include "util/uint_set.h"
 #include "ast/ast_util.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/for_each_expr.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/datatype_decl_plugin.h"
-
-#include "qe/qe_vartest.h"
-#include "qe/qe_solve_plugin.h"
+#include "tactic/tactical.h"
+#include "qe/mbp/mbp_solve_plugin.h"
+#include "qe/qe_lite.h"
 
 namespace qel {
 
@@ -73,7 +72,7 @@ namespace qel {
         beta_reducer    m_subst;
         expr_ref_vector m_subst_map;
         expr_ref_vector m_new_exprs;
-        plugin_manager<qe::solve_plugin> m_solvers;
+        plugin_manager<mbp::solve_plugin> m_solvers;
 
         ptr_vector<expr> m_map;
         int_vector       m_pos2var;
@@ -296,7 +295,7 @@ namespace qel {
             if (m.is_eq(e, lhs, rhs)) {
                 fid = get_sort(lhs)->get_family_id();
             }
-            qe::solve_plugin* p = m_solvers.get_plugin(fid);
+            auto* p = m_solvers.get_plugin(fid);
             if (p) {
                 expr_ref res = (*p)(e);
                 if (res != e && m.is_eq(res, lhs, rhs) && is_variable(lhs)) {
@@ -703,9 +702,9 @@ namespace qel {
         void set_is_variable_proc(is_variable_proc& proc) { 
             m_is_variable = &proc;
             m_solvers.reset();
-            m_solvers.register_plugin(qe::mk_arith_solve_plugin(m, proc));            
-            m_solvers.register_plugin(qe::mk_basic_solve_plugin(m, proc));            
-            m_solvers.register_plugin(qe::mk_bv_solve_plugin(m, proc));            
+            m_solvers.register_plugin(mbp::mk_arith_solve_plugin(m, proc));            
+            m_solvers.register_plugin(mbp::mk_basic_solve_plugin(m, proc));
+            m_solvers.register_plugin(mbp::mk_bv_solve_plugin(m, proc));
         }
 
         void operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index f7925b98b..da9211ac5 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -38,9 +38,9 @@ Notes:
 #include "model/model_evaluator.h"
 #include "solver/solver.h"
 #include "qe/qe_mbi.h"
-#include "qe/qe_term_graph.h"
-#include "qe/qe_arith.h"
-#include "qe/qe_arrays.h"
+#include "qe/mbp/mbp_term_graph.h"
+#include "qe/mbp/mbp_arith.h"
+#include "qe/mbp/mbp_arrays.h"
 
 
 namespace qe {
@@ -263,8 +263,8 @@ namespace qe {
         return avars;
     }
 
-    vector<def> uflia_mbi::arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits) {
-        arith_project_plugin ap(m);
+    vector<mbp::def> uflia_mbi::arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits) {
+        mbp::arith_project_plugin ap(m);
         ap.set_check_purified(false);
         return ap.project(*mdl.get(), avars, lits);
     }
@@ -308,7 +308,7 @@ namespace qe {
         expr_ref_vector alits(m), uflits(m);
         split_arith(lits, alits, uflits);
         auto avars = get_arith_vars(lits);
-        vector<def> defs = arith_project(mdl, avars, alits);
+        vector<mbp::def> defs = arith_project(mdl, avars, alits);
         for (auto const& d : defs) uflits.push_back(m.mk_eq(d.var, d.term));
         TRACE("qe", tout << "uflits: " << uflits << "\n";);
         project_euf(mdl, uflits);
@@ -354,7 +354,7 @@ namespace qe {
        \brief add difference certificates to formula.       
     */
     void uflia_mbi::add_dcert(model_ref& mdl, expr_ref_vector& lits) {        
-        term_graph tg(m);
+        mbp::term_graph tg(m);
         add_arith_dcert(*mdl.get(), lits);
         func_decl_ref_vector shared(m_shared_trail);
         tg.set_vars(shared, false);
@@ -406,7 +406,7 @@ namespace qe {
      * \brief project private symbols.
      */
     void uflia_mbi::project_euf(model_ref& mdl, expr_ref_vector& lits) {
-        term_graph tg(m);
+        mbp::term_graph tg(m);
         func_decl_ref_vector shared(m_shared_trail);
         tg.set_vars(shared, false);
         tg.add_lits(lits);
diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h
index 34a2c1799..d7b825fcd 100644
--- a/src/qe/qe_mbi.h
+++ b/src/qe/qe_mbi.h
@@ -20,7 +20,8 @@ Revision History:
 
 #pragma once
 
-#include "qe/qe_arith.h"
+#include "qe/mbp/mbp_arith.h"
+#include "qe/mbp/mbp_plugin.h"
 #include "util/lbool.h"
 
 namespace qe {
@@ -126,7 +127,7 @@ namespace qe {
         void add_arith_dcert(model& mdl, expr_ref_vector& lits);
         void add_arith_dcert(model& mdl, expr_ref_vector& lits, app* a, app* b);
         app_ref_vector get_arith_vars(expr_ref_vector const& lits);
-        vector<def> arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits);
+        vector<::mbp::def> arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits);
         void project_euf(model_ref& mdl, expr_ref_vector& lits);
         void split_arith(expr_ref_vector const& lits, 
                          expr_ref_vector& alits,
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index 9692783d8..1e1b60d56 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -27,9 +27,9 @@ Revision History:
 #include "ast/for_each_expr.h"
 #include "ast/scoped_proof.h"
 #include "qe/qe_mbp.h"
-#include "qe/qe_arith.h"
-#include "qe/qe_arrays.h"
-#include "qe/qe_datatypes.h"
+#include "qe/mbp/mbp_arith.h"
+#include "qe/mbp/mbp_arrays.h"
+#include "qe/mbp/mbp_datatypes.h"
 #include "qe/qe_lite.h"
 #include "model/model_pp.h"
 #include "model/model_evaluator.h"
@@ -37,93 +37,26 @@ Revision History:
 
 using namespace qe;
 
-struct noop_op_proc {
-    void operator()(expr*) {}
-};
 
-
-void project_plugin::mark_rec(expr_mark& visited, expr* e) {
-    for_each_expr_proc<noop_op_proc> fe;    
-    for_each_expr(fe, visited, e);
-}
-
-void project_plugin::mark_rec(expr_mark& visited, expr_ref_vector const& es) {
-    for (unsigned i = 0; i < es.size(); ++i) {
-        mark_rec(visited, es[i]);
-    }
-}
-
-/**
-   \brief return two terms that are equal in the model.
-   The distinct term t is false in model, so there 
-   are at least two arguments of t that are equal in the model.
-*/
-expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) {
-    SASSERT(m.is_distinct(t));
-    expr_ref val(m);
-    expr_ref_vector vals(m);
-    obj_map<expr, expr*> val2expr;
-    app* alit = to_app(t);
-    if (alit->get_num_args() == 2) {
-        return expr_ref(m.mk_eq(alit->get_arg(0), alit->get_arg(1)), m);
-    }
-    for (expr * e1 : *alit) {
-        expr *e2;
-        val = model(e1);
-        TRACE("qe", tout << mk_pp(e1, m) << " |-> " << val << "\n";);
-        if (val2expr.find(val, e2)) {
-            return expr_ref(m.mk_eq(e1, e2), m);
-        }
-        val2expr.insert(val, e1);
-        vals.push_back(val);
-    }
-    for (unsigned i = 0; i < alit->get_num_args(); ++i) {
-        for (unsigned j = i + 1; j < alit->get_num_args(); ++j) {
-            expr* e1 = alit->get_arg(i);
-            expr* e2 = alit->get_arg(j);
-            val = m.mk_eq(e1, e2);
-            if (!model.is_false(val))
-                return expr_ref(m.mk_eq(e1, e2), m);
-        }
-    }
-    UNREACHABLE();
-    return expr_ref(nullptr, m);
-}
-
-
-void project_plugin::erase(expr_ref_vector& lits, unsigned& i) {
-    lits[i] = lits.back();
-    lits.pop_back();
-    --i;
-}
-
-void project_plugin::push_back(expr_ref_vector& lits, expr* e) {
-    if (lits.get_manager().is_true(e)) return;
-    lits.push_back(e);
-}
-
-
-class mbp::impl {
+class mbproj::impl {
     ast_manager& m;
-    params_ref                 m_params;
-    th_rewriter m_rw;
-    ptr_vector<project_plugin> m_plugins;
-    expr_mark m_visited;
-    expr_mark m_bool_visited;
+    params_ref                      m_params;
+    th_rewriter                     m_rw;
+    ptr_vector<mbp::project_plugin> m_plugins;
 
     // parameters
     bool m_reduce_all_selects;
     bool m_dont_sub;
 
-    void add_plugin(project_plugin* p) {
+    void add_plugin(mbp::project_plugin* p) {
         family_id fid = p->get_family_id();
-        SASSERT(!m_plugins.get(fid, 0));
-        m_plugins.setx(fid, p, 0);
+        SASSERT(!m_plugins.get(fid, nullptr));
+        m_plugins.setx(fid, p, nullptr);
     }
 
-    project_plugin* get_plugin(app* var) {
+    mbp::project_plugin* get_plugin(app* var) {
         family_id fid = m.get_sort(var)->get_family_id();
-        return m_plugins.get(fid, 0);
+        return m_plugins.get(fid, nullptr);
     }
 
     bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
@@ -132,20 +65,20 @@ class mbp::impl {
             return false;
         }
         bool reduced = false;
-        for (unsigned i = 0; i < vars.size(); ++i) { 
-            is_var.mark(vars[i].get());
-        }
-        expr_ref tmp(m), t(m), v(m);            
+        for (expr* v : vars)
+            is_var.mark(v);
+        expr_ref tmp(m), t(m), v(m);
+
         for (unsigned i = 0; i < lits.size(); ++i) {
-            expr* e = lits[i].get(), *l, *r;
+            expr* e = lits.get(i), * l, * r;
             if (m.is_eq(e, l, r) && reduce_eq(is_var, l, r, v, t)) {
                 reduced = true;
-                project_plugin::erase(lits, i);
+                mbp::project_plugin::erase(lits, i);
                 expr_safe_replace sub(m);
                 sub.insert(v, t);
                 is_rem.mark(v);
                 for (unsigned j = 0; j < lits.size(); ++j) {
-                    sub(lits[j].get(), tmp);
+                    sub(lits.get(j), tmp);
                     m_rw(tmp);
                     lits[j] = tmp;
                 }
@@ -153,20 +86,17 @@ class mbp::impl {
         }
         if (reduced) {
             unsigned j = 0;
-            for (app* v : vars) {
-                if (!is_rem.is_marked(v)) {
+            for (app* v : vars)
+                if (!is_rem.is_marked(v))
                     vars[j++] = v;
-                }
-            }
             vars.shrink(j);
         }
         return reduced;
     }
 
     bool reduce_eq(expr_mark& is_var, expr* l, expr* r, expr_ref& v, expr_ref& t) {
-        if (is_var.is_marked(r)) {
-            std::swap(l, r);
-        }
+        if (is_var.is_marked(r)) 
+            std::swap(l, r);        
         if (is_var.is_marked(l)) {
             contains_app cont(m, to_app(l));
             if (!cont(r)) {
@@ -178,340 +108,155 @@ class mbp::impl {
         return false;
     }
 
-
     void filter_variables(model& model, app_ref_vector& vars, expr_ref_vector& lits, expr_ref_vector& unused_lits) {
         expr_mark lit_visited;
-        project_plugin::mark_rec(lit_visited, lits);
+        mbp::project_plugin::mark_rec(lit_visited, lits);
         unsigned j = 0;
-        for (app* var : vars) {
-            if (lit_visited.is_marked(var)) {
+        for (app* var : vars)
+            if (lit_visited.is_marked(var))
                 vars[j++] = var;
-                }
-            }
         vars.shrink(j);
     }
 
-    // over-approximation
-    bool contains_uninterpreted(expr* v) {
-        return true;
-    }
-
-    bool extract_bools(model_evaluator& eval, expr_ref_vector& fmls, expr* fml) {
-        TRACE("qe", tout << "extract bools: " << mk_pp(fml, m) << "\n";);
-        ptr_vector<expr> todo;
-        expr_safe_replace sub(m);
-        m_visited.reset();
-        bool found_bool = false;
-        if (is_app(fml)) {
-            todo.append(to_app(fml)->get_num_args(), to_app(fml)->get_args());
-        }
-        while (!todo.empty()) {
-            expr* e = todo.back();
-            todo.pop_back();
-            if (m_visited.is_marked(e)) {
-                continue;
-            }
-            m_visited.mark(e);
-            if (m.is_bool(e) && !m.is_true(e) && !m.is_false(e) && m.inc()) {
-                expr_ref val = eval(e);
-                TRACE("qe", tout << "found: " << mk_pp(e, m) << " " << val << "\n";);
-                if (!m.inc())
-                    continue;
-                if (!m.is_true(val) && !m.is_false(val) && contains_uninterpreted(val)) {
-                    throw default_exception("could not evaluate Boolean in model");
-                }
-                SASSERT(m.is_true(val) || m.is_false(val));
-
-                if (!m_bool_visited.is_marked(e)) {
-                    fmls.push_back(m.is_true(val) ? e : mk_not(m, e));
-                }
-                sub.insert(e, val);
-                m_bool_visited.mark(e);                
-                found_bool = true;
-            }
-            else if (is_app(e)) {
-                todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
-            }
-            else {
-                TRACE("qe", tout << "expression not handled " << mk_pp(e, m) << "\n";);
-            }
-        }
-        if (found_bool) {
-            expr_ref tmp(m);
-            sub(fml, tmp);
-            expr_ref val = eval(tmp);
-            if (!m.is_true(val) && !m.is_false(val))
-                return false;
-            fmls.push_back(m.is_true(val) ? tmp : mk_not(m, tmp));
-        }
-        return found_bool;
-    }
-
     void project_bools(model& mdl, app_ref_vector& vars, expr_ref_vector& fmls) {
         expr_safe_replace sub(m);
         expr_ref val(m);
-        model_evaluator eval(mdl, m_params);        
+        model_evaluator eval(mdl, m_params);
         eval.set_model_completion(true);
         unsigned j = 0;
-        for (unsigned i = 0; i < vars.size(); ++i) {
-            app* var = vars[i].get();
-            if (m.is_bool(var)) {
-                sub.insert(var, eval(var));
-            }
-            else {
-                vars[j++] = var;
-                }
-            }
-        if (j == vars.size()) {
-            return;
+        for (app* var : vars) {
+            if (m.is_bool(var)) 
+                sub.insert(var, eval(var));            
+            else 
+                vars[j++] = var;            
         }
+        if (j == vars.size()) 
+            return;        
         vars.shrink(j);
-            j = 0;
-            for (unsigned i = 0; i < fmls.size(); ++i) {
-            expr* fml = fmls[i].get();
+        j = 0;
+        for (expr* fml : fmls) {
             sub(fml, val);
-                m_rw(val);
-                if (!m.is_true(val)) {
+            m_rw(val);
+            if (!m.is_true(val)) {
                 TRACE("qe", tout << mk_pp(fml, m) << " -> " << val << "\n";);
                 fmls[j++] = val;
-                    }
-                }
-        fmls.shrink(j);
             }
+        }
+        fmls.shrink(j);
+    }
 
 
     void subst_vars(model_evaluator& eval, app_ref_vector const& vars, expr_ref& fml) {
-        expr_safe_replace sub (m);
-        for (app * v : vars) {
-            sub.insert(v, eval(v));
-            }
+        expr_safe_replace sub(m);
+        for (app* v : vars) 
+            sub.insert(v, eval(v));        
         sub(fml);
-        }
+    }
 
     struct index_term_finder {
-        ast_manager&     m;
+        ast_manager& m;
         array_util       m_array;
         app_ref          m_var;
         expr_ref_vector& m_res;
 
-        index_term_finder (ast_manager &mgr, app* v, expr_ref_vector &res): 
-            m(mgr), m_array (m), m_var (v, m), m_res (res) {}
+        index_term_finder(ast_manager& mgr, app* v, expr_ref_vector& res) :
+            m(mgr), m_array(m), m_var(v, m), m_res(res) {}
 
-        void operator() (var *n) {}
-        void operator() (quantifier *n) {}
-        void operator() (app *n) {
-            expr *e1, *e2;
-            if (m_array.is_select (n)) {
-                for (expr * arg : *n) {
-                    if (m.get_sort(arg) == m.get_sort(m_var) && arg != m_var) 
-                        m_res.push_back (arg);
-                } 
+        void operator() (var* n) {}
+        void operator() (quantifier* n) {}
+        void operator() (app* n) {
+            expr* e1, * e2;
+            if (m_array.is_select(n)) {
+                for (expr* arg : *n) {
+                    if (m.get_sort(arg) == m.get_sort(m_var) && arg != m_var)
+                        m_res.push_back(arg);
+                }
             }
             else if (m.is_eq(n, e1, e2)) {
-                if (e1 == m_var) 
-                    m_res.push_back(e2); 
-                else if (e2 == m_var) 
-                    m_res.push_back(e1); 
+                if (e1 == m_var)
+                    m_res.push_back(e2);
+                else if (e2 == m_var)
+                    m_res.push_back(e1);
             }
         }
     };
 
-    bool project_var (model_evaluator& eval, app* var, expr_ref& fml) {
+    bool project_var(model_evaluator& eval, app* var, expr_ref& fml) {
         expr_ref val = eval(var);
-        
-        TRACE ("mbqi_project_verbose", tout << "MBQI: var: " << mk_pp (var, m) << "\n" << "fml: " << fml << "\n";);
-        expr_ref_vector terms (m);
-        index_term_finder finder (m, var, terms);
-        for_each_expr (finder, fml);        
-        
-        TRACE ("mbqi_project_verbose", tout << "terms:\n" << terms;);
-        
-        for (expr * term : terms) {
+
+        TRACE("mbqi_project_verbose", tout << "MBQI: var: " << mk_pp(var, m) << "\n" << "fml: " << fml << "\n";);
+        expr_ref_vector terms(m);
+        index_term_finder finder(m, var, terms);
+        for_each_expr(finder, fml);
+
+        TRACE("mbqi_project_verbose", tout << "terms:\n" << terms;);
+
+        for (expr* term : terms) {
             expr_ref tval = eval(term);
-            
-            TRACE ("mbqi_project_verbose", tout << "term: " << mk_pp (term, m) << " tval: " << tval << " val: " << val << "\n";);
+
+            TRACE("mbqi_project_verbose", tout << "term: " << mk_pp(term, m) << " tval: " << tval << " val: " << val << "\n";);
 
             // -- if the term does not contain an occurrence of var
             // -- and is in the same equivalence class in the model
-            if (tval == val && !occurs (var, term)) {
-                TRACE ("mbqi_project",
-                       tout << "MBQI: replacing " << mk_pp (var, m) << " with " << mk_pp (term, m) << "\n";);
+            if (tval == val && !occurs(var, term)) {
+                TRACE("mbqi_project",
+                    tout << "MBQI: replacing " << mk_pp(var, m) << " with " << mk_pp(term, m) << "\n";);
                 expr_safe_replace sub(m);
-                sub.insert (var, term);
-                sub (fml);
+                sub.insert(var, term);
+                sub(fml);
                 return true;
             }
         }
 
-        TRACE ("mbqi_project",
-               tout << "MBQI: failed to eliminate " << mk_pp (var, m) << " from " << fml << "\n";);
+        TRACE("mbqi_project",
+            tout << "MBQI: failed to eliminate " << mk_pp(var, m) << " from " << fml << "\n";);
 
         return false;
     }
 
-    void project_vars (model &M, app_ref_vector &vars, expr_ref &fml)  {
+    void project_vars(model& M, app_ref_vector& vars, expr_ref& fml) {
         model_evaluator eval(M);
         eval.set_model_completion(false);
         // -- evaluate to initialize eval cache
-        (void) eval (fml);
+        eval(fml);
         unsigned j = 0;
-        for (app * v : vars) {
-            if (!project_var (eval, v, fml)) {
-                vars[j++] = v;
-            }
-        }
+        for (app* v : vars) 
+            if (!project_var(eval, v, fml)) 
+                vars[j++] = v;                    
         vars.shrink(j);
     }
 
 public:
 
     opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
-        arith_project_plugin arith(m);
+        mbp::arith_project_plugin arith(m);
         return arith.maximize(fmls, mdl, t, ge, gt);
     }
 
-    void extract_literals(model& model, expr_ref_vector& fmls) {
-        expr_ref val(m);
-        model_evaluator eval(model);
-        eval.set_expand_array_equalities(true);
-        TRACE("qe", tout << fmls << "\n";);
-        for (unsigned i = 0; i < fmls.size(); ++i) {
-            expr* fml = fmls[i].get(), *nfml, *f1, *f2, *f3;
-            SASSERT(m.is_bool(fml));
-            if (m.is_not(fml, nfml) && m.is_distinct(nfml)) {
-                fmls[i] = project_plugin::pick_equality(m, model, nfml);
-                --i;
-            }
-            else if (m.is_or(fml)) {
-                for (unsigned j = 0; j < to_app(fml)->get_num_args(); ++j) {
-                    val = eval(to_app(fml)->get_arg(j));
-                    if (m.is_true(val)) {
-                        fmls[i] = to_app(fml)->get_arg(j);
-                        --i;
-                        break;
-                    }
-                }
-            }
-            else if (m.is_and(fml)) {
-                fmls.append(to_app(fml)->get_num_args(), to_app(fml)->get_args());
-                project_plugin::erase(fmls, i);
-            }
-            else if (m.is_iff(fml, f1, f2) || (m.is_not(fml, nfml) && m.is_xor(nfml, f1, f2))) {
-                val = eval(f1);
-                if (m.is_false(val)) {
-                    f1 = mk_not(m, f1);
-                    f2 = mk_not(m, f2);
-                }
-                fmls[i] = f1;
-                project_plugin::push_back(fmls, f2);
-                --i;
-            }
-            else if (m.is_implies(fml, f1, f2)) {
-                val = eval(f2);
-                if (m.is_true(val)) {
-                    fmls[i] = f2;
-                }
-                else {
-                    fmls[i] = mk_not(m, f1);
-                }
-                --i;
-            }
-            else if (m.is_ite(fml, f1, f2, f3)) {
-                val = eval(f1);                
-                if (m.is_true(val)) {
-                    project_plugin::push_back(fmls, f1);
-                    project_plugin::push_back(fmls, f2);
-                }
-                else {
-                    project_plugin::push_back(fmls, mk_not(m, f1));
-                    project_plugin::push_back(fmls, f3);
-                }
-                project_plugin::erase(fmls, i);
-            }
-            else if (m.is_not(fml, nfml) && m.is_not(nfml, nfml)) {
-                project_plugin::push_back(fmls, nfml);
-                project_plugin::erase(fmls, i);
-            }
-            else if (m.is_not(fml, nfml) && m.is_and(nfml)) {
-                for (unsigned j = 0; j < to_app(nfml)->get_num_args(); ++j) {
-                    val = eval(to_app(nfml)->get_arg(j));
-                    if (m.is_false(val)) {
-                        fmls[i] = mk_not(m, to_app(nfml)->get_arg(j));
-                        --i;
-                        break;
-                    }
-                }
-            }
-            else if (m.is_not(fml, nfml) && m.is_or(nfml)) {
-                for (unsigned j = 0; j < to_app(nfml)->get_num_args(); ++j) {
-                    project_plugin::push_back(fmls, mk_not(m, to_app(nfml)->get_arg(j)));
-                }
-                project_plugin::erase(fmls, i);                
-            }
-            else if ((m.is_not(fml, nfml) && m.is_iff(nfml, f1, f2)) || m.is_xor(fml, f1, f2)) {
-                val = eval(f1);
-                if (m.is_true(val)) {
-                    f2 = mk_not(m, f2);
-                }
-                else {
-                    f1 = mk_not(m, f1);
-                }
-                project_plugin::push_back(fmls, f1);
-                project_plugin::push_back(fmls, f2);
-                project_plugin::erase(fmls, i);
-            }
-            else if (m.is_not(fml, nfml) && m.is_implies(nfml, f1, f2)) {
-                project_plugin::push_back(fmls, f1);
-                project_plugin::push_back(fmls, mk_not(m, f2));
-                project_plugin::erase(fmls, i);
-            }
-            else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) {
-                val = eval(f1);                
-                if (m.is_true(val)) {
-                    project_plugin::push_back(fmls, f1);
-                    project_plugin::push_back(fmls, mk_not(m, f2));
-                }
-                else {
-                    project_plugin::push_back(fmls, mk_not(m, f1));
-                    project_plugin::push_back(fmls, mk_not(m, f3));
-                }
-                project_plugin::erase(fmls, i);
-            }
-            else if (m.is_not(fml, nfml)) {
-                if (extract_bools(eval, fmls, nfml)) {
-                    project_plugin::erase(fmls, i);
-                }
-            }
-            else {
-                if (extract_bools(eval, fmls, fml)) {
-                    project_plugin::erase(fmls, i);
-                }
-                // TBD other Boolean operations.
-            }
-        }
-        TRACE("qe", tout << fmls << "\n";);
-        m_bool_visited.reset();
+    void extract_literals(model& model, app_ref_vector const& vars, expr_ref_vector& fmls) {
+        mbp::project_plugin proj(m);
+        proj.extract_literals(model, vars, fmls);
     }
 
-    impl(ast_manager& m, params_ref const& p):m(m), m_params(p), m_rw(m) {
-        add_plugin(alloc(arith_project_plugin, m));
-        add_plugin(alloc(datatype_project_plugin, m));
-        add_plugin(alloc(array_project_plugin, m));
+    impl(ast_manager& m, params_ref const& p) :m(m), m_params(p), m_rw(m) {
+        add_plugin(alloc(mbp::arith_project_plugin, m));
+        add_plugin(alloc(mbp::datatype_project_plugin, m));
+        add_plugin(alloc(mbp::array_project_plugin, m));
         updt_params(p);
     }
 
     ~impl() {
-        std::for_each(m_plugins.begin(), m_plugins.end(), delete_proc<project_plugin>());
+        std::for_each(m_plugins.begin(), m_plugins.end(), delete_proc<mbp::project_plugin>());
     }
 
     void updt_params(params_ref const& p) {
         m_params.append(p);
         m_reduce_all_selects = m_params.get_bool("reduce_all_selects", false);
-        m_dont_sub   = m_params.get_bool("dont_sub", false);
+        m_dont_sub = m_params.get_bool("dont_sub", false);
     }
 
     void preprocess_solve(model& model, app_ref_vector& vars, expr_ref_vector& fmls) {
-        extract_literals(model, fmls);
+        extract_literals(model, vars, fmls);
         bool change = true;
         while (change && !vars.empty()) {
             change = solve(model, vars, fmls);
@@ -520,13 +265,13 @@ public:
                     change = true;
                 }
             }
-        }        
+        }
     }
 
     bool validate_model(model& model, expr_ref_vector const& fmls) {
         expr_ref val(m);
         model_evaluator eval(model);
-        for (expr * f : fmls) {
+        for (expr* f : fmls) {
             VERIFY(!model.is_false(f));
         }
         return true;
@@ -544,7 +289,7 @@ public:
         while (progress && !vars.empty() && !fmls.empty() && m.limit().inc()) {
             app_ref_vector new_vars(m);
             progress = false;
-            for (project_plugin * p : m_plugins) {
+            for (mbp::project_plugin* p : m_plugins) {
                 if (p) {
                     (*p)(model, vars, fmls);
                 }
@@ -552,7 +297,7 @@ public:
             while (!vars.empty() && !fmls.empty() && m.limit().inc()) {
                 var = vars.back();
                 vars.pop_back();
-                project_plugin* p = get_plugin(var);
+                mbp::project_plugin* p = get_plugin(var);
                 if (p && (*p)(model, var, vars, fmls)) {
                     progress = true;
                 }
@@ -566,19 +311,17 @@ public:
                 expr_safe_replace sub(m);
                 val = model(var);
                 sub.insert(var, val);
-                for (unsigned i = 0; i < fmls.size(); ++i) {
-                    sub(fmls[i].get(), tmp);
+                unsigned j = 0;
+                for (expr* f : fmls) {
+                    sub(f, tmp);
                     m_rw(tmp);
-                    if (m.is_true(tmp)) {
-                        project_plugin::erase(fmls, i);
-                    }
-                    else {
-                        fmls[i] = tmp;
-                    }
-                }            
+                    if (!m.is_true(tmp))
+                        fmls[j++] = tmp;
+                }
+                fmls.shrink(j);
                 progress = true;
-            }        
-            if (!m.limit().inc()) 
+            }
+            if (!m.limit().inc())
                 return;
             vars.append(new_vars);
             if (progress) {
@@ -592,13 +335,13 @@ public:
         SASSERT(validate_model(model, fmls));
         TRACE("qe", tout << vars << " " << fmls << "\n";);
     }
-    
+
     void do_qe_lite(app_ref_vector& vars, expr_ref& fml) {
         qe_lite qe(m, m_params, false);
-        qe (vars, fml);
-        m_rw (fml);            
-        TRACE ("qe", tout << "After qe_lite:\n" << fml << "\n" << "Vars: " << vars << "\n";);        
-        SASSERT (!m.is_false (fml));
+        qe(vars, fml);
+        m_rw(fml);
+        TRACE("qe", tout << "After qe_lite:\n" << fml << "\n" << "Vars: " << vars << "\n";);
+        SASSERT(!m.is_false(fml));
     }
 
     void do_qe_bool(model& mdl, app_ref_vector& vars, expr_ref& fml) {
@@ -609,130 +352,122 @@ public:
     }
 
     void spacer(app_ref_vector& vars, model& mdl, expr_ref& fml) {
-        TRACE ("qe", tout << "Before projection:\n" << fml << "\n" << "Vars: " << vars << "\n";);
+        TRACE("qe", tout << "Before projection:\n" << fml << "\n" << "Vars: " << vars << "\n";);
 
-        model_evaluator eval(mdl, m_params);        
+        model_evaluator eval(mdl, m_params);
         eval.set_model_completion(true);
-        app_ref_vector other_vars (m);
-        app_ref_vector array_vars (m);
-        array_util arr_u (m);
-        arith_util ari_u (m);
+        app_ref_vector other_vars(m);
+        app_ref_vector array_vars(m);
+        array_util arr_u(m);
+        arith_util ari_u(m);
 
         flatten_and(fml);
 
-
         while (!vars.empty()) {
 
             do_qe_lite(vars, fml);
 
             do_qe_bool(mdl, vars, fml);
-            
+
             // sort out vars into bools, arith (int/real), and arrays
             for (app* v : vars) {
                 if (arr_u.is_array(v)) {
-                    array_vars.push_back (v);
-                } 
-                else {
-                    other_vars.push_back (v);
+                    array_vars.push_back(v);
                 }
-            }        
-            
-            TRACE ("qe", tout << "Array vars: " << array_vars << "\n";);
-            
-            vars.reset ();
-            
-            // project arrays
-            qe::array_project_plugin ap(m);
-            ap(mdl, array_vars, fml, vars, m_reduce_all_selects);
-            SASSERT (array_vars.empty ());
-            m_rw (fml);
-            SASSERT (!m.is_false (fml));
+                else {
+                    other_vars.push_back(v);
+                }
+            }
 
-            TRACE ("qe",
-                   tout << "extended model:\n" << mdl;
-                   tout << "Vars: " << vars << "\n";
-                   );            
+            TRACE("qe", tout << "Array vars: " << array_vars << "\n";);
+
+            vars.reset();
+
+            // project arrays
+            mbp::array_project_plugin ap(m);
+            ap(mdl, array_vars, fml, vars, m_reduce_all_selects);
+            SASSERT(array_vars.empty());
+            m_rw(fml);
+            SASSERT(!m.is_false(fml));
+
+            TRACE("qe",
+                tout << "extended model:\n" << mdl;
+                tout << "Vars: " << vars << "\n";);
         }
-                        
+
         // project reals, ints and other variables.
-        if (!other_vars.empty ()) {
-            TRACE ("qe", tout << "Other vars: " << other_vars << "\n" << mdl;);
-                        
+        if (!other_vars.empty()) {
+            TRACE("qe", tout << "Other vars: " << other_vars << "\n" << mdl;);
+
             expr_ref_vector fmls(m);
-            flatten_and (fml, fmls);
-            
+            flatten_and(fml, fmls);
+
             (*this)(false, other_vars, mdl, fmls);
-            fml = mk_and (fmls);
+            fml = mk_and(fmls);
             m_rw(fml);
-                        
-            TRACE ("qe",
-                   tout << "Projected other vars:\n" << fml << "\n";
-                   tout << "Remaining other vars:\n" << other_vars << "\n";);
-            SASSERT (!m.is_false (fml));
+
+            TRACE("qe",
+                tout << "Projected other vars:\n" << fml << "\n";
+            tout << "Remaining other vars:\n" << other_vars << "\n";);
+            SASSERT(!m.is_false(fml));
         }
-        
-        if (!other_vars.empty ()) {
-            project_vars (mdl, other_vars, fml);
+
+        if (!other_vars.empty()) {
+            project_vars(mdl, other_vars, fml);
             m_rw(fml);
         }
-        
+
         // substitute any remaining other vars
-        if (!m_dont_sub && !other_vars.empty ()) {
-            subst_vars (eval, other_vars, fml);
-            TRACE ("qe", tout << "After substituting remaining other vars:\n" << fml << "\n";);
+        if (!m_dont_sub && !other_vars.empty()) {
+            subst_vars(eval, other_vars, fml);
+            TRACE("qe", tout << "After substituting remaining other vars:\n" << fml << "\n";);
             // an extra round of simplification because subst_vars is not simplifying
             m_rw(fml);
             other_vars.reset();
         }
-        
+
         SASSERT(!eval.is_false(fml));
-                
-        vars.reset ();
+
+        vars.reset();
         vars.append(other_vars);
-    }    
-    
+    }
+
 };
-    
-mbp::mbp(ast_manager& m, params_ref const& p) {
-    scoped_no_proof _sp (m);
+
+mbproj::mbproj(ast_manager& m, params_ref const& p) {
+    scoped_no_proof _sp(m);
     m_impl = alloc(impl, m, p);
 }
-        
-mbp::~mbp() {
+
+mbproj::~mbproj() {
     dealloc(m_impl);
 }
-        
-void mbp::updt_params(params_ref const& p) {
+
+void mbproj::updt_params(params_ref const& p) {
     m_impl->updt_params(p);
 }
-       
-void mbp::get_param_descrs(param_descrs & r) {
+
+void mbproj::get_param_descrs(param_descrs& r) {
     r.insert("reduce_all_selects", CPK_BOOL, "(default: false) reduce selects");
     r.insert("dont_sub", CPK_BOOL, "(default: false) disable substitution of values for free variables");
 }
-        
-void mbp::operator()(bool force_elim, app_ref_vector& vars, model& mdl, expr_ref_vector& fmls) {
-    scoped_no_proof _sp (fmls.get_manager());
+
+void mbproj::operator()(bool force_elim, app_ref_vector& vars, model& mdl, expr_ref_vector& fmls) {
+    scoped_no_proof _sp(fmls.get_manager());
     (*m_impl)(force_elim, vars, mdl, fmls);
 }
 
-void mbp::spacer(app_ref_vector& vars, model& mdl, expr_ref& fml) {
-    scoped_no_proof _sp (fml.get_manager());
+void mbproj::spacer(app_ref_vector& vars, model& mdl, expr_ref& fml) {
+    scoped_no_proof _sp(fml.get_manager());
     m_impl->spacer(vars, mdl, fml);
 }
 
-void mbp::solve(model& model, app_ref_vector& vars, expr_ref_vector& fmls) {
-    scoped_no_proof _sp (fmls.get_manager());
+void mbproj::solve(model& model, app_ref_vector& vars, expr_ref_vector& fmls) {
+    scoped_no_proof _sp(fmls.get_manager());
     m_impl->preprocess_solve(model, vars, fmls);
 }
-        
-void mbp::extract_literals(model& model, expr_ref_vector& lits) {
-    scoped_no_proof _sp (lits.get_manager());
-    m_impl->extract_literals(model, lits);
-}
 
-
-opt::inf_eps mbp::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
-    scoped_no_proof _sp (fmls.get_manager());
+opt::inf_eps mbproj::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
+    scoped_no_proof _sp(fmls.get_manager());
     return m_impl->maximize(fmls, mdl, t, ge, gt);
 }
diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h
index c63f202bf..daa65de7a 100644
--- a/src/qe/qe_mbp.h
+++ b/src/qe/qe_mbp.h
@@ -28,55 +28,13 @@ Revision History:
 
 namespace qe {
 
-    struct cant_project {};
-
-    struct def {
-        expr_ref var, term;
-        def(const expr_ref& v, expr_ref& t): var(v), term(t) {}
-    };
-
-    class project_plugin {
-    public:
-        virtual ~project_plugin() {}
-        virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) = 0;
-        /**
-           \brief partial solver.
-        */
-        virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) = 0;
-        virtual family_id get_family_id() = 0;
-
-        virtual void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { };
-
-        /**
-           \brief project vars modulo model, return set of definitions for eliminated variables.
-           - vars in/out: returns variables that were not eliminated
-           - lits in/out: returns projected literals
-           - returns set of definitions
-             (TBD: in triangular form, the last definition can be substituted into definitions that come before)
-        */
-        virtual vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) = 0;
-
-        /**
-           \brief model based saturation. Saturates theory axioms to equi-satisfiable literals over EUF,
-           such that 'shared' are not retained for EUF.
-         */
-        virtual void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) = 0;
-
-
-        static expr_ref pick_equality(ast_manager& m, model& model, expr* t);
-        static void erase(expr_ref_vector& lits, unsigned& i);
-        static void push_back(expr_ref_vector& lits, expr* lit);
-        static void mark_rec(expr_mark& visited, expr* e);
-        static void mark_rec(expr_mark& visited, expr_ref_vector const& es);
-    };
-
-    class mbp {
+    class mbproj {
         class impl;
         impl * m_impl;
     public:
-        mbp(ast_manager& m, params_ref const& p = params_ref());
+        mbproj(ast_manager& m, params_ref const& p = params_ref());
 
-        ~mbp();
+        ~mbproj();
 
         void updt_params(params_ref const& p);
 
@@ -95,12 +53,6 @@ namespace qe {
         */
         void solve(model& model, app_ref_vector& vars, expr_ref_vector& lits);
 
-        /**
-           \brief
-           Extract literals from formulas based on model.
-         */
-        void extract_literals(model& model, expr_ref_vector& lits);
-
         /**
            \brief
            Maximize objective t under current model for constraints in fmls.
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 4f903e815..be4d98fff 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -607,7 +607,7 @@ namespace qe {
         params_ref                 m_params;
         stats                      m_stats;
         statistics                 m_st;
-        qe::mbp                    m_mbp;
+        qe::mbproj                 m_mbp;
         kernel                     m_fa;
         kernel                     m_ex;
         pred_abs                   m_pred_abs;
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index e8f40cdca..736024781 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -76,7 +76,7 @@ namespace sat {
             ~scoped_drating() { ext.m_drating = false;  }
         };
         virtual void init_search() {}
-        virtual bool propagate(sat::literal l, sat::ext_constraint_idx idx) { UNREACHABLE(); return false; }
+        virtual bool propagated(sat::literal l, sat::ext_constraint_idx idx) { UNREACHABLE(); return false; }
         virtual bool unit_propagate() = 0;        
         virtual bool is_external(bool_var v) { return false; }
         virtual double get_reward(literal l, ext_constraint_idx idx, literal_occs_fun& occs) const { return 0; }
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index e8fb74051..c78e7995c 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -1354,7 +1354,7 @@ namespace sat {
         watch_list::iterator it = wlist.begin(), it2 = it, end = wlist.end();
         for (; it != end && !inconsistent(); ++it) {
             SASSERT(it->get_kind() == watched::EXT_CONSTRAINT);
-            bool keep = m_s.m_ext->propagate(l, it->get_ext_constraint_idx());
+            bool keep = m_s.m_ext->propagated(l, it->get_ext_constraint_idx());
             if (m_search_mode == lookahead_mode::lookahead1 && !m_inconsistent) {
                 lookahead_literal_occs_fun literal_occs_fn(*this);
                 m_lookahead_reward += m_s.m_ext->get_reward(l, it->get_ext_constraint_idx(), literal_occs_fn);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index b22debbc6..24e072b2b 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1180,7 +1180,7 @@ namespace sat {
             }
             case watched::EXT_CONSTRAINT:
                 SASSERT(m_ext);
-                keep = m_ext->propagate(l, it->get_ext_constraint_idx());
+                keep = m_ext->propagated(l, it->get_ext_constraint_idx());
                 if (m_inconsistent) {
                     if (!keep) {
                         ++it;
diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt
index 51a65c0f2..197fe9aaf 100644
--- a/src/sat/smt/CMakeLists.txt
+++ b/src/sat/smt/CMakeLists.txt
@@ -20,6 +20,7 @@ z3_add_component(sat_smt
     bv_internalize.cpp
     bv_invariant.cpp
     bv_solver.cpp
+    dt_solver.cpp
     euf_ackerman.cpp
     euf_internalize.cpp
     euf_invariant.cpp
diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index 8a1f2ca31..82ff03f04 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -53,12 +53,7 @@ namespace arith {
     }
 
     std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { 
-        auto& jst = euf::th_propagation::from_index(idx);
-        for (auto lit : euf::th_propagation::lits(jst))
-            out << lit << " ";
-        for (auto eq : euf::th_propagation::eqs(jst))
-            out << eq.first->get_expr_id() << " == " << eq.second->get_expr_id() << " ";
-        return out;
+        return euf::th_propagation::from_index(idx).display(out);
     }
 
     std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { 
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index d72180460..0105089c0 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -61,14 +61,10 @@ namespace arith {
         m_asserted.push_back(l);
     }
 
-    euf::th_solver* solver::clone(sat::solver* s, euf::solver& ctx) {
-        arith::solver* result = alloc(arith::solver, ctx, get_id());
-        ast_translation tr(m, ctx.get_manager());
-        for (unsigned i = result->get_num_vars(); i < get_num_vars(); ++i) {
-            expr* e1 = var2expr(i);
-            expr* e2 = tr(e1);
-            result->mk_evar(e2);
-        }
+    euf::th_solver* solver::clone(euf::solver& dst_ctx) {
+        arith::solver* result = alloc(arith::solver, dst_ctx, get_id());
+        for (unsigned i = result->get_num_vars(); i < get_num_vars(); ++i) 
+            result->mk_evar(ctx.copy(dst_ctx, var2enode(i))->get_expr());        
 
         unsigned v = 0;
         result->m_bounds.resize(m_bounds.size());
@@ -1425,19 +1421,7 @@ namespace arith {
 
     void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) {
         auto& jst = euf::th_propagation::from_index(idx);
-        for (auto lit : euf::th_propagation::lits(jst))
-            r.push_back(lit);
-        for (auto eq : euf::th_propagation::eqs(jst))
-            ctx.add_antecedent(eq.first, eq.second);
-
-        if (!probing && ctx.use_drat()) {
-            literal_vector lits;
-            for (auto lit : euf::th_propagation::lits(jst))
-                lits.push_back(~lit);
-            lits.push_back(l);
-            ctx.get_drat().add(lits, status());
-            for (auto eq : euf::th_propagation::eqs(jst))
-                IF_VERBOSE(0, verbose_stream() << "drat-log with equalities is TBD " << eq.first->get_expr_id() << "\n");
-        }
+        ctx.get_antecedents(l, jst, r, probing);
     }
+
 }
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index cb0380766..7190c7407 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -410,7 +410,6 @@ namespace arith {
         solver(euf::solver& ctx, theory_id id);
         ~solver() override;
         bool is_external(bool_var v) override { return false; }
-        bool propagate(literal l, sat::ext_constraint_idx idx) override { UNREACHABLE(); return false; }
         void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override;
         void asserted(literal l) override;
         sat::check_result check() override;
@@ -419,7 +418,7 @@ namespace arith {
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
         void collect_statistics(statistics& st) const override;
-        euf::th_solver* clone(sat::solver* s, euf::solver& ctx) override;
+        euf::th_solver* clone(euf::solver& ctx) override;
         bool use_diseqs() const override { return true; }
         void new_eq_eh(euf::th_eq const& eq) override { mk_eq_axiom(eq.v1(), eq.v2()); }
         void new_diseq_eh(euf::th_eq const& de) override { mk_eq_axiom(de.v1(), de.v2()); }
diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp
index 44e506d93..19caa7222 100644
--- a/src/sat/smt/array_internalize.cpp
+++ b/src/sat/smt/array_internalize.cpp
@@ -26,7 +26,10 @@ namespace array {
             TRACE("array", tout << mk_pp(e, m) << "\n";);
             return sat::null_literal;
         }
-        return expr2literal(e);
+        auto lit = expr2literal(e);
+        if (sign)
+            lit.neg();
+        return lit;
     }
 
     void solver::internalize(expr* e, bool redundant) {
diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp
index 4df6df2a5..3a8913760 100644
--- a/src/sat/smt/array_solver.cpp
+++ b/src/sat/smt/array_solver.cpp
@@ -151,15 +151,10 @@ namespace array {
         st.update("array splits",       m_stats.m_num_eq_splits);
     }
 
-    euf::th_solver* solver::clone(sat::solver* s, euf::solver& ctx) {
-        auto* result = alloc(solver, ctx, get_id());
-        ast_translation tr(m, ctx.get_manager());
-        for (unsigned i = 0; i < get_num_vars(); ++i) {
-            expr* e1 = var2expr(i);
-            expr* e2 = tr(e1);
-            euf::enode* n = ctx.get_enode(e2);
-            result->mk_var(n);
-        }
+    euf::th_solver* solver::clone(euf::solver& dst_ctx) {
+        auto* result = alloc(solver, dst_ctx, get_id());
+        for (unsigned i = 0; i < get_num_vars(); ++i)          
+            result->mk_var(ctx.copy(dst_ctx, var2enode(i)));        
         return result;
     }
 
diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h
index b46dfd761..4fbd70e92 100644
--- a/src/sat/smt/array_solver.h
+++ b/src/sat/smt/array_solver.h
@@ -192,7 +192,6 @@ namespace array {
         solver(euf::solver& ctx, theory_id id);
         ~solver() override;
         bool is_external(bool_var v) override { return false; }
-        bool propagate(literal l, sat::ext_constraint_idx idx) override { UNREACHABLE(); return false; }
         void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override {}
         void asserted(literal l) override {}
         sat::check_result check() override;
@@ -201,7 +200,7 @@ namespace array {
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
         void collect_statistics(statistics& st) const override;
-        euf::th_solver* clone(sat::solver* s, euf::solver& ctx) override;
+        euf::th_solver* clone(euf::solver& ctx) override;
         void new_eq_eh(euf::th_eq const& eq) override;
         bool use_diseqs() const override { return true; }
         void new_diseq_eh(euf::th_eq const& eq) override;
@@ -217,5 +216,7 @@ namespace array {
         void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
         void unmerge_eh(theory_var v1, theory_var v2) {}
+
+        euf::enode_vector const& parent_selects(euf::enode* n) const { return m_var_data[n->get_th_var(get_id())]->m_parent_selects; }
     };
 }
diff --git a/src/sat/smt/ba_solver.cpp b/src/sat/smt/ba_solver.cpp
index bc15b8a58..69455f307 100644
--- a/src/sat/smt/ba_solver.cpp
+++ b/src/sat/smt/ba_solver.cpp
@@ -1484,7 +1484,7 @@ namespace sat {
     /*
       \brief return true to keep watching literal.
     */
-    bool ba_solver::propagate(literal l, ext_constraint_idx idx) {
+    bool ba_solver::propagated(literal l, ext_constraint_idx idx) {
         SASSERT(value(l) == l_true);
         constraint& c = index2constraint(idx);
         if (c.lit() != null_literal && l.var() == c.lit().var()) {
@@ -3137,16 +3137,16 @@ namespace sat {
     }
 
     extension* ba_solver::copy(solver* s) {
-        return clone_aux(s, m, si, m_id);
+        return clone_aux(m, *s, si, m_id);
     }
 
-    euf::th_solver* ba_solver::clone(solver* new_s, euf::solver& new_ctx) {
-        return clone_aux(new_s, new_ctx.get_manager(), new_ctx.get_si(), get_id());
+    euf::th_solver* ba_solver::clone(euf::solver& new_ctx) {
+        return clone_aux(new_ctx.get_manager(), new_ctx.s(), new_ctx.get_si(), get_id());
     }
 
-    euf::th_solver* ba_solver::clone_aux(solver* new_s, ast_manager& m, sat::sat_internalizer& si, euf::theory_id id) {
+    euf::th_solver* ba_solver::clone_aux(ast_manager& m, sat::solver& s, sat::sat_internalizer& si, euf::theory_id id) {
         ba_solver* result = alloc(ba_solver, m, si, id);
-        result->set_solver(new_s);
+        result->set_solver(&s);
         copy_constraints(result, m_constraints);
         return result;
     }
diff --git a/src/sat/smt/ba_solver.h b/src/sat/smt/ba_solver.h
index 703aa9438..6e8173080 100644
--- a/src/sat/smt/ba_solver.h
+++ b/src/sat/smt/ba_solver.h
@@ -151,7 +151,7 @@ namespace sat {
         unsigned_vector           m_weights;
         svector<wliteral>         m_wlits;
 
-        euf::th_solver* clone_aux(sat::solver* new_s, ast_manager& m, sat::sat_internalizer& si, euf::theory_id id);
+        euf::th_solver* clone_aux(ast_manager& m, sat::solver& s, sat::sat_internalizer& si, euf::theory_id id);
 
         bool subsumes(card& c1, card& c2, literal_vector& comp);
         bool subsumes(card& c1, clause& c2, bool& self);
@@ -402,7 +402,7 @@ namespace sat {
         void add_xr(literal_vector const& lits);
 
         bool is_external(bool_var v) override;
-        bool propagate(literal l, ext_constraint_idx idx) override;
+        bool propagated(literal l, ext_constraint_idx idx) override;
         bool unit_propagate() override { return false; }
         lbool resolve_conflict() override;
         void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r, bool probing) override;
@@ -433,7 +433,7 @@ namespace sat {
         literal internalize(expr* e, bool sign, bool root, bool redundant) override;
         void internalize(expr* e, bool redundant) override;
         bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
-        euf::th_solver* clone(solver* s, euf::solver& ctx) override;
+        euf::th_solver* clone(euf::solver& ctx) override;
 
         ptr_vector<constraint> const & constraints() const { return m_constraints; }
         std::ostream& display(std::ostream& out, constraint const& c, bool values) const;
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index 8165b2743..8e82cad8e 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -260,7 +260,6 @@ namespace bv {
     double solver::get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const { return 0; }
     bool solver::is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) { return false; }
     bool solver::is_external(bool_var v) { return true; }
-    bool solver::propagate(literal l, sat::ext_constraint_idx idx) { return false; }
 
     void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) {
         auto& c = bv_justification::from_index(idx);
@@ -649,7 +648,7 @@ namespace bv {
 
     sat::extension* solver::copy(sat::solver* s) { UNREACHABLE(); return nullptr; }
 
-    euf::th_solver* solver::clone(sat::solver* s, euf::solver& ctx) {
+    euf::th_solver* solver::clone(euf::solver& ctx) {
         bv::solver* result = alloc(bv::solver, ctx, get_id());
         ast_translation tr(m, ctx.get_manager());
         for (unsigned i = 0; i < get_num_vars(); ++i) {
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index b9894a34f..87dede42b 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -309,7 +309,6 @@ namespace bv {
         double get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const override;
         bool is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) override;
         bool is_external(bool_var v) override;
-        bool propagate(literal l, sat::ext_constraint_idx idx) override;
         void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r, bool probing) override;
         void asserted(literal l) override;
         sat::check_result check() override;
@@ -324,7 +323,7 @@ namespace bv {
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
         void collect_statistics(statistics& st) const override;
-        euf::th_solver* clone(sat::solver* s, euf::solver& ctx) override;
+        euf::th_solver* clone(euf::solver& ctx) override;
         extension* copy(sat::solver* s) override;       
         void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override {}
         void gc() override {}
diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
new file mode 100644
index 000000000..ba36af1ec
--- /dev/null
+++ b/src/sat/smt/dt_solver.cpp
@@ -0,0 +1,785 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    dt_solver.h
+
+Abstract:
+
+    Theory plugin for altegraic datatypes
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-08
+
+--*/
+
+#include "sat/smt/dt_solver.h"
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/array_solver.h"
+
+namespace euf {
+    class solver;
+}
+
+namespace dt {
+
+    solver::solver(euf::solver& ctx, theory_id id) :
+        th_euf_solver(ctx, m.get_family_name(id), id),
+        dt(m),
+        m_autil(m),
+        m_find(*this),
+        m_args(m)
+    {}
+
+    solver::~solver() {
+        std::for_each(m_var_data.begin(), m_var_data.end(), delete_proc<var_data>());
+        m_var_data.reset();
+    }
+
+    void solver::clone_var(solver& src, theory_var v) {
+        enode* n = src.ctx.copy(ctx, src.var2enode(v));
+        VERIFY(v == th_euf_solver::mk_var(n));
+        m_var_data.push_back(alloc(var_data));
+        var_data* d_dst = m_var_data[v];
+        var_data* d_src = src.m_var_data[v];
+        ctx.attach_th_var(n, this, v);
+        if (d_src->m_constructor && !d_dst->m_constructor)
+            d_dst->m_constructor = src.ctx.copy(ctx, d_src->m_constructor);
+        for (auto* r : d_src->m_recognizers)
+            d_dst->m_recognizers.push_back(src.ctx.copy(ctx, r));
+    }
+
+    euf::th_solver* solver::clone(euf::solver& dst_ctx) {
+        auto* result = alloc(solver, dst_ctx, get_id());
+        for (unsigned v = 0; v < get_num_vars(); ++v)
+            result->clone_var(*this, v);
+        return result;
+    }
+
+    solver::final_check_st::final_check_st(solver& s) : s(s) {
+        SASSERT(s.m_to_unmark1.empty());
+        SASSERT(s.m_to_unmark2.empty());
+        s.m_used_eqs.reset();
+        s.m_dfs.reset();
+    }
+
+    solver::final_check_st::~final_check_st() {
+        s.clear_mark();
+    }
+
+    void solver::clear_mark() {
+        for (enode* n : m_to_unmark1)
+            n->unmark1();
+        for (enode* n : m_to_unmark2)
+            n->unmark2();
+        m_to_unmark1.reset();
+        m_to_unmark2.reset();
+    }
+
+    void solver::oc_mark_on_stack(enode* n) {
+        n = n->get_root();
+        n->mark1();
+        m_to_unmark1.push_back(n);
+    }
+
+    void solver::oc_mark_cycle_free(enode* n) {
+        n = n->get_root();
+        n->mark2();
+        m_to_unmark2.push_back(n);
+    }
+
+    void solver::oc_push_stack(enode* n) {
+        m_dfs.push_back(std::make_pair(EXIT, n));
+        m_dfs.push_back(std::make_pair(ENTER, n));
+    }
+
+    /**
+       \brief Assert the axiom (antecedent => lhs = rhs)
+       antecedent may be null_literal
+    */
+    void solver::assert_eq_axiom(enode* lhs, expr* rhs, literal antecedent) {
+        if (antecedent == sat::null_literal)
+            add_unit(eq_internalize(lhs->get_expr(), rhs));
+        else if (s().value(antecedent) == l_true) {
+            euf::th_propagation* jst = euf::th_propagation::mk(*this, antecedent);
+            ctx.propagate(lhs, e_internalize(rhs), jst);
+        }
+        else
+            add_clause(~antecedent, eq_internalize(lhs->get_expr(), rhs));
+    }
+
+    /**
+       \brief Assert the equality (= n (c (acc_1 n) ... (acc_m n))) where
+       where acc_i are the accessors of constructor c.
+    */
+    void solver::assert_is_constructor_axiom(enode* n, func_decl* c, literal antecedent) {
+        expr* e = n->get_expr();
+        TRACE("dt", tout << "creating axiom (= n (c (acc_1 n) ... (acc_m n))) for\n"
+            << mk_pp(c, m) << " " << mk_pp(e, m) << "\n";);
+        m_stats.m_assert_cnstr++;
+        SASSERT(dt.is_constructor(c));
+        SASSERT(is_datatype(e));
+        SASSERT(c->get_range() == m.get_sort(e));
+        m_args.reset();
+        ptr_vector<func_decl> const& accessors = *dt.get_constructor_accessors(c);
+        SASSERT(c->get_arity() == accessors.size());
+        for (func_decl* d : accessors)
+            m_args.push_back(m.mk_app(d, e));
+        expr_ref con(m.mk_app(c, m_args), m);
+        assert_eq_axiom(n, con, antecedent);
+    }
+
+    /**
+       \brief Given a constructor n := (c a_1 ... a_m) assert the axioms
+       (= (acc_1 n) a_1)
+       ...
+       (= (acc_m n) a_m)
+    */
+    void solver::assert_accessor_axioms(enode* n) {
+        m_stats.m_assert_accessor++;
+        expr* e = n->get_expr();
+        SASSERT(is_constructor(n));
+        func_decl* d = n->get_decl();
+        ptr_vector<func_decl> const& accessors = *dt.get_constructor_accessors(d);
+        SASSERT(n->num_args() == accessors.size());
+        unsigned i = 0;
+        for (func_decl* acc : accessors) {
+            app_ref acc_app(m.mk_app(acc, e), m);
+            assert_eq_axiom(n->get_arg(i), acc_app);
+            ++i;
+        }
+    }
+
+    /**
+       \brief Sign a conflict for r := is_mk(a), c := mk(...), not(r),  and c == a.
+    */
+    void solver::sign_recognizer_conflict(enode* c, enode* r) {
+        SASSERT(is_constructor(c));
+        SASSERT(is_recognizer(r));
+        SASSERT(dt.get_recognizer_constructor(r->get_decl()) == c->get_decl());
+        SASSERT(c->get_root() == r->get_arg(0)->get_root());
+        TRACE("dt", tout << ctx.bpp(c) << "\n" << ctx.bpp(r) << "\n";);
+        literal l = ctx.enode2literal(r);
+        SASSERT(s().value(l) == l_false);
+        clear_mark();
+        auto* jst = euf::th_propagation::mk(*this, ~l, c, r->get_arg(0));
+        ctx.set_conflict(jst);
+    }
+
+    /**
+       \brief Given a field update n := { r with field := v } for constructor C, assert the axioms:
+       (=> (is-C r) (= (acc_j n) (acc_j r))) for acc_j != field
+       (=> (is-C r) (= (field n) v))         for acc_j != field
+       (=> (not (is-C r)) (= n r))
+       (=> (is-C r) (is-C n))
+    */
+    void solver::assert_update_field_axioms(enode* n) {
+        m_stats.m_assert_update_field++;
+        SASSERT(is_update_field(n));
+        expr* own = n->get_expr();
+        expr* arg1 = n->get_arg(0)->get_expr();
+        func_decl* upd = n->get_decl();
+        func_decl* acc = to_func_decl(upd->get_parameter(0).get_ast());
+        func_decl* con = dt.get_accessor_constructor(acc);
+        func_decl* rec = dt.get_constructor_is(con);
+        ptr_vector<func_decl> const& accessors = *dt.get_constructor_accessors(con);
+        app_ref rec_app(m.mk_app(rec, arg1), m);
+        app_ref acc_app(m);
+        literal is_con = b_internalize(rec_app);
+        for (func_decl* acc1 : accessors) {
+            enode* arg;
+            if (acc1 == acc) {
+                arg = n->get_arg(1);
+            }
+            else {
+                acc_app = m.mk_app(acc1, arg1);
+                arg = e_internalize(acc_app);
+            }
+            app_ref acc_own(m.mk_app(acc1, own), m);
+            assert_eq_axiom(arg, acc_own, is_con);
+        }
+        // update_field is identity if 'n' is not created by a matching constructor.        
+        assert_eq_axiom(n, arg1, ~is_con);
+        app_ref n_is_con(m.mk_app(rec, own), m);
+        add_clause(~is_con, mk_literal(n_is_con));
+    }
+
+    euf::theory_var solver::mk_var(enode* n) {
+        if (is_attached_to_var(n))
+            return n->get_th_var(get_id());
+        euf::theory_var r = th_euf_solver::mk_var(n);
+        VERIFY(r == static_cast<theory_var>(m_find.mk_var()));
+        SASSERT(r == static_cast<int>(m_var_data.size()));
+        m_var_data.push_back(alloc(var_data));
+        var_data* d = m_var_data[r];
+        ctx.attach_th_var(n, this, r);
+        if (is_constructor(n)) {
+            d->m_constructor = n;
+            assert_accessor_axioms(n);
+        }
+        else if (is_update_field(n)) {
+            assert_update_field_axioms(n);
+        }
+        else {
+            sort* s = m.get_sort(n->get_expr());
+            if (dt.get_datatype_num_constructors(s) == 1)
+                assert_is_constructor_axiom(n, dt.get_datatype_constructors(s)->get(0));
+            else if (get_config().m_dt_lazy_splits == 0 || (get_config().m_dt_lazy_splits == 1 && !s->is_infinite()))
+                mk_split(r);
+        }
+        return r;
+    }
+
+
+    /**
+       \brief Create a new case split for v. That is, create the atom (is_mk v) and mark it as relevant.
+       If first is true, it means that v does not have recognizer yet.
+    */
+    void solver::mk_split(theory_var v) {
+        m_stats.m_splits++;
+
+        v = m_find.find(v);
+        enode* n = var2enode(v);
+        sort* srt = m.get_sort(n->get_expr());
+        func_decl* non_rec_c = dt.get_non_rec_constructor(srt);
+        unsigned non_rec_idx = dt.get_constructor_idx(non_rec_c);
+        var_data* d = m_var_data[v];
+        SASSERT(d->m_constructor == nullptr);
+        func_decl* r = nullptr;
+
+        TRACE("dt", tout << "non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";);
+
+        enode* recognizer = d->m_recognizers.get(non_rec_idx, nullptr);
+        if (recognizer == nullptr)
+            r = dt.get_constructor_is(non_rec_c);
+        else if (ctx.value(recognizer) != l_false)
+            // if is l_true, then we are done
+            // otherwise wait for recognizer to be assigned.
+            return;
+        else {
+            // look for a slot of d->m_recognizers that is 0, or it is not marked as relevant and is unassigned.
+            unsigned idx = 0;
+            ptr_vector<func_decl> const& constructors = *dt.get_datatype_constructors(srt);
+            for (enode* curr : d->m_recognizers) {
+                if (curr == nullptr) {
+                    // found empty slot...
+                    r = dt.get_constructor_is(constructors[idx]);
+                    break;
+                }
+                else if (ctx.value(curr) != l_false)
+                    return;
+                ++idx;
+            }
+            if (r == nullptr)
+                return; // all recognizers are asserted to false... conflict will be detected...
+        }
+        SASSERT(r != nullptr);
+        app_ref r_app(m.mk_app(r, n->get_expr()), m);
+        TRACE("dt", tout << "creating split: " << mk_pp(r_app, m) << "\n";);
+        b_internalize(r_app);
+    }
+
+    void solver::apply_sort_cnstr(enode* n, sort* s) {
+        force_push();
+        // Remark: If s is an infinite sort, then it is not necessary to create
+        // a theory variable. 
+        // 
+        // Actually, when the logical context has quantifiers, it is better to 
+        // disable this optimization.
+        // Example:
+        // 
+        //   (forall (l list) (a Int) (= (len (cons a l)) (+ (len l) 1)))
+        //   (assert (> (len a) 1)
+        //   
+        // If the theory variable is not created for 'a', then a wrong model will be generated.
+        TRACE("dt", tout << "apply_sort_cnstr: #" << n->get_expr_id() << " " << mk_pp(n->get_expr(), m) << "\n";);
+        TRACE("dt_bug",
+            tout << "apply_sort_cnstr:\n" << mk_pp(n->get_expr(), m) << " ";
+            tout << dt.is_datatype(s) << " ";
+            if (dt.is_datatype(s)) tout << "is-infinite: " << s->is_infinite() << " ";
+            if (dt.is_datatype(s)) tout << "attached: " << is_attached_to_var(n) << " ";
+            tout << "\n";);
+
+        if (!is_attached_to_var(n) &&
+            (/*ctx.has_quantifiers()*/ true ||
+                (dt.is_datatype(s) && dt.has_nested_arrays()) ||
+                (dt.is_datatype(s) && !s->is_infinite()))) {
+            mk_var(n);
+        }
+    }
+
+
+    void solver::new_eq_eh(euf::th_eq const& eq) {
+        force_push();
+        m_find.merge(eq.v1(), eq.v2());
+    }
+
+    void solver::asserted(literal lit) {
+        force_push();
+        enode* n = bool_var2enode(lit.var());
+        if (!is_recognizer(n))
+            return;
+        TRACE("dt", tout << "assigning recognizer: #" << n->get_expr_id() << " " << ctx.bpp(n) << "\n";);
+        SASSERT(n->num_args() == 1);
+        enode* arg = n->get_arg(0);
+        theory_var tv = arg->get_th_var(get_id());
+        tv = m_find.find(tv);
+        var_data* d = m_var_data[tv];
+        func_decl* r = n->get_decl();
+        func_decl* c = dt.get_recognizer_constructor(r);
+        if (!lit.sign()) {
+            SASSERT(tv != euf::null_theory_var);
+            if (d->m_constructor != nullptr && d->m_constructor->get_decl() == c)
+                return; // do nothing
+            assert_is_constructor_axiom(arg, c, lit);
+        }
+        else if (d->m_constructor == nullptr)                   // make sure a constructor is attached
+            propagate_recognizer(tv, n);
+        else if (d->m_constructor->get_decl() == c)             // conflict
+            sign_recognizer_conflict(d->m_constructor, n);
+    }
+
+    void solver::add_recognizer(theory_var v, enode* recognizer) {
+        SASSERT(is_recognizer(recognizer));
+        v = m_find.find(v);
+        var_data* d = m_var_data[v];
+        sort* s = recognizer->get_decl()->get_domain(0);
+        if (d->m_recognizers.empty()) {
+            SASSERT(dt.is_datatype(s));
+            d->m_recognizers.resize(dt.get_datatype_num_constructors(s), nullptr);
+        }
+        SASSERT(d->m_recognizers.size() == dt.get_datatype_num_constructors(s));
+        unsigned c_idx = dt.get_recognizer_constructor_idx(recognizer->get_decl());
+        if (d->m_recognizers[c_idx] == nullptr) {
+            lbool val = ctx.value(recognizer);
+            TRACE("dt", tout << "adding recognizer to v" << v << " rec: #" << recognizer->get_expr_id() << " val: " << val << "\n";);
+            if (val == l_true) {
+                // do nothing... 
+                // If recognizer assignment was already processed, then
+                // d->m_constructor is already set.
+                // Otherwise, it will be set when asserted is invoked.
+                return;
+            }
+            if (val == l_false && d->m_constructor != nullptr) {
+                func_decl* c_decl = dt.get_recognizer_constructor(recognizer->get_decl());
+                if (d->m_constructor->get_decl() == c_decl) {
+                    // conflict
+                    sign_recognizer_conflict(d->m_constructor, recognizer);
+                }
+                return;
+            }
+            SASSERT(val == l_undef || (val == l_false && d->m_constructor == nullptr));
+            d->m_recognizers[c_idx] = recognizer;
+            ctx.push(set_vector_idx_trail<euf::solver, enode>(d->m_recognizers, c_idx));
+            if (val == l_false)
+                propagate_recognizer(v, recognizer);
+        }
+    }
+
+    /**
+       \brief Propagate a recognizer assigned to false.
+    */
+    void solver::propagate_recognizer(theory_var v, enode* recognizer) {
+        SASSERT(is_recognizer(recognizer));
+        SASSERT(static_cast<int>(m_find.find(v)) == v);
+        SASSERT(ctx.value(recognizer) == l_false);
+        unsigned num_unassigned = 0;
+        unsigned unassigned_idx = UINT_MAX;
+        enode* n = var2enode(v);
+        sort* srt = m.get_sort(n->get_expr());
+        var_data* d = m_var_data[v];
+        if (d->m_recognizers.empty()) {
+            theory_var w = recognizer->get_arg(0)->get_th_var(get_id());
+            SASSERT(w != euf::null_theory_var);
+            add_recognizer(w, recognizer);
+        }
+        CTRACE("dt", d->m_recognizers.empty(), ctx.display(tout););
+        SASSERT(!d->m_recognizers.empty());
+        literal_vector lits;
+        enode_pair_vector eqs;
+        unsigned idx = 0;
+        for (enode* r : d->m_recognizers) {
+            if (!r) {
+                if (num_unassigned == 0)
+                    unassigned_idx = idx;
+                num_unassigned++;
+            }
+            else if (ctx.value(r) == l_true)
+                return; // nothing to be propagated
+            else if (ctx.value(r) == l_false) {
+                SASSERT(r->num_args() == 1);
+                lits.push_back(~ctx.enode2literal(r));
+                if (n != r->get_arg(0)) {
+                    // Argument of the current recognizer is not necessarily equal to n.
+                    // This can happen when n and r->get_arg(0) are in the same equivalence class.
+                    // We must add equality as an assumption to the conflict or propagation
+                    SASSERT(n->get_root() == r->get_arg(0)->get_root());
+                    eqs.push_back(euf::enode_pair(n, r->get_arg(0)));
+                }
+            }
+            ++idx;
+        }
+        TRACE("dt", tout << "propagate " << num_unassigned << " eqs: " << eqs.size() << "\n";);
+        if (num_unassigned == 0)
+            ctx.set_conflict(euf::th_propagation::mk(*this, lits, eqs));
+        else if (num_unassigned == 1) {
+            // propagate remaining recognizer
+            SASSERT(!lits.empty());
+            enode* r = d->m_recognizers[unassigned_idx];
+            literal consequent;
+            if (!r) {
+                ptr_vector<func_decl> const& constructors = *dt.get_datatype_constructors(srt);
+                func_decl* rec = dt.get_constructor_is(constructors[unassigned_idx]);
+                app_ref rec_app(m.mk_app(rec, n->get_expr()), m);
+                consequent = b_internalize(rec_app);
+            }
+            else
+                consequent = ctx.enode2literal(r);
+            ctx.propagate(consequent, euf::th_propagation::mk(*this, lits, eqs));
+        }
+        else if (get_config().m_dt_lazy_splits == 0 || (!srt->is_infinite() && get_config().m_dt_lazy_splits == 1))
+            // there are more than 2 unassigned recognizers...
+            // if eager splits are enabled... create new case split            
+            mk_split(v);
+    }
+
+    void solver::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) {
+        // v1 is the new root
+        TRACE("dt", tout << "merging v" << v1 << " v" << v2 << "\n";);
+        SASSERT(v1 == static_cast<int>(m_find.find(v1)));
+        var_data* d1 = m_var_data[v1];
+        var_data* d2 = m_var_data[v2];
+        auto* con1 = d1->m_constructor;
+        auto* con2 = d2->m_constructor;
+        if (con2 != nullptr) {
+            if (con1 == nullptr) {
+                ctx.push(set_ptr_trail<euf::solver, enode>(con1));
+                // check whether there is a recognizer in d1 that conflicts with con2;
+                if (!d1->m_recognizers.empty()) {
+                    unsigned c_idx = dt.get_constructor_idx(con2->get_decl());
+                    enode* recognizer = d1->m_recognizers[c_idx];
+                    if (recognizer != nullptr && ctx.value(recognizer) == l_false) {
+                        sign_recognizer_conflict(con2, recognizer);
+                        return;
+                    }
+                }
+                d1->m_constructor = con2;
+            }
+            else if (con1->get_decl() != con2->get_decl())
+                add_unit(~eq_internalize(con1->get_expr(), con2->get_expr()));
+        }
+        for (enode* e : d2->m_recognizers)
+            if (e)
+                add_recognizer(v1, e);
+    }
+
+    ptr_vector<euf::enode> const& solver::get_array_args(enode* n) {
+        m_array_args.reset();
+        array::solver* th = dynamic_cast<array::solver*>(ctx.fid2solver(m_autil.get_family_id()));
+        for (enode* p : th->parent_selects(n))
+            m_array_args.push_back(p);
+        app_ref def(m_autil.mk_default(n->get_expr()), m);
+        m_array_args.push_back(ctx.get_enode(def));
+        return m_array_args;
+    }
+
+    // Assuming `app` is equal to a constructor term, return the constructor enode
+    inline euf::enode* solver::oc_get_cstor(enode* app) {
+        theory_var v = app->get_root()->get_th_var(get_id());
+        SASSERT(v != euf::null_theory_var);
+        v = m_find.find(v);
+        var_data* d = m_var_data[v];
+        SASSERT(d->m_constructor);
+        return d->m_constructor;
+    }
+
+    void solver::explain_is_child(enode* parent, enode* child) {
+        enode* parentc = oc_get_cstor(parent);
+        if (parent != parentc)
+            m_used_eqs.push_back(enode_pair(parent, parentc));
+
+        // collect equalities on all children that may have been used.
+        bool found = false;
+        auto add = [&](enode* arg) {
+            if (arg->get_root() == child->get_root()) {
+                if (arg != child)
+                    m_used_eqs.push_back(enode_pair(arg, child));
+                found = true;
+            }
+        };
+        for (enode* arg : euf::enode_args(parentc)) {
+            add(arg);
+            sort* s = m.get_sort(arg->get_expr());
+            if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s)))
+                for (enode* aarg : get_array_args(arg))
+                    add(aarg);
+        }
+        VERIFY(found);
+    }
+
+    // explain the cycle root -> ... -> app -> root
+    void solver::occurs_check_explain(enode* app, enode* root) {
+        TRACE("dt", tout << "occurs_check_explain " << ctx.bpp(app) << " <-> " << ctx.bpp(root) << "\n";);
+
+        // first: explain that root=v, given that app=cstor(...,v,...)
+
+        explain_is_child(app, root);
+
+        // now explain app=cstor(..,v,..) where v=root, and recurse with parent of app
+        while (app->get_root() != root->get_root()) {
+            enode* parent_app = m_parent[app->get_root()];
+            explain_is_child(parent_app, app);
+            SASSERT(is_constructor(parent_app));
+            app = parent_app;
+        }
+
+        SASSERT(app->get_root() == root->get_root());
+        if (app != root)
+            m_used_eqs.push_back(enode_pair(app, root));
+
+        TRACE("dt",
+            tout << "occurs_check\n"; for (enode_pair const& p : m_used_eqs) tout << ctx.bpp(p.first) << " - " << ctx.bpp(p.second) << " ";);
+    }
+
+    // start exploring subgraph below `app`
+    bool solver::occurs_check_enter(enode* app) {
+        app = app->get_root();
+        theory_var v = app->get_th_var(get_id());
+        if (v == euf::null_theory_var)
+            return false;
+        v = m_find.find(v);
+        var_data* d = m_var_data[v];
+        if (!d->m_constructor)
+            return false;
+        enode* parent = d->m_constructor;
+        oc_mark_on_stack(parent);
+        for (enode* arg : euf::enode_args(parent)) {
+            if (oc_cycle_free(arg))
+                continue;
+            if (oc_on_stack(arg)) {
+                // arg was explored before app, and is still on the stack: cycle
+                occurs_check_explain(parent, arg);
+                return true;
+            }
+            // explore `arg` (with parent)
+            expr* earg = arg->get_expr();
+            sort* s = m.get_sort(earg);
+            if (dt.is_datatype(s)) {
+                m_parent.insert(arg->get_root(), parent);
+                oc_push_stack(arg);
+            }
+            else if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s))) {
+                for (enode* aarg : get_array_args(arg)) {
+                    if (oc_cycle_free(aarg))
+                        continue;
+                    if (oc_on_stack(aarg)) {
+                        occurs_check_explain(parent, aarg);
+                        return true;
+                    }
+                    if (is_datatype(aarg)) {
+                        m_parent.insert(aarg->get_root(), parent);
+                        oc_push_stack(aarg);
+                    }
+                }
+            }
+        }
+        return false;
+    }
+
+    /**
+       \brief Check if n can be reached starting from n and following equalities and constructors.
+       For example, occur_check(a1) returns true in the following set of equalities:
+       a1 = cons(v1, a2)
+       a2 = cons(v2, a3)
+       a3 = cons(v3, a1)
+    */
+    bool solver::occurs_check(enode* n) {
+        TRACE("dt", tout << "occurs check: " << ctx.bpp(n) << "\n";);
+        m_stats.m_occurs_check++;
+
+        bool res = false;
+        oc_push_stack(n);
+
+        // DFS traversal from `n`. Look at top element and explore it.
+        while (!res && !m_dfs.empty()) {
+            stack_op op = m_dfs.back().first;
+            enode* app = m_dfs.back().second;
+            m_dfs.pop_back();
+
+            if (oc_cycle_free(app))
+                continue;
+
+            TRACE("dt", tout << "occurs check loop: " << ctx.bpp(app) << (op == ENTER ? " enter" : " exit") << "\n";);
+
+            switch (op) {
+            case ENTER:
+                res = occurs_check_enter(app);
+                break;
+
+            case EXIT:
+                oc_mark_cycle_free(app);
+                break;
+            }
+        }
+
+        if (res) {
+            clear_mark();
+            ctx.set_conflict(euf::th_propagation::mk(*this, m_used_eqs));
+        }
+        return res;
+    }
+
+    sat::check_result solver::check() {
+        force_push();
+        int num_vars = get_num_vars();
+        sat::check_result r = sat::check_result::CR_DONE;
+        final_check_st _guard(*this);
+        int start = s().rand()();
+        for (int i = 0; i < num_vars; i++) {
+            theory_var v = (i + start) % num_vars;
+            if (v == static_cast<int>(m_find.find(v))) {
+                enode* node = var2enode(v);
+                if (!is_datatype(node))
+                    continue;
+                if (!oc_cycle_free(node) && occurs_check(node))
+                    // conflict was detected... 
+                    return sat::check_result::CR_CONTINUE;
+                if (get_config().m_dt_lazy_splits > 0) {
+                    // using lazy case splits...
+                    var_data* d = m_var_data[v];
+                    if (d->m_constructor == nullptr) {
+                        clear_mark();
+                        mk_split(v);
+                        r = sat::check_result::CR_CONTINUE;
+                    }
+                }
+            }
+        }
+        return r;
+    }
+
+    void solver::pop_core(unsigned num_scopes) {
+        th_euf_solver::pop_core(num_scopes);
+        std::for_each(m_var_data.begin() + get_num_vars(), m_var_data.end(), delete_proc<var_data>());
+        m_var_data.shrink(get_num_vars());
+        SASSERT(m_find.get_num_vars() == m_var_data.size());
+        SASSERT(m_find.get_num_vars() == get_num_vars());
+    }
+
+    void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) {
+        auto& jst = euf::th_propagation::from_index(idx);
+        ctx.get_antecedents(l, jst, r, probing);
+    }
+
+    void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
+        theory_var v = n->get_th_var(get_id());
+        v = m_find.find(v);
+        SASSERT(v != euf::null_theory_var);
+        enode* con = m_var_data[v]->m_constructor;
+        func_decl* c_decl = con->get_decl();
+        m_args.reset();
+        for (enode* arg : euf::enode_args(m_var_data[v]->m_constructor))
+            m_args.push_back(values.get(arg->get_root_id()));
+        values.set(n->get_root_id(), m.mk_app(c_decl, m_args));
+    }
+
+    void solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
+        theory_var v = n->get_th_var(get_id());
+        for (enode* arg : euf::enode_args(m_var_data[m_find.find(v)]->m_constructor))
+            dep.add(n, arg);
+    }
+
+    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+        if (!visit_rec(m, e, sign, root, redundant)) {
+            TRACE("dt", tout << mk_pp(e, m) << "\n";);
+            return sat::null_literal;
+        }
+        auto lit = ctx.expr2literal(e);
+        if (sign)
+            lit.neg();
+        return lit;
+    }
+
+    void solver::internalize(expr* e, bool redundant) {
+        visit_rec(m, e, false, false, redundant);
+    }
+
+    bool solver::visit(expr* e) {
+        if (visited(e))
+            return true;
+        if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
+            ctx.internalize(e, m_is_redundant);
+            if (is_datatype(e))
+                mk_var(expr2enode(e));
+            return true;
+        }
+        m_stack.push_back(sat::eframe(e));
+        return false;
+    }
+
+    bool solver::visited(expr* e) {
+        euf::enode* n = expr2enode(e);
+        return n && n->is_attached_to(get_id());
+    }
+
+    bool solver::post_visit(expr* term, bool sign, bool root) {
+        euf::enode* n = expr2enode(term);
+        SASSERT(!n || !n->is_attached_to(get_id()));
+        if (!n)
+            n = mk_enode(term);
+        SASSERT(!n->is_attached_to(get_id()));
+        if (is_constructor(term) || is_update_field(term)) {
+            for (enode* arg : euf::enode_args(n)) {
+                sort* s = m.get_sort(arg->get_expr());
+                if (dt.is_datatype(s))
+                    mk_var(arg);
+                else if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s))) {
+                    app_ref def(m_autil.mk_default(arg->get_expr()), m);
+                    mk_var(e_internalize(def));
+                }
+            }
+            mk_var(n);
+        }
+        else if (is_recognizer(term)) {
+            enode* arg = n->get_arg(0);
+            theory_var v = mk_var(arg);
+            add_recognizer(v, n);
+            mk_var(n);
+        }
+        else {
+            SASSERT(is_accessor(term));
+            SASSERT(n->num_args() == 1);
+            mk_var(n->get_arg(0));
+        }
+        return true;
+    }
+
+    void solver::collect_statistics(::statistics& st) const {
+        st.update("datatype occurs check", m_stats.m_occurs_check);
+        st.update("datatype splits", m_stats.m_splits);
+        st.update("datatype constructor ax", m_stats.m_assert_cnstr);
+        st.update("datatype accessor ax", m_stats.m_assert_accessor);
+        st.update("datatype update ax", m_stats.m_assert_update_field);
+    }
+
+    std::ostream& solver::display(std::ostream& out) const {
+        unsigned num_vars = get_num_vars();
+        if (num_vars > 0)
+            out << "Theory datatype:\n";
+        for (unsigned v = 0; v < num_vars; v++)
+            display_var(out, v);
+        return out;
+    }
+
+    void solver::display_var(std::ostream& out, theory_var v) const {
+        var_data* d = m_var_data[v];
+        out << "v" << v << " #" << var2expr(v)->get_id() << " -> v" << m_find.find(v) << " ";
+        if (d->m_constructor)
+            out << ctx.bpp(d->m_constructor);
+        else
+            out << "(null)";
+        out << "\n";
+    }
+}
diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h
new file mode 100644
index 000000000..7015cfdd1
--- /dev/null
+++ b/src/sat/smt/dt_solver.h
@@ -0,0 +1,159 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    dt_solver.h
+
+Abstract:
+
+    Theory plugin for altegraic datatypes
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-08
+
+--*/
+#pragma once
+
+#include "sat/smt/sat_th.h"
+#include "ast/datatype_decl_plugin.h"
+#include "ast/array_decl_plugin.h"
+
+namespace euf {
+    class solver;
+}
+
+namespace dt {
+
+    class solver : public euf::th_euf_solver {
+        typedef euf::theory_var theory_var;
+        typedef euf::theory_id theory_id;
+        typedef euf::enode enode;
+        typedef euf::enode_pair enode_pair;
+        typedef euf::enode_pair_vector enode_pair_vector;
+        typedef sat::bool_var bool_var;
+        typedef sat::literal literal;
+        typedef sat::literal_vector literal_vector;
+        typedef union_find<solver, euf::solver>  dt_union_find;
+
+        struct var_data {
+            ptr_vector<enode> m_recognizers; //!< recognizers of this equivalence class that are being watched.
+            enode *           m_constructor; //!< constructor of this equivalence class, 0 if there is no constructor in the eqc.
+            var_data():
+                m_constructor(nullptr) {
+            }
+        };
+
+        // class for managing state of final_check
+        class final_check_st {
+            solver& s;
+        public:
+            final_check_st(solver& s);
+            ~final_check_st();
+        };
+
+        struct stats {
+            unsigned   m_occurs_check, m_splits;
+            unsigned   m_assert_cnstr, m_assert_accessor, m_assert_update_field;
+            void reset() { memset(this, 0, sizeof(*this)); }
+            stats() { reset(); }
+        };
+
+        datatype_util         dt;
+        array_util            m_autil;
+        stats                 m_stats;
+        ptr_vector<var_data>  m_var_data;
+        dt_union_find         m_find;
+        expr_ref_vector       m_args;
+
+        bool is_constructor(expr * f) const { return dt.is_constructor(f); }
+        bool is_recognizer(expr * f) const { return dt.is_recognizer(f); }
+        bool is_accessor(expr * f) const { return dt.is_accessor(f); }
+        bool is_update_field(expr * f) const { return dt.is_update_field(f); }
+
+        bool is_constructor(enode * n) const { return is_constructor(n->get_expr()); }
+        bool is_recognizer(enode * n) const { return is_recognizer(n->get_expr()); }
+        bool is_accessor(enode * n) const { return is_accessor(n->get_expr()); }
+        bool is_update_field(enode * n) const { return dt.is_update_field(n->get_expr()); }
+
+        bool is_datatype(expr* e) const { return dt.is_datatype(m.get_sort(e)); }
+        bool is_datatype(enode* n) const { return is_datatype(n->get_expr()); }
+
+        void assert_eq_axiom(enode * lhs, expr * rhs, literal antecedent = sat::null_literal);
+        void assert_is_constructor_axiom(enode * n, func_decl * c, literal antecedent = sat::null_literal);
+        void assert_accessor_axioms(enode * n);
+        void assert_update_field_axioms(enode * n);
+        void add_recognizer(theory_var v, enode * recognizer);
+        void propagate_recognizer(theory_var v, enode * r);
+        void sign_recognizer_conflict(enode * c, enode * r);
+
+        typedef enum { ENTER, EXIT } stack_op;
+        typedef obj_map<enode, enode*> parent_tbl;
+        typedef std::pair<stack_op, enode*> stack_entry;
+
+        ptr_vector<enode>     m_to_unmark1;
+        ptr_vector<enode>     m_to_unmark2;
+        enode_pair_vector     m_used_eqs; // conflict, if any
+        parent_tbl            m_parent; // parent explanation for occurs_check
+        svector<stack_entry>  m_dfs; // stack for DFS for occurs_check
+
+        void clear_mark();
+
+        void oc_mark_on_stack(enode * n);
+        bool oc_on_stack(enode * n) const { return n->get_root()->is_marked1(); }
+
+        void oc_mark_cycle_free(enode * n);
+        bool oc_cycle_free(enode * n) const { return n->get_root()->is_marked2(); }
+
+        void oc_push_stack(enode * n);
+        ptr_vector<enode> m_array_args;
+        ptr_vector<enode> const& get_array_args(enode* n);
+
+        void pop_core(unsigned n) override;
+
+        enode * oc_get_cstor(enode * n);
+        bool occurs_check(enode * n);
+        bool occurs_check_enter(enode * n);
+        void occurs_check_explain(enode * top, enode * root);
+        void explain_is_child(enode* parent, enode* child);
+
+        void mk_split(theory_var v);
+
+        void display_var(std::ostream & out, theory_var v) const;
+
+        // internalize
+        bool visit(expr* e) override;
+        bool visited(expr* e) override;
+        bool post_visit(expr* e, bool sign, bool root) override;
+        void clone_var(solver& src, theory_var v);
+        
+    public:
+        solver(euf::solver& ctx, theory_id id);
+        ~solver() override;
+
+        bool is_external(bool_var v) override { return false; }
+        void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override;
+        void asserted(literal l) override;
+        sat::check_result check() override;
+
+        std::ostream& display(std::ostream& out) const override;
+        std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { return euf::th_propagation::from_index(idx).display(out); }
+        std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { return display_justification(out, idx); }
+        void collect_statistics(statistics& st) const override;
+        euf::th_solver* clone(euf::solver& ctx) override;
+        void new_eq_eh(euf::th_eq const& eq) override;
+        bool unit_propagate() override { return false; }
+        void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
+        void add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
+        sat::literal internalize(expr* e, bool sign, bool root, bool redundant) override;
+        void internalize(expr* e, bool redundant) override;
+        euf::theory_var mk_var(euf::enode* n) override;
+        void apply_sort_cnstr(euf::enode* n, sort* s) override;
+        bool is_shared(theory_var v) const override { return false; }
+
+        void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
+        void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
+        void unmerge_eh(theory_var v1, theory_var v2) {}
+    };
+}
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index 9f61d6f48..2a1670cc7 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -134,14 +134,14 @@ namespace euf {
             lit = lit2;
         }
 
-        m_var2expr.reserve(v + 1, nullptr);
-        if (m_var2expr[v]) {
+        m_bool_var2expr.reserve(v + 1, nullptr);
+        if (m_bool_var2expr[v]) {
             SASSERT(m_egraph.find(e));
             SASSERT(m_egraph.find(e)->bool_var() == v);
             return lit;
         }
         TRACE("euf", tout << "attach " << v << " " << mk_bounded_pp(e, m) << "\n";);
-        m_var2expr[v] = e;
+        m_bool_var2expr[v] = e;
         m_var_trail.push_back(v);
         enode* n = m_egraph.find(e);
         if (!n) 
@@ -367,12 +367,15 @@ namespace euf {
                 return true;
 
         return false;
-
     }
 
     expr_ref solver::mk_eq(expr* e1, expr* e2) {
-        if (e1 == e2)
+        expr_ref _e1(e1, m);
+        expr_ref _e2(e2, m);
+        if (m.are_equal(e1, e2))
             return expr_ref(m.mk_true(), m);
+        if (m.are_distinct(e1, e2))
+            return expr_ref(m.mk_false(), m);
         expr_ref r(m.mk_eq(e2, e1), m);
         if (!m_egraph.find(r))
             r = m.mk_eq(e1, e2);
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index cbb49b847..281906eae 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -84,7 +84,7 @@ namespace euf {
 
     void solver::log_antecedents(std::ostream& out, literal l, literal_vector const& r) {
         for (sat::literal l : r) {
-            expr* n = m_var2expr[l.var()];
+            expr* n = m_bool_var2expr[l.var()];
             out << ~l << ": ";
             if (!l.sign()) out << "! ";
             out << mk_bounded_pp(n, m) << "\n";
@@ -93,7 +93,7 @@ namespace euf {
         if (l != sat::null_literal) {
             out << l << ": ";
             if (l.sign()) out << "! ";
-            expr* n = m_var2expr[l.var()];
+            expr* n = m_bool_var2expr[l.var()];
             out << mk_bounded_pp(n, m) << "\n";
         }
     }
diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp
index 8896954c0..77590346b 100644
--- a/src/sat/smt/euf_relevancy.cpp
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -64,7 +64,7 @@ namespace euf {
         m_relevant_expr_ids.resize(max_id + 1, false);
         auto const& core = m_dual_solver->core();
         for (auto lit : core) {
-            expr* e = m_var2expr.get(lit.var(), nullptr);
+            expr* e = m_bool_var2expr.get(lit.var(), nullptr);
             if (e)
                 todo.push_back(e);
         }
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 2b1da2240..bdac9b3e8 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -26,6 +26,7 @@ Author:
 #include "sat/smt/arith_solver.h"
 #include "sat/smt/q_solver.h"
 #include "sat/smt/fpa_solver.h"
+#include "sat/smt/dt_solver.h"
 
 namespace euf {
 
@@ -60,9 +61,9 @@ namespace euf {
     * retrieve extension that is associated with Boolean variable.
     */
     th_solver* solver::bool_var2solver(sat::bool_var v) {
-        if (v >= m_var2expr.size())
+        if (v >= m_bool_var2expr.size())
             return nullptr;
-        expr* e = m_var2expr[v];
+        expr* e = m_bool_var2expr[v];
         if (!e)
             return nullptr;
         return expr2solver(e);
@@ -81,10 +82,8 @@ namespace euf {
         auto* ext = m_id2solver.get(fid, nullptr);
         if (ext)
             return ext;
-        ext = alloc(q::solver, *this);
-        ext->set_solver(m_solver);
-        ext->push_scopes(s().num_scopes());
-        add_solver(fid, ext);
+        ext = alloc(q::solver, *this, fid);
+        add_solver(ext);
         return ext;
     }
 
@@ -101,34 +100,37 @@ namespace euf {
         array_util au(m);
         fpa_util fpa(m);
         arith_util arith(m);
-        if (pb.get_family_id() == fid) 
+        datatype_util dt(m);
+        if (pb.get_family_id() == fid)
             ext = alloc(sat::ba_solver, *this, fid);
-        else if (bvu.get_family_id() == fid) 
+        else if (bvu.get_family_id() == fid)
             ext = alloc(bv::solver, *this, fid);
-        else if (au.get_family_id() == fid) 
+        else if (au.get_family_id() == fid)
             ext = alloc(array::solver, *this, fid);
-        else if (fpa.get_family_id() == fid) 
+        else if (fpa.get_family_id() == fid)
             ext = alloc(fpa::solver, *this);
         else if (arith.get_family_id() == fid)
             ext = alloc(arith::solver, *this, fid);
+        else if (dt.get_family_id() == fid)
+            ext = alloc(dt::solver, *this, fid);
         
-        if (ext) {
-            if (use_drat())
-                s().get_drat().add_theory(fid, ext->name());
-            ext->set_solver(m_solver);
-            ext->push_scopes(s().num_scopes());
-            add_solver(fid, ext);
-            if (ext->use_diseqs())
-                m_egraph.set_th_propagates_diseqs(fid);
-        }
+        if (ext) 
+            add_solver(ext);        
         else if (f) 
             unhandled_function(f);
         return ext;
     }
 
-    void solver::add_solver(family_id fid, th_solver* th) {
+    void solver::add_solver(th_solver* th) {
+        family_id fid = th->get_id();
+        if (use_drat())
+            s().get_drat().add_theory(fid, th->name());
+        th->set_solver(m_solver);
+        th->push_scopes(s().num_scopes());
         m_solvers.push_back(th);
         m_id2solver.setx(fid, th, nullptr);
+        if (th->use_diseqs())
+            m_egraph.set_th_propagates_diseqs(fid);
     }
 
     void solver::unhandled_function(func_decl* f) {
@@ -146,7 +148,7 @@ namespace euf {
     }
 
     bool solver::is_external(bool_var v) {
-        if (nullptr != m_var2expr.get(v, nullptr))
+        if (nullptr != m_bool_var2expr.get(v, nullptr))
             return true;
         for (auto* s : m_solvers)
             if (s->is_external(v))
@@ -154,10 +156,18 @@ namespace euf {
         return false;
     }
 
-    bool solver::propagate(literal l, ext_constraint_idx idx) { 
+    bool solver::propagated(literal l, ext_constraint_idx idx) { 
         auto* ext = sat::constraint_base::to_extension(idx);
         SASSERT(ext != this);
-        return ext->propagate(l, idx);
+        return ext->propagated(l, idx);
+    }
+
+    void solver::set_conflict(ext_constraint_idx idx) {
+        s().set_conflict(sat::justification::mk_ext_justification(s().scope_lvl(), idx));
+    }
+
+    void solver::propagate(literal lit, ext_justification_idx idx) {
+        s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx));
     }
 
     void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) {
@@ -192,6 +202,23 @@ namespace euf {
             log_antecedents(l, r);
     }
 
+    void solver::get_antecedents(literal l, th_propagation& jst, literal_vector& r, bool probing) {
+        for (auto lit : euf::th_propagation::lits(jst))
+            r.push_back(lit);
+        for (auto eq : euf::th_propagation::eqs(jst))
+            add_antecedent(eq.first, eq.second);
+
+        if (!probing && use_drat()) {
+            literal_vector lits;
+            for (auto lit : euf::th_propagation::lits(jst))
+                lits.push_back(~lit);
+            lits.push_back(l);
+            get_drat().add(lits, sat::status::th(m_is_redundant, jst.ext().get_id()));
+            for (auto eq : euf::th_propagation::eqs(jst))
+                IF_VERBOSE(0, verbose_stream() << "drat-log with equalities is TBD " << eq.first->get_expr_id() << "\n");
+        }
+    }
+
     void solver::add_antecedent(enode* a, enode* b) {
         m_egraph.explain_eq<size_t>(m_explain, a, b);
     }
@@ -217,7 +244,7 @@ namespace euf {
             m_egraph.explain<size_t>(m_explain);
             break;
         case constraint::kind_t::eq:
-            e = m_var2expr[l.var()];
+            e = m_bool_var2expr[l.var()];
             n = m_egraph.find(e);
             SASSERT(n);
             SASSERT(n->is_equality());
@@ -225,7 +252,7 @@ namespace euf {
             m_egraph.explain_eq<size_t>(m_explain, n->get_arg(0), n->get_arg(1));
             break;
         case constraint::kind_t::lit:
-            e = m_var2expr[l.var()];
+            e = m_bool_var2expr[l.var()];
             n = m_egraph.find(e);
             SASSERT(n);
             SASSERT(m.is_bool(n->get_expr()));
@@ -238,7 +265,7 @@ namespace euf {
     }
 
     void solver::asserted(literal l) {
-        expr* e = m_var2expr.get(l.var(), nullptr);
+        expr* e = m_bool_var2expr.get(l.var(), nullptr);
         if (!e) {
             TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << "\n";);
             return;        
@@ -421,7 +448,7 @@ namespace euf {
         m_egraph.pop(n);
         scope const & s = m_scopes[m_scopes.size() - n];
         for (unsigned i = m_var_trail.size(); i-- > s.m_var_lim; )
-            m_var2expr[m_var_trail[i]] = nullptr;
+            m_bool_var2expr[m_var_trail[i]] = nullptr;
         m_var_trail.shrink(s.m_var_lim);        
         m_scopes.shrink(m_scopes.size() - n);
         SASSERT(m_egraph.num_scopes() == m_scopes.size());
@@ -534,7 +561,7 @@ namespace euf {
         m_egraph.display(out);
         out << "bool-vars\n";
         for (unsigned v : m_var_trail) {
-            expr* e = m_var2expr[v];
+            expr* e = m_bool_var2expr[v];
             out << v << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1) << "\n";        
         }
         for (auto* e : m_solvers)
@@ -584,6 +611,17 @@ namespace euf {
         st.update("euf ackerman", m_stats.m_ackerman);
     }
 
+    enode* solver::copy(solver& dst_ctx, enode* src_n) {
+        if (!src_n)
+            return nullptr;
+        ast_translation tr(m, dst_ctx.get_manager(), false);
+        expr* e1 = src_n->get_expr();
+        expr* e2 = tr(e1);
+        euf::enode* n2 = dst_ctx.get_enode(e2);
+        SASSERT(n2);
+        return n2;
+    }
+
     sat::extension* solver::copy(sat::solver* s) { 
         auto* r = alloc(solver, *m_to_m, *m_to_si);
         r->m_config = m_config;
@@ -596,10 +634,12 @@ namespace euf {
         };
         r->m_egraph.copy_from(m_egraph, copy_justification);        
         r->set_solver(s);
-        for (unsigned i = 0; i < m_id2solver.size(); ++i) {
-            auto* e = m_id2solver[i];
-            if (e)
-                r->add_solver(i, e->clone(s, *r));
+        for (auto* s_orig : m_id2solver) {
+            if (s_orig) {
+                auto* s_clone = s_orig->clone(*r);
+                r->add_solver(s_clone);
+                s_clone->set_solver(s);
+            }
         }
         return r;
     }
@@ -653,8 +693,8 @@ namespace euf {
     unsigned solver::max_var(unsigned w) const { 
         for (auto* e : m_solvers)
             w = e->max_var(w);
-        for (unsigned sz = m_var2expr.size(); sz-- > 0; ) {
-            expr* n = m_var2expr[sz];
+        for (unsigned sz = m_bool_var2expr.size(); sz-- > 0; ) {
+            expr* n = m_bool_var2expr[sz];
             if (n && m.is_bool(n)) {
                 w = std::max(w, sz);
                 break;
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 8cee826ca..2c8d46be3 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -94,7 +94,7 @@ namespace euf {
         scoped_ptr<sat::dual_solver> m_dual_solver;
         user::solver*          m_user_propagator{ nullptr };
 
-        ptr_vector<expr>                                m_var2expr;
+        ptr_vector<expr>                                m_bool_var2expr;
         ptr_vector<size_t>                              m_explain;
         unsigned                                        m_num_scopes{ 0 };
         unsigned_vector                                 m_var_trail;
@@ -132,8 +132,7 @@ namespace euf {
         th_solver* quantifier2solver();
         th_solver* expr2solver(expr* e);
         th_solver* bool_var2solver(sat::bool_var v);
-        th_solver* fid2solver(family_id fid) const { return m_id2solver.get(fid, nullptr); }
-        void add_solver(family_id fid, th_solver* th);
+        void add_solver(th_solver* th);
         void init_ackerman();
 
         // model building
@@ -214,10 +213,13 @@ namespace euf {
         ast_manager& get_manager() { return m; }
         enode* get_enode(expr* e) const { return m_egraph.find(e); }
         sat::literal expr2literal(expr* e) const { return enode2literal(get_enode(e)); }
-        sat::literal enode2literal(enode* e) const { return sat::literal(e->bool_var(), false); }
+        sat::literal enode2literal(enode* n) const { return sat::literal(n->bool_var(), false); }
+        lbool value(enode* n) const { return s().value(enode2literal(n)); }
         smt_params const& get_config() const { return m_config; }
         region& get_region() { return m_trail.get_region(); }
         egraph& get_egraph() { return m_egraph; }
+        th_solver* fid2solver(family_id fid) const { return m_id2solver.get(fid, nullptr); }
+
         template <typename C>
         void push(C const& c) { m_trail.push(c); }
         template <typename V>
@@ -238,13 +240,22 @@ namespace euf {
         double get_reward(literal l, ext_constraint_idx idx, sat::literal_occs_fun& occs) const override;
         bool is_extended_binary(ext_justification_idx idx, literal_vector& r) override;
         bool is_external(bool_var v) override;
-        bool propagate(literal l, ext_constraint_idx idx) override;
+        bool propagated(literal l, ext_constraint_idx idx) override;
         bool unit_propagate() override;
-        bool propagate(enode* a, enode* b, ext_justification_idx);
+
+        void propagate(literal lit, ext_justification_idx idx);
+        bool propagate(enode* a, enode* b, ext_justification_idx idx);
+        void set_conflict(ext_justification_idx idx);
+
+        void propagate(literal lit, th_propagation* p) { propagate(lit, p->to_index()); }
+        bool propagate(enode* a, enode* b, th_propagation* p) { return propagate(a, b, p->to_index()); }
+        void set_conflict(th_propagation* p) { set_conflict(p->to_index()); }
+
         bool set_root(literal l, literal r) override;
         void flush_roots() override;
 
         void get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) override;
+        void get_antecedents(literal l, th_propagation& jst, literal_vector& r, bool probing);
         void add_antecedent(enode* a, enode* b);
         void asserted(literal l) override;
         sat::check_result check() override;
@@ -260,8 +271,10 @@ namespace euf {
         std::ostream& display(std::ostream& out) const override;
         std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override;
         std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const override;
+        euf::egraph::b_pp bpp(enode* n) { return m_egraph.bpp(n); }
         void collect_statistics(statistics& st) const override;
         extension* copy(sat::solver* s) override;
+        enode* copy(solver& dst_ctx, enode* src_n);
         void find_mutexes(literal_vector& lits, vector<literal_vector>& mutexes) override;
         void gc() override;
         void pop_reinit() override;
@@ -288,7 +301,7 @@ namespace euf {
         expr_ref mk_eq(expr* e1, expr* e2);
         expr_ref mk_eq(euf::enode* n1, euf::enode* n2) { return mk_eq(n1->get_expr(), n2->get_expr()); }
         euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, n, args); }
-        expr* bool_var2expr(sat::bool_var v) { return m_var2expr.get(v, nullptr); }
+        expr* bool_var2expr(sat::bool_var v) { return m_bool_var2expr.get(v, nullptr); }
         sat::literal attach_lit(sat::literal lit, expr* e);
         void unhandled_function(func_decl* f);
         th_rewriter& get_rewriter() { return m_rewriter; }
diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp
index ceb36daf3..63a9ba2a1 100644
--- a/src/sat/smt/fpa_solver.cpp
+++ b/src/sat/smt/fpa_solver.cpp
@@ -42,8 +42,7 @@ namespace fpa {
     }
 
 
-    expr_ref solver::convert(expr* e)
-    {
+    expr_ref solver::convert(expr* e) {    
         expr_ref res(m);
         expr* ccnv;
         TRACE("t_fpa", tout << "converting " << mk_ismt2_pp(e, m) << std::endl;);
@@ -105,6 +104,8 @@ namespace fpa {
     }
 
     bool solver::visit(expr* e) {
+        if (visited(e))
+            return true;
         if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
             ctx.internalize(e, m_is_redundant);
             return true;
@@ -161,12 +162,12 @@ namespace fpa {
         SASSERT(m_fpa_util.is_float(n->get_expr()) || m_fpa_util.is_rm(n->get_expr()));
         SASSERT(n->get_decl()->get_range() == s);
 
-        expr* owner = n->get_expr();
-
         if (is_attached_to_var(n))
             return;
         attach_new_th_var(n);
 
+        expr* owner = n->get_expr();
+
         if (m_fpa_util.is_rm(s) && !m_fpa_util.is_bv2rm(owner)) {
             // For every RM term, we need to make sure that it's
             // associated bit-vector is within the valid range.
diff --git a/src/sat/smt/fpa_solver.h b/src/sat/smt/fpa_solver.h
index 386da39ac..a7e866ccd 100644
--- a/src/sat/smt/fpa_solver.h
+++ b/src/sat/smt/fpa_solver.h
@@ -71,7 +71,7 @@ namespace fpa {
         void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override { UNREACHABLE(); }
         sat::check_result check() override { return sat::check_result::CR_DONE; }
 
-        euf::th_solver* clone(sat::solver*, euf::solver& ctx) override { return alloc(solver, ctx); }
+        euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); }
 
     };
 
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index eba177f1a..f007fce83 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -94,7 +94,8 @@ namespace q {
         init_solver();
         ::solver::scoped_push _sp(*m_solver);
         expr_ref_vector vars(m);
-        expr_ref body = specialize(q, vars);        
+        quantifier* q_flat = qs.flatten(q);
+        expr_ref body = specialize(q_flat, vars);    
         m_solver->assert_expr(body);
         lbool r = m_solver->check_sat(0, nullptr);
         if (r == l_undef)
@@ -105,17 +106,17 @@ namespace q {
         m_solver->get_model(mdl0); 
         expr_ref proj(m);
         auto add_projection = [&](model& mdl, bool inv) {
-            proj = project(mdl, q, vars, inv);
+            proj = project(mdl, q_flat, vars, inv);
             if (!proj)
                 return;
             if (is_forall(q))
                 qs.add_clause(~ctx.expr2literal(q), ctx.b_internalize(proj));
             else
-                qs.add_clause(ctx.expr2literal(q), ~ctx.b_internalize(proj));
+                qs.add_clause(ctx.expr2literal(q),  ~ctx.b_internalize(proj));
         };
         bool added = false;
 #if 0
-        m_model_finder.restrict_instantiations(*m_solver, *mdl0, q, vars);
+        m_model_finder.restrict_instantiations(*m_solver, *mdl0, q_flat, vars);
         for (unsigned i = 0; i < m_max_cex && l_true == m_solver->check_sat(0, nullptr); ++i) {
             m_solver->get_model(mdl1);
             add_projection(*mdl1, true);
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 6f2d73a27..2cc4d84ec 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -24,8 +24,8 @@ Author:
 
 namespace q {
 
-    solver::solver(euf::solver& ctx):
-        th_euf_solver(ctx, symbol("quant"), ctx.get_manager().get_family_id(symbol("quant"))),
+    solver::solver(euf::solver& ctx, family_id fid) :
+        th_euf_solver(ctx, ctx.get_manager().get_family_name(fid), fid),
         m_mbqi(ctx,  *this)
     {}
 
@@ -61,8 +61,9 @@ namespace q {
         st.update("quantifier asserts", m_stats.m_num_quantifier_asserts);
     }
 
-    euf::th_solver* solver::clone(sat::solver* s, euf::solver& ctx) {
-        return alloc(solver, ctx);
+    euf::th_solver* solver::clone(euf::solver& ctx) {
+        family_id fid = ctx.get_manager().mk_family_id(symbol("quant"));
+        return alloc(solver, ctx, fid);
     }
 
     bool solver::unit_propagate() {
diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h
index 08c5c8fb3..9cbe98f14 100644
--- a/src/sat/smt/q_solver.h
+++ b/src/sat/smt/q_solver.h
@@ -53,7 +53,7 @@ namespace q {
 
     public:
 
-        solver(euf::solver& ctx);
+        solver(euf::solver& ctx, family_id fid);
         ~solver() override {}
         bool is_external(sat::bool_var v) override { return false; }
         void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override {}
@@ -64,7 +64,7 @@ namespace q {
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { UNREACHABLE(); return out; }
         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { UNREACHABLE(); return out; }
         void collect_statistics(statistics& st) const override;
-        euf::th_solver* clone(sat::solver* s, euf::solver& ctx) override;
+        euf::th_solver* clone(euf::solver& ctx) override;
         bool unit_propagate() override;
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
         void internalize(expr* e, bool redundant) override { UNREACHABLE(); }
diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp
index 137c7fb31..07b9e3323 100644
--- a/src/sat/smt/sat_th.cpp
+++ b/src/sat/smt/sat_th.cpp
@@ -201,30 +201,61 @@ namespace euf {
     }
 
     sat::literal th_euf_solver::eq_internalize(expr* a, expr* b) { 
-        return b_internalize(ctx.mk_eq(a, b)); 
+        expr_ref eq(ctx.mk_eq(a, b), m);
+        return b_internalize(eq); 
     }
 
     unsigned th_propagation::get_obj_size(unsigned num_lits, unsigned num_eqs) {
         return sizeof(th_propagation) + sizeof(sat::literal) * num_lits + sizeof(enode_pair) * num_eqs;
     }
 
-    th_propagation::th_propagation(sat::literal_vector const& lits, enode_pair_vector const& eqs) {
-        m_num_literals = lits.size();
-        m_num_eqs = eqs.size();
+    th_propagation::th_propagation(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs) {
+        m_num_literals = n_lits;
+        m_num_eqs = n_eqs;
         m_literals = reinterpret_cast<literal*>(reinterpret_cast<char*>(this) + sizeof(th_propagation));
-        unsigned i = 0;
-        for (sat::literal lit : lits)
-            m_literals[i++] = lit;
-        m_eqs = reinterpret_cast<enode_pair*>(reinterpret_cast<char*>(this) + sizeof(th_propagation) + sizeof(literal) * m_num_literals);
-        i = 0;
-        for (auto eq : eqs)
-            m_eqs[i++] = eq;
+        for (unsigned i = 0; i < n_lits; ++i)
+            m_literals[i] = lits[i];
+        m_eqs = reinterpret_cast<enode_pair*>(reinterpret_cast<char*>(this) + sizeof(th_propagation) + sizeof(literal) * n_lits);
+        for (unsigned i = 0; i < n_eqs; ++i)
+            m_eqs[i] = eqs[i];        
     }
 
     th_propagation* th_propagation::mk(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs) {
-        region& r = th.ctx.get_region();
-        void* mem = r.allocate(get_obj_size(lits.size(), eqs.size()));
-        sat::constraint_base::initialize(mem, &th);
-        return new (sat::constraint_base::ptr2mem(mem)) th_propagation(lits, eqs);
+        return mk(th, lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr());
     }
+
+    th_propagation* th_propagation::mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs) {
+        region& r = th.ctx.get_region();
+        void* mem = r.allocate(get_obj_size(n_lits, n_eqs));
+        sat::constraint_base::initialize(mem, &th);
+        return new (sat::constraint_base::ptr2mem(mem)) th_propagation(n_lits, lits, n_eqs, eqs);
+    }
+
+    th_propagation* th_propagation::mk(th_euf_solver& th, enode_pair_vector const& eqs) {
+        return mk(th, 0, nullptr, eqs.size(), eqs.c_ptr());
+    }
+
+    th_propagation* th_propagation::mk(th_euf_solver& th, sat::literal lit) {
+        return mk(th, 1, &lit, 0, nullptr);
+    }
+
+    th_propagation* th_propagation::mk(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) {
+        enode_pair eq(x, y);
+        return mk(th, 1, &lit, 1, &eq);
+    }
+
+    th_propagation* th_propagation::mk(th_euf_solver& th, euf::enode* x, euf::enode* y) {
+        enode_pair eq(x, y);
+        return mk(th, 0, nullptr, 1, &eq);
+    }
+
+    std::ostream& th_propagation::display(std::ostream& out) const {
+        for (auto lit : euf::th_propagation::lits(*this))
+            out << lit << " ";
+        for (auto eq : euf::th_propagation::eqs(*this))
+            out << eq.first->get_expr_id() << " == " << eq.second->get_expr_id() << " ";
+        return out;
+    }
+
+
 }
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index e6bb2be0a..e0e99bb08 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -101,7 +101,7 @@ namespace euf {
     public:
         th_solver(ast_manager& m, symbol const& name, euf::theory_id id) : extension(name, id), m(m) {}
 
-        virtual th_solver* clone(sat::solver* s, euf::solver& ctx) = 0;
+        virtual th_solver* clone(euf::solver& ctx) = 0;
 
         virtual void new_eq_eh(euf::th_eq const& eq) {}
 
@@ -150,7 +150,7 @@ namespace euf {
         sat::literal eq_internalize(expr* a, expr* b);
 
         euf::enode* e_internalize(expr* e) { internalize(e, m_is_redundant); return expr2enode(e); }
-        euf::enode* mk_enode(expr* e, bool suppress_args);
+        euf::enode* mk_enode(expr* e, bool suppress_args = false);
         expr_ref mk_eq(expr* e1, expr* e2);
         expr_ref mk_var_eq(theory_var v1, theory_var v2) { return mk_eq(var2expr(v1), var2expr(v2)); }
 
@@ -187,14 +187,19 @@ namespace euf {
 
 
     class th_propagation {
-        unsigned    m_num_literals;
-        unsigned    m_num_eqs;
-        sat::literal*    m_literals;
-        enode_pair* m_eqs;
+        unsigned       m_num_literals;
+        unsigned       m_num_eqs;
+        sat::literal*  m_literals;
+        enode_pair*    m_eqs;
         static unsigned get_obj_size(unsigned num_lits, unsigned num_eqs);
-        th_propagation(sat::literal_vector const& lits, enode_pair_vector const& eqs);
+        th_propagation(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs);
     public:
         static th_propagation* mk(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs);
+        static th_propagation* mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs);
+        static th_propagation* mk(th_euf_solver& th, enode_pair_vector const& eqs);
+        static th_propagation* mk(th_euf_solver& th, sat::literal lit);
+        static th_propagation* mk(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y);
+        static th_propagation* mk(th_euf_solver& th, euf::enode* x, euf::enode* y);
 
         sat::ext_constraint_idx to_index() const {
             return sat::constraint_base::mem2base(this);
@@ -203,18 +208,24 @@ namespace euf {
             return *reinterpret_cast<th_propagation*>(sat::constraint_base::from_index(idx)->mem());
         }
 
+        sat::extension& ext() const {
+            return *sat::constraint_base::to_extension(to_index());
+        }
+
+        std::ostream& display(std::ostream& out) const;
+
         class lits {
-            th_propagation& th;
+            th_propagation const& th;
         public:
-            lits(th_propagation& th) : th(th) {}
+            lits(th_propagation const& th) : th(th) {}
             sat::literal const* begin() const { return th.m_literals; }
             sat::literal const* end() const { return th.m_literals + th.m_num_literals; }
         };
 
         class eqs {
-            th_propagation& th;
+            th_propagation const& th;
         public:
-            eqs(th_propagation& th) : th(th) {}
+            eqs(th_propagation const& th) : th(th) {}
             enode_pair const* begin() const { return th.m_eqs; }
             enode_pair const* end() const { return th.m_eqs + th.m_num_eqs; }
         };
diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp
index c50b91ec2..fb67f7e90 100644
--- a/src/sat/smt/user_solver.cpp
+++ b/src/sat/smt/user_solver.cpp
@@ -146,12 +146,10 @@ namespace user {
         return display_justification(out, idx);     
     }
 
-    euf::th_solver* solver::clone(sat::solver* dst_s, euf::solver& dst_ctx) {
+    euf::th_solver* solver::clone(euf::solver& dst_ctx) {
         auto* result = alloc(solver, dst_ctx);
-        result->set_solver(dst_s);
-        ast_translation tr(m, dst_ctx.get_manager(), false);
-        for (unsigned i = 0; i < get_num_vars(); ++i) 
-            result->add_expr(tr(var2expr(i)));
+        for (unsigned i = 0; i < get_num_vars(); ++i)
+            result->add_expr(ctx.copy(dst_ctx, var2enode(i))->get_expr());
         return result;
     }
 
diff --git a/src/sat/smt/user_solver.h b/src/sat/smt/user_solver.h
index 2d8b530e1..ab2eaaad9 100644
--- a/src/sat/smt/user_solver.h
+++ b/src/sat/smt/user_solver.h
@@ -124,7 +124,7 @@ namespace user {
         std::ostream& display(std::ostream& out) const override;
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
-        euf::th_solver* clone(sat::solver* s, euf::solver& ctx) override;
+        euf::th_solver* clone(euf::solver& ctx) override;
 
     };
 };
diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp
index a6891a298..28733764f 100644
--- a/src/test/qe_arith.cpp
+++ b/src/test/qe_arith.cpp
@@ -4,7 +4,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 --*/
 
-#include "qe/qe_arith.h"
+#include "qe/mbp/mbp_arith.h"
 #include "qe/qe.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "parsers/smt2/smt2parser.h"
@@ -80,7 +80,7 @@ static void test(app* var, expr_ref& fml) {
         if (result != l_true) return;
         ctx.get_model(md);
     }    
-    VERIFY(qe::arith_project(*md, var, lits));
+    VERIFY(mbp::arith_project(*md, var, lits));
     pr = mk_and(lits);
    
     std::cout << "original:  " << mk_pp(fml, m) << "\n";
@@ -265,7 +265,7 @@ static void test2(char const *ex) {
     fml2 = m.mk_exists(bound.size(), sorts.c_ptr(), names.c_ptr(), fml2);
     qe::expr_quant_elim qe(m, params);
     for (unsigned i = 0; i < vars.size(); ++i) {
-        VERIFY(qe::arith_project(*md, vars[i].get(), lits));
+        VERIFY(mbp::arith_project(*md, vars[i].get(), lits));
     }
     pr1 = mk_and(lits);
     qe(m.mk_true(), fml2, pr2);
@@ -382,7 +382,7 @@ static void add_random_ineq(
 }
 
 static void test_maximize(opt::model_based_opt& mbo, ast_manager& m, unsigned num_vars, expr_ref_vector const& fmls, app* t) {
-    qe::arith_project_plugin plugin(m);
+    mbp::arith_project_plugin plugin(m);
     model mdl(m);    
     arith_util a(m);
     for (unsigned i = 0; i < num_vars; ++i) {
@@ -442,7 +442,7 @@ static void check_random_ineqs() {
 static void test_project() {
     ast_manager m;
     reg_decl_plugins(m);    
-    qe::arith_project_plugin plugin(m);    
+    mbp::arith_project_plugin plugin(m);    
     arith_util a(m);
     app_ref_vector vars(m);
     expr_ref_vector lits(m), ds(m);