def_exc bounds refinement is asymmetric

[sim642]

This is something I found out while tracing various versions during PR #1756 and is added as a test there:

  if (-10 <= x) {
    __goblint_check(-128 <= x);
  }

  if (x <= 10) {
    __goblint_check(x <= 127); // TODO
  }

Turns out that def_exc refinements on the negative side are more precise than on the positive side. In particular:

1. starting (-10) returns [-7,31] for an int.
2. ending 10 returns [-31,31], although [-31,7] would make much more sense.
3. of_interval (-10, 10) looks like it returns [-7,7], although this can't be tested with refinements from the C program itself.

The latter point is particularly interesting and relevant for #1756. Base analysis branch refinement only uses starting and ending and can meet conjunctive bounds together, which for -10 <= x && x <= 10 returns [-7,31]. This is less precise than what def_exc's of_interval would like to return (but we cannot use it directly for that).
Thus, this causes an inconsistency where meet of starting and ending is less precise than of_interval for no good reason. Base analysis refinement has been designed with the assumption that this wouldn't be the case.

[sim642]

This is somehow related to PR #1723, although it doesn't need such a generalization.
Still, the behavior of IntDomain0.Size.min_range_sign_agnostic is weird and seems to cause the asymmetric bounds.