Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm