To ensure the quality of an information system, the conceptual schema that represents its domain must be semantically correct. We present a prototype to automatically check whether a UML schema with OCL constraints is right in this sense. It is well known that the full expressiveness of OCL leads to undecidability of reasoning. To deal with this problem, our approach finds a compromise between expressiveness and decidability, thus being able to handle very expressive constraints guaranteeing termination in many cases.