Document quantifiers & code contracts support

[SaswatPadhi]

Just a TODO ticket to properly document the code contracts support (Felipe -> function contracts, I -> loop contracts) at some point.

As Felipe suggested @ #6145 (comment), we should also document the restricted quantifier support with the SAT backend. If this is already documented somewhere please point us to it.

[martin-cs]

Yes; a page in the manual about code contracts and how to do deductive verification would be amazing and would be make accessible all of the great work you have been doing.

I don't think the limitations of the SAT backend are documented anywhere.