Introduce program slicing

[jeroenk]

Introduce program slicing (in particular with respect to assume statements) to:

1. avoid unnecessary invariant speculation, and
2. make non-array-access parts of code simpler.

Point 2. interacts with benign race checking, so some care is needed here. When slicing cannot eliminate non-array-access parts, we could try replacing expensive operations with UFs, maybe reinterpreting them based on counterexamples.

It is important to have a look at the expense of slicing using transitive closures.