Merge branch 'master' into issue-1722

Author: sim642

.git-blame-ignore-revs

@@ -43,3 +43,6 @@ c3e2cc848479ae86de5542b6ab0e75a74e9cf8c9
 
 # Trim trailing whitespace in BitfieldDomain
 d4e2a5f84ed3b7fbff89e34b2f7833de975e0671
+
+# Fix BaseInvariant indentation
+15e7a7ebd34e9fabdd4129e97eb86830fea8395f

.github/workflows/metadata.yml

@@ -42,7 +42,7 @@ jobs:
         uses: actions/checkout@v5
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v4
+        uses: actions/setup-node@v5
         with:
           node-version: ${{ matrix.node-version }}
 

.github/workflows/options.yml

@@ -18,7 +18,7 @@ jobs:
         uses: actions/checkout@v5
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v4
+        uses: actions/setup-node@v5
         with:
           node-version: ${{ matrix.node-version }}
 

.github/workflows/semgrep.yml

@@ -22,7 +22,7 @@ jobs:
         run: semgrep scan --config .semgrep/ --sarif > semgrep.sarif
 
       - name: Upload SARIF file to GitHub Advanced Security Dashboard
-        uses: github/codeql-action/upload-sarif@v3
+        uses: github/codeql-action/upload-sarif@v4
         with:
           sarif_file: semgrep.sarif
         if: always()

.github/workflows/unlocked.yml

@@ -224,7 +224,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v4
+        uses: actions/setup-node@v5
         with:
           node-version: ${{ matrix.node-version }}
 

CHANGELOG.md

@@ -1,18 +1,19 @@
-## v2.6.0 Awkward Aardvark (unreleased)
+## v2.6.0 Awkward Aardvark
 * Add division by zero analysis (#1764).
 * Add bitfield domain (#1623).
 * Add weakly-relational C-2PO pointer analysis (#1485).
 * Add widening delay (#1358, #1442, #1483).
 * Add narrowing of globals to top-down solver (#1636).
 * Add weak dependencies to top-down solver (#1746, #1747).
 * Add YAML ghost witness generation (#1394).
+* Remove GraphML witness generation (#1732, #1733, #1738).
 * Use C standard option for preprocessing (#1807).
 * Add bash completion for array options (#1670, #1705, #1750).
 * Make `malloc(0)` semantics configurable (#1418, #1777).
 * Update path-sensitive analyses (#1785, #1791, #1792).
 * Fix evaluation of library function arguments (#1758, #1761).
 * Optimize affine equalities analysis using sparse matrices (#1459, #1625).
-* Prepare for parallelism (#1708, #1744, #1748).
+* Prepare for parallelism (#1708, #1744, #1748, #1781, #1790).
 
 ## v2.5.0
 Functionally equivalent to Goblint in SV-COMP 2025.

conf/svcomp-ghost.json

@@ -114,6 +114,7 @@
   "witness": {
     "yaml": {
       "enabled": true,
+      "sv-comp-true-only": false,
       "format-version": "2.1",
       "entry-types": [
         "flow_insensitive_invariant",

conf/svcomp.json

@@ -91,6 +91,7 @@
   "witness": {
     "yaml": {
       "enabled": true,
+      "sv-comp-true-only": false,
       "format-version": "2.0",
       "entry-types": [
         "invariant_set"

conf/svcomp24.json

@@ -110,6 +110,7 @@
   "witness": {
     "yaml": {
       "enabled": true,
+      "sv-comp-true-only": false,
       "format-version": "2.0",
       "entry-types": [
         "invariant_set"

conf/svcomp25.json

@@ -91,6 +91,7 @@
   "witness": {
     "yaml": {
       "enabled": true,
+      "sv-comp-true-only": false,
       "format-version": "2.0",
       "entry-types": [
         "invariant_set"