Skip to content

Conversation

@DrMichaelPetter
Copy link
Collaborator

@DrMichaelPetter DrMichaelPetter commented Nov 7, 2025

A branch to collect newest insights into portfolio configurations and patches for the portfolio runner

  • Embrace context gas
  • Catch goblint not producing any verdict, esp. segfault
  • Deactivate apron octagon autotuner

@DrMichaelPetter DrMichaelPetter added sv-comp SV-COMP (analyses, results), witnesses precision labels Nov 7, 2025
@sim642 sim642 added this to the SV-COMP 2026 milestone Nov 7, 2025
@sim642
Copy link
Member

sim642 commented Nov 10, 2025

Are you still working on some more tuning or should I submit a new SV-COMP artifact with this already?

@DrMichaelPetter
Copy link
Collaborator Author

DrMichaelPetter commented Nov 11, 2025

We are good to go now

@sim642 sim642 merged commit 3ec10b4 into master Nov 11, 2025
19 checks passed
@sim642 sim642 deleted the multishot-tuning branch November 11, 2025 13:48
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

precision sv-comp SV-COMP (analyses, results), witnesses

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants