Skip to content

Convert some old YAML witnesses to version 2.0#1812

Merged
sim642 merged 4 commits intomasterfrom
yaml-witness-convert
Sep 29, 2025
Merged

Convert some old YAML witnesses to version 2.0#1812
sim642 merged 4 commits intomasterfrom
yaml-witness-convert

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented Sep 2, 2025

No description provided.

@sim642 sim642 self-assigned this Sep 2, 2025
@sim642 sim642 added cleanup Refactoring, clean-up testing sv-comp SV-COMP (analyses, results), witnesses labels Sep 2, 2025
metadata' used to have format_version 2.0, so never equaled.
Change format_version at the end instead.
@sim642 sim642 added this to the v2.7.0 Bamboozled Buffalo milestone Sep 4, 2025
@sim642 sim642 marked this pull request as ready for review September 4, 2025 10:45
@sim642 sim642 removed their assignment Sep 4, 2025
@sim642 sim642 merged commit 66746b0 into master Sep 29, 2025
15 of 19 checks passed
@sim642 sim642 deleted the yaml-witness-convert branch September 29, 2025 07:00
sim642 added a commit that referenced this pull request Sep 29, 2025
sim642 added a commit to sim642/opam-repository that referenced this pull request Nov 27, 2025
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).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

cleanup Refactoring, clean-up sv-comp SV-COMP (analyses, results), witnesses testing

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant