Prover Approximations

In order to check programs in a finite amount of time, the Prover simplifies the code being verified. This section describes the mechanisms for simplification.

Warning

The approximations described in this section may be unsound, meaning that they can cause real bugs to be overlooked by the Prover.