/*@ // before: predicate empty_range(struct Range range) = range.lob == range.upb + 1; */
/*@ // after: predicate empty_range(struct Range range) = range.lob > 0 && range.lob == range.upb + 1; predicate total_range(struct Range range) = range.lob == 0 && range.upb == UINT64_MAX; */