diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp
index f3a275508..9cd357ed5 100644
--- a/src/api/api_datatype.cpp
+++ b/src/api/api_datatype.cpp
@@ -475,12 +475,12 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
-        if (!decls || idx >= decls->size()) {
+        unsigned n = dt_util.get_datatype_num_constructors(_t);        
+        if (idx >= n) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        func_decl* decl = (*decls)[idx];
+        func_decl* decl = dt_util.get_constructor(_t, idx);
         mk_c(c)->save_ast_trail(decl);
         return of_func_decl(decl);
     }
@@ -505,12 +505,12 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
-        if (!decls || idx >= decls->size()) {
+        unsigned n = dt_util.get_datatype_num_constructors(_t);
+        if (idx >= n) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
-            RETURN_Z3(0);                        
+            return 0;
         }
-        func_decl* decl = (*decls)[idx];
+        func_decl* decl = dt_util.get_constructor(_t, idx);
         decl = dt_util.get_constructor_recognizer(decl);
         mk_c(c)->save_ast_trail(decl);
         RETURN_Z3(of_func_decl(decl));
@@ -528,12 +528,12 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);            
         }
-        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
-        if (!decls || idx_c >= decls->size()) {
+        unsigned n = dt_util.get_datatype_num_constructors(_t);
+        if (idx_c >= n) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
-            RETURN_Z3(0);                        
+            return 0;
         }
-        func_decl* decl = (*decls)[idx_c];
+        func_decl* decl = dt_util.get_constructor(_t, idx_c);
         if (decl->get_arity() <= idx_a) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);                        
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index 96b678fb2..af9c125f7 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -168,8 +168,7 @@ class datatype_util {
     obj_map<sort, bool>                         m_is_recursive;
     ast_ref_vector                              m_asts;
     ptr_vector<ptr_vector<func_decl> >          m_vectors;
-
-    func_decl * get_constructor(sort * ty, unsigned c_id);
+    
     func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
 
 public:
@@ -185,7 +184,12 @@ public:
     bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); }
     bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); }
     ptr_vector<func_decl> const * get_datatype_constructors(sort * ty);
-    unsigned get_datatype_num_constructors(sort * ty) { return get_datatype_constructors(ty)->size(); }
+    unsigned get_datatype_num_constructors(sort * ty) { 
+        SASSERT(is_datatype(ty));
+        unsigned tid = ty->get_parameter(1).get_int();
+        unsigned o = ty->get_parameter(3 + 2 * tid).get_int();
+        return ty->get_parameter(o).get_int(); 
+    }
     unsigned get_constructor_idx(func_decl * f) const { SASSERT(is_constructor(f)); return f->get_parameter(1).get_int(); }
     unsigned get_recognizer_constructor_idx(func_decl * f) const { SASSERT(is_recognizer(f)); return f->get_parameter(1).get_int(); }
     func_decl * get_non_rec_constructor(sort * ty);
@@ -197,6 +201,8 @@ public:
     bool are_siblings(sort * s1, sort * s2);
     void reset();
     void display_datatype(sort *s, std::ostream& strm);
+
+    func_decl * get_constructor(sort * ty, unsigned c_id);
 };
 
 #endif /* _DATATYPE_DECL_PLUGIN_H_ */