diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index e48c23905..9f4f9431c 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -1,9 +1,11 @@
 #include<vector>
 #include"z3++.h"
 
-
 using namespace z3;
 
+
+
+
 /**
    Demonstration of how Z3 can be used to prove validity of
    De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) }
@@ -985,6 +987,7 @@ void extract_example() {
 }
 
 int main() {
+
     try {
         demorgan(); std::cout << "\n";
         find_model_example1(); std::cout << "\n";
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 49fa10d94..cff59cd80 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -89,6 +89,7 @@ namespace api {
         m_bv_util(m()),
         m_datalog_util(m()),
         m_fpa_util(m()),
+	m_dtutil(m()),
         m_last_result(m()),
         m_ast_trail(m()),
         m_replay_stack() {
diff --git a/src/api/api_context.h b/src/api/api_context.h
index 58394c028..f02dc6f16 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -58,6 +58,7 @@ namespace api {
         bv_util                    m_bv_util;
         datalog::dl_decl_util      m_datalog_util;
         fpa_util                   m_fpa_util;
+	datatype_util              m_dtutil;
 
         // Support for old solver API
         smt_params                 m_fparams;
@@ -119,6 +120,7 @@ namespace api {
         bv_util & bvutil() { return m_bv_util; }
         datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
         fpa_util & fpautil() { return m_fpa_util; }
+	datatype_util& dtutil() { return m_dtutil; }
         family_id get_basic_fid() const { return m_basic_fid; }
         family_id get_array_fid() const { return m_array_fid; }
         family_id get_arith_fid() const { return m_arith_fid; }
diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp
index 9cd357ed5..a9794c980 100644
--- a/src/api/api_datatype.cpp
+++ b/src/api/api_datatype.cpp
@@ -36,7 +36,7 @@ extern "C" {
         RESET_ERROR_CODE(); 
         mk_c(c)->reset_last_result();
         ast_manager& m = mk_c(c)->m();
-        datatype_util dt_util(m);
+        datatype_util& dt_util = mk_c(c)->dtutil();
 
         sort_ref_vector tuples(m);
         sort* tuple;
@@ -102,7 +102,7 @@ extern "C" {
         RESET_ERROR_CODE();
         mk_c(c)->reset_last_result();
         ast_manager& m = mk_c(c)->m();
-        datatype_util dt_util(m);
+        datatype_util& dt_util = mk_c(c)->dtutil();
 
         sort_ref_vector sorts(m);
         sort* e;
@@ -451,7 +451,7 @@ extern "C" {
         RESET_ERROR_CODE();
         CHECK_VALID_AST(t, 0);
         sort * _t = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         
         if (!dt_util.is_datatype(_t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
@@ -470,17 +470,17 @@ extern "C" {
         RESET_ERROR_CODE();
         CHECK_VALID_AST(t, 0);   
         sort * _t = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         if (!dt_util.is_datatype(_t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        unsigned n = dt_util.get_datatype_num_constructors(_t);        
-        if (idx >= n) {
+        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
+        if (idx >= decls->size()) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        func_decl* decl = dt_util.get_constructor(_t, idx);
+        func_decl* decl = (*decls)[idx];
         mk_c(c)->save_ast_trail(decl);
         return of_func_decl(decl);
     }
@@ -499,18 +499,18 @@ extern "C" {
         LOG_Z3_get_datatype_sort_recognizer(c, t, idx);
         RESET_ERROR_CODE();   
         sort * _t = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         
         if (!dt_util.is_datatype(_t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-        unsigned n = dt_util.get_datatype_num_constructors(_t);
-        if (idx >= n) {
+        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
+        if (idx >= decls->size()) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        func_decl* decl = dt_util.get_constructor(_t, idx);
+        func_decl* decl = (*decls)[idx];
         decl = dt_util.get_constructor_recognizer(decl);
         mk_c(c)->save_ast_trail(decl);
         RETURN_Z3(of_func_decl(decl));
@@ -522,18 +522,18 @@ extern "C" {
         LOG_Z3_get_datatype_sort_constructor_accessor(c, t, idx_c, idx_a);
         RESET_ERROR_CODE();  
         sort * _t = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         
         if (!dt_util.is_datatype(_t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);            
         }
-        unsigned n = dt_util.get_datatype_num_constructors(_t);
-        if (idx_c >= n) {
+        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
+        if (idx_c >= decls->size()) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        func_decl* decl = dt_util.get_constructor(_t, idx_c);
+        func_decl* decl = (*decls)[idx_c];
         if (decl->get_arity() <= idx_a) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);                        
@@ -555,7 +555,7 @@ extern "C" {
         LOG_Z3_get_tuple_sort_mk_decl(c, t);
         RESET_ERROR_CODE();  
         sort * tuple = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
@@ -570,7 +570,7 @@ extern "C" {
         LOG_Z3_get_tuple_sort_num_fields(c, t);
         RESET_ERROR_CODE();   
         sort * tuple = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;            
@@ -593,7 +593,7 @@ extern "C" {
         LOG_Z3_get_tuple_sort_field_decl(c, t, i);
         RESET_ERROR_CODE();  
         sort * tuple = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) {
             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 af9c125f7..3f7f01364 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -170,6 +170,7 @@ class datatype_util {
     ptr_vector<ptr_vector<func_decl> >          m_vectors;
     
     func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
+    func_decl * get_constructor(sort * ty, unsigned c_id);
 
 public:
     datatype_util(ast_manager & m);
@@ -202,7 +203,6 @@ public:
     void reset();
     void display_datatype(sort *s, std::ostream& strm);
 
-    func_decl * get_constructor(sort * ty, unsigned c_id);
 };
 
 #endif /* _DATATYPE_DECL_PLUGIN_H_ */