title: Counterexample output of Z3
body: <p>When a formula in Z3 is unsat and (get-proof) is specified there is an output which I don't find any information about what it is. Where can I find any documentation about that?</p>
  
  <p>Seems to me quite unreadable, is there possibly any tool that takes this as an input?</p>
  
  <p>Cheers,
  Matt</p>