- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8066d7e8-6a9d-48f7-a516-cc3b8545af9c
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: ea98e2b8-cc12-489f-9ae9-2e3957ac0df7
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: d93fef3e-c877-4c61-b4f8-b8cf219757ac
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 433d40d6-41f0-4648-b493-e8bf52bb6f4c
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 7f6d889c-69ee-4cfa-8aa1-395abf7ffb9f
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 3932e7cd-bf70-4aa1-9062-29a3a11a6adb
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: e54f3d6a-d1e9-4bac-82fd-452c21237f29
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: e92d33a4-f817-459b-ada8-b48aac249c9d
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: d90fa7ea-4e91-4be3-848b-b6b6f09750a3
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: be9691e3-3c35-44da-8807-815f892f9d31
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: be391cb7-d22c-4d49-8d0e-353632bc893e
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 8a06492d-9d84-48b2-a0d6-3cd3e76e433e
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 6474dd89-1c50-4ffc-b6ba-18e254f23618
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 50695d09-f6aa-481f-89f1-d072ca4bd458
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: e6da69ae-5197-483c-a0e2-7985de71213d
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: c5100448-0080-4fe2-aede-6e1ec7005029
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: cb63168e-f98c-4d60-9d35-5602b04fb10d
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 878e76f1-d732-4fda-aa9a-cae5f75f3d11
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 326c5b12-6df5-4916-9dc5-047d673d6ef2
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 0728c34f-b8ee-47ea-8d81-61cee168bf6d
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 7bef3bd7-179f-478c-a159-188d6ba91510
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: c8761576-e330-4c97-ac0e-b50a112bb905
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: e32fea04-019b-4230-8dd0-c9221dc54cee
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 17829425-abc6-4ad8-8592-4bccefbc1510
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 8b7a3a3f-6206-482d-a35e-c6938f5059c0
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 6dcd85a9-795a-477b-889a-686f60d30a1f
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 817ecbc2-efbb-43cc-86f6-0da82019d594
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: e373b760-70a2-4ce4-b918-879abe04c81e
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 4394b0d9-071d-44d3-9d9b-651ac8295c2e
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 895ad335-ef89-4e3d-a770-cb53fa883be2
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 1d383fe7-3229-432b-b5e4-67fd3f2f46fd
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: d2af2349-e524-4d45-98d3-720e06128770
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: e99577f9-61fc-4443-90fe-70eb07395526
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: c6c43400-7552-4796-aa40-6c06364ce0ac
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: cda07663-3f77-4fb3-b99a-689d8b221ad8
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: eaa8dcb4-bcd9-4c71-a24d-50caff1baaba
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: b2af5ecf-b199-4166-bbcd-9194443b135f
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: db7be3a5-9fdf-4518-93dc-3200f48bd09a
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 78e42b57-061a-45f1-be7a-83d0bc75b826
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 96ba0389-cc51-48dd-b410-b8a208966164
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 730750f7-8f00-4e91-b7af-420e95f1d96d
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 3210e5e8-db05-4ee5-92a0-415e8d7f17fd
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 6d6a9401-9583-4118-9a85-0c73d3a327b5
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 10f508d6-dddf-43f0-969d-500be46b521a
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 9c5f9183-597e-44da-af46-860cb1cfb269
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 92c791fa-f97a-4338-8167-ba659cdab3e0
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 480dcb2d-c429-4657-90dd-5069af5ecb4f
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 891d5a01-c27e-4363-89a9-977ae57c7cec
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: db781714-0a74-4712-a471-b63779983d6e
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: a599db65-fb22-48c4-8258-63bf5ac6b10a
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: eed4e229-2ce3-414a-996a-36834f1c7115
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: 21714272-5792-4984-9aa9-bd43fcab2a0a
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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: d5f02037-e9d0-4219-a865-6bb66ad073ac
    creation_time: 2023-02-02T14:22:57Z
    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''
        ''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
