Under-approximated models can lead to spurious UNSAT results
in JBMC; however, we can mark over-approximated cases as
notModelled and JBMC will detect them and give a warning that
behaviour is over-approximating when reporting SAT.

Without the cast we get a spurious UNSAT.

Under-approximated models can lead to spurious UNSAT results
in JBMC; however, we can mark over-approximated cases as
notModelled and JBMC will detect them and give a warning that
behaviour is over-approximating when reporting SAT.

This is necessary to make comparisons such as
o.getClass() == o.getClass() succeed.