## Warning messages during proof computation

### Warning: when foo is in i1, bar cannot be proved.

When Gappa applies a case splitting bar $foo, it splits the interval of foo until the property about bar holds for any sub-interval. If the maximal dichotomy depth has been reached yet the property still does not hold, the warning message displays the failing sub-interval (the leftmost one). { x in [-2,1] -> x / x in [1,1] } x / x$ x;
Warning: when x is in [-1b-99 {-1.57772e-30, -2^(-99)}, 1b-100 {7.88861e-31, 2^(-100)}], BND(x / x, [1, 1]) cannot be proved.
Error: some properties were not satisfied:
BND(x / x)

Option switch: -W[no-]dichotomy-failure.

### Warning: case split on foo has not produced any interesting new result.

This warning is displayed when Gappa is successful in finding a case split that satisfies the goals, yet the results obtained on the sub-intervals are not interesting: they have already been proved through a simpler analysis.

{ x in [1,2] -> x + 1 in ? }
$x; Warning: case split on x has not produced any interesting new result. Results: x + 1 in [2, 3] Option switch: -W[no-]dichotomy-failure. ### Warning: case split on foo has no range to split. This warning is displayed when Gappa is unable to find the initial range on which to split cases. { x in [-1,1] -> 1 in ? }$ 1 / x;
Warning: case split on 1 / x has no range to split.
Results:
1 in [1, 1]

Option switch: -W[no-]dichotomy-failure.

### Warning: case split on foo is not goal-driven anymore.

This warning is displayed when Gappa is supposed to find the best case split for proving a property, yet it does not know the range for this property or it has already proved it.

{ x in [-1,1] -> x + 1 in ? }
x + 1 \$ x;
Warning: case split on x is not goal-driven anymore.
Results:
x + 1 in [0, 2]

Option switch: -W[no-]dichotomy-failure.