diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 4bc9b5170..6aaa13349 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -960,6 +960,11 @@ namespace datatype {
         return to_func_decl(recognizer->get_parameter(0).get_ast());
     }
 
+    func_decl * util::get_update_accessor(func_decl * updt) const {
+        SASSERT(is_update_field(updt));
+        return to_func_decl(updt->get_parameter(0).get_ast());
+    }
+
     bool util::is_recursive(sort * ty) {
         SASSERT(is_datatype(ty));
         bool r = false;
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index 5292ab6b9..63a850ea8 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -350,6 +350,7 @@ namespace datatype {
         ptr_vector<func_decl> const * get_constructor_accessors(func_decl * constructor);
         func_decl * get_accessor_constructor(func_decl * accessor);
         func_decl * get_recognizer_constructor(func_decl * recognizer) const;
+        func_decl * get_update_accessor(func_decl * update) const;
         family_id get_family_id() const { return m_family_id; }
         bool are_siblings(sort * s1, sort * s2);
         bool is_func_decl(op_kind k, unsigned num_params, parameter const* params, func_decl* f);
diff --git a/src/ast/rewriter/datatype_rewriter.cpp b/src/ast/rewriter/datatype_rewriter.cpp
index 4d688e682..4196a5051 100644
--- a/src/ast/rewriter/datatype_rewriter.cpp
+++ b/src/ast/rewriter/datatype_rewriter.cpp
@@ -70,17 +70,18 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
             return BR_FAILED;
         app * a = to_app(args[0]);
         func_decl * c_decl = a->get_decl();
-        if (c_decl != m_util.get_accessor_constructor(f)) {
+        func_decl * acc = m_util.get_update_accessor(f);
+        if (c_decl != m_util.get_accessor_constructor(acc)) {
             result = a;
             return BR_DONE;
         }
-        ptr_vector<func_decl> const & acc = *m_util.get_constructor_accessors(c_decl);
-        SASSERT(acc.size() == a->get_num_args());
-        unsigned num = acc.size();
+        ptr_vector<func_decl> const & accs = *m_util.get_constructor_accessors(c_decl);
+        SASSERT(accs.size() == a->get_num_args());
+        unsigned num = accs.size();
         ptr_buffer<expr> new_args;
         for (unsigned i = 0; i < num; ++i) {
             
-            if (f == acc[i]) {
+            if (acc == accs[i]) {
                 new_args.push_back(args[1]);
             }
             else {