Hernan Ponce de Leon

> Why do you say that? Because you wrote _"So from that point of view, it's clear that sref is a subset of sloc."_ Imagine you have something like this...

> In your example, if you say y is an alias to x, then aren't you implicitly assuming they're the same location? This example fits in what I initially wrote...

The last comment was useful, and I think I am starting to understand this. Is the following correct? I can have two instructions accessing the same buffer (reference) and thus...

But wouldn't the offset/range tell you precisely which location you end up accessing? Or could still be the case that the same buffer/offset/range (i.e., reference) access two different locations?

Great. This clarifies it for me. Thanks @jeffbolznv for bearing with me 😅

@jeffbolznv it seems that even if `sref` is not guaranteed to be a subset of `sloc`, [the litmus parser enforces this](https://github.com/KhronosGroup/Vulkan-MemoryModel/blob/master/alloy/litmus.cpp#L573-L596). The initial value of `pgmsloc` at line 573 is...

The tests from 889fcd9bec7dc617578eeb0393b08c3018f0d18a are variants of the test mentioned in #34

The alias analysis did not finish overnight for `benchmarks/folds/was.c`. @xeren do you have any idea why the performance is so bad in this example?

Sorry (spell checker). This code https://github.com/hernanponcedeleon/Dat3M/blob/master/benchmarks/lfds/wsq.c

BTW ... both the field sensitive/insensitive analysis finish below 1 sec and seems to produce good results, e.g. ``` [08.09.2024] 17:14:41 [INFO] AliasAnalysis.fromConfig - Selected alias analysis: FIELD_SENSITIVE [08.09.2024] 17:14:41...