tosem: Consistently parse z3 model from check sat

 * Move into z3 model api
 * Adapt to full mavo or may only encoding