This new phase is invoked after the extraction phase. It will rewrite
precondition (and postcondition) of functions to add instanceOf when the
parameter (and return type) is a case class concrete type (instead of abstract
class).

If not done, then during the mapping to Z3 we lose the precise subtype
information, and Z3 will be able to find non valid counter-examples,
of a different case class for example.

Since tests are very important, we introduce two testcases that make
sure the issue is fixed. We also needed to update the Testcase runners
to make use of the new pipeline.