Postconditions for that variables mentioned in these postconditions
should be in counterexample are now marked with label "model_vc_post".

Variables corresponding to return values are no longer handled by
transformation intro_vc_vars_counterexmp. They must have location
of the corresponding postcondition, label "model" or "model_trace", and
label of the form "model_trace:name@result". Generartion of these labels
to variables corresponding to return values created in WP is for future
work.