In interval analysis, we have support for adding Invariants based on the current abstract state of the statement. For example:

int a = * ? 0 : 10;
//> ASSUME(a >= 0 && a <= 10);

These invariants, however, can cause unexpected effects on the slicer. Let's say for instance:

int a = * ? 0 : 10;
//> ASSUME(a >= 0 && a <= 10);
ASSERT(b == 1);

We can't slice a even though it does not affect the property. This is because the assumption adds it as a dependency. Also, we can't just slice assumptions. These assumptions might create some contradiction:

int a = 0;
int  b = 0;
assume(a != 0);
assert(b != 0);

However, this is different for the intervals. We know that the abstract state is reachable and does not have a contradiction in the invariant. This means that they are safe to slice.

I guess the easiest solution is to create a new boolean flag for assumptions. What do you think?