goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

Fix test for relational unassume with strengthening #1387

Closed sim642 closed 3 months ago

sim642 commented 3 months ago

Closes #1373.

The previously-working behavior without type bounds was actually somewhat odd (as explained by the added comments), so it doesn't need to work anymore. The actual update is just to the example which uses <= instead of < in the paper. That avoids the oddity.

This also includes a small Lincons1 fix in strengthening to make the behavior consistent between octagons and polyhedra.