Correctness of UML diagrams annotated with OCL constraints can be checked using bounded verification. We show an automatic technique to choose the best bounds