Discrepancy between eager encoding and CAAT with overflowing accesses #642
Description
In the presence of buffer-overflows our alias analysis is unsound and there can be different same-address accesses that are not considered aliasing and thus will not appear in the loc relation of an eager encoding.
However, the CAAT solver established the loc relation in an execution by comparing the address values directly thus ignoring the (unsound) alias analysis.
This results in cases where the CAAT solver and the eager encoding return different verdicts.
What do we do about this?
The alias analysis is intentionally unsound in overflow cases, so we cannot blame this issue on the analysis.
I guess the most reasonable fix is to let CAAT inherit this unsoundness by querying the alias analysis between same-address accesses?
Alternatively we live with this discrepancy as it only appears on benchmarks where we are unsound anyways.