Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Oct 24, 2025

This is a continuation of #1812.
Eventually we can get rid of YAML witnesses version 0.1 support.

@sim642 sim642 added this to the v2.7.0 Bamboozled Buffalo milestone Oct 24, 2025
@sim642 sim642 added cleanup Refactoring, clean-up testing sv-comp SV-COMP (analyses, results), witnesses labels Oct 24, 2025
@sim642 sim642 merged commit 924372d into master Oct 27, 2025
19 checks passed
@sim642 sim642 deleted the yaml-witness-convert-2 branch October 27, 2025 12:46
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.

2 participants