FalsePositiveRefutationBRVisitor had a bug where the constraints were not
properly collected thus crosschecked with Z3.
This patch demonstratest and fixes that bug.
The visitor wanted to collect all the constraints on a BugPath.
Since it is a visitor, it stated the visitation of the BugPath with the node
before the ErrorNode. As a final step, it visited the ErrorNode explicitly,
before it processed the collected constraints.
In principle, the ErrorNode should have visited before every other node.
Since the constraints were collected into a map, mapping each symbol to its
RangeSet, if the map already had a mapping with the symbol, then it was skipped.
This behavior was flawed if:
We already had a constraint on a symbol, but az the end in the ErrorNode we have
a stricter constraint on that. Therefore, this visitor would not utilize that
stricter constraint during the crosscheck validation.