- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 301d8b49-d4c4-4d2c-a2a6-32d5825a5428
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6497801f-073b-4bac-b649-d84a434a2d4d
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 76917045-b904-4050-a673-878ed5e406ec
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: db470ac2-7210-48b9-ad1f-05d11cc8e2b5
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: f131b84e-bbd5-48bc-9b9b-6aa8be0bdb86
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: -9223372036854775807L <= foffset
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a69fe22f-a434-46a6-8152-b13bbce0afcd
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: a4fb2af5-2fda-4ac0-beba-2d3bd4c853b4
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: dca6dee7-2537-42be-96c2-91f93dbfcd58
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: aecc75b1-3b72-4d44-8e63-fa3bf50344f0
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 75c2d908-9eb2-4f48-8069-3c727026b33b
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 4c6d5d7a-0edf-4f5d-9e99-4185d94a8f39
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 18a464fd-73a7-4e6c-984a-676fd50b90e4
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 2365d1b6-0266-4aac-b179-b204fe777121
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: ce45d939-60e3-442a-b899-be579876152a
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: a4a0097c-3f86-4f60-9a5b-771280c236ab
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 3122ccc7-7daf-4eb9-8b39-1df3274836f7
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 71dbc780-1192-4f20-a161-908455223ca7
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 42352f00-d43e-44dc-ac2e-d5971e30bc89
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 5e8ba511-8b08-446b-a0c5-f7a4b771d956
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 26ee1a75-814b-447c-a3c3-dd4f8ec29c88
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 94ec95c3-3ebc-48c4-8fa8-c2cdcb9dbcbb
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 8618c0a6-30ab-4b19-ac17-f13c13689261
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 4a9b645b-4f6f-43e0-875b-f992369c113a
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 670c6df5-3795-4ab4-854d-f1e52c4d1140
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 81cf4d91-eb88-4547-9c24-c7bf5d6eade1
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 79f780a1-2da1-4ee2-9edc-c29143a07039
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c8aa5654-6a45-4d7f-8378-d9b4d00af5c2
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 1f976f1d-2a52-48d6-bd91-3ba86c135fba
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: dc967b54-6fa3-4b25-807e-446b7a2939c0
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 5fc58e6a-9775-4470-bbfd-8c720563c183
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 322ef0f8-5099-41fe-99ae-669cb28957e6
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 40cec358-363d-4d64-aed6-63a3a8604eff
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 0252e573-db01-4163-8a81-36af8b413a32
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 365e0271-e6de-4a00-a086-4b75c8d7c0a6
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: cec670d4-ce10-430a-b1bd-940bab9184ba
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c08f5eea-b017-49b3-91bb-3c1c5bfb2de7
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 347b45e0-5b91-4ee5-b02d-5c86f206feeb
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 21914f9a-3809-49d6-91ae-1623a76ea16b
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 5a96b713-7c37-463b-9e6d-3d0dee490346
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: fac8d277-cda5-4a96-bb64-236b0075a588
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 066c8b3e-5ee6-4b41-8ecc-9d79c2f7d32e
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c1e8eeb0-e0f7-40dc-825f-7e486ec66b41
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 8ab55492-b182-4453-ac32-f5a4d6bcdaf1
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 023e9484-6c51-4700-a3ba-3f773a5848d9
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c2c900c6-7c96-4723-8602-83b43515d894
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: e00cb6d7-97e3-4a89-8c8a-3a9e0fb5f7ba
    creation_time: 2023-02-02T14:22:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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
