Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Feb 2, 2026

It was revealed by dashboard evaluation that we weren't doing the overflow check at modulo, while Mopsa was.

TODO

@sim642 sim642 added this to the SV-COMP 2027 milestone Feb 2, 2026
@sim642 sim642 added the sv-comp SV-COMP (analyses, results), witnesses label Feb 2, 2026
@sim642 sim642 added the pr-dependency Depends or builds on another PR, which should be merged before label Feb 2, 2026
@sim642
Copy link
Member Author

sim642 commented Feb 3, 2026

I did a fast SV-COMP run with level01 and there's no change to verdicts: https://goblint.cs.ut.ee/results/314-all-level01-pr-1935-after/table-generator-cmp.diff.html.
So this doesn't suddenly cause us to find overflows where we didn't find before in SV-COMP (which certainly would've been possible).

@sim642 sim642 marked this pull request as ready for review February 4, 2026 09:25
@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Feb 4, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug explainability sv-comp SV-COMP (analyses, results), witnesses unsound

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant