title: What will Z3 return when model_completion is set to false?
body: <p>When querying a model, with <code>model_completion</code> set to <code>false</code> in <code>Z3_model_eval</code>: What will Z3 return to signify that an interpretation is a "don't care"?</p>
  
  <p>In case someone wants to suggest that: I guess it's probably not the return value of the function <code>Z3_model_eval</code>, since the <code>z3++.h</code> file (the C++ API) contains the lines:</p>
  
  <pre><code>Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &amp;r);
  check_error();
  if (status == Z3_FALSE)
      throw exception("failed to evaluate expression");
  </code></pre>
  
  <p>In general: How does Z3 signify that a certain constant is a "don't care" in a model?</p>