diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp
index 4f265eb79..981ddb798 100644
--- a/src/ast/sls/sls_datatype_plugin.cpp
+++ b/src/ast/sls/sls_datatype_plugin.cpp
@@ -313,6 +313,7 @@ namespace sls {
 
         // assign fresh values to uninterpeted nodes
         for (euf::enode* n : deps.top_sorted()) {
+            TRACE("dt", tout << g->bpp(n) << "\n");
             SASSERT(n->is_root());
             expr* e = n->get_expr();
             if (!dt.is_datatype(e))
@@ -321,24 +322,11 @@ namespace sls {
             if (m_values.get(id, nullptr))
                 continue;
             auto con = get_constructor(n);
-            if (con)
-                continue;
-            m_values.setx(id, m_model->get_fresh_value(e->get_sort()));
-            TRACE("dt", tout << "Fresh interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n");
-        }
-
-        // finally populate values to other nodes.
-        for (euf::enode* n : deps.top_sorted()) {
-            SASSERT(n->is_root());
-            unsigned id = n->get_id();
-            expr* e = n->get_expr();
-            if (!dt.is_datatype(e))
-                continue;
-            if (m_values.get(id))
-                continue;
-            euf::enode* con = get_constructor(n);
-            if (!con)
+            if (!con) {
+                m_values.setx(id, m_model->get_fresh_value(e->get_sort()));
+                TRACE("dt", tout << "Fresh interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n");
                 continue;
+            }
             auto f = con->get_decl();
             args.reset();
             for (auto arg : euf::enode_args(con)) {
@@ -388,12 +376,15 @@ namespace sls {
         svector<color_t> color;
         unsigned_vector dfsnum;
         svector<std::tuple<unsigned, euf::enode*, unsigned>> todo;
+        obj_map<sort, ptr_vector<expr>> sorts;
         for (auto n : g->nodes()) {
             if (!n->is_root())
                 continue;
             expr* e = n->get_expr();
             if (!dt.is_datatype(e))
                 continue;
+            sort* s = e->get_sort();
+            sorts.insert_if_not_there(s, ptr_vector<expr>()).push_back(e);
 
             auto c = color.get(e->get_id(), white);
             SASSERT(c != grey);
@@ -458,13 +449,14 @@ namespace sls {
         }
 
 
-        //
-        // sort_size sz = dt.et_datatype_size(s);
-        // if (sz.is_finite()) 
-        //     - sz.size() < |T of sort s|
-        //     - ensure that there are at most sz.size() distinct elements.
-        //     - not distinct(t1, ..., tn) where n = sz.size() + 1        
-        // 
+        for (auto const& [s, elems] : sorts) {
+            auto sz = s->get_num_elements();
+
+            if (!sz.is_finite() || sz.size() >= elems.size())
+                continue;
+            ctx.add_constraint(m.mk_not(m.mk_distinct((unsigned)sz.size() + 1, elems.data())));                       
+        }
+
         return false;
     }
 
diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp
index f4393bd01..d679e88cd 100644
--- a/src/ast/sls/sls_euf_plugin.cpp
+++ b/src/ast/sls/sls_euf_plugin.cpp
@@ -433,14 +433,12 @@ namespace sls {
                 auto n = to_app(e)->get_num_args();
                 expr_ref_vector eqs(m);
                 for (unsigned i = 0; i < n; ++i) {
-                    auto arg = to_app(e)->get_arg(i);
-                    auto a = ctx.get_value(arg);
+                    auto a = m_g->find(to_app(e)->get_arg(i));
                     for (unsigned j = i + 1; j < n; ++j) {
-                        auto argb = to_app(e)->get_arg(j);
-                        auto b = ctx.get_value(argb);
-                        if (a == b)
+                        auto b = m_g->find(to_app(e)->get_arg(j));
+                        if (a->get_root() == b->get_root())
                             goto done_distinct;
-                        eqs.push_back(m.mk_eq(arg, argb));
+                        eqs.push_back(m.mk_eq(a->get_expr(), b->get_expr()));
                     }
                 }
                 // distinct(a, b, c) or a = b or a = c or b = c