diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 66bba1e03..a61a0a219 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -376,7 +376,7 @@ namespace euf {
 
         if (!n1->merge_enabled() && !n2->merge_enabled())
             return;
-        SASSERT(n1->get_expr()->get_sort() == n2->get_expr()->get_sort());
+        SASSERT(n1->get_sort() == n2->get_sort());
         enode* r1 = n1->get_root();
         enode* r2 = n2->get_root();
         if (r1 == r2)
@@ -560,7 +560,7 @@ namespace euf {
             return false;
         if (ra->interpreted() && rb->interpreted())
             return true;
-        if (ra->get_expr()->get_sort() != rb->get_expr()->get_sort())
+        if (ra->get_sort() != rb->get_sort())
             return true;
         expr_ref eq(m.mk_eq(a->get_expr(), b->get_expr()), m);
         m_tmp_eq->m_args[0] = a;
@@ -787,8 +787,8 @@ namespace euf {
             enode* n2 = m_nodes[i];
             enode* n2t = n1t ? old_expr2new_enode[n1->get_expr_id()] : nullptr;
             SASSERT(!n1t || n2t);
-            SASSERT(!n1t || n1->get_expr()->get_sort() == n1t->get_expr()->get_sort());
-            SASSERT(!n1t || n2->get_expr()->get_sort() == n2t->get_expr()->get_sort());
+            SASSERT(!n1t || n1->get_sort() == n1t->get_sort());
+            SASSERT(!n1t || n2->get_sort() == n2t->get_sort());
             if (n1t && n2->get_root() != n2t->get_root()) 
                 merge(n2, n2t, n1->m_justification.copy(copy_justification));
         }
diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h
index 61e68665d..2c67f66bc 100644
--- a/src/ast/euf/euf_enode.h
+++ b/src/ast/euf/euf_enode.h
@@ -198,6 +198,7 @@ namespace euf {
         bool is_root() const { return m_root == this; }
         enode* get_root() const { return m_root; }
         expr*  get_expr() const { return m_expr; }
+        sort*  get_sort() const { return m_expr->get_sort(); }
         app*  get_app() const { return to_app(m_expr); }
         func_decl* get_decl() const { return is_app(m_expr) ? to_app(m_expr)->get_decl() : nullptr; }
         unsigned get_expr_id() const { return m_expr->get_id(); }
diff --git a/src/sat/dimacs.cpp b/src/sat/dimacs.cpp
index 3fbb02c37..458c129f1 100644
--- a/src/sat/dimacs.cpp
+++ b/src/sat/dimacs.cpp
@@ -179,7 +179,33 @@ namespace dimacs {
         return m_buffer.c_ptr();
     }
 
+    char const* drat_parser::parse_quoted_symbol() {
+        SASSERT(*in == '|');
+        m_buffer.reset();
+        m_buffer.push_back(*in);
+        bool escape = false;
+        ++in;
+        while (true) {
+            auto c = *in;
+            if (c == EOF) 
+                throw lex_error();
+            else if (c == '\n') 
+                ;
+            else if (c == '|' && !escape) {
+                ++in;
+                m_buffer.push_back(c);
+                m_buffer.push_back(0);
+                return m_buffer.c_ptr();
+            }
+            escape = (c == '\\');
+            m_buffer.push_back(c);
+            ++in;
+        }
+    }
+
     char const* drat_parser::parse_sexpr() {
+        if (*in == '|')
+            return parse_quoted_symbol();
         m_buffer.reset();
         unsigned lp = 0;
         while (!is_whitespace(in) || lp > 0) {
diff --git a/src/sat/dimacs.h b/src/sat/dimacs.h
index 690f5b0fc..58f3953a0 100644
--- a/src/sat/dimacs.h
+++ b/src/sat/dimacs.h
@@ -84,6 +84,7 @@ namespace dimacs {
 
         char const* parse_sexpr();
         char const* parse_identifier();
+        char const* parse_quoted_symbol();
         int read_theory_id();
         bool next();
 
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index d60ca4d02..1bfaf2b17 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -121,6 +121,7 @@ namespace sat {
         virtual bool should_research(sat::literal_vector const& core) { return false;}
         virtual void add_assumptions() {}
         virtual bool tracking_assumptions() { return false; }
+        virtual bool enable_self_propagate() const { return false; }
 
         virtual bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
                                 std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) {                                
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 0a3de5393..d07390810 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -318,7 +318,7 @@ namespace arith {
         reset_evidence();
         for (auto const& ev : e)
             set_evidence(ev.ci(), m_core, m_eqs);
-        auto* jst = euf::th_propagation::mk(*this, m_core, m_eqs);
+        auto* jst = euf::th_propagation::propagate(*this, m_core, m_eqs, n1, n2);
         ctx.propagate(n1, n2, jst->to_index());
     }
 
@@ -718,7 +718,7 @@ namespace arith {
         set_evidence(ci4, m_core, m_eqs);
         enode* x = var2enode(v1);
         enode* y = var2enode(v2);
-        auto* jst = euf::th_propagation::mk(*this, m_core, m_eqs);
+        auto* jst = euf::th_propagation::propagate(*this, m_core, m_eqs, x, y);
         ctx.propagate(x, y, jst->to_index());
     }
 
@@ -1141,7 +1141,7 @@ namespace arith {
             add_clause(m_core2);
         }
         else {
-            auto* jst = euf::th_propagation::mk(*this, core, eqs);
+            auto* jst = euf::th_propagation::propagate(*this, core, eqs, lit);
             ctx.propagate(lit, jst->to_index());
         }
     }
diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp
index 90e01b4e3..d59e42635 100644
--- a/src/sat/smt/array_model.cpp
+++ b/src/sat/smt/array_model.cpp
@@ -47,7 +47,7 @@ namespace array {
     void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
         SASSERT(a.is_array(n->get_expr()));
         ptr_vector<expr> args;
-        sort* srt = n->get_expr()->get_sort();
+        sort* srt = n->get_sort();
         unsigned arity = get_array_arity(srt);
         func_decl * f    = mk_aux_decl_for_array_sort(m, srt);
         func_interp * fi = alloc(func_interp, m, arity);
diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp
index 78e2bda79..e235126a8 100644
--- a/src/sat/smt/array_solver.cpp
+++ b/src/sat/smt/array_solver.cpp
@@ -206,7 +206,7 @@ namespace array {
 
     void solver::add_parent_select(theory_var v_child, euf::enode* select) {
         SASSERT(a.is_select(select->get_expr()));
-        SASSERT(select->get_arg(0)->get_expr()->get_sort() == var2expr(v_child)->get_sort());
+        SASSERT(select->get_arg(0)->get_sort() == var2expr(v_child)->get_sort());
 
         v_child = find(v_child);
         ctx.push_vec(get_var_data(v_child).m_parent_selects, select);
diff --git a/src/sat/smt/ba_solver.cpp b/src/sat/smt/ba_solver.cpp
index 1e93090ca..649e8c8db 100644
--- a/src/sat/smt/ba_solver.cpp
+++ b/src/sat/smt/ba_solver.cpp
@@ -2640,7 +2640,7 @@ namespace sat {
     unsigned ba_solver::set_non_external() {
         // set variables to be non-external if they are not used in theory constraints.
         unsigned ext = 0;
-        if (!incremental_mode()) {
+        if (!incremental_mode() && s().get_extension() == this) {
             for (unsigned v = 0; v < s().num_vars(); ++v) {
                 literal lit(v, false);
                 if (s().is_external(v) && 
diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
index b0f7f0789..fde0e3ac5 100644
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@@ -103,9 +103,11 @@ namespace dt {
         expr* e1 = n1->get_expr();
         if (antecedent == sat::null_literal)
             add_unit(eq_internalize(e1, e2));
-        else if (s().value(antecedent) == l_true) 
-            ctx.propagate(n1, e_internalize(e2), euf::th_propagation::mk(*this, antecedent));
-        else 
+        else if (s().value(antecedent) == l_true) {
+            euf::enode* n2 = e_internalize(e2);
+            ctx.propagate(n1, n2, euf::th_propagation::propagate(*this, antecedent, n1, n2));
+        }
+        else
             add_clause(~antecedent, eq_internalize(e1, e2));
     }
 
@@ -114,24 +116,17 @@ namespace dt {
        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";);
+        TRACE("dt", tout << mk_pp(c, m) << " " << ctx.bpp(n) << "\n";);
         m_stats.m_assert_cnstr++;
+        expr* e = n->get_expr();
         SASSERT(dt.is_constructor(c));
         SASSERT(is_datatype(e));
         SASSERT(c->get_range() == e->get_sort());
         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)
+        for (func_decl* d : *dt.get_constructor_accessors(c))
             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);
-        enode* n2 = e_internalize(con);
-        theory_var v1 = n->get_th_var(get_id());
-        theory_var v2 = n2->get_th_var(get_id());
-        m_find.merge(v1, v2);
     }
 
     /**
@@ -142,13 +137,11 @@ namespace dt {
     */
     void solver::assert_accessor_axioms(enode* n) {
         m_stats.m_assert_accessor++;
-        expr* e = n->get_expr();
         SASSERT(is_constructor(n));
+        expr* e = n->get_expr();
         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) {
+        for (func_decl* acc : *dt.get_constructor_accessors(d)) {
             app_ref acc_app(m.mk_app(acc, e), m);
             assert_eq_axiom(n->get_arg(i), acc_app);
             ++i;
@@ -167,8 +160,7 @@ namespace dt {
         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);
+        ctx.set_conflict(euf::th_propagation::conflict(*this, ~l, c, r->get_arg(0)));
     }
 
     /**
@@ -228,11 +220,11 @@ namespace dt {
         else if (is_recognizer(n))
             ;
         else {
-            sort* s = n->get_expr()->get_sort();
+            sort* s = n->get_sort();
             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);
+                mk_split(r, false);
         }
         return r;
     }
@@ -242,12 +234,12 @@ namespace dt {
        \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) {        
+    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_expr()->get_sort();
+        sort* srt = n->get_sort();
         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];
@@ -258,32 +250,37 @@ namespace dt {
 
 
         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.
+            if (is_final) s().display(std::cout);
+            VERIFY(!is_final);
             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) {
+            auto 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) {
+                    VERIFY(!is_final);
                     return;
                 }
                 ++idx;
             }
-            if (r == nullptr)
+            if (r == nullptr) {
+                VERIFY(!is_final);
                 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);
@@ -308,10 +305,10 @@ namespace dt {
         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";);
+        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 ||
@@ -342,52 +339,52 @@ namespace dt {
         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)
+            if (d->m_constructor && 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 == 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) {
         TRACE("dt", tout << "add recognizer " << v << " " << mk_pp(recognizer->get_expr(), m) << "\n";);
-        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));
+        SASSERT(is_recognizer(recognizer));
+        SASSERT(dt.is_datatype(s));
+        if (d->m_recognizers.empty())
             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<enode>(d->m_recognizers, c_idx));
-            if (val == l_false)
-                propagate_recognizer(v, recognizer);
+        if (d->m_recognizers[c_idx])
+            return;
+
+        lbool val = ctx.value(recognizer);
+        TRACE("dt", tout << "adding recognizer to v" << v << " rec: #" << recognizer->get_expr_id() << " val: " << val << "\n";);
+
+        // do nothing... 
+        // If recognizer assignment was already processed, then
+        // d->m_constructor is already set.
+        // Otherwise, it will be set when asserted is invoked.
+        if (val == l_true)
+            return;
+
+        if (val == l_false && d->m_constructor) {
+            // conflict
+            if (d->m_constructor->get_decl() == dt.get_recognizer_constructor(recognizer->get_decl()))
+                sign_recognizer_conflict(d->m_constructor, recognizer);
+            return;
         }
+        SASSERT(val == l_undef || (val == l_false && !d->m_constructor));
+        ctx.push(set_vector_idx_trail<enode>(d->m_recognizers, c_idx));
+        d->m_recognizers[c_idx] = recognizer;
+        if (val == l_false)
+            propagate_recognizer(v, recognizer);
     }
 
     /**
@@ -400,27 +397,22 @@ namespace dt {
         unsigned num_unassigned = 0;
         unsigned unassigned_idx = UINT_MAX;
         enode* n = var2enode(v);
-        sort* srt = n->get_expr()->get_sort();
+        sort* srt = n->get_sort();
         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);
+            add_recognizer(v, recognizer);
+            return;
         }
+
         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)
+            if (r && ctx.value(r) == l_true)
                 return; // nothing to be propagated
-            else if (ctx.value(r) == l_false) {
+            if (r && ctx.value(r) == l_false) {
                 SASSERT(r->num_args() == 1);
                 lits.push_back(~ctx.enode2literal(r));
                 if (n != r->get_arg(0)) {
@@ -431,30 +423,35 @@ namespace dt {
                     eqs.push_back(euf::enode_pair(n, r->get_arg(0)));
                 }
             }
+            else {
+                if (num_unassigned == 0)
+                    unassigned_idx = idx;
+                ++num_unassigned;
+            }
             ++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));
+            ctx.set_conflict(euf::th_propagation::conflict(*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]);
+            if (r)
+                consequent = ctx.enode2literal(r);
+            else {
+                func_decl* con = (*dt.get_datatype_constructors(srt))[unassigned_idx];
+                func_decl* rec = dt.get_constructor_is(con);
                 app_ref rec_app(m.mk_app(rec, n->get_expr()), m);
                 consequent = mk_literal(rec_app);
             }
-            else
-                consequent = ctx.enode2literal(r);
-            ctx.propagate(consequent, euf::th_propagation::mk(*this, lits, eqs));
+            ctx.propagate(consequent, euf::th_propagation::propagate(*this, 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...
             // if eager splits are enabled... create new case split            
-            mk_split(v);
+            mk_split(v, false);
     }
 
     void solver::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) {
@@ -465,22 +462,20 @@ namespace dt {
         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<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;
-                    }
+        if (con1 && con2 && con1->get_decl() != con2->get_decl())
+            ctx.set_conflict(euf::th_propagation::conflict(*this, con1, con2));
+        else if (con2 && !con1) {
+            ctx.push(set_ptr_trail<enode>(d1->m_constructor));
+            // 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 && 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()));
+            d1->m_constructor = con2;
         }
         for (enode* e : d2->m_recognizers)
             if (e)
@@ -523,7 +518,7 @@ namespace dt {
         };
         for (enode* arg : euf::enode_args(parentc)) {
             add(arg);
-            sort* s = arg->get_expr()->get_sort();
+            sort* s = arg->get_sort();
             if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s)))
                 for (enode* aarg : get_array_args(arg))
                     add(aarg);
@@ -638,7 +633,7 @@ namespace dt {
 
         if (res) {
             clear_mark();
-            ctx.set_conflict(euf::th_propagation::mk(*this, m_used_eqs));
+            ctx.set_conflict(euf::th_propagation::conflict(*this, m_used_eqs));
             TRACE("dt", tout << "occurs check conflict: " << ctx.bpp(n) << "\n";);
         }
         return res;
@@ -652,23 +647,20 @@ namespace dt {
         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;
-                    }
-                }
-            }
+            if (v != static_cast<int>(m_find.find(v)))
+                continue;
+            enode* node = var2enode(v);
+            if (!is_datatype(node))
+                continue;
+            if (dt.is_recursive(node->get_sort()) && !oc_cycle_free(node) && occurs_check(node))
+                return sat::check_result::CR_CONTINUE;
+            if (get_config().m_dt_lazy_splits == 0)
+                continue;
+            if (m_var_data[v]->m_constructor)
+                continue;
+            clear_mark();
+            mk_split(v, true);
+            r = sat::check_result::CR_CONTINUE;
         }
         return r;
     }
@@ -704,7 +696,7 @@ namespace dt {
             return;
         euf::enode* con = m_var_data[m_find.find(v)]->m_constructor;
         if (con->num_args() == 0)
-            dep.insert(n, nullptr);                
+            dep.insert(n, nullptr);
         for (enode* arg : euf::enode_args(con))
             dep.add(n, arg->get_root());
     }
@@ -750,7 +742,7 @@ namespace dt {
         SASSERT(!n->is_attached_to(get_id()));
         if (is_constructor(term) || is_update_field(term)) {
             for (enode* arg : euf::enode_args(n)) {
-                sort* s = arg->get_expr()->get_sort();
+                sort* s = arg->get_sort();
                 if (dt.is_datatype(s))
                     mk_var(arg);
                 else if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s))) {
@@ -759,20 +751,20 @@ namespace dt {
                 }
             }
             mk_var(n);
-            
+
         }
         else if (is_recognizer(term)) {
             mk_var(n);
             enode* arg = n->get_arg(0);
             theory_var v = mk_var(arg);
-            add_recognizer(v, n);               
+            add_recognizer(v, n);
         }
         else {
             SASSERT(is_accessor(term));
             SASSERT(n->num_args() == 1);
             mk_var(n->get_arg(0));
         }
-       
+
         return true;
     }
 
diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h
index 07021057c..04d3a21b1 100644
--- a/src/sat/smt/dt_solver.h
+++ b/src/sat/smt/dt_solver.h
@@ -118,7 +118,7 @@ namespace dt {
         void occurs_check_explain(enode * top, enode * root);
         void explain_is_child(enode* parent, enode* child);
 
-        void mk_split(theory_var v);
+        void mk_split(theory_var v, bool is_final);
 
         void display_var(std::ostream & out, theory_var v) const;
 
@@ -152,6 +152,7 @@ namespace dt {
         void apply_sort_cnstr(euf::enode* n, sort* s) override;
         bool is_shared(theory_var v) const override { return false; }
         lbool get_phase(bool_var v) override { return l_true; }
+        bool enable_self_propagate() const override { return true; }
 
         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) {}
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index 9f8339e0d..b742809e5 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -31,11 +31,11 @@ namespace euf {
         if (is_app(e)) {
             app* a = to_app(e);
             drat_log_decl(a->get_decl());
+            std::stringstream strm;
+            strm << mk_ismt2_func(a->get_decl(), m);
             if (a->get_num_parameters() == 0)
-                get_drat().def_begin('e', e->get_id(), a->get_decl()->get_name().str());
+                get_drat().def_begin('e', e->get_id(), strm.str());
             else {
-                std::stringstream strm;
-                strm << mk_ismt2_func(a->get_decl(), m);
                 get_drat().def_begin('e', e->get_id(), strm.str());
             }
             for (expr* arg : *a)
@@ -128,19 +128,26 @@ namespace euf {
 
     void solver::log_justification(literal l, th_propagation const& jst) {
         literal_vector lits;
-        for (auto lit : euf::th_propagation::lits(jst))
-            lits.push_back(~lit);
-        lits.push_back(l);
         unsigned nv = s().num_vars();
         expr_ref_vector eqs(m);
-        for (auto eq : euf::th_propagation::eqs(jst)) {
+        auto add_lit = [&](enode_pair const& eq) {
             ++nv;
             literal lit(nv, false);
             eqs.push_back(m.mk_eq(eq.first->get_expr(), eq.second->get_expr()));
             drat_eq_def(lit, eqs.back());            
-            lits.push_back(lit);
-        }
-        
+            return lit;
+        };
+
+        for (auto lit : euf::th_propagation::lits(jst))
+            lits.push_back(~lit);
+        if (l != sat::null_literal)
+            lits.push_back(l);
+        for (auto eq : euf::th_propagation::eqs(jst)) 
+            lits.push_back(~add_lit(eq));
+        if (jst.lit_consequent() != sat::null_literal && jst.lit_consequent() != l) 
+            lits.push_back(jst.lit_consequent());
+        if (jst.eq_consequent().first != nullptr) 
+            lits.push_back(add_lit(jst.eq_consequent()));
         get_drat().add(lits, sat::status::th(m_is_redundant, jst.ext().get_id()));
     }
 
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 5118b8fca..b8ceb7fc2 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -397,6 +397,8 @@ namespace euf {
             auto* ext = sat::constraint_base::to_extension(idx);                
             if (ext->get_id() != e.id())
                 return false;
+            if (ext->enable_self_propagate())
+                return false;
         }
         return true;
     }
diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp
index c52fc13ce..3faad5855 100644
--- a/src/sat/smt/sat_th.cpp
+++ b/src/sat/smt/sat_th.cpp
@@ -229,7 +229,9 @@ namespace euf {
         return sat::constraint_base::obj_size(sizeof(th_propagation) + sizeof(sat::literal) * num_lits + sizeof(enode_pair) * num_eqs);
     }
 
-    th_propagation::th_propagation(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs) {
+    th_propagation::th_propagation(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& p) {
+        m_consequent = c;
+        m_eq = p;
         m_num_literals = n_lits;
         m_num_eqs = n_eqs;
         m_literals = reinterpret_cast<literal*>(reinterpret_cast<char*>(this) + sizeof(th_propagation));
@@ -237,36 +239,53 @@ namespace euf {
             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];        
+            m_eqs[i] = eqs[i];       
+ 
     }
 
-    th_propagation* th_propagation::mk(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& 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) {
+    th_propagation* th_propagation::mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y) {
         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);
+        return new (sat::constraint_base::ptr2mem(mem)) th_propagation(n_lits, lits, n_eqs, eqs, c, enode_pair(x, y));
     }
 
-    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::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent) {
+        return mk(th, lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), consequent, nullptr, nullptr);
     }
 
-    th_propagation* th_propagation::mk(th_euf_solver& th, sat::literal lit) {
-        return mk(th, 1, &lit, 0, nullptr);
+    th_propagation* th_propagation::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y) {
+        return mk(th, lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), sat::null_literal, x, y);
     }
 
-    th_propagation* th_propagation::mk(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) {
+    th_propagation* th_propagation::propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) {
+        return mk(th, 1, &lit, 0, nullptr, sat::null_literal, x, y);
+    }
+
+    th_propagation* th_propagation::conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs) {
+        return conflict(th, lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr());
+    }
+
+    th_propagation* th_propagation::conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs) {
+        return mk(th, n_lits, lits, n_eqs, eqs, sat::null_literal, nullptr, nullptr);
+    }
+
+    th_propagation* th_propagation::conflict(th_euf_solver& th, enode_pair_vector const& eqs) {
+        return conflict(th, 0, nullptr, eqs.size(), eqs.c_ptr());
+    }
+
+    th_propagation* th_propagation::conflict(th_euf_solver& th, sat::literal lit) {
+        return conflict(th, 1, &lit, 0, nullptr);
+    }
+
+    th_propagation* th_propagation::conflict(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);
+        return conflict(th, 1, &lit, 1, &eq);
     }
 
-    th_propagation* th_propagation::mk(th_euf_solver& th, euf::enode* x, euf::enode* y) {
+    th_propagation* th_propagation::conflict(th_euf_solver& th, euf::enode* x, euf::enode* y) {
         enode_pair eq(x, y);
-        return mk(th, 0, nullptr, 1, &eq);
+        return conflict(th, 0, nullptr, 1, &eq);
     }
 
     std::ostream& th_propagation::display(std::ostream& out) const {
@@ -274,6 +293,10 @@ namespace euf {
             out << lit << " ";
         for (auto eq : euf::th_propagation::eqs(*this))
             out << eq.first->get_expr_id() << " == " << eq.second->get_expr_id() << " ";
+        if (m_consequent != sat::null_literal)
+            out << "--> " << m_consequent;
+        if (m_eq.first != nullptr)
+            out << "--> " << m_eq.first->get_expr_id() << " == " << m_eq.second->get_expr_id();
         return out;
     }
 
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index 5576672d9..b59931e68 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -193,19 +193,27 @@ namespace euf {
 
 
     class th_propagation {
+        sat::literal   m_consequent { sat::null_literal };
+        enode_pair     m_eq { enode_pair() };
         unsigned       m_num_literals;
-        unsigned       m_num_eqs;
+        unsigned       m_num_eqs;        
         sat::literal*  m_literals;
         enode_pair*    m_eqs;
         static size_t get_obj_size(unsigned num_lits, unsigned num_eqs);
-        th_propagation(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs);
+        th_propagation(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& eq);
+        static th_propagation* mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y);
+
     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);
+        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, 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);
+        static th_propagation* conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y);
+        static th_propagation* conflict(th_euf_solver& th, euf::enode* x, euf::enode* y);
+        static th_propagation* propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y);
+        static th_propagation* propagate(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal consequent);
+        static th_propagation* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent);
+        static th_propagation* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y);
 
         sat::ext_constraint_idx to_index() const {
             return sat::constraint_base::mem2base(this);
@@ -236,6 +244,10 @@ namespace euf {
             enode_pair const* end() const { return th.m_eqs + th.m_num_eqs; }
         };
 
+        sat::literal lit_consequent() const { return m_consequent; }
+
+        enode_pair eq_consequent() const { return m_eq; }
+
     };
 
 
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 66a27b1fb..d97234515 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -458,7 +458,7 @@ namespace smt {
             TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";);
             TRACE("add_eq_detail", tout << "assigning\n" << enode_pp(n1, *this) << "\n" << enode_pp(n2, *this) << "\n";
                   tout << "kind: " << js.get_kind() << "\n";);
-            SASSERT(n1->get_owner()->get_sort() == n2->get_owner()->get_sort());
+            SASSERT(n1->get_sort() == n2->get_sort());
 
             m_stats.m_num_add_eq++;
             enode * r1 = n1->get_root();
@@ -1099,14 +1099,14 @@ namespace smt {
        context.
     */
     bool context::is_diseq(enode * n1, enode * n2) const {
-        SASSERT(n1->get_owner()->get_sort() == n2->get_owner()->get_sort());
+        SASSERT(n1->get_sort() == n2->get_sort());
         context * _this = const_cast<context*>(this);
         if (!m_is_diseq_tmp) {
             app * eq       = m.mk_eq(n1->get_owner(), n2->get_owner());
             m.inc_ref(eq);
             _this->m_is_diseq_tmp = enode::mk_dummy(m, m_app2enode, eq);
         }
-        else if (m_is_diseq_tmp->get_owner()->get_arg(0)->get_sort() != n1->get_owner()->get_sort()) {
+        else if (m_is_diseq_tmp->get_owner()->get_arg(0)->get_sort() != n1->get_sort()) {
             m.dec_ref(m_is_diseq_tmp->get_owner());
             app * eq = m.mk_eq(n1->get_owner(), n2->get_owner());
             m.inc_ref(eq);
@@ -4475,7 +4475,7 @@ namespace smt {
     }
 
     bool context::get_value(enode * n, expr_ref & value) {
-        sort * s      = n->get_owner()->get_sort();
+        sort * s      = n->get_sort();
         family_id fid = s->get_family_id();
         theory * th   = get_theory(fid);
         if (th == nullptr)
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index fb43d2299..59dd75bc5 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -171,13 +171,10 @@ namespace smt {
         unsigned get_owner_id() const { return m_owner->get_id(); }
         unsigned get_expr_id() const { return m_owner->get_id(); }
 
-        func_decl * get_decl() const {
-            return m_owner->get_decl();
-        }
+        func_decl * get_decl() const { return m_owner->get_decl(); }
+        unsigned get_decl_id() const { return m_owner->get_decl()->get_decl_id(); }
 
-        unsigned get_decl_id() const {
-            return m_owner->get_decl()->get_decl_id();
-        }
+        sort* get_sort() const { return m_owner->get_sort(); }
 
         unsigned hash() const {
             return m_owner->hash();
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index b07ada6fa..d502f7599 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -94,7 +94,7 @@ namespace smt {
         for (enode * r : m_context->enodes()) {
             if (r == r->get_root() && (m_context->is_relevant(r) || m.is_value(r->get_expr()))) {
                 roots.push_back(r);
-                sort * s      = r->get_owner()->get_sort();
+                sort * s      = r->get_sort();
                 model_value_proc * proc = nullptr;
                 if (m.is_bool(s)) {
                     CTRACE("model", m_context->get_assignment(r) == l_undef, 
@@ -117,7 +117,7 @@ namespace smt {
                         }
                         else {
                             TRACE("model", tout << "creating fresh value for #" << r->get_owner_id() << "\n";);
-                            proc = alloc(fresh_value_proc, mk_extra_fresh_value(r->get_owner()->get_sort()));
+                            proc = alloc(fresh_value_proc, mk_extra_fresh_value(r->get_sort()));
                         }
                     }
                     else {
@@ -136,7 +136,7 @@ namespace smt {
         SASSERT(r == r->get_root());
         expr * n = r->get_owner();
         if (!m.is_model_value(n)) {
-            sort * s = r->get_owner()->get_sort();
+            sort * s = r->get_sort();
             n = m_model->get_fresh_value(s);
             CTRACE("model", n == 0, 
                    tout << mk_pp(r->get_owner(), m) << "\nsort:\n" << mk_pp(s, m) << "\n";
@@ -183,12 +183,12 @@ namespace smt {
                 return true;
             bool visited = true;
             for (enode * r : roots) {
-                if (r->get_owner()->get_sort() != s)
+                if (r->get_sort() != s)
                     continue;
                 SASSERT(r == r->get_root());
                 if (root2proc[r]->is_fresh()) 
                     continue; // r is associated with a fresh value...
-                TRACE("mg_top_sort", tout << "fresh!" << src.get_value()->get_idx() << " -> #" << r->get_owner_id() << " " << mk_pp(r->get_owner()->get_sort(), m) << "\n";);
+                TRACE("mg_top_sort", tout << "fresh!" << src.get_value()->get_idx() << " -> #" << r->get_owner_id() << " " << mk_pp(r->get_sort(), m) << "\n";);
                 visit_child(source(r), colors, todo, visited);
                 TRACE("mg_top_sort", tout << "visited: " << visited << ", todo.size(): " << todo.size() << "\n";);
             }
@@ -307,7 +307,7 @@ namespace smt {
                       enode * n = curr.get_enode();
                       SASSERT(n->get_root() == n);
                       tout << mk_pp(n->get_owner(), m) << "\n";
-                      sort * s = n->get_owner()->get_sort();
+                      sort * s = n->get_sort();
                       tout << curr << " " << mk_pp(s, m);
                       tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n";
                   }
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 7fc40a4cc..a88d4b734 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -274,7 +274,7 @@ namespace smt {
             assert_update_field_axioms(n);
         }
         else {
-            sort * s      = n->get_owner()->get_sort();
+            sort * s      = n->get_sort();
             if (m_util.get_datatype_num_constructors(s) == 1) {
                 func_decl * c = m_util.get_datatype_constructors(s)->get(0);
                 assert_is_constructor_axiom(n, c, null_literal);
@@ -333,7 +333,7 @@ namespace smt {
             //
             for (unsigned i = 0; i < num_args; i++) {
                 enode * arg = e->get_arg(i);
-                sort * s    = arg->get_owner()->get_sort();
+                sort * s    = arg->get_sort();
                 if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
                     app_ref def(m_autil.mk_default(arg->get_owner()), m);
                     if (!ctx.e_internalized(def)) {
@@ -528,7 +528,7 @@ namespace smt {
                 }
                 found = true;
             }
-            sort * s = arg->get_owner()->get_sort();
+            sort * s = arg->get_sort();
             if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
                 for (enode* aarg : get_array_args(arg)) {
                     if (aarg->get_root() == child->get_root()) {
@@ -610,7 +610,7 @@ namespace smt {
                         occurs_check_explain(parent, aarg);
                         return true;
                     }
-                    if (m_util.is_datatype(aarg->get_owner()->get_sort())) {
+                    if (m_util.is_datatype(aarg->get_sort())) {
                         m_parent.insert(aarg->get_root(), parent);
                         oc_push_stack(aarg);
                     }
@@ -853,7 +853,7 @@ namespace smt {
                 }
                 return;
             }
-            SASSERT(val == l_undef || (val == l_false && d->m_constructor == 0));
+            SASSERT(val == l_undef || (val == l_false && d->m_constructor == nullptr));
             d->m_recognizers[c_idx] = recognizer;
             m_trail_stack.push(set_vector_idx_trail<enode>(d->m_recognizers, c_idx));
             if (val == l_false) {
@@ -872,7 +872,7 @@ namespace smt {
         unsigned num_unassigned  = 0;
         unsigned unassigned_idx  = UINT_MAX;
         enode * n       = get_enode(v);
-        sort * dt       = n->get_owner()->get_sort();
+        sort * dt       = n->get_sort();
         var_data * d    = m_var_data[v];
         if (d->m_recognizers.empty()) {
             theory_var w = recognizer->get_arg(0)->get_th_var(get_id());
@@ -955,7 +955,7 @@ namespace smt {
     void theory_datatype::mk_split(theory_var v) {
         v                     = m_find.find(v);
         enode * n             = get_enode(v);
-        sort * s              = n->get_owner()->get_sort();
+        sort * s              = n->get_sort();
         func_decl * non_rec_c = m_util.get_non_rec_constructor(s); 
         unsigned non_rec_idx  = m_util.get_constructor_idx(non_rec_c);
         var_data * d          = m_var_data[v];
diff --git a/src/util/trail.h b/src/util/trail.h
index 2f3e5ecde..6450fc85a 100644
--- a/src/util/trail.h
+++ b/src/util/trail.h
@@ -254,7 +254,7 @@ public:
     }
 
     void undo() override {
-        m_vector[m_idx] = 0;
+        m_vector[m_idx] = nullptr;
     }
 };