An SMT-based approach for generating trace examples and counter-examples of parametric properties