Techniques are disclosed for automatically determining whether a potential constraint set to be applied to a portion of a circuit are overconstrained. An environment circuit supplies inputs to the circuit portion. Embodiments of the invention recognize that if the environment circuit produces a set of outputs that contain a pattern that is not present in the potential constraint set, then the potential constraint set is overconstrained. A verification tool establishes the properties for the environmental circuit based on the potential constraint set. If the verification tool determines that the outputs produced by the environment circuit conflict with the properties of the environment circuit, then the verification tool concludes that the potential constraint set is overconstrained, because the environment circuit produces a pattern that is not present in the potential constraint set. Advantageously, the laborious and error-prone process of manually determining the proper inputs to apply during formal verification is avoided.