- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93ad1995-da7f-48de-8ce3-f03108a7fefb
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1166
    column: 6
    function: trc_trace
  location_invariant:
    string: 1U <= level
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e53f2023-819c-45e8-93cd-3f3e56523cf1
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1166
    column: 6
    function: trc_trace
  location_invariant:
    string: 12U <= line
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad557116-51e5-4347-a7fd-128065446204
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1166
    column: 6
    function: trc_trace
  location_invariant:
    string: a <= 4U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2f1136b-45b8-4449-9ca6-92aff8e36fc0
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1166
    column: 6
    function: trc_trace
  location_invariant:
    string: a <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33453e03-4dda-4f95-9d63-174497b2a35d
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1166
    column: 6
    function: trc_trace
  location_invariant:
    string: level <= 64U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78939c15-eb24-435b-b1ba-144be48fabf4
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1166
    column: 6
    function: trc_trace
  location_invariant:
    string: level <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3807f916-30bb-4ca1-9a71-eb1b889510f5
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1166
    column: 6
    function: trc_trace
  location_invariant:
    string: line <= 85U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 254ac315-18d1-44bd-8cbf-3fd342d2dad6
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1166
    column: 6
    function: trc_trace
  location_invariant:
    string: line <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e9d624e-e8c7-4ee9-afc1-3144c2b1d8ab
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1166
    column: 6
    function: trc_trace
  location_invariant:
    string: level != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10eebbe1-dda1-4c5c-b6e7-b4460b8726f6
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1166
    column: 6
    function: trc_trace
  location_invariant:
    string: line != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a404b9fe-2d86-4003-beac-72a72532835d
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1179
    column: 6
    function: trc_trace
  location_invariant:
    string: 1U <= level
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d0bd9f9-6d1c-46ed-a0ce-1597c2bb31e0
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1179
    column: 6
    function: trc_trace
  location_invariant:
    string: 12U <= line
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9334e659-8895-4df7-9ffd-facfc73d5179
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1179
    column: 6
    function: trc_trace
  location_invariant:
    string: a <= 4U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd4a5e44-9ba8-4d69-ab15-e44125844847
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1179
    column: 6
    function: trc_trace
  location_invariant:
    string: a <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8c807e7-e21a-4c95-9b8e-5a9cba15aa82
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1179
    column: 6
    function: trc_trace
  location_invariant:
    string: level <= 64U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8f09114-3b96-4c7c-a941-b9ab7e67fb68
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1179
    column: 6
    function: trc_trace
  location_invariant:
    string: level <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c89c9c0-efdd-4c41-91e8-9a4b9002471a
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1179
    column: 6
    function: trc_trace
  location_invariant:
    string: line <= 85U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b664a83d-3b94-4ba5-a1df-07fe56ab98b7
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1179
    column: 6
    function: trc_trace
  location_invariant:
    string: line <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a2af4aa-4cb7-4514-a948-d5bd40cd939e
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1179
    column: 6
    function: trc_trace
  location_invariant:
    string: level != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be165f1e-3326-4342-bc5d-dabbd7951bd1
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1179
    column: 6
    function: trc_trace
  location_invariant:
    string: line != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e3525af-a6a9-432e-a2ca-cfef99e1c7b0
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1222
    column: 6
    function: trc_trace
  location_invariant:
    string: 1U <= level
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a872ee6-1e18-4c30-bbe7-083667eb2cdc
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1222
    column: 6
    function: trc_trace
  location_invariant:
    string: 12U <= line
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d741f96-f7e5-4ebd-bcbe-f3d3aa567870
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1222
    column: 6
    function: trc_trace
  location_invariant:
    string: a <= 4U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d24ede0d-ed3d-4b35-8b39-8f76a74542d0
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1222
    column: 6
    function: trc_trace
  location_invariant:
    string: a <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 670207ac-c59c-4f26-a162-9b5f6d590288
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1222
    column: 6
    function: trc_trace
  location_invariant:
    string: level <= 64U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 666739af-f979-4eb6-9ec1-80ca17f0655a
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1222
    column: 6
    function: trc_trace
  location_invariant:
    string: level <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08c26958-70bb-4317-ade8-62db4837d802
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1222
    column: 6
    function: trc_trace
  location_invariant:
    string: line <= 85U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 473a0c18-770c-472f-9d07-b378770b8581
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1222
    column: 6
    function: trc_trace
  location_invariant:
    string: line <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e440bf45-afb3-4f4b-9fd7-eda1159f6262
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1222
    column: 6
    function: trc_trace
  location_invariant:
    string: level != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea9a2782-9b95-470d-a535-13ed795c0446
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1222
    column: 6
    function: trc_trace
  location_invariant:
    string: line != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9e60686-352d-4608-bc23-77dd3931753e
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: 0 <= unit
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4fbd5b14-0ee3-44ee-81c3-499c5b628fc8
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: 0 <= thread
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4e139e8-e081-4285-be57-c43e4f4e0025
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: 1U <= level
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f77647d0-31f2-4bbb-a435-000cb209dfe7
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: 12U <= line
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57d0c1f4-2dfd-4b75-bbe8-42c37e33f3e5
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: a <= 4U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e064069d-60c4-4fb8-99fd-304da26cfe01
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: a <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82adb089-e080-413f-94f7-ade03a674594
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: level <= 64U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80009ba8-2d17-4115-a2f6-45b10c81605e
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: level <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8023fbf-5846-4b09-b0e8-34fdcecfddd0
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: line <= 85U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc650d49-26fb-4c14-9b09-e0734b9f7314
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: line <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d18266f0-6b57-4e13-9163-105b629fd2c4
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: unit <= 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3cc4d7d-9a33-45b3-ac83-3b783762c5e0
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: thread <= 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57bfee90-bb93-4d77-b2a4-cac452107a03
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: level != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb757661-e11c-4342-af85-db4b4594b231
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1274
    column: 2
    function: trc_trace
  location_invariant:
    string: line != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49d5d1b5-3431-4368-af8e-461a9a3ebdb6
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 737
    column: 2
    function: trc_turn_thread_on
  location_invariant:
    string: 0 <= ret
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29a1f3dd-930a-40b1-a80e-3ef187136d31
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 737
    column: 2
    function: trc_turn_thread_on
  location_invariant:
    string: ret <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 72790f5b-e32a-4fa4-8769-8872057d3b64
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 879
    column: 9
    function: trc_add_level
  loop_invariant:
    string: i <= 307U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 58725b64-adce-47b2-8991-e1a4bea2c7cb
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 881
    column: 11
    function: trc_add_level
  loop_invariant:
    string: i <= 306U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 55e13807-ed05-4c94-9fb1-d920b14b39b1
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 642
    column: 11
    function: trc_remove_thread
  loop_invariant:
    string: 0 <= ret
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7506d9a5-cebc-4472-a3c9-512454ab2916
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 642
    column: 11
    function: trc_remove_thread
  loop_invariant:
    string: ret <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9897dca8-fbcc-45ce-bf3d-11e0d9e58aae
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1263
    column: 11
    function: trc_trace
  loop_invariant:
    string: 0 <= unit
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 83397510-0d4b-4bf8-b1f6-1a0371ddc94c
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1263
    column: 11
    function: trc_trace
  loop_invariant:
    string: 0 <= thread
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2dfe33d9-1343-4b00-8b67-6616a1ea4ce6
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1263
    column: 11
    function: trc_trace
  loop_invariant:
    string: unit <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d2321e6-2def-4ad2-8a51-9979e4f120c2
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 1263
    column: 11
    function: trc_trace
  loop_invariant:
    string: thread <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: be4115cd-c255-425c-8b72-e1e6f66dc8e2
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 436
    column: 9
    function: trc_init
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 96866c19-3b0a-4724-b45d-03816390c60a
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/ctrace_comb.c
    file_hash: 8286f88b59628d8b6d907707fae2a99e55c0d27b6edf55966eaafaefc219c6ea
    line: 436
    column: 9
    function: trc_init
  loop_invariant:
    string: i <= 307
    type: assertion
    format: C
