This presentation is the third in the context of our work on OIL, a language for modelling control software, where we have enabled the use of model checking via a translation to mCRL2. In this presentation we will dive a bit deeper into the complexity of this translation. Also, to test the feasibility of our methods we have applied them to a second model from Canon, which is considerably larger than the one discussed in the previous presentation. We will discuss what issues we have encountered while doing so and how we solved them.