Added an annotation, :split_here, for predicate statements.
The annotation allows the programmer to manually indicate
where the verification of a procedure implementation should be
split into pieces.