Splits on ACSL predicates do not try to split and reduce states in which the
predicate is already satisfied or refuted.

A split has failed if the reduced state is equal to the entry state _and_
the predicate evaluates to Unknown.
If the predicate evaluates to True/False in the entry state, then the state
cannot be reduced: the reduced state is then equal to the entry state), but
this is not a failure: the split holds.