v0.3.1

SV-COMP 2026 version

What's Changed

• Use external dependencies from Maven by @schuessf in #694
• Loop invariant based extraction of redundancy sets by @Paswalt in #698
• Refactor assert orders by @schuessf in #699
• Add support for attributes to labels in Boogie by @Heizmann in #702
• Support quantifiers in ACSL by @schuessf in #704
• ASTBuilder: Generate sealed class hierarchy by @maul-esel in #707
• Move FakePointerExpression out of ACSL AST & refactor pointer backtranslation by @maul-esel in #708
• Add auxiliary attribute to labels by @Heizmann in #709
• Refactor unchecked reads to improve support for dereferences in ACSL by @schuessf in #703
• Refactor handling of standard functions and predefined types by @schuessf in #714
• Add locations of interest (LOIs) to ICFG by @Heizmann in #713
• Rename ASSERTandASSUME to CHECK by @Heizmann in #718
• Produce invariants at labels by @Heizmann in #717
• Group settings of C translation by @Heizmann in #719
• Let BlockEncoder throw ToolchainCanceledExceptions by @Heizmann in #721
• Fix nondeterminism bug in BlockEncodingV2 by @Heizmann in #722
• Bugfix: Insert continue label before loop by @Heizmann in #723
• Extend library models to support unpreprocessed C programs by @schuessf in #720
• Support invariants at labels in Referee by @Heizmann in #728
• update c settings by @Heizmann in #734
• Add setting whether ACSL assertions should be checked by @schuessf in #724
• Introduce the memory neutrality property by @Heizmann in #752
• Use Ant build task to generate versioning information by @bahnwaerter in #743
• Move complete handling of functions to MathLibraryModel, support additional functions by @schuessf in #750
• Add 1-Dimensional memory model for memory safe tasks by @jankoerner in #756
• Use multiple AST nodes in CLocation by @schuessf in #760

New Contributors

• @Paswalt made their first contribution in #698
• @jankoerner made their first contribution in #756

Full Changelog: v0.3.0...v0.3.1