Improved use of types and subtypes in FDL
The Examiner now makes better use of types and subtypes in FDL. It is becoming increasingly common to use other provers such as Isabelle, Riposte and Alt Ergo (via SPARKBridge with Victor) to discharge SPARK VCs. It can be very beneficial to these provers to have richer type information included in the FDL. Consequently, the Examiner has been modified to produce such information. This change is backward compatible, so the Simplifier will still accept the generated FDL and discharge VCs as before. Other proof systems can make use of this information to significantly narrow the bounds for variables they reason about.