fix error in reading Z3 result model