diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt
index 0a0769918..9284af431 100644
--- a/src/sat/smt/CMakeLists.txt
+++ b/src/sat/smt/CMakeLists.txt
@@ -14,7 +14,6 @@ z3_add_component(sat_smt
     ba_internalize.cpp
     ba_pb.cpp
     ba_solver.cpp
-    ba_xor.cpp
     bv_ackerman.cpp
     bv_delay_internalize.cpp
     bv_internalize.cpp
@@ -41,7 +40,6 @@ z3_add_component(sat_smt
     sat_dual_solver.cpp
     sat_th.cpp
     user_solver.cpp
-    xor_solver.cpp
   COMPONENT_DEPENDENCIES
     sat
     ast
diff --git a/src/sat/smt/ba_constraint.h b/src/sat/smt/ba_constraint.h
index 365f9284f..cd132257b 100644
--- a/src/sat/smt/ba_constraint.h
+++ b/src/sat/smt/ba_constraint.h
@@ -24,13 +24,11 @@ namespace ba {
 
     enum class tag_t {
         card_t,
-        pb_t,
-        xr_t
+        pb_t
     };
 
     class card;
     class pb;
-    class xr;
     class pb_base;
 
     inline lbool value(sat::model const& m, literal l) { return l.sign() ? ~m[l.var()] : m[l.var()]; }
@@ -82,14 +80,11 @@ namespace ba {
         size_t obj_size() const { return m_obj_size; }
         card& to_card();
         pb&  to_pb();
-        xr& to_xr();
         card const& to_card() const;
         pb const&  to_pb() const;
-        xr const& to_xr() const;
         pb_base const& to_pb_base() const; 
         bool is_card() const { return m_tag == tag_t::card_t; }
         bool is_pb() const { return m_tag == tag_t::pb_t; }
-        bool is_xr() const { return m_tag == tag_t::xr_t; }
 
         bool is_watched(solver_interface const& s, literal lit) const;
         void unwatch_literal(solver_interface& s, literal lit);
diff --git a/src/sat/smt/ba_internalize.cpp b/src/sat/smt/ba_internalize.cpp
index 7ccb4b4ae..e44690534 100644
--- a/src/sat/smt/ba_internalize.cpp
+++ b/src/sat/smt/ba_internalize.cpp
@@ -29,36 +29,10 @@ namespace sat {
         flet<bool> _redundant(m_is_redundant, redundant);
         if (m_pb.is_pb(e)) 
             return internalize_pb(e, sign, root);
-        if (m.is_xor(e))
-            return internalize_xor(e, sign, root);
         UNREACHABLE();
         return null_literal;
     }
 
-    literal ba_solver::internalize_xor(expr* e, bool sign, bool root) {
-        sat::literal_vector lits;
-        sat::bool_var v = s().add_var(true);
-        lits.push_back(literal(v, true));
-        auto add_expr = [&](expr* a) {
-            literal lit = si.internalize(a, m_is_redundant);
-            s().set_external(lit.var());
-            lits.push_back(lit);
-        };
-        expr* e1 = nullptr;
-        while (m.is_iff(e, e1, e))
-            add_expr(e1);
-        add_expr(e);
-        // ensure that = is converted to xor
-        for (unsigned i = 1; i + 1 < lits.size(); ++i) {
-            lits[i].neg();
-        }
-        add_xr(lits, m_is_redundant);
-        auto* aig = s().get_cut_simplifier();
-        if (aig) aig->add_xor(~lits.back(), lits.size() - 1, lits.c_ptr() + 1);
-        sat::literal lit(v, sign);
-        return literal(v, sign);
-    }
-
     literal ba_solver::internalize_pb(expr* e, bool sign, bool root) {
         SASSERT(m_pb.is_pb(e));
         app* t = to_app(e);
@@ -313,19 +287,6 @@ namespace sat {
         return fml;
     }
 
-    expr_ref ba_solver::get_xor(std::function<expr_ref(sat::literal)>& lit2expr, xr const& x) {
-        ptr_buffer<expr> lits;
-        for (sat::literal l : x) {
-            lits.push_back(lit2expr(l));
-        }
-        expr_ref fml(m.mk_xor(x.size(), lits.c_ptr()), m);
-
-        if (x.lit() != sat::null_literal) {
-            fml = m.mk_eq(lit2expr(x.lit()), fml);
-        }
-        return fml;
-    }
-
     bool ba_solver::to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) {
         for (auto* c : constraints()) {
             switch (c->tag()) {
@@ -335,9 +296,6 @@ namespace sat {
             case ba::tag_t::pb_t:
                 fmls.push_back(get_pb(l2e, c->to_pb()));
                 break;
-            case ba::tag_t::xr_t:
-                fmls.push_back(get_xor(l2e, c->to_xr()));
-                break;
             }
         }
         return true;
diff --git a/src/sat/smt/ba_solver.cpp b/src/sat/smt/ba_solver.cpp
index 649e8c8db..882e5783d 100644
--- a/src/sat/smt/ba_solver.cpp
+++ b/src/sat/smt/ba_solver.cpp
@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Extension for cardinality and xor reasoning.
+    Extension for cardinality reasoning.
 
 Author:
 
@@ -21,7 +21,6 @@ Author:
 #include "sat/smt/ba_solver.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/sat_simplifier_params.hpp"
-#include "sat/sat_xor_finder.h"
 
 namespace sat {
 
@@ -40,7 +39,6 @@ namespace sat {
             UNREACHABLE();
         }
         SASSERT(validate_conflict(c));
-        if (c.is_xr() && value(lit) == l_true) lit.neg();
         SASSERT(value(lit) == l_false);
         set_conflict(justification::mk_ext_justification(s().scope_lvl(), c.cindex()), ~lit);
         SASSERT(inconsistent());
@@ -749,16 +747,6 @@ namespace sat {
                     for (literal l : m_lemma) process_antecedent(~l, offset);
                     break;
                 }
-                case ba::tag_t::xr_t: {
-                    // jus.push_back(js);
-                    m_lemma.reset();
-                    inc_bound(offset);
-                    inc_coeff(consequent, offset);
-                    get_xr_antecedents(consequent, idx, js, m_lemma);
-                    for (literal l : m_lemma) 
-                        process_antecedent(~l, offset);
-                    break;
-                }
                 default:
                     UNREACHABLE();
                     break;
@@ -1444,7 +1432,6 @@ namespace sat {
         switch (c.tag()) {
         case ba::tag_t::card_t: return add_assign(c.to_card(), l);
         case ba::tag_t::pb_t: return add_assign(c.to_pb(), l);
-        case ba::tag_t::xr_t: return add_assign(c.to_xr(), l);
         }
         UNREACHABLE();
         return l_undef;
@@ -1683,7 +1670,6 @@ namespace sat {
         switch (c.tag()) {
         case ba::tag_t::card_t: get_antecedents(l, c.to_card(), r); break;
         case ba::tag_t::pb_t: get_antecedents(l, c.to_pb(), r); break;
-        case ba::tag_t::xr_t: get_antecedents(l, c.to_xr(), r); break;
         default: UNREACHABLE(); break;            
         }
         if (get_config().m_drat && m_solver && !probing) {
@@ -2036,9 +2022,6 @@ namespace sat {
         case ba::tag_t::pb_t:
             simplify(c.to_pb());
             break;
-        case ba::tag_t::xr_t:
-            simplify(c.to_xr());
-            break;
         default:
             UNREACHABLE();
         }                
@@ -2064,10 +2047,6 @@ namespace sat {
             for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]);
             for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]);    
             unit_strengthen();
-            if (s().get_config().m_xor_solver) {
-                extract_xor();
-                merge_xor();
-            }
             cleanup_clauses();
             cleanup_constraints();
             update_pure();
@@ -2290,10 +2269,6 @@ namespace sat {
         case ba::tag_t::pb_t:
             recompile(c.to_pb());
             break;
-        case ba::tag_t::xr_t:
-            add_xr(c.to_xr().literals(), c.learned());
-            remove_constraint(c, "recompile xor");
-            break;
         default:
             UNREACHABLE();
         }                
@@ -2495,7 +2470,6 @@ namespace sat {
         switch (c.tag()) {
         case ba::tag_t::card_t: split_root(c.to_card()); break;
         case ba::tag_t::pb_t: split_root(c.to_pb()); break;
-        case ba::tag_t::xr_t: NOT_IMPLEMENTED_YET(); break;
         }
     }
 
@@ -2595,12 +2569,6 @@ namespace sat {
                     if (lit != null_literal) m_cnstr_use_list[(~l).index()].push_back(cp);
                 }  
                 break;            
-            case ba::tag_t::xr_t: 
-                for (literal l : cp->to_xr()) {
-                    m_cnstr_use_list[l.index()].push_back(cp);
-                    m_cnstr_use_list[(~l).index()].push_back(cp);
-                }             
-                break;            
             }
         }
     }
@@ -3188,13 +3156,6 @@ namespace sat {
                 result->add_pb_ge(p.lit(), wlits, p.k(), p.learned());
                 break;
             }
-            case ba::tag_t::xr_t: {
-                xr const& x = cp->to_xr();
-                lits.reset();
-                for (literal l : x) lits.push_back(l);
-                result->add_xr(lits, x.learned());        
-                break;
-            }
             default:
                 UNREACHABLE();
             }                
@@ -3607,17 +3568,6 @@ namespace sat {
             if (p.lit() != null_literal) ineq.push(~p.lit(), offset * p.k());
             break;
         }
-        case ba::tag_t::xr_t: {
-            xr& x = cnstr.to_xr();
-            literal_vector ls;
-            SASSERT(lit != null_literal);
-            get_antecedents(lit, x, ls);                
-            ineq.reset(offset);
-            for (literal l : ls) ineq.push(~l, offset);
-            literal lxr = x.lit();                
-            if (lxr != null_literal) ineq.push(~lxr, offset);
-            break;
-        }
         default:
             UNREACHABLE();
             break;
@@ -3860,7 +3810,7 @@ namespace sat {
                 card const& c = cp->to_card();
                 unsigned n = c.size();
                 unsigned k = c.k();
-                
+
                 if (c.lit() == null_literal) {
                     //    c.lits() >= k 
                     // <=> 
@@ -3885,7 +3835,7 @@ namespace sat {
                     for (literal l : c) lits.push_back(l), coeffs.push_back(1);
                     lits.push_back(~c.lit()); coeffs.push_back(n - k + 1);
                     add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), n);
-                    
+
                     lits.reset();
                     coeffs.reset();
                     for (literal l : c) lits.push_back(~l), coeffs.push_back(1);
@@ -3900,7 +3850,7 @@ namespace sat {
                 coeffs.reset();
                 unsigned sum = 0;
                 for (wliteral wl : p) sum += wl.first;
-                
+
                 if (p.lit() == null_literal) {
                     //   w1 + .. + w_n >= k
                     // <=> 
@@ -3919,7 +3869,7 @@ namespace sat {
                     lits.push_back(p.lit()), coeffs.push_back(p.k());
                     for (wliteral wl : p) lits.push_back(~(wl.second)), coeffs.push_back(wl.first);
                     add_pb(lits.size(), lits.c_ptr(), coeffs.c_ptr(), sum);
-                    
+
                     lits.reset();
                     coeffs.reset();
                     lits.push_back(~p.lit()), coeffs.push_back(sum + 1 - p.k());
@@ -3928,8 +3878,6 @@ namespace sat {
                 }
                 break;
             }
-            case ba::tag_t::xr_t:
-                return false;
             }
         }
         return true;
diff --git a/src/sat/smt/ba_solver.h b/src/sat/smt/ba_solver.h
index 0cf4b001f..103136189 100644
--- a/src/sat/smt/ba_solver.h
+++ b/src/sat/smt/ba_solver.h
@@ -9,7 +9,6 @@ Abstract:
 
     Cardinality extensions, 
     Pseudo Booleans, 
-    Xors
 
 Author:
 
@@ -29,7 +28,6 @@ Revision History:
 #include "sat/smt/ba_constraint.h"
 #include "sat/smt/ba_card.h"
 #include "sat/smt/ba_pb.h"
-#include "sat/smt/ba_xor.h"
 #include "util/small_object_allocator.h"
 #include "util/scoped_ptr_vector.h"
 #include "util/sorting_network.h"
@@ -40,11 +38,8 @@ namespace sat {
     typedef ba::constraint constraint;
     typedef ba::wliteral wliteral;
     typedef ba::card card;
-    typedef ba::xr xr;
     typedef ba::pb_base pb_base;
     typedef ba::pb pb;
-
-    class xor_finder;
     
     class ba_solver : public euf::th_solver, public ba::solver_interface {
 
@@ -200,7 +195,6 @@ namespace sat {
         lbool add_assign(constraint& c, literal l);
         bool incremental_mode() const;
         void simplify(constraint& c);
-        void pre_simplify(xor_finder& xu, constraint& c);
         void set_conflict(constraint& c, literal lit) override;
         void assign(constraint& c, literal lit) override;
         bool assigned_above(literal above, literal below);
@@ -234,18 +228,6 @@ namespace sat {
         lbool eval(card const& c) const;
         lbool eval(model const& m, card const& c) const;
 
-
-        // xr specific functionality
-        lbool add_assign(xr& x, literal alit);
-        void get_xr_antecedents(literal l, unsigned index, justification js, literal_vector& r);
-        void get_antecedents(literal l, xr const& x, literal_vector & r);
-        void simplify(xr& x);
-        void extract_xor();
-        void merge_xor();
-        bool clausify(xr& x);
-        void flush_roots(xr& x);
-        lbool eval(xr const& x) const;
-        lbool eval(model const& m, xr const& x) const;
         
         // pb functionality
         unsigned m_a_max{ 0 };
@@ -329,7 +311,6 @@ namespace sat {
 
         // validation utilities
         bool validate_conflict(card const& c) const;
-        bool validate_conflict(xr const& x) const;
         bool validate_conflict(pb const& p) const;
         bool validate_assign(literal_vector const& lits, literal lit);
         bool validate_lemma();
@@ -364,11 +345,8 @@ namespace sat {
 
         constraint* add_at_least(literal l, literal_vector const& lits, unsigned k, bool learned);
         constraint* add_pb_ge(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
-        constraint* add_xr(literal_vector const& lits, bool learned);
-        literal     add_xor_def(literal_vector& lits, bool learned = false);
         bool        all_distinct(literal_vector const& lits);
         bool        all_distinct(clause const& c);
-        bool        all_distinct(xr const& x);
 
         void copy_core(ba_solver* result, bool learned);
         void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints);
@@ -386,12 +364,9 @@ namespace sat {
         void convert_pb_args(app* t, literal_vector& lits);
         bool m_is_redundant{ false };
         literal internalize_pb(expr* e, bool sign, bool root);
-        literal internalize_xor(expr* e, bool sign, bool root);
-
         // Decompile
         expr_ref get_card(std::function<expr_ref(sat::literal)>& l2e, card const& c);
         expr_ref get_pb(std::function<expr_ref(sat::literal)>& l2e, pb const& p);
-        expr_ref get_xor(std::function<expr_ref(sat::literal)>& l2e, xr const& x);
 
     public:
         ba_solver(euf::solver& ctx, euf::theory_id id);
@@ -400,7 +375,6 @@ namespace sat {
         void set_lookahead(lookahead* l) override { m_lookahead = l; }
         void add_at_least(bool_var v, literal_vector const& lits, unsigned k);
         void add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
-        void add_xr(literal_vector const& lits);
 
         bool is_external(bool_var v) override;
         bool propagated(literal l, ext_constraint_idx idx) override;
@@ -411,7 +385,7 @@ namespace sat {
         check_result check() override;
         void push() override;
         void pop(unsigned n) override;
-        void pre_simplify() override;
+        void pre_simplify() override {}
         void simplify() override;
         void clauses_modifed() override;
         lbool get_phase(bool_var v) override;
diff --git a/src/sat/smt/ba_xor.cpp b/src/sat/smt/ba_xor.cpp
deleted file mode 100644
index 3914739ae..000000000
--- a/src/sat/smt/ba_xor.cpp
+++ /dev/null
@@ -1,192 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    ba_xor.cpp
-
-Abstract:
- 
-    Interface for Xor constraints.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2017-01-30
-
---*/
-
-#include "sat/smt/ba_xor.h"
-#include "sat/smt/ba_solver.h"
-
-namespace ba {
-
-    xr& constraint::to_xr() {
-        SASSERT(is_xr());
-        return static_cast<xr&>(*this);
-    }
-
-    xr const& constraint::to_xr() const {
-        SASSERT(is_xr());
-        return static_cast<xr const&>(*this);
-    }
-
-    xr::xr(unsigned id, literal_vector const& lits) :
-        constraint(ba::tag_t::xr_t, id, sat::null_literal, lits.size(), get_obj_size(lits.size())) {
-        for (unsigned i = 0; i < size(); ++i) {
-            m_lits[i] = lits[i];
-        }
-    }
-
-
-    bool xr::is_watching(literal l) const {
-        return
-            l == (*this)[0] || l == (*this)[1] ||
-            ~l == (*this)[0] || ~l == (*this)[1];
-    }
-
-    bool xr::well_formed() const {
-        uint_set vars;
-        if (lit() != sat::null_literal) vars.insert(lit().var());
-        for (literal l : *this) {
-            bool_var v = l.var();
-            if (vars.contains(v)) return false;
-            vars.insert(v);
-        }
-        return true;
-    }
-
-    std::ostream& xr::display(std::ostream& out) const {
-        for (unsigned i = 0; i < size(); ++i) {
-            out << (*this)[i] << " ";
-            if (i + 1 < size()) out << "x ";
-        }
-        return out;
-    }
-
-    void xr::clear_watch(solver_interface& s) {
-        auto& x = *this;
-        x.reset_watch();
-        x.unwatch_literal(s, x[0]);
-        x.unwatch_literal(s, x[1]);
-        x.unwatch_literal(s, ~x[0]);
-        x.unwatch_literal(s, ~x[1]);
-    }
-
-
-    bool xr::init_watch(solver_interface& s) {
-        auto& x = *this;
-        x.clear_watch(s);
-        VERIFY(x.lit() == sat::null_literal);
-        TRACE("ba", x.display(tout););
-        unsigned sz = x.size();
-        unsigned j = 0;
-        for (unsigned i = 0; i < sz && j < 2; ++i) {
-            if (s.value(x[i]) == l_undef) {
-                x.swap(i, j);
-                ++j;
-            }
-        }
-        switch (j) {
-        case 0:
-            if (!parity(s, 0)) {
-                unsigned l = s.lvl(x[0]);
-                j = 1;
-                for (unsigned i = 1; i < sz; ++i) {
-                    if (s.lvl(x[i]) > l) {
-                        j = i;
-                        l = s.lvl(x[i]);
-                    }
-                }
-                s.set_conflict(x, x[j]);
-            }
-            return false;
-        case 1:
-            SASSERT(x.lit() == sat::null_literal || s.value(x.lit()) == l_true);
-            s.assign(x, parity(s, 1) ? ~x[0] : x[0]);
-            return false;
-        default:
-            SASSERT(j == 2);
-            x.watch_literal(s, x[0]);
-            x.watch_literal(s, x[1]);
-            x.watch_literal(s, ~x[0]);
-            x.watch_literal(s, ~x[1]);
-            return true;
-        }
-    }
-
-    bool xr::parity(solver_interface const& s, unsigned offset) const {
-        auto const& x = *this;
-        bool odd = false;
-        unsigned sz = x.size();
-        for (unsigned i = offset; i < sz; ++i) {
-            SASSERT(s.value(x[i]) != l_undef);
-            if (s.value(x[i]) == l_true) {
-                odd = !odd;
-            }
-        }
-        return odd;
-    }
-
-
-    std::ostream& xr::display(std::ostream& out, solver_interface const& s, bool values) const {
-        auto const& x = *this;
-        out << "xr: ";
-        for (literal l : x) {
-            out << l;
-            if (values) {
-                out << "@(" << s.value(l);
-                if (s.value(l) != l_undef) {
-                    out << ":" << s.lvl(l);
-                }
-                out << ") ";
-            }
-            else {
-                out << " ";
-            }
-        }
-        return out << "\n";
-    }
-
-    bool xr::validate_unit_propagation(solver_interface const& s, literal alit) const {
-        if (s.value(lit()) != l_true) return false;
-        for (unsigned i = 1; i < size(); ++i) {
-            if (s.value((*this)[i]) == l_undef) return false;
-        }
-        return true;
-    }
-
-    lbool xr::eval(solver_interface const& s) const {
-        auto const& x = *this;
-        bool odd = false;        
-        for (auto l : x) {
-            switch (s.value(l)) {
-            case l_true: odd = !odd; break;
-            case l_false: break;
-            default: return l_undef;
-            }
-        }
-        return odd ? l_true : l_false;
-    }
-
-    lbool xr::eval(sat::model const& m) const {
-        auto const& x = *this;
-        bool odd = false;        
-        for (auto l : x) {
-            switch (ba::value(m, l)) {
-            case l_true: odd = !odd; break;
-            case l_false: break;
-            default: return l_undef;
-            }
-        }
-        return odd ? l_true : l_false;
-    }
-
-    void xr::init_use_list(sat::ext_use_list& ul) const {
-        auto idx = cindex();
-        for (auto l : *this) {
-            ul.insert(l, idx);
-            ul.insert(~l, idx);
-        }
-    }
-
-}
diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
index fde0e3ac5..2c6c7faf2 100644
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@@ -236,10 +236,14 @@ namespace dt {
     */
     void solver::mk_split(theory_var v, bool is_final) {
         m_stats.m_splits++;
-
         v = m_find.find(v);
         enode* n = var2enode(v);
         sort* srt = n->get_sort();
+        if (dt.is_enum_sort(srt)) {
+            mk_enum_split(v);
+            return;
+        }
+                    
         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];
@@ -289,6 +293,32 @@ namespace dt {
         s().set_phase(lit);
     }
 
+    void solver::mk_enum_split(theory_var v) {
+        enode* n = var2enode(v);
+        var_data* d = m_var_data[v];
+        sort* srt = n->get_sort();
+        auto const& constructors = *dt.get_datatype_constructors(srt);
+        unsigned sz = constructors.size();
+        int start = s().rand()();
+        m_lits.reset();
+        for (unsigned i = 0; i < sz; ++i) {
+            unsigned j = (i + start) % sz;
+            sat::literal lit = eq_internalize(n->get_expr(), m.mk_const(constructors[j]));
+            switch (s().value(lit)) {
+            case l_undef:
+                s().set_phase(lit);
+                return;
+            case l_true:
+                return;
+            case l_false:
+                m_lits.push_back(~lit);
+                break;
+            }
+        }
+        ctx.set_conflict(euf::th_propagation::conflict(*this, m_lits));
+    }
+
+
     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
@@ -406,7 +436,7 @@ namespace dt {
 
         CTRACE("dt", d->m_recognizers.empty(), ctx.display(tout););
         SASSERT(!d->m_recognizers.empty());
-        literal_vector lits;
+        m_lits.reset();
         enode_pair_vector eqs;
         unsigned idx = 0;
         for (enode* r : d->m_recognizers) {
@@ -414,7 +444,7 @@ namespace dt {
                 return; // nothing to be propagated
             if (r && ctx.value(r) == l_false) {
                 SASSERT(r->num_args() == 1);
-                lits.push_back(~ctx.enode2literal(r));
+                m_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.
@@ -432,10 +462,10 @@ namespace dt {
         }
         TRACE("dt", tout << "propagate " << num_unassigned << " eqs: " << eqs.size() << "\n";);
         if (num_unassigned == 0)
-            ctx.set_conflict(euf::th_propagation::conflict(*this, lits, eqs));
+            ctx.set_conflict(euf::th_propagation::conflict(*this, m_lits, eqs));
         else if (num_unassigned == 1) {
             // propagate remaining recognizer
-            SASSERT(!lits.empty());
+            SASSERT(!m_lits.empty());
             enode* r = d->m_recognizers[unassigned_idx];
             literal consequent;
             if (r)
@@ -446,7 +476,7 @@ namespace dt {
                 app_ref rec_app(m.mk_app(rec, n->get_expr()), m);
                 consequent = mk_literal(rec_app);
             }
-            ctx.propagate(consequent, euf::th_propagation::propagate(*this, lits, eqs, consequent));
+            ctx.propagate(consequent, euf::th_propagation::propagate(*this, m_lits, eqs, consequent));
         }
         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...
diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h
index 04d3a21b1..528e2c508 100644
--- a/src/sat/smt/dt_solver.h
+++ b/src/sat/smt/dt_solver.h
@@ -97,6 +97,7 @@ namespace dt {
         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
+        sat::literal_vector   m_lits;
 
         void clear_mark();
 
@@ -119,6 +120,7 @@ namespace dt {
         void explain_is_child(enode* parent, enode* child);
 
         void mk_split(theory_var v, bool is_final);
+        void mk_enum_split(theory_var v);
 
         void display_var(std::ostream & out, theory_var v) const;
 
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index b59931e68..52ff3e3cc 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -205,6 +205,7 @@ namespace euf {
 
     public:
         static th_propagation* conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs);
+        static th_propagation* conflict(th_euf_solver& th, sat::literal_vector const& lits) { return conflict(th, lits.size(), lits.c_ptr(), 0, nullptr); }
         static th_propagation* conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs);
         static th_propagation* conflict(th_euf_solver& th, enode_pair_vector const& eqs);
         static th_propagation* conflict(th_euf_solver& th, sat::literal lit);
diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.d
similarity index 93%
rename from src/sat/smt/xor_solver.cpp
rename to src/sat/smt/xor_solver.d
index c9a11b0a9..8930b4ad9 100644
--- a/src/sat/smt/xor_solver.cpp
+++ b/src/sat/smt/xor_solver.d
@@ -416,3 +416,24 @@ namespace sat {
 
 
 }
+
+
+        // xr specific functionality
+        lbool add_assign(xr& x, literal alit);
+        void get_xr_antecedents(literal l, unsigned index, justification js, literal_vector& r);
+        void get_antecedents(literal l, xr const& x, literal_vector & r);
+        void simplify(xr& x);
+        void extract_xor();
+        void merge_xor();
+        bool clausify(xr& x);
+        void flush_roots(xr& x);
+        lbool eval(xr const& x) const;
+        lbool eval(model const& m, xr const& x) const;
+        bool validate_conflict(xr const& x) const;
+        constraint* add_xr(literal_vector const& lits, bool learned);
+        literal     add_xor_def(literal_vector& lits, bool learned = false);
+        bool        all_distinct(xr const& x);
+        expr_ref get_xor(std::function<expr_ref(sat::literal)>& l2e, xr const& x);
+        void add_xr(literal_vector const& lits);
+
+#include "sat/sat_xor_finder.h"
\ No newline at end of file