Formal analysis of piecewise affine systems through formula-guided refinement