Discretization of Temporal Models with Application to Planning with SMT