Skip to content

Move custom YAML witness flow_insensitive_invariant entries under invariant_set#1853

Merged
sim642 merged 2 commits intomasterfrom
yaml-witness-invariant-set-flow-insensitive
Oct 28, 2025
Merged

Move custom YAML witness flow_insensitive_invariant entries under invariant_set#1853
sim642 merged 2 commits intomasterfrom
yaml-witness-invariant-set-flow-insensitive

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented Oct 24, 2025 •
edited
Loading

This is on top of #1852.

This should be almost the final step for getting rid of YAML witness version 0.1 stuff (invariants outside of invariant_set entry).

@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 pr-dependency Depends or builds on another PR, which should be merged before labels Oct 24, 2025
Base automatically changed from yaml-witness-convert-2 to master October 27, 2025 12:46
@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Oct 27, 2025
@sim642 sim642 force-pushed the yaml-witness-invariant-set-flow-insensitive branch from 165933e to 45c04d1 Compare October 27, 2025 13:01
@sim642 sim642 merged commit 9662188 into master Oct 28, 2025
19 checks passed
@sim642 sim642 deleted the yaml-witness-invariant-set-flow-insensitive branch October 28, 2025 13:42
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

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

Projects

None yet

Milestone

v2.7.0 Bamboozled Buffalo

Development

Successfully merging this pull request may close these issues.

1 participant

@sim642