SV-COMP'25

This release contains binaries for the SV-COMP'25 competition.

Minimal necessary packages for Ubuntu 24.04 LTS:

• openjdk-17-jre-headless
• libgomp1
• libmpfr-dev
• clang-format (for running the preprocessing step on no-overflow and termination tasks)

What's Changed

• XCFA-refactor 2023 [draft] by @leventeBajczi in #198
• Deploy doc only on master, test always by @leventeBajczi in #250
• Z3 update by @leventeBajczi in #254
• Updated actions to fix release message, docker push by @leventeBajczi in #255
• Docker update by @leventeBajczi in #256
• Disabled llvm-related modules unless clang-15 is installed by @leventeBajczi in #260
• Fix smtinterpol interpolation (#253) by @leventeBajczi in #261
• [AutoPR] Reformatted code by @thetabotmaintainer in #262
• Adding JavaSMT support by @leventeBajczi in #258
• C frontend fix by @leventeBajczi in #252
• Added multi formalism to create product of arbitrary number of formal… by @RipplB in #251
• [AutoPR] Reformatted code by @thetabotmaintainer in #269
• SMTLIB integration fixes by @mondokm in #271
• Enumtype smtlib by @RipplB in #272
• This PR adds support for CHC solving via dedicated CHC solvers (including Z3) by @leventeBajczi in #275
• MDD-based analysis by @mondokm in #281
• Horn checker by @leventeBajczi in #282
• Added bounded portfolio by @AdamZsofi in #284
• Build tool upgrades and other various quality of life improvements by @RipplB in #283
• Change all reference of codestyle to new path by @RipplB in #285
• Allow $ in xsts variable names by @mondokm in #287
• Bounded analysis improvements, CLI bindings for CFA,STS,XSTS by @mondokm in #286
• Update linux-build-test-deploy.yml by @leventeBajczi in #288
• Not using caching builds for maven publish by @leventeBajczi in #290
• Update java-common.gradle.kts by @leventeBajczi in #291
• Portfolio CI update by @leventeBajczi in #293
• Added CHC algorithm to Xsts by @leventeBajczi in #289
• Xsts cli clikt by @RipplB in #292
• XSTS Cli fixes by @mondokm in #294
• added new flag --only-svcomp-witness by @AdamZsofi in #296
• Frontend update 2024 by @leventeBajczi in #305
• Added thorn creation to action by @leventeBajczi in #307
• Spotless instead of intellij formatting by @leventeBajczi in #306
• Reformat fix by @leventeBajczi in #309
• Generalize abstractor, refiner, cegarchecker, visualizer by @RipplB in #304
• Witnesses 2.0 by @leventeBajczi in #312
• Fixed variable naming in ReferenceElimination by @leventeBajczi in #308
• OC checker by @csanadtelbisz in #264
• Minor Xcfa pass & oc checker fixes by @csanadtelbisz in #316
• Added specification transformation by @leventeBajczi in #317
• Document spotless formatting (including plugin and git hook setup) by @AdamZsofi in #320
• EmergenTheta Update by @leventeBajczi in #314
• Added support for _Atomic variable by @leventeBajczi in #318
• Portfolio update by @leventeBajczi in #321
• Ci update by @leventeBajczi in #323
• Xcfa oc checker optimization fix by @csanadtelbisz in #324
• Memsafety and memcleanup by @leventeBajczi in #322
• Fix memloc by @leventeBajczi in #325

New Contributors

• @RipplB made their first contribution in #251

Full Changelog: svcomp24...svcomp25