Other error messages during parsing

Error: undefined intervals are restricted to conclusions.

You are not allowed to use an interrogation mark for an interval that appears in negative position in the logical formula.

{ x in ? -> x + 1 in [0,1] }

Error: the range of foo is an empty interval.

An interval has been interpreted as having reverted bounds.

{ x in [2,1] }
Error: the range of x is an empty interval.

Interval bounds are replaced by binary floating-point numbers. As a consequence, Gappa can encounter an empty interval when it tightens a range appearing in a goal. For example, the empty set is the biggest representable interval that is a subset of the singleton {1.3}. So Gappa fails to prove the following property.

{ 1.3 in [1.3,1.3] }
Error: the range of 13e-1 is an empty interval.

Error: zero appears as a denominator in a rewriting rule.

Gappa has a detected that a divisor is trivially equal to zero in an expression that appears in a rewriting rule. This is most certainly an error.

{ 1 in ? }
y -> y * (x - x) / (x - x);