Update YAML witness validation result for refutation under new scorin…

…g schema
goblint · Nov 6, 2024 · 546a8d0 · 546a8d0
1 parent 7719082
commit 546a8d0
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
@@ -892,7 +892,9 @@ struct
     | true when !cnt_disabled > 0 ->
       Error "witness disabled"
     | _ when !cnt_refuted > 0 ->
-      Ok (Svcomp.Result.False None)
+      (* Refuted only when assuming the invariant is reachable. *)
+      (* Ok (Svcomp.Result.False None) *) (* Wasn't a problem because valid*->correctness->false gave 0 points under old validator track scoring schema: https://doi.org/10.1007/978-3-031-22308-2_8. *)
+      Ok Svcomp.Result.Unknown (* Now valid*->correctness->false gives 1p (negative) points under new validator track scoring schema: https://doi.org/10.1007/978-3-031-57256-2_15. *)
     | _ when !cnt_unconfirmed > 0 ->
       Ok Unknown
     | _ ->