Known bug causing double-checking alerts: soundness bug in wrapped intervals #1
Description
There is a known bug in the implementation of wrapped intervals here.
We know that there is at least a bug in the implementation of the subtract function. This bug means that sometimes, the interval result is wrongly too large or missing values. Because the interval can be wrongly too large, there are sometimes false positives in the double-checking results on transformed code computation simplification assembly. It is difficult to reproduce, since it manifests only following some code patterns, but is reproducible by running our ASPLOS '24 evaluation scripts with compsimp and doublechecking enabled.
The fix is to at least fix the bug in the subtraction function in wrapped intervals.