On SV-COMP's SoftwareSystems-DeviceDriversLinux64-ReachSafety, universally enabling region (with offsets), var_eq and symb_locks after these fixes didn't have any unintended consequences. No additional unsoundness appeared (within 60s time limit). In 31 cases a previous timeout/error turned into a correct answer and in 10 cases a previous correct answer turned into a timeout, which isn't too surprising given the extra analyses.

This is necessary to merge, but could you create a low-priority ticket to document some underlying issues that need some further investigation. I can recall the following:

• It is not clear to me why accesses are handled as exp rather than lval.
• The field offset handling is fairly suspect and should be documented. I am not 100% convinced adding field-sensitivity to the region analysis in this way is sound, even for non-overlapping fields.

Was there anything else that was confusing?

in 10 cases a previous correct answer turned into a timeout

Depending on when you ran the tests, some of this might also be due to the narrowing being the same as meet in Def_Exc by mistake which we introduced in #97 and fixed in #100.