- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 091c1a92-4622-46a1-81d1-e398e4cf5860
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1156
    column: 2
    function: http_get
  location_invariant:
    string: (-0x7FFFFFFF-1) <= foffset
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79c82bc0-8dd1-4b42-8ab2-04eed3bef5ff
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1156
    column: 2
    function: http_get
  location_invariant:
    string: -2147483647 <= dr
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a0c9845-1723-4ffa-9c46-0414604e46b6
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1156
    column: 2
    function: http_get
  location_invariant:
    string: 1 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f57e541d-8366-4752-b944-4e76644b55cc
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1156
    column: 2
    function: http_get
  location_invariant:
    string: foffset <= 2147483647L
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 828c5bab-beba-42c1-9cb5-ba732ebee059
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1156
    column: 2
    function: http_get
  location_invariant:
    string: sd != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c561da2-6112-4b72-ad36-3b4a420bdaba
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1156
    column: 2
    function: http_get
  location_invariant:
    string: dr != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83414789-1fad-4881-abbb-f6a736d321b4
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1168
    column: 4
    function: http_get
  location_invariant:
    string: (-0x7FFFFFFF-1) <= foffset
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d03a9fb-5d12-494d-9a9a-b651f3012b84
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1168
    column: 4
    function: http_get
  location_invariant:
    string: 1 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73872b6c-aa6d-4170-90d4-4da0d436efd8
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1168
    column: 4
    function: http_get
  location_invariant:
    string: foffset <= 2147483647L
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff9f0241-954a-439c-9d50-09f2d910143d
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1168
    column: 4
    function: http_get
  location_invariant:
    string: sd != -1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 64288795-5ae1-4135-9b22-6f8001f20c76
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 788
    column: 9
    function: revstr
  loop_invariant:
    string: size != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ff75c7ed-9c3f-4443-9c33-f6ff1a0b8aa2
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 846
    column: 9
    function: updateProgressBar
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 49834360-cf18-45d0-92d1-b16e8fb58d36
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 851
    column: 9
    function: updateProgressBar
  loop_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 91c071af-1acc-48ef-b5a4-1658fa04a9a9
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 985
    column: 11
    function: http_head_req
  loop_invariant:
    string: sd != -1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1603cb89-0a92-47ba-aaee-bbdb3899f2a0
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 401
    column: 9
    function: get
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e6574b1-5ebd-4610-804b-05007fc7ea33
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 401
    column: 9
    function: get
  loop_invariant:
    string: 0 <= ret
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 87936d13-8a99-45f9-af90-1c7d647a4ebc
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 401
    column: 9
    function: get
  loop_invariant:
    string: ret <= 10
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a3b7778c-9574-4681-9058-36ff69c923cf
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 401
    column: 9
    function: get
  loop_invariant:
    string: ret <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 03a6eb40-e155-4fa0-bf69-cf27c5b3aa13
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 401
    column: 9
    function: get
  loop_invariant:
    string: fd != -1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f8bd0305-6bdf-4027-89ef-1991794d3ed3
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1036
    column: 9
    function: sigint_handler
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e49bd66-9815-401b-a45b-9b9bc8cce475
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 427
    column: 9
    function: get
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5bc93323-c055-4ee9-8280-2c9e4cf71bf5
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 427
    column: 9
    function: get
  loop_invariant:
    string: 0 <= ret
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dba98586-30ad-4d60-92bd-8fecab270e07
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 427
    column: 9
    function: get
  loop_invariant:
    string: 0 <= nok
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 903f4d15-8790-4c65-b967-26f8e7eb82a0
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 427
    column: 9
    function: get
  loop_invariant:
    string: ret <= 10
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c18f56b6-c0b7-4835-a486-6cf463d4d46e
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 427
    column: 9
    function: get
  loop_invariant:
    string: ret <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: aa16f782-c895-45b4-bb59-9b0528b38c1a
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 427
    column: 9
    function: get
  loop_invariant:
    string: fd != -1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c6389230-a87a-4476-90e3-1a21da6281fc
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1133
    column: 9
    function: http_get
  loop_invariant:
    string: (-0x7FFFFFFF-1) <= foffset
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f095764-53cd-4311-bd51-7256e5a6eb08
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1133
    column: 9
    function: http_get
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c3ac6f7a-3ffa-4c0f-ad89-e35527591e7b
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1133
    column: 9
    function: http_get
  loop_invariant:
    string: foffset <= 2147483647L
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1aada8e7-20a3-4bd4-bcf0-5f8d2cdab3fb
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1133
    column: 9
    function: http_get
  loop_invariant:
    string: sd != -1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 815ea5ce-fa35-43d9-a1af-d1c1ffb91f37
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1133
    column: 9
    function: http_get
  loop_invariant:
    string: dr != -1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 64b82b18-af0c-4f8b-ba23-31472268eb9d
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 499
    column: 9
    function: resume_get
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d8e32dea-f8e7-4518-a629-a706301227cf
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 499
    column: 9
    function: resume_get
  loop_invariant:
    string: fd != -1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 41a61007-3a04-4dcd-b610-5d00fd995bec
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 511
    column: 9
    function: resume_get
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 89484ece-3300-4ff3-96a6-200871cff0c7
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 511
    column: 9
    function: resume_get
  loop_invariant:
    string: fd != -1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: de0a63d4-6d60-4f0e-b0a7-0fcc54344d9b
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1158
    column: 9
    function: http_get
  loop_invariant:
    string: (-0x7FFFFFFF-1) <= foffset
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 60120f09-273b-4677-8e54-d1e5d7844b1a
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1158
    column: 9
    function: http_get
  loop_invariant:
    string: 1 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fc6f8486-60a6-4b96-af92-27c4fd93db1e
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1158
    column: 9
    function: http_get
  loop_invariant:
    string: foffset <= 2147483647L
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ba7f34d-37fb-4ff9-8349-5a5f0e4e0039
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 1158
    column: 9
    function: http_get
  loop_invariant:
    string: sd != -1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f17bcab5-e50a-4e20-8ac3-e71338b60b78
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 516
    column: 9
    function: resume_get
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c990c6b-69f1-4a98-8b24-6074d3faa96c
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 516
    column: 9
    function: resume_get
  loop_invariant:
    string: 0 <= nok
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7126a0a5-0599-4f9d-b11d-32dca6c9ea8b
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 516
    column: 9
    function: resume_get
  loop_invariant:
    string: fd != -1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c4537477-c11b-439f-904a-6cb87639cc75
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 593
    column: 9
    function: parse_url
  loop_invariant:
    string: -2147483647 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 11fee1e4-686c-4191-b289-4da6c239f5cc
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 593
    column: 9
    function: parse_url
  loop_invariant:
    string: i <= 1025
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2cc50354-e1f7-4523-9648-58fb46f4a6fa
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 599
    column: 13
    function: parse_url
  loop_invariant:
    string: i <= 1024
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 968161ba-afca-4dad-948c-2b3034b70f00
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 609
    column: 13
    function: parse_url
  loop_invariant:
    string: i <= 1024
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d382092f-076d-4f81-bb10-015e7994c06e
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 609
    column: 13
    function: parse_url
  loop_invariant:
    string: j <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 237ff673-4ddb-4015-8e5a-6a9cf5b639c1
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 611
    column: 17
    function: parse_url
  loop_invariant:
    string: i <= 1024
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cbfbaa47-b41a-45f8-8253-437048007895
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 611
    column: 17
    function: parse_url
  loop_invariant:
    string: j <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 131d1553-35dd-48dc-84b2-c6ec979baefb
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 634
    column: 9
    function: parse_url
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e348b9d6-aa0e-4779-80a4-df40800e17bf
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 634
    column: 9
    function: parse_url
  loop_invariant:
    string: i <= 1025
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ea93be04-eb52-4a57-99d4-2a106026d3a0
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 646
    column: 9
    function: parse_url
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b26518d-88a2-4ab4-b024-9f5cb7ca4405
    creation_time: 2023-02-02T15:11:58Z
    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/aget_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/aget_comb.c
    file_hash: bbbaaeb6c6acb00654ea4f158fb6b5ddc5d6c2f07986d0f18b5c4a82ce706290
    line: 646
    column: 9
    function: parse_url
  loop_invariant:
    string: i <= 513
    type: assertion
    format: C
