Bugs in multiple interval_template.h methods

[cesaro]

Multiple methods in src/util/interval_template.h are buggy, because they forget to check for empty intervals. I don't know how to expose CBMC bugs for the issues below, but I suspect that doing so is possible.

Methods is_less_than_eq and is_less_than

Interval [a, b] is less (or equal) than [c,d] if either of them is empty, in addition to the logic that the code in these two methods already implement. With the current implementation, empty interval [4,3] is less than empty interval [5,4], but [6,5] is not less than [5,4], which causes a somewhat arbitrary behavior.

Same remark about operator <= and operator ==, further below in the same file. Empty sets always compare true for equal or less-than-equal.

Method approx_union_with

Interval A union with B is equal to A if B is empty, and equal to B if A is empty (in addition the logic that the method already has). That produces a much better approximate union.