Unsoundness due to enabled region-offsets

Open SchiJoha opened this issue 2 years ago • 1 comments

This is the same scenario as in issue #1298. All analyses are set context-insensitively, and the sv-comp test goblint-regression/06-symbeq_04-funloop_hard1.i is analyzed with the svcomp24 configuration. As stated in #1298 the SV-COMP result is true (but false is expected). If one disables the region-offsets analysis ("region-offsets": true ---> "region-offsets": false) in the svcomp24.json configuration, the SV-COMP result is unknown (and hence correct). This may hint at an error in region-offsets.

Dec 19 '23 14:12 SchiJoha