Since rL335814, if the constraint manager cannot find a range set for A - B (where A and B are symbols) it looks for a range for B - A and returns it negated if it exists. However, if a range set for both A - B and B - A is stored then it only returns the first one. If we both use A - B and B - A, these expressions behave as two totally unrelated symbols. This way we miss some useful deductions which may lead to false negatives or false positives.
This tiny patch changes this behavior: if the symbolic expression the constraint manager is looking for is a difference A - B, it tries to retrieve the range for both A - B and B - A and if both exists it returns the intersection of range A - B and the negated range of B - A. This way every time a checker applies new constraints to the symbolic difference or to its negated it always affects both the original difference and its negated.