From 86ac20faf65ea3aaaed43aa17c3682e4e6a8dadf Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@hotmail.com>
Date: Wed, 25 Mar 2015 11:35:44 -0700
Subject: [PATCH] cache datatype util in context to avoid performance bug,
 codeplex issue 195

Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
---
 examples/c++/example.cpp | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index 0f0dd5ebf..1278a50e4 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -1,10 +1,28 @@
 #include<vector>
 #include"z3++.h"
-
+#include<strstream>
 
 using namespace z3;
 
 
+void slow() {
+  context ctx;
+  unsigned sortSize = 200000;
+  char** names = new char*[sortSize];
+  func_decl_vector enum_consts(ctx);
+  func_decl_vector enum_testers(ctx);
+  for (unsigned i = 0; i < sortSize; ++i) {
+    std::stringstream strm;
+    strm << "c" << i;
+    names[i] = strdup(strm.str().c_str());
+  }
+  sort s = ctx.enumeration_sort("enumT", sortSize, names, enum_consts, enum_testers);
+  std::vector<Z3_func_decl> decls;
+  for (unsigned i = 0; i < sortSize; ++i) {
+    decls.push_back(Z3_get_datatype_sort_constructor(ctx, s, i));
+  }
+}
+
 /**
    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 +1004,8 @@ void extract_example() {
 }
 
 int main() {
+  slow();
+  return 0;
     try {
         demorgan(); std::cout << "\n";
         find_model_example1(); std::cout << "\n";