diff --git a/conf/svcomp-validate.json b/conf/svcomp-validate.json
new file mode 100644
index 0000000000..a234aeb0d5
--- /dev/null
+++ b/conf/svcomp-validate.json
@@ -0,0 +1,142 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless",
+      "unassume"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+
+        "ldv_malloc",
+
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc",
+        "ldv_kzalloc"
+      ]
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    },
+    "widen": {
+      "tokens": true
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": false
+    },
+    "yaml": {
+      "enabled": false,
+      "strict": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "location_invariant",
+        "loop_invariant",
+        "invariant_set",
+        "violation_sequence"
+      ],
+      "invariant-types": [
+        "location_invariant",
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": true,
+      "other": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index 85b33edc79..8f8892b8be 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -71,18 +71,6 @@ struct
         | _ -> ()
       );
 
-    let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = {
-      file = location.file_name;
-      line = location.line;
-      column = location.column;
-      byte = -1;
-      endLine = -1;
-      endColumn = -1;
-      endByte = -1;
-      synthetic = false;
-    }
-    in
-
     let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.unassume")) with
       | Ok yaml -> yaml
       | Error (`Msg m) ->
@@ -125,7 +113,7 @@ struct
       in
 
       let unassume_location_invariant (location_invariant: YamlWitnessType.LocationInvariant.t) =
-        let loc = loc_of_location location_invariant.location in
+        let loc = YamlWitness.loc_of_location location_invariant.location in
         let inv = location_invariant.location_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
 
@@ -137,7 +125,7 @@ struct
       in
 
       let unassume_loop_invariant (loop_invariant: YamlWitnessType.LoopInvariant.t) =
-        let loc = loc_of_location loop_invariant.location in
+        let loc = YamlWitness.loc_of_location loop_invariant.location in
         let inv = loop_invariant.loop_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
 
@@ -187,7 +175,7 @@ struct
       in
 
       let unassume_precondition_loop_invariant (precondition_loop_invariant: YamlWitnessType.PreconditionLoopInvariant.t) =
-        let loc = loc_of_location precondition_loop_invariant.location in
+        let loc = YamlWitness.loc_of_location precondition_loop_invariant.location in
         let pre = precondition_loop_invariant.precondition.string in
         let inv = precondition_loop_invariant.loop_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
@@ -202,7 +190,7 @@ struct
       let unassume_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) =
 
         let unassume_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
-          let loc = loc_of_location location_invariant.location in
+          let loc = YamlWitness.loc_of_location location_invariant.location in
           let inv = location_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
@@ -214,7 +202,7 @@ struct
         in
 
         let unassume_loop_invariant (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) =
-          let loc = loc_of_location loop_invariant.location in
+          let loc = YamlWitness.loc_of_location loop_invariant.location in
           let inv = loop_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index f26cd50184..7b07c3ca35 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -2608,7 +2608,8 @@
                   "precondition_loop_invariant",
                   "loop_invariant_certificate",
                   "precondition_loop_invariant_certificate",
-                  "invariant_set"
+                  "invariant_set",
+                  "violation_sequence"
                 ]
               },
               "default": [
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 7134211d32..2bdd2ced4c 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -43,13 +43,20 @@ struct
       specification
     }
 
-  let location ~location:(loc: Cil.location) ~(location_function): Location.t = {
-    file_name = loc.file;
-    file_hash = sha256_file loc.file;
-    line = loc.line;
-    column = loc.column;
-    function_ = location_function;
-  }
+  let location ~location:(loc: Cil.location) ~(location_function): Location.t =
+    let file_hash =
+      match GobConfig.get_string "witness.yaml.format-version" with
+      | "0.1" -> Some (sha256_file loc.file)
+      | "2.0" -> None
+      | _ -> assert false
+    in
+    {
+      file_name = loc.file;
+      file_hash;
+      line = loc.line;
+      column = Some loc.column;
+      function_ = Some location_function;
+    }
 
   let invariant invariant: Invariant.t = {
     string = invariant;
@@ -524,6 +531,17 @@ let init () =
       Svcomp.errorwith "witness missing"
     )
 
+let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = {
+  file = location.file_name;
+  line = location.line;
+  column = Option.value location.column ~default:1;
+  byte = -1;
+  endLine = -1;
+  endColumn = -1;
+  endByte = -1;
+  synthetic = false;
+}
+
 module ValidationResult =
 struct
   (* constructor order is important for the chain lattice *)
@@ -562,17 +580,6 @@ struct
   module InvariantParser = WitnessUtil.InvariantParser
   module VR = ValidationResult
 
-  let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = {
-    file = location.file_name;
-    line = location.line;
-    column = location.column;
-    byte = -1;
-    endLine = -1;
-    endColumn = -1;
-    endByte = -1;
-    synthetic = false;
-  }
-
   let validate () =
     let location_locator = Locator.create () in
     let loop_locator = Locator.create () in
@@ -806,6 +813,15 @@ struct
         None
       in
 
+      let validate_violation_sequence (violation_sequence: YamlWitnessType.ViolationSequence.t) =
+        (* TODO: update cnt-s appropriately (needs access to SV-COMP result pre-witness validation) *)
+        (* Nothing needs to be checked here!
+           If program is correct and we can prove it, we output true, which counts as refutation of violation witness.
+           If program is correct and we cannot prove it, we output unknown.
+           If program is incorrect, we output unknown. *)
+        None
+      in
+
       match entry_type_enabled target_type, entry.entry_type with
       | true, LocationInvariant x ->
         validate_location_invariant x
@@ -815,7 +831,9 @@ struct
         validate_precondition_loop_invariant x
       | true, InvariantSet x ->
         validate_invariant_set x
-      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _) ->
+      | true, ViolationSequence x ->
+        validate_violation_sequence x
+      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _ | ViolationSequence _) ->
         incr cnt_disabled;
         M.info_noloc ~category:Witness "disabled entry of type %s" target_type;
         None
diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml
index 1630e05b69..4fc2029801 100644
--- a/src/witness/yamlWitnessType.ml
+++ b/src/witness/yamlWitnessType.ml
@@ -106,29 +106,45 @@ module Location =
 struct
   type t = {
     file_name: string;
-    file_hash: string;
+    file_hash: string option;
     line: int;
-    column: int;
-    function_: string;
+    column: int option;
+    function_: string option;
   }
   [@@deriving ord]
 
   let to_yaml {file_name; file_hash; line; column; function_} =
-    `O [
-      ("file_name", `String file_name);
-      ("file_hash", `String file_hash);
-      ("line", `Float (float_of_int line));
-      ("column", `Float (float_of_int column));
-      ("function", `String function_);
-    ]
+    `O ([
+        ("file_name", `String file_name);
+      ] @ (match file_hash with
+        | Some file_hash -> [
+            ("file_hash", `String file_hash);
+          ]
+        | None ->
+          []
+      ) @ [
+          ("line", `Float (float_of_int line));
+        ] @ (match column with
+        | Some column -> [
+            ("column", `Float (float_of_int column));
+          ]
+        | None ->
+          []
+      ) @ (match function_ with
+        | Some function_ -> [
+            ("function", `String function_);
+          ]
+        | None ->
+          []
+      ))
 
   let of_yaml y =
     let open GobYaml in
     let+ file_name = y |> find "file_name" >>= to_string
-    and+ file_hash = y |> find "file_hash" >>= to_string
+    and+ file_hash = y |> Yaml.Util.find "file_hash" >>= option_map to_string
     and+ line = y |> find "line" >>= to_int
-    and+ column = y |> find "column" >>= to_int
-    and+ function_ = y |> find "function" >>= to_string in
+    and+ column = y |> Yaml.Util.find "column" >>= option_map to_int
+    and+ function_ = y |> Yaml.Util.find "function" >>= option_map to_string in
     {file_name; file_hash; line; column; function_}
 end
 
@@ -426,6 +442,205 @@ struct
   let entry_type = "precondition_loop_invariant_certificate"
 end
 
+module ViolationSequence =
+struct
+
+  module Constraint =
+  struct
+    type t = {
+      value: string;
+      format: string option;
+    }
+    [@@deriving ord]
+
+    let to_yaml {value; format} =
+      `O ([
+          ("value", `String value);
+        ] @ (match format with
+          | Some format -> [
+              ("format", `String format);
+            ]
+          | None ->
+            []
+        ))
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ value = y |> find "value" >>= to_string
+      and+ format = y |> Yaml.Util.find "format" >>= option_map to_string in
+      {value; format}
+  end
+
+  module Assumption =
+  struct
+    type t = {
+      location: Location.t;
+      action: string;
+      constraint_: Constraint.t;
+    }
+    [@@deriving ord]
+
+    let waypoint_type = "assumption"
+
+    let to_yaml' {location; action; constraint_} =
+      [
+        ("location", Location.to_yaml location);
+        ("action", `String action);
+        ("constraint", Constraint.to_yaml constraint_);
+      ]
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ location = y |> find "location" >>= Location.of_yaml
+      and+ action = y |> find "action" >>= to_string
+      and+ constraint_ = y |> find "constraint" >>= Constraint.of_yaml in
+      {location; action; constraint_}
+  end
+
+  module Target =
+  struct
+    type t = {
+      location: Location.t;
+      action: string;
+    }
+    [@@deriving ord]
+
+    let waypoint_type = "target"
+
+    let to_yaml' {location; action} =
+      [
+        ("location", Location.to_yaml location);
+        ("action", `String action);
+      ]
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ location = y |> find "location" >>= Location.of_yaml
+      and+ action = y |> find "action" >>= to_string in
+      {location; action}
+  end
+
+  module FunctionEnter =
+  struct
+    include Target
+
+    let waypoint_type = "function_enter"
+  end
+
+  module FunctionReturn =
+  struct
+    include Assumption
+
+    let waypoint_type = "function_return"
+  end
+
+  module Branching =
+  struct
+    include Assumption
+
+    let waypoint_type = "branching"
+  end
+
+  (* TODO: could maybe use GADT, but adds ugly existential layer to entry type pattern matching *)
+  module WaypointType =
+  struct
+    type t =
+      | Assumption of Assumption.t
+      | Target of Target.t
+      | FunctionEnter of FunctionEnter.t
+      | FunctionReturn of FunctionReturn.t
+      | Branching of Branching.t
+    [@@deriving ord]
+
+    let waypoint_type = function
+      | Assumption _ -> Assumption.waypoint_type
+      | Target _ -> Target.waypoint_type
+      | FunctionEnter _ -> FunctionEnter.waypoint_type
+      | FunctionReturn _ -> FunctionReturn.waypoint_type
+      | Branching _ -> Branching.waypoint_type
+
+    let to_yaml' = function
+      | Assumption x -> Assumption.to_yaml' x
+      | Target x -> Target.to_yaml' x
+      | FunctionEnter x -> FunctionEnter.to_yaml' x
+      | FunctionReturn x -> FunctionReturn.to_yaml' x
+      | Branching x -> Branching.to_yaml' x
+
+    let of_yaml y =
+      let open GobYaml in
+      let* waypoint_type = y |> find "type" >>= to_string in
+      if waypoint_type = Assumption.waypoint_type then
+        let+ x = y |> Assumption.of_yaml in
+        Assumption x
+      else if waypoint_type = Target.waypoint_type then
+        let+ x = y |> Target.of_yaml in
+        Target x
+      else if waypoint_type = FunctionEnter.waypoint_type then
+        let+ x = y |> FunctionEnter.of_yaml in
+        FunctionEnter x
+      else if waypoint_type = FunctionReturn.waypoint_type then
+        let+ x = y |> FunctionReturn.of_yaml in
+        FunctionReturn x
+      else if waypoint_type = Branching.waypoint_type then
+        let+ x = y |> Branching.of_yaml in
+        Branching x
+      else
+        Error (`Msg "type")
+  end
+
+  module Waypoint =
+  struct
+    type t = {
+      waypoint_type: WaypointType.t;
+    }
+    [@@deriving ord]
+
+    let to_yaml {waypoint_type} =
+      `O [
+        ("waypoint", `O ([
+             ("type", `String (WaypointType.waypoint_type waypoint_type));
+           ] @ WaypointType.to_yaml' waypoint_type)
+        )
+      ]
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ waypoint_type = y |> find "waypoint" >>= WaypointType.of_yaml in
+      {waypoint_type}
+  end
+
+  module Segment =
+  struct
+    type t = {
+      segment: Waypoint.t list;
+    }
+    [@@deriving ord]
+
+    let to_yaml {segment} =
+      `O [("segment", `A (List.map Waypoint.to_yaml segment))]
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ segment = y |> find "segment" >>= list >>= list_map Waypoint.of_yaml in
+      {segment}
+  end
+
+  type t = {
+    content: Segment.t list;
+  }
+  [@@deriving ord]
+
+  let entry_type = "violation_sequence"
+
+  let to_yaml' {content} =
+    [("content", `A (List.map Segment.to_yaml content))]
+
+  let of_yaml y =
+    let open GobYaml in
+    let+ content = y |> find "content" >>= list >>= list_map Segment.of_yaml in
+    {content}
+end
+
 (* TODO: could maybe use GADT, but adds ugly existential layer to entry type pattern matching *)
 module EntryType =
 struct
@@ -437,6 +652,7 @@ struct
     | LoopInvariantCertificate of LoopInvariantCertificate.t
     | PreconditionLoopInvariantCertificate of PreconditionLoopInvariantCertificate.t
     | InvariantSet of InvariantSet.t
+    | ViolationSequence of ViolationSequence.t
   [@@deriving ord]
 
   let entry_type = function
@@ -447,6 +663,7 @@ struct
     | LoopInvariantCertificate _ -> LoopInvariantCertificate.entry_type
     | PreconditionLoopInvariantCertificate _ -> PreconditionLoopInvariantCertificate.entry_type
     | InvariantSet _ -> InvariantSet.entry_type
+    | ViolationSequence _ -> ViolationSequence.entry_type
 
   let to_yaml' = function
     | LocationInvariant x -> LocationInvariant.to_yaml' x
@@ -456,6 +673,7 @@ struct
     | LoopInvariantCertificate x -> LoopInvariantCertificate.to_yaml' x
     | PreconditionLoopInvariantCertificate x -> PreconditionLoopInvariantCertificate.to_yaml' x
     | InvariantSet x -> InvariantSet.to_yaml' x
+    | ViolationSequence x -> ViolationSequence.to_yaml' x
 
   let of_yaml y =
     let open GobYaml in
@@ -481,6 +699,9 @@ struct
     else if entry_type = InvariantSet.entry_type then
       let+ x = y |> InvariantSet.of_yaml in
       InvariantSet x
+    else if entry_type = ViolationSequence.entry_type then
+      let+ x = y |> ViolationSequence.of_yaml in
+      ViolationSequence x
     else
       Error (`Msg "entry_type")
 end
diff --git a/tests/regression/witness/violation.t/correct-hard.c b/tests/regression/witness/violation.t/correct-hard.c
new file mode 100644
index 0000000000..ce2b50a0c0
--- /dev/null
+++ b/tests/regression/witness/violation.t/correct-hard.c
@@ -0,0 +1,9 @@
+void reach_error(){}
+extern int __VERIFIER_nondet_int();
+
+int main() {
+  int x = __VERIFIER_nondet_int();
+  if (x != x)
+    reach_error();
+  return 0;
+}
diff --git a/tests/regression/witness/violation.t/correct-hard.yml b/tests/regression/witness/violation.t/correct-hard.yml
new file mode 100644
index 0000000000..b8af2c2193
--- /dev/null
+++ b/tests/regression/witness/violation.t/correct-hard.yml
@@ -0,0 +1,26 @@
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.0"
+    uuid: 4412af70-389a-475e-849c-e57e5b92019e
+    creation_time: 2024-06-14T15:35:00+03:00
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - correct-hard.c
+      input_file_hashes:
+        correct-hard.c: 5cc49c1ce5a9aef64286c2a6e57f6955c5f4f9b19b43056507ae87a802802447
+      specification: G ! call(reach_error())
+      data_model: ILP32
+      language: C
+  content:
+  - segment:
+    - waypoint:
+        type: target
+        action: follow
+        location:
+          file_name: correct-hard.c
+          line: 7
+          column: 5
+          function: main
diff --git a/tests/regression/witness/violation.t/correct.c b/tests/regression/witness/violation.t/correct.c
new file mode 100644
index 0000000000..30f58a2f7e
--- /dev/null
+++ b/tests/regression/witness/violation.t/correct.c
@@ -0,0 +1,5 @@
+void reach_error(){}
+
+int main() {
+  return 0;
+}
diff --git a/tests/regression/witness/violation.t/correct.yml b/tests/regression/witness/violation.t/correct.yml
new file mode 100644
index 0000000000..1f1d4f41da
--- /dev/null
+++ b/tests/regression/witness/violation.t/correct.yml
@@ -0,0 +1,26 @@
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.0"
+    uuid: 4412af70-389a-475e-849c-e57e5b92019d
+    creation_time: 2024-06-14T15:35:00+03:00
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - correct.c
+      input_file_hashes:
+        correct.c: 6f760cf7f33fc152738bf3514fe623cc94e52cad9ddc2f0e744595ce0de07530
+      specification: G ! call(reach_error())
+      data_model: ILP32
+      language: C
+  content:
+  - segment:
+    - waypoint:
+        type: target
+        action: follow
+        location:
+          file_name: correct.c
+          line: 4
+          column: 3
+          function: main
diff --git a/tests/regression/witness/violation.t/incorrect.c b/tests/regression/witness/violation.t/incorrect.c
new file mode 100644
index 0000000000..ff56fa2ef4
--- /dev/null
+++ b/tests/regression/witness/violation.t/incorrect.c
@@ -0,0 +1,6 @@
+void reach_error(){}
+
+int main() {
+  reach_error();
+  return 0;
+}
diff --git a/tests/regression/witness/violation.t/incorrect.yml b/tests/regression/witness/violation.t/incorrect.yml
new file mode 100644
index 0000000000..dd57ce3ca1
--- /dev/null
+++ b/tests/regression/witness/violation.t/incorrect.yml
@@ -0,0 +1,26 @@
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.0"
+    uuid: 4412af70-389a-475e-849c-e57e5b92019c
+    creation_time: 2024-06-14T15:35:00+03:00
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - incorrect.c
+      input_file_hashes:
+        incorrect.c: 1af4fd9e76418e4b95af9950b58248127e7c2d9eb791e1c9b92da53952e0fca2
+      specification: G ! call(reach_error())
+      data_model: ILP32
+      language: C
+  content:
+  - segment:
+    - waypoint:
+        type: target
+        action: follow
+        location:
+          file_name: incorrect.c
+          line: 4
+          column: 3
+          function: main
diff --git a/tests/regression/witness/violation.t/run.t b/tests/regression/witness/violation.t/run.t
new file mode 100644
index 0000000000..1fc408635e
--- /dev/null
+++ b/tests/regression/witness/violation.t/run.t
@@ -0,0 +1,57 @@
+Violation witness for a correct program can be refuted by proving the program correct and returning `true`:
+
+  $ goblint --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct.c --set witness.yaml.validate correct.yml
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
+  [Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (correct.c:1:1-1:20)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 1 (1 in uncalled functions)
+    total lines: 3
+  [Info][Witness] witness validation summary:
+    confirmed: 0
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 0
+  SV-COMP result: true
+
+If a correct progtam cannot be proven correct, return `unknown` for the violation witness:
+
+  $ goblint --set ana.activated[-] expRelation --enable ana.sv-comp.functions --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct-hard.c --set witness.yaml.validate correct-hard.yml
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Info][Witness] witness validation summary:
+    confirmed: 0
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 0
+  SV-COMP result: unknown
+
+Violation witness for an incorrect program cannot be proven correct, so return `unknown`:
+
+  $ goblint --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" incorrect.c --set witness.yaml.validate incorrect.yml
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 0
+    total lines: 4
+  [Info][Witness] witness validation summary:
+    confirmed: 0
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 0
+  SV-COMP result: unknown
diff --git a/tests/util/yamlWitnessStrip.ml b/tests/util/yamlWitnessStrip.ml
index 8a5046d6ff..1c015b0f67 100644
--- a/tests/util/yamlWitnessStrip.ml
+++ b/tests/util/yamlWitnessStrip.ml
@@ -10,8 +10,13 @@ struct
 
   let strip_file_hashes {entry_type} =
     let stripped_file_hash = "$FILE_HASH" in
-    let location_strip_file_hash location: Location.t =
-      {location with file_hash = stripped_file_hash}
+    let location_strip_file_hash (location: Location.t): Location.t =
+      let file_hash =
+        match location.file_hash with
+        | Some _ -> Some stripped_file_hash (* TODO: or just map to None always? *)
+        | None -> None
+      in
+      {location with file_hash}
     in
     let target_strip_file_hash target: Target.t =
       {target with file_hash = stripped_file_hash}
@@ -26,6 +31,25 @@ struct
       in
       {invariant_type}
     in
+    let waypoint_strip_file_hash ({waypoint_type}: ViolationSequence.Waypoint.t): ViolationSequence.Waypoint.t =
+      let waypoint_type: ViolationSequence.WaypointType.t =
+        match waypoint_type with
+        | Assumption x ->
+          Assumption {x with location = location_strip_file_hash x.location}
+        | Target x ->
+          Target {x with location = location_strip_file_hash x.location}
+        | FunctionEnter x ->
+          FunctionEnter {x with location = location_strip_file_hash x.location}
+        | FunctionReturn x ->
+          FunctionReturn {x with location = location_strip_file_hash x.location}
+        | Branching x ->
+          Branching {x with location = location_strip_file_hash x.location}
+      in
+      {waypoint_type}
+    in
+    let segment_strip_file_hash ({segment}: ViolationSequence.Segment.t): ViolationSequence.Segment.t =
+      {segment = List.map waypoint_strip_file_hash segment}
+    in
     let entry_type: EntryType.t =
       match entry_type with
       | LocationInvariant x ->
@@ -42,6 +66,8 @@ struct
         PreconditionLoopInvariantCertificate {x with target = target_strip_file_hash x.target}
       | InvariantSet x ->
         InvariantSet {content = List.map invariant_strip_file_hash x.content}
+      | ViolationSequence x ->
+        ViolationSequence {content = List.map segment_strip_file_hash x.content}
     in
     {entry_type}