Slicing for Correctness: Only emit slice warnings if statement can be sliced in all procs it occurs

[Philipp15b]

Some proof rules copy statements into multiple locations. For example, the k-induction rule copies the loop body, or the AST rule encoding generates multiple procs and coprocs with the loop body. If the slice solver determines that a statement can be sliced in one particular location, the corresponding message must only be emitted only if it can be sliced in every occurrence.

Note that the situation is not as annoying when slicing for errors: there we can just emit the message whenever the statement is part of at least one error.