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.