Make SV-COMP validation strict

goblint · Nov 20, 2023 · ecd48aa · ecd48aa
1 parent f709482
commit ecd48aa
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 3 deletions.
diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json
@@ -114,6 +114,7 @@
     },
     "yaml": {
       "enabled": false,
+      "strict": true,
       "format-version": "2.0",
       "entry-types": [
         "location_invariant",

diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
@@ -2487,6 +2487,12 @@
               "type": "string",
               "default": ""
             },
+            "strict": {
+              "title": "witness.yaml.strict",
+              "description": "",
+              "type": "boolean",
+              "default": false
+            },
             "unassume": {
               "title": "witness.yaml.unassume",
               "description": "YAML witness input path",

diff --git a/src/witness/witness.ml b/src/witness/witness.ml
@@ -665,11 +665,18 @@ struct
     | Some false -> print_svcomp_result "ERROR (verify)"
     | _ ->
       if get_string "witness.yaml.validate" <> "" then (
-        if !YamlWitness.cnt_refuted > 0 then
+        match get_bool "witness.yaml.strict" with
+        | true when !YamlWitness.cnt_error > 0 ->
+          print_svcomp_result "ERROR (witness error)"
+        | true when !YamlWitness.cnt_unsupported > 0 ->
+          print_svcomp_result "ERROR (witness unsupported)"
+        | true when !YamlWitness.cnt_disabled > 0 ->
+          print_svcomp_result "ERROR (witness disabled)"
+        | _ when !YamlWitness.cnt_refuted > 0 ->
           print_svcomp_result (Result.to_string (False None))
-        else if !YamlWitness.cnt_unconfirmed > 0 then
+        | _ when !YamlWitness.cnt_unconfirmed > 0 ->
           print_svcomp_result (Result.to_string Unknown)
-        else
+        | _ ->
           write entrystates
       )
       else