- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd5f55a7-b0e3-473e-8346-0cfdd1a8c751
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 3d8d20e0-2a19-4838-abeb-b2ff7ebb377b
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: c6c6e298-3d7e-4c78-9652-844447b8b0a3
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 4a413c7e-ace0-47cb-8338-08e288c9f59e
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 58125c0c-088c-4771-b257-22f0239f359c
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 1e697daa-857b-494d-bfe0-c50d98a95779
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: f9ac08eb-6e4c-447e-9ebd-7684787d1a07
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: d48d4f02-261a-4d4c-8810-3dd1812fb85a
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 3bc2968a-27e2-4ce4-8c55-2b0d64b2f9b1
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 9f0e9925-eb0d-4620-b222-84f1f610a9fd
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: aac88617-e848-4390-93dd-d090a4e7dfed
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: f2fbe7da-1961-45e9-8ccb-8744b26ed7e9
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 9106fced-d721-4c18-bf5a-ff773c32abf3
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: f1cdeb62-cbcd-4675-a378-9e9b57f57425
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 0a9c94a0-6e77-4f54-8f60-eae2def40603
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 54c459a6-1625-4e8d-8842-301e46232393
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: b166df58-4e02-4e69-a3c8-0e95757ae91d
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: da9acad3-6a34-434b-83d7-d76a44055db9
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: b077c695-2c16-4a35-b4e8-5ee3db2e1b97
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: dbb5ed7d-f5cd-4544-9221-f97ddc509909
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: f833c538-87a2-4fd9-8190-fb3b57fb82dc
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: becbee5a-aca2-493f-a1f4-f522e717eb33
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 188f8b79-8040-4547-ba1a-8ab77a7d565f
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 7024bfd5-72ec-45da-a3c4-33ad130a2738
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 42876311-4394-4ef9-9da4-b4c93f545c01
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 39331f82-2465-44d0-8555-b82400ee91df
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: f8cd4c99-4aea-4fc1-87c9-d2efd61e79ea
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 3043360d-1af1-46d2-9c74-b1c669701f05
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: b9ceafda-f9bf-4dc3-a957-18ad5e8f0734
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 09d7b7f8-50d5-4004-8a5b-4bd3a062b6aa
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 00ee49a9-7c31-4a5e-a164-8d6381055749
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 4c352060-bac1-4d5b-96b5-60f5acb3addc
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 4baba73e-7aef-4ec8-813e-e0e9b0eae00a
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 96792a9b-c376-4c67-b134-7b7def2e25c9
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 9a299a98-419c-45a5-90be-f37d6b22d296
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 47bb581f-1a4c-49ef-aef5-89c49a9f2ea2
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: f4ddb388-12af-4e7b-bfd2-e98d647bfb60
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 511794e2-7f0a-4122-9584-94418c7f5a97
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: e81f7b61-c598-421a-9bef-a08da850eab5
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 96d9b362-73ea-4072-a51b-8f0b930a8b23
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 29a0198a-7a6f-4599-bf9c-e77d5f563c16
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: d78435fb-378a-426d-8a7e-d954778f1ae4
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 8ad7dd5a-9875-4fd8-b5c7-0f6f7f9d4741
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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 != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 410c6672-9183-46aa-82be-ea06357f2597
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: f1107d6d-e3f1-42e0-84f9-1391decfb571
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 7adf5f18-1b50-4d0f-8132-dee386b1e429
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: d6de7c34-ba65-4e82-9370-f9633787ba01
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 20f46a5e-97e4-405f-920a-74fee25448d8
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 6cfb7a6c-57e8-4882-851c-0a2d548fb616
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: 32613ba9-d1fe-4c89-a280-2433673becea
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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: aa70376b-8467-4fcd-a8fe-80e98c1e3002
    creation_time: 2023-02-02T15:11:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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''
        ''mine'' ''/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
