title: Can the output of intermediate models be disabled?
body: <p>A formula with quantifiers contains declaration of <code>trans</code> function. Z3 successfully finds the model and prints it. But it also prints models for  functions like <code>trans!1!4464</code>, <code>trans!7!4463</code> .. which are not used anywhere in the model. What is it? How can I disable this output?</p>
  
  <p>Here is the query: <a href="http://dl.dropbox.com/u/444947/asyn_arbiter_bound_16.smt2" rel="nofollow">http://dl.dropbox.com/u/444947/asyn_arbiter_bound_16.smt2</a>
  and here is Z3's output - <a href="http://dl.dropbox.com/u/444947/asyn_arbiter_bound_16_result.txt" rel="nofollow">http://dl.dropbox.com/u/444947/asyn_arbiter_bound_16_result.txt</a></p>