diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp
index c58be15d1..ae140545a 100644
--- a/src/ast/sls/sls_context.cpp
+++ b/src/ast/sls/sls_context.cpp
@@ -337,6 +337,17 @@ namespace sls {
         return false;
     }
 
+    bool context::check_ackerman(app* e) const {
+        if (e->get_num_args() == 0)
+            return false;
+        auto f = e->get_decl();
+        if (is_uninterp(f))
+            return true;
+        auto fid = f->get_family_id();
+        auto p = m_plugins.get(fid, nullptr);        
+        return !p || p->check_ackerman(f);
+    }
+
     expr_ref context::get_value(expr* e) {
         sort* s = e->get_sort();
         auto fid = s->get_family_id();
diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h
index 73959e457..818f2a9f3 100644
--- a/src/ast/sls/sls_context.h
+++ b/src/ast/sls/sls_context.h
@@ -58,6 +58,7 @@ namespace sls {
         virtual void collect_statistics(statistics& st) const = 0;
         virtual void reset_statistics() = 0;
         virtual bool include_func_interp(func_decl* f) const { return false; }
+        virtual bool check_ackerman(func_decl* f) const { return false; }
     };
 
     using clause = ptr_iterator<sat::literal>;
@@ -224,6 +225,7 @@ namespace sls {
         bool is_fixed(expr* e);        
         bool is_relevant(expr* e);  
         bool add_constraint(expr* e);
+        bool check_ackerman(app* e) const;
         ptr_vector<expr> const& subterms();        
         ast_manager& get_manager() { return m; }
         std::ostream& display(std::ostream& out) const;
diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp
index 4de6ca1c9..076dc5626 100644
--- a/src/ast/sls/sls_datatype_plugin.cpp
+++ b/src/ast/sls/sls_datatype_plugin.cpp
@@ -570,6 +570,21 @@ namespace sls {
         return false; 
     }
 
+    bool datatype_plugin::check_ackerman(func_decl* f) const {
+        if (dt.is_accessor(f))
+            return true;
+        if (dt.is_constructor(f)) {
+            for (unsigned i = 0; i < f->get_arity(); ++i) {
+                if (f->get_range() != f->get_domain(i))
+                    return true;
+            }
+            return false;
+        }
+        if (dt.get_constructor_is(f))
+            return false;
+        return true;
+    }
+
     std::ostream& datatype_plugin::display(std::ostream& out) const {
         for (auto a : m_axioms)
             out << mk_bounded_pp(a, m, 3) << "\n";
diff --git a/src/ast/sls/sls_datatype_plugin.h b/src/ast/sls/sls_datatype_plugin.h
index f06e24963..0507c68c0 100644
--- a/src/ast/sls/sls_datatype_plugin.h
+++ b/src/ast/sls/sls_datatype_plugin.h
@@ -94,6 +94,7 @@ namespace sls {
         bool set_value(expr* e, expr* v) override { return false; }
         void repair_literal(sat::literal lit) override {}
         bool include_func_interp(func_decl* f) const override;
+        bool check_ackerman(func_decl* f) const override;
 
         bool repair_down(app* e) override;
         void repair_up(app* e) override;
diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp
index e4745d02e..3b75419b6 100644
--- a/src/ast/sls/sls_euf_plugin.cpp
+++ b/src/ast/sls/sls_euf_plugin.cpp
@@ -53,17 +53,8 @@ namespace sls {
         if (!is_app(e))
             return;
         app* a = to_app(e);
-        if (a->get_num_args() == 0)
-            return;
-        if (!is_uninterp(e)) {
-            return;
-            family_id fid = a->get_family_id();
-            if (fid == basic_family_id)
-                return;
-            if (all_of(*a, [&](expr* arg) { return !is_app(arg) || fid == to_app(arg)->get_family_id(); }))
-                return;            
-        }
-
+        if (!ctx.check_ackerman(a)) 
+            return;               
         auto f = a->get_decl();
         if (!m_app.contains(f))
             m_app.insert(f, ptr_vector<app>());