Introduce program slicing (in particular with respect to assume statements) to:
avoid unnecessary invariant speculation, and
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.
Introduce program slicing (in particular with respect to assume statements) to:
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.