This directory contains various example programs
where contracts has been added to some operations.

The current contract verifier is able to statically prove
all contracts as valid. Hence, it is also the test suite
for the contract verifier.

Just for documentation, the subdirectory `unprovable_contracts`
contains examples where contracts cannot be proved (since they
do not hold).