Forall Exprs

[TIFitis]

Forall expressions are not supported by cbmc, we need it in the precondition part.
Without forall expr, we can only handle monotonous functions.