Skip to content

Fix some questionable invariants in SV-COMP 2025 witnesses#1818

Merged
sim642 merged 6 commits intomasterfrom
issue-1722
Oct 23, 2025
Merged

Fix some questionable invariants in SV-COMP 2025 witnesses#1818
sim642 merged 6 commits intomasterfrom
issue-1722

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented Sep 4, 2025

This addresses instances from #1722.

@sim642 sim642 added this to the SV-COMP 2026 milestone Sep 4, 2025
@sim642 sim642 added bug unsound usability sv-comp SV-COMP (analyses, results), witnesses labels Sep 4, 2025
@sim642
Copy link
Copy Markdown
Member Author

sim642 commented Oct 10, 2025

Out of curiosity, I did some experiments to see how the number of invariants in witnesses changed:
image
(https://goblint.cs.ut.ee/results/279-all-pr-1818-after/table-generator-cmp.table.html#/scatter?toolX=2&columnX=5&toolY=3&columnY=5&results=All&line=10&regression=None)

@sim642
Copy link
Copy Markdown
Member Author

sim642 commented Oct 17, 2025

I now did additional fast runs with Goblint Validator also included: https://goblint.cs.ut.ee/results/282-all-validate-pr-1818-after/table-generator-cmp2.table.html#/.

Overall, the number of invariants for the validator changed as follows:

Confirmed Unconfirmed Refuted Error
Before 875324 107439 5923 11330
After 835291 64189 662 9466

The number of unconfirmed and refuted invariants decreased significantly. The decrease in confirmed invariants should not be problematic: if we no longer generate reflexive equalities, then we cannot trivially validate them either.
The number of validated witnesses actually increased from 9304 to 9427.

@sim642 sim642 merged commit 2557b9f into master Oct 23, 2025
21 checks passed
@sim642 sim642 deleted the issue-1722 branch October 23, 2025 07:20
sim642 added a commit that referenced this pull request Oct 23, 2025
@sim642
Fix InvariantCil indentation (PR #1818)
2fa1e42
sim642 added a commit to sim642/opam-repository that referenced this pull request Nov 27, 2025
@sim642
[new release] goblint (2.7.0)
055a60d 
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2026.

* Add sequential portfolio for SV-COMP (goblint/analyzer#1845, goblint/analyzer#1867, goblint/analyzer#1877).
* Add struct bitfield support (goblint/analyzer#1739, goblint/analyzer#1823).
* Improve bitwise operations for integer domains (goblint/analyzer#1739).
* Reimplement HTML output in OCaml (goblint/analyzer#1752).
* Remove YAML witness version 0.1 support (goblint/analyzer#1812, goblint/analyzer#1817, goblint/analyzer#1852, goblint/analyzer#1853, goblint/analyzer#1855).
* Fix incorrect invariants in witnesses (goblint/analyzer#1818, goblint/analyzer#1876).
* Simplify relational invariants in witnesses (goblint/analyzer#1826, goblint/analyzer#1871, goblint/analyzer#1873).
* Fix argument types in Goblint stubs (goblint/analyzer#1684, goblint/analyzer#1814, goblint/analyzer#1779, goblint/analyzer#1820).
@sim642 sim642 mentioned this pull request Nov 27, 2025
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

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

Projects

None yet

Milestone

SV-COMP 2026

Development

Successfully merging this pull request may close these issues.

1 participant

@sim642