Skip to content

nla-digbench-scaling/geo1-ll2_unwindbound1: no-overflow verdict

In !1515 (merged) this task was added as the buggy version of the fixed task. The MR claimed overflows in the non-scaling versions of the tasks, linking to SV-COMP 2024 results.

However, scaling versions of the same tasks may have different results, especially at low unwinding bound. In particular, in the same results for the scaling tasks Ultimate returned true instead. Nevertheless, it was copied as ll2 with expected no-overflow verdict being false.

@schuessf Was this maybe a mistake and nla-digbench-scaling/geo1-ll2_unwindbound1 doesn't actually contain an overflow? Or where is the overflow supposed to be there?

Goblint's interval analysis cannot find any overflow in that task, nor can I manually. I suppose this might be a special case with the unwinding bound 1.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information