SV-COMP 2026 development

.gitignore

@@ -54,6 +54,7 @@ goblint.bc.js
 *.rej
 
 sv-comp/goblint.zip
+scripts/sv-comp/goblint.zip
 
 privPrecCompare
 privPrecCompare-creduce

Makefile

@@ -2,3 +2,21 @@ native :
 
 % :
 	@./make.sh $@
+
+
+.PHONY: sv-comp-tag sv-comp-build sv-comp-smoketest-ubuntu sv-comp-smoketest-competition sv-comp-smoketest sv-comp
+
+sv-comp-tag:
+	git tag -m "SV-COMP 2026" svcomp26
+
+sv-comp-build: sv-comp-tag
+	docker build . -f scripts/sv-comp/Dockerfile --output=scripts/sv-comp/
+
+sv-comp-smoketest-ubuntu: sv-comp-tag
+	docker build . -f scripts/sv-comp/Dockerfile --target smoketest-ubuntu
+
+sv-comp-smoketest-competition: sv-comp-tag
+	docker build . -f scripts/sv-comp/Dockerfile --target smoketest-competition
+
+sv-comp-smoketest: sv-comp-smoketest-ubuntu sv-comp-smoketest-competition;
+sv-comp: sv-comp-smoketest sv-comp-build;

conf/svcomp.json → conf/svcomp26/level00-validate.json

@@ -6,12 +6,11 @@
     },
     "int": {
       "def_exc": true,
-      "enums": false,
-      "interval": true
+      "enums": false
     },
     "float": {
-      "interval": true,
-      "evaluate_math_functions": true
+      "interval": false,
+      "evaluate_math_functions": false
     },
     "activated": [
       "base",
@@ -27,12 +26,12 @@
       "expRelation",
       "mhp",
       "assert",
-      "var_eq",
       "symb_locks",
       "region",
       "thread",
       "threadJoins",
-      "abortUnless"
+      "abortUnless",
+      "unassume"
     ],
     "path_sens": [
       "mutex",
@@ -61,16 +60,16 @@
         "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
-        "enums",
-        "congruence",
-        "octagon",
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
         "noOverflows",
         "termination",
         "tmpSpecialAnalysis"
       ]
+    },
+    "widen": {
+      "tokens": true
     }
   },
   "exp": {
@@ -90,25 +89,25 @@
   },
   "witness": {
     "yaml": {
-      "enabled": true,
-      "sv-comp-true-only": false,
+      "enabled": false,
+      "strict": true,
       "format-version": "2.0",
       "entry-types": [
-        "invariant_set"
+        "invariant_set",
+        "violation_sequence"
       ],
       "invariant-types": [
+        "location_invariant",
         "loop_invariant"
       ]
     },
     "invariant": {
       "loop-head": true,
-      "after-lock": false,
-      "other": false,
-      "accessed": false,
-      "exact": true
+      "after-lock": true,
+      "other": true
     }
   },
   "pre": {
-    "enabled": false
+    "transform-paths": false
   }
 }

conf/svcomp26/level00.json

@@ -6,7 +6,7 @@
     },
     "int": {
       "def_exc": true,
-        "enums": false
+      "enums": false
     },
     "float": {
       "interval": false,
@@ -30,7 +30,7 @@
       "region",
       "thread",
       "threadJoins",
-        "abortUnless"
+      "abortUnless"
     ],
     "path_sens": [
       "mutex",
@@ -39,7 +39,7 @@
       "expsplit",
       "activeSetjmp",
       "memLeak",
-        "threadflag"
+      "threadflag"
     ],
     "context": {
       "widen": false
@@ -86,6 +86,7 @@
   "witness": {
     "yaml": {
       "enabled": true,
+      "sv-comp-true-only": false,
       "format-version": "2.0",
       "entry-types": [
         "invariant_set"
@@ -103,6 +104,6 @@
     }
   },
   "pre": {
-    "enabled": false
+    "transform-paths": false
   }
 }

conf/svcomp-validate.json → conf/svcomp26/level01-validate.json

@@ -113,6 +113,6 @@
     }
   },
   "pre": {
-    "enabled": false
+    "transform-paths": false
   }
 }

conf/svcomp26/level01.json

@@ -109,6 +109,6 @@
     }
   },
   "pre": {
-    "enabled": false
+    "transform-paths": false
   }
 }

conf/svcomp26/level02-validate.json

@@ -0,0 +1,134 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": true,
+      "congruence": true,
+      "bitfield":true,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless",
+      "affeq",
+      "apron",
+      "unassume"
+    ],
+    "apron": {
+      "domain": "octagon"
+    },
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      },
+      "structs": {
+        "domain": "sets"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "reduceAnalyses",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    },
+    "widen": {
+      "tokens": true
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "solvers": {
+    "td3": {
+      "widen_gas": 30,
+      "side_widen_gas": 30
+    }
+  },
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "yaml": {
+      "enabled": false,
+      "strict": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set",
+        "violation_sequence"
+      ],
+      "invariant-types": [
+        "location_invariant",
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": true,
+      "other": true
+    }
+  },
+  "pre": {
+    "transform-paths": false
+  }
+}

conf/svcomp26/level02.json

@@ -107,6 +107,7 @@
   "witness": {
     "yaml": {
       "enabled": true,
+      "sv-comp-true-only": false,
       "format-version": "2.0",
       "entry-types": [
         "invariant_set"
@@ -124,6 +125,6 @@
     }
   },
   "pre": {
-    "enabled": false
+    "transform-paths": false
   }
 }