mu-mmint: Fix refinements for all mavo models (part 2)

 * Optimize z3 calls
 * Keep adding null analysis