diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index 81af289d3..67af5eb34 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -5,6 +5,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) }
@@ -986,6 +987,9 @@ void extract_example() {
 }
 
 int main() {
+  slow();
+  return 0;
+
     try {
         demorgan(); std::cout << "\n";
         find_model_example1(); std::cout << "\n";
diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp
index 7acd93bf0..a9794c980 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;
         }
-        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);
     }
@@ -505,12 +505,12 @@ extern "C" {
             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));
@@ -528,12 +528,12 @@ extern "C" {
             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);                        
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_ */