diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp
index ef68a7dd5..d4617356a 100644
--- a/src/ast/sls/sat_ddfw.cpp
+++ b/src/ast/sls/sat_ddfw.cpp
@@ -572,8 +572,8 @@ namespace sat {
             transfer_weight(from_idx, to_idx, w);
         }
         //verbose_stream() << m_shifts << " " << m_flips << " " << shifted << "\n";
-        if (!shifted)
-            m_reinit_next = m_flips;
+        if (!shifted && m_restart_next > m_flips)
+            m_restart_next =  m_flips + (m_restart_next - m_flips) / 2;
         // DEBUG_CODE(invariant(););
     }
 
diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp
index 7b17fe5a8..dc535f04e 100644
--- a/src/ast/sls/sls_datatype_plugin.cpp
+++ b/src/ast/sls/sls_datatype_plugin.cpp
@@ -96,10 +96,10 @@ namespace sls {
         expr* t = nullptr, *z = nullptr;
         for (auto s : ctx.subterms()) {
             if (dt.is_accessor(s, t) && dt.is_recursive(t) && dt.is_recursive(s))
-                add_edge(s, t, sat::null_literal);
+                add_edge(s, t, m.mk_app(dt.get_constructor_is(dt.get_accessor_constructor(to_app(s)->get_decl())), t));
             if (dt.is_constructor(s) && dt.is_recursive(s)) {
                 for (auto arg : *to_app(s))
-                    add_edge(arg, s, sat::null_literal);
+                    add_edge(arg, s, nullptr);
             }
         }
         expr* x = nullptr, *y = nullptr;
@@ -114,27 +114,27 @@ namespace sls {
             sat::literal lp(v, false), ln(v, true);
             if (dt.is_accessor(x, z) && dt.is_recursive(z)) {
                 if (ctx.is_unit(lp))
-                    add_edge(y, z, sat::null_literal);
+                    add_edge(y, z, nullptr);
                 else if (ctx.is_unit(ln))
                     ;
                 else
-                    add_edge(y, z, lp);                    
+                    add_edge(y, z, e);                    
             }
             if (dt.is_accessor(y, z) && dt.is_recursive(z)) {
                 if (ctx.is_unit(lp))
-                    add_edge(x, z, sat::null_literal);
+                    add_edge(x, z, m.mk_app(dt.get_constructor_is(dt.get_accessor_constructor(to_app(y)->get_decl())), z));
                 else if (ctx.is_unit(ln))
                     ;
                 else
-                    add_edge(x, z, lp);                    
+                    add_edge(x, z, e);                    
             }            
         }
         add_path_axioms();
     }
 
-    void datatype_plugin::add_edge(expr* child, expr* parent, sat::literal lit) {
-        TRACE("dt", tout << mk_bounded_pp(child, m) << " <- " << mk_bounded_pp(parent, m) << " " << lit << "\n");
-        m_parents.insert_if_not_there(child, svector<parent_t>()).push_back({parent, lit});
+    void datatype_plugin::add_edge(expr* child, expr* parent, expr* cond) {
+        m_parents.insert_if_not_there(child, vector<parent_t>()).push_back({parent, expr_ref(cond, m)});
+        TRACE("dt", tout << mk_bounded_pp(child, m) << " <- " << mk_bounded_pp(parent, m) << " " << mk_bounded_pp(cond, m) << "\n");
     }
 
     void datatype_plugin::add_path_axioms() {
@@ -148,21 +148,21 @@ namespace sls {
         }
     }
 
-    void datatype_plugin::add_path_axioms(ptr_vector<expr>& children, sat::literal_vector& lits, svector<parent_t> const& parents) {
-        for (auto const& [parent, lit] : parents) {
-            if (lit != sat::null_literal)                    
-                lits.push_back(~lit);
+    void datatype_plugin::add_path_axioms(ptr_vector<expr>& children, sat::literal_vector& lits, vector<parent_t> const& parents) {
+        for (auto const& [parent, cond] : parents) {
+            if (cond)                    
+                lits.push_back(~ctx.mk_literal(cond));
             if (children.contains(parent)) {
                 // only assert loop clauses for proper loops
                 if (parent == children[0])
                     ctx.add_clause(lits);
-                if (lit != sat::null_literal)                    
+                if (cond)                    
                     lits.pop_back();
                 continue;
             }
             if (children[0]->get_sort() == parent->get_sort()) {
                 lits.push_back(~ctx.mk_literal(m.mk_eq(children[0], parent)));
-                TRACE("dt", tout << lits << "\n");
+                TRACE("dt", for (auto lit : lits) tout << (lit.sign() ? "~": "") << mk_pp(ctx.atom(lit.var()), m) << "\n";);
                 ctx.add_clause(lits);
                 lits.pop_back();
             }
@@ -173,7 +173,7 @@ namespace sls {
                 add_path_axioms(children, lits, parents2);
                 children.pop_back();                
             }
-            if (lit != sat::null_literal)                    
+            if (cond)                    
                 lits.pop_back();
         }
     }
@@ -414,6 +414,7 @@ namespace sls {
             }
             IF_VERBOSE(1, verbose_stream() << "cycle\n"; for (auto e : diseqs) verbose_stream() << mk_pp(e, m) << "\n";);
             ctx.add_constraint(m.mk_or(diseqs));
+            ++m_stats.m_num_occurs;
         };
 
         for (auto n : g->nodes()) {
@@ -516,6 +517,7 @@ namespace sls {
         
     void datatype_plugin::collect_statistics(statistics& st) const {
         st.update("sls-dt-axioms", m_axioms.size());
+        st.update("sls-dt-occurs-conflicts", m_stats.m_num_occurs);
     }
     
     void datatype_plugin::reset_statistics() {}
diff --git a/src/ast/sls/sls_datatype_plugin.h b/src/ast/sls/sls_datatype_plugin.h
index c29e42d9d..dffe32a0f 100644
--- a/src/ast/sls/sls_datatype_plugin.h
+++ b/src/ast/sls/sls_datatype_plugin.h
@@ -26,17 +26,17 @@ namespace sls {
     
     class datatype_plugin : public plugin {
         struct stats {
-            unsigned m_num_axioms = 0;
+            unsigned m_num_occurs = 0;
             void reset() { memset(this, 0, sizeof(*this)); }
         };
         struct parent_t {
             expr*        parent;
-            sat::literal lit;
+            expr_ref     condition; 
         };
         euf_plugin& euf;
         scoped_ptr<euf::egraph>& g;
         obj_map<sort, ptr_vector<expr>> m_dts;
-        obj_map<expr, svector<parent_t>> m_parents;
+        obj_map<expr, vector<parent_t>> m_parents;
         
         mutable datatype_util dt;
         expr_ref_vector m_axioms, m_values;
@@ -44,9 +44,9 @@ namespace sls {
         stats m_stats;
 
         void collect_path_axioms();
-        void add_edge(expr* child, expr* parent, sat::literal lit);
+        void add_edge(expr* child, expr* parent, expr* cond);
         void add_path_axioms();
-        void add_path_axioms(ptr_vector<expr>& children, sat::literal_vector& lits, svector<parent_t> const& parents);
+        void add_path_axioms(ptr_vector<expr>& children, sat::literal_vector& lits, vector<parent_t> const& parents);
         void add_axioms();
         
         void init_values();