In the mCRL2 toolset, formal properties are specified in the modal mu-calculus with data. This formalism allows the use of quantifiers (∀ and ∃) to bind data variables. However, when a user puts a quantifier in the wrong place, our current set of tools maybe unable to solve the resulting model checking problem. An example of such a poorly written property is ∀d:D.[true*.drop(d)]false. In this talk, I will show an automated technique to fix such errors. We perform the analysis on the level of parameterised Boolean equation systems (PBESs), that encode the combination of a model and a property.