title: Wrapping entities from Z3 C API
body: <p>I'm experimenting with enumeration sorts in Z3 as described in <a href="https://stackoverflow.com/questions/15085232/how-to-use-enumerated-constants-after-calling-of-some-tactic-in-z3">How to use enumerated constants after calling of some tactic in Z3?</a> and I noticed that I might have some misunderstanding on how to use C and C++ api properly. Let's consider the following example. </p>
  
  <pre><code>   context z3_cont;
     Z3_symbol e_names[2 ];
     Z3_func_decl e_consts[2];
     Z3_func_decl e_testers[2];
  
     e_names[0] = Z3_mk_string_symbol(z3_cont, "x1"); 
     e_names[1] = Z3_mk_string_symbol(z3_cont, "x2"); 
     Z3_symbol e_name = Z3_mk_string_symbol(z3_cont, "enum_type");  
     Z3_sort new_enum_sort = Z3_mk_enumeration_sort(z3_cont, e_name, 2, e_names, e_consts, e_testers);
  
     sort enum_sort = to_sort(z3_cont, new_enum_sort);
     expr e_const0(z3_cont), e_const1(z3_cont);
  
  /* WORKS!
     func_decl a_decl = to_func_decl(z3_cont, e_consts[0]);
     func_decl b_decl = to_func_decl(z3_cont, e_consts[1]);
     e_const0 = a_decl(0, 0);
     e_const1 = b_decl(0, 0);   
  */
     // SEGFAULT when doing cout
     e_const0 = to_func_decl(z3_cont, e_consts[0])(0, 0);
     e_const1 = to_func_decl(z3_cont, e_consts[1])(0, 0);
  
     cout &lt;&lt; e_const0 &lt;&lt; " " &lt;&lt; e_const1 &lt;&lt; endl;
  </code></pre>
  
  <p>I expected the two variants of code to nicely wrap the C entity Z3_func_decl with a smart pointer so I can use with C++ api, however only the first variant seems to be correct. So my questions are</p>
  
  <ol>
  <li><p>Is this a correct behavior that the second  way doesn't work? If so, how can I better understand the reasons of why it shouldn't?</p></li>
  <li><p>What happens with unwrapped C entities, as for example Z3_symbol e_name - here I don't wrap it, I don't increment references.  So will the memory be managed properly? Is it safe to use it? when the object will be destroyed? </p></li>
  <li><p>A minor question: I didn't see the to_symbol() function in C++ api. Is it just unnecessary? </p></li>
  </ol>
  
  <p>Thank you. </p>