From 8059a5a0b75e1ff4bbf25e946efece8de7f25278 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@hotmail.com>
Date: Wed, 25 Mar 2015 11:36:01 -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 | 20 --------------------
 1 file changed, 20 deletions(-)

diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index 1278a50e4..81af289d3 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -1,27 +1,9 @@
 #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
@@ -1004,8 +986,6 @@ void extract_example() {
 }
 
 int main() {
-  slow();
-  return 0;
     try {
         demorgan(); std::cout << "\n";
         find_model_example1(); std::cout << "\n";