diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index e48c23905..0f0dd5ebf 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -4,6 +4,7 @@
 
 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) }
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 f3a275508..7e9dc6689 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,7 +470,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);
             return 0;
@@ -499,7 +499,7 @@ 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);
@@ -522,7 +522,7 @@ 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);
@@ -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);