diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index f08efb00a..8183744b5 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -576,7 +576,7 @@ namespace datalog {
 
     void context::check_uninterpreted_free(rule_ref& r) {
         func_decl* f = 0;
-        if (r->has_uninterpreted_non_predicates(f)) {
+        if (r->has_uninterpreted_non_predicates(m, f)) {
             std::stringstream stm;
             stm << "Uninterpreted '" 
                 << f->get_name() 
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 96e2b163a..184a5fa02 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -43,6 +43,7 @@ Revision History:
 #include"expr_safe_replace.h"
 #include"filter_model_converter.h"
 #include"scoped_proof.h"
+#include"datatype_decl_plugin.h"
 
 namespace datalog {
 
@@ -881,9 +882,12 @@ namespace datalog {
     }
 
     struct uninterpreted_function_finder_proc {
+        ast_manager& m;
+        datatype_util m_dt;
         bool m_found;
         func_decl* m_func;
-        uninterpreted_function_finder_proc() : m_found(false), m_func(0) {}
+        uninterpreted_function_finder_proc(ast_manager& m): 
+            m(m), m_dt(m), m_found(false), m_func(0) {}
         void operator()(var * n) { }
         void operator()(quantifier * n) { }
         void operator()(app * n) {
@@ -891,6 +895,14 @@ namespace datalog {
                 m_found = true;
                 m_func = n->get_decl();
             }
+            else if (m_dt.is_accessor(n)) {
+                sort* s = m.get_sort(n->get_arg(0));
+                SASSERT(m_dt.is_datatype(s));
+                if (m_dt.get_datatype_constructors(s)->size() > 1) {
+                    m_found = true;
+                    m_func = n->get_decl();
+                }
+            }
         }
 
         bool found(func_decl*& f) const { f = m_func; return m_found; }
@@ -900,9 +912,9 @@ namespace datalog {
     // non-predicates may appear only in the interpreted tail, it is therefore 
     // sufficient only to check the tail.
     //
-    bool rule::has_uninterpreted_non_predicates(func_decl*& f) const {
+    bool rule::has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const {
         unsigned sz = get_tail_size();
-        uninterpreted_function_finder_proc proc;
+        uninterpreted_function_finder_proc proc(m);
         expr_mark visited;
         for (unsigned i = get_uninterpreted_tail_size(); i < sz && !proc.found(f); ++i) {
             for_each_expr(proc, visited, get_tail(i));
@@ -910,6 +922,7 @@ namespace datalog {
         return proc.found(f);
     }
 
+
     struct quantifier_finder_proc {
         bool m_exist;
         bool m_univ;
diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h
index 77bf9ac74..1c31dc6b4 100644
--- a/src/muz/base/dl_rule.h
+++ b/src/muz/base/dl_rule.h
@@ -293,7 +293,7 @@ namespace datalog {
         */
         bool is_in_tail(const func_decl * p, bool only_positive=false) const;
 
-        bool has_uninterpreted_non_predicates(func_decl*& f) const;
+        bool has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const;
         void has_quantifiers(bool& existential, bool& universal) const;
         bool has_quantifiers() const;
         bool has_negation() const;