- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43d1dac1-b304-4c8b-a982-1639936ddcef
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 1156
    column: 12
    function: test_bindings_once
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 631d40db-ccfa-4561-b15c-4f2b01b31faf
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 1156
    column: 12
    function: test_bindings_once
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d03163ad-18c5-406b-b7da-33420f920e48
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 1169
    column: 6
    function: test_bindings_once
  location_invariant:
    string: 0 <= lastcheck
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e73fe807-99cb-45ea-b61b-c81dda3bd97b
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 1169
    column: 6
    function: test_bindings_once
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 15175ad3-7b7c-42d7-ba6b-08c7ea43930f
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 1169
    column: 6
    function: test_bindings_once
  location_invariant:
    string: lastcheck <= 899
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 615fabf3-51e5-4a46-8f8f-609ca3421222
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 1169
    column: 6
    function: test_bindings_once
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df38da1c-3093-41c5-bc34-4279f236f3d8
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 257
    column: 2
    function: find_domain
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d836b9eb-4334-4125-b28c-eb6b679825db
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 257
    column: 2
    function: find_domain
  location_invariant:
    string: 0 <= count
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a79cfa8-5deb-4a68-b10d-78bef05ca752
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 257
    column: 2
    function: find_domain
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e7acea3d-756c-4b6b-a628-373e771025dc
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 257
    column: 2
    function: find_domain
  location_invariant:
    string: count <= 2
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8566f230-47c0-4915-8bb2-73e3f6615b43
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 295
    column: 10
    function: find_domain
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3e07828-13b0-4692-83d4-fb7422ce6e93
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 295
    column: 10
    function: find_domain
  location_invariant:
    string: 1 <= count
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 763fcba8-05d5-4c95-828c-e2e735f596a1
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 295
    column: 10
    function: find_domain
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce0aa57d-4f7e-495b-b81e-68799b7d8aaf
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 295
    column: 10
    function: find_domain
  location_invariant:
    string: count <= 2
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 201b309f-129b-4d99-b179-b384e7b37f6c
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 311
    column: 6
    function: find_domain
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c16919c1-2867-4107-a5e1-7440137bd186
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 311
    column: 6
    function: find_domain
  location_invariant:
    string: 1 <= count
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 893b1b83-b8d7-4271-a9d6-209c55b6ea18
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 311
    column: 6
    function: find_domain
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 277c1fe7-100c-4903-9248-f20bc73263fb
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 311
    column: 6
    function: find_domain
  location_invariant:
    string: count <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3aca4261-83ff-4be4-bf91-c00df47a1511
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 425
    column: 11
    function: add_server
  loop_invariant:
    string: 0 <= check_syntax
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 271bd983-6890-49ed-aa5c-f6180fc51cee
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 425
    column: 11
    function: add_server
  loop_invariant:
    string: 0 <= active
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 825c0e48-909c-4b17-833b-d2bff0c3b3c3
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 425
    column: 11
    function: add_server
  loop_invariant:
    string: check_syntax <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1dd366fd-b0d9-42d1-9cda-daf0d7d69556
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 425
    column: 11
    function: add_server
  loop_invariant:
    string: active <= 30
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a16727ac-4ecb-4516-968d-d3dbf8ee03e9
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 447
    column: 11
    function: add_server
  loop_invariant:
    string: 0 <= check_syntax
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5558b8d5-81f4-4f7b-9b9d-eee37de7a068
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 447
    column: 11
    function: add_server
  loop_invariant:
    string: 0 <= active
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c06b59b-19c1-44a8-b4a1-674d2d3e9ca3
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 447
    column: 11
    function: add_server
  loop_invariant:
    string: check_syntax <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d2c6db8-2d74-4b04-bbe2-438b44aa7c7b
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 447
    column: 11
    function: add_server
  loop_invariant:
    string: active <= 30
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f157564b-8575-4a5d-a171-115c4e4d8877
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 120
    column: 9
    function: load_config
  loop_invariant:
    string: 0 <= check_syntax
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 39ff3ea7-8b3e-4162-ab87-fa6d3091daf0
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 120
    column: 9
    function: load_config
  loop_invariant:
    string: 0 <= have_entries
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bbd2df8c-7833-41b6-8896-bd1f540653f4
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 120
    column: 9
    function: load_config
  loop_invariant:
    string: 0 <= bad_entries
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ab382d1-dbb7-47d0-8f13-b5939169e98e
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 120
    column: 9
    function: load_config
  loop_invariant:
    string: check_syntax <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d98315b3-6e45-4e93-9f76-b7afb02c561b
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 152
    column: 11
    function: load_config
  loop_invariant:
    string: 0 <= check_syntax
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2200ad92-bc09-42ce-9f68-46b3d2074208
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 152
    column: 11
    function: load_config
  loop_invariant:
    string: 0 <= have_entries
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 864ea0ed-0830-462a-b760-504a49e8e2a4
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 152
    column: 11
    function: load_config
  loop_invariant:
    string: 0 <= bad_entries
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 45df99ef-4d0a-4ec4-9818-122a80e97619
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 152
    column: 11
    function: load_config
  loop_invariant:
    string: 1 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 22497c8d-54d4-4a02-ad16-22a814a5c4bc
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 152
    column: 11
    function: load_config
  loop_invariant:
    string: check_syntax <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 81fab3ab-cc43-4483-ac7d-1f2d41f31935
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 152
    column: 11
    function: load_config
  loop_invariant:
    string: n != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fbb918e-b189-44cc-8950-8917bb61152c
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 660
    column: 11
    function: main
  loop_invariant:
    string: 0 <= ypset
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e73d168-8522-48df-932d-1b29b793344a
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 660
    column: 11
    function: main
  loop_invariant:
    string: 0 <= broken_server
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f070d2d-dade-4464-8290-2a8c90e1113a
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 660
    column: 11
    function: main
  loop_invariant:
    string: 0 <= use_broadcast
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9077edc9-57cd-4ba1-a6e4-c7d56c188774
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 660
    column: 11
    function: main
  loop_invariant:
    string: 0 <= local_only
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a3cc53ec-2434-4f64-8a68-8992a78b95a3
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 660
    column: 11
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a1405835-69f9-4f47-a343-fb392e4c805c
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 660
    column: 11
    function: main
  loop_invariant:
    string: 1 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5535b59a-779b-414f-831a-d08923916dc3
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 660
    column: 11
    function: main
  loop_invariant:
    string: ypset <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ac7a0634-7c01-4499-8fe5-72267703225c
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 660
    column: 11
    function: main
  loop_invariant:
    string: broken_server <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7429144f-5517-4ff5-bcf2-f0871014fba9
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 660
    column: 11
    function: main
  loop_invariant:
    string: use_broadcast <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a832820-ccc1-4cdd-886d-ef5ef96cac29
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 660
    column: 11
    function: main
  loop_invariant:
    string: local_only <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 186f9c4c-9997-4681-9ba2-539ea97c96dc
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 692
    column: 9
    function: main
  loop_invariant:
    string: 1 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a55e5b3d-f2e1-44fd-b9b9-824ffe5c3a5a
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 772
    column: 9
    function: ping_all
  loop_invariant:
    string: i <= 30UL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c0cf3fb9-bad7-4070-84a5-b68dd163ac6d
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 823
    column: 11
    function: ping_all
  loop_invariant:
    string: 1UL <= pings_count
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d4ca3ceb-54e5-4099-b60c-2c1f765440b1
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 823
    column: 11
    function: ping_all
  loop_invariant:
    string: pings_count != 0UL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a2d38e38-81e1-4501-953a-dfc45f091785
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 834
    column: 9
    function: ping_all
  loop_invariant:
    string: 1UL <= pings_count
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d760645-a85c-4e81-a734-4b68157bed9c
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 834
    column: 9
    function: ping_all
  loop_invariant:
    string: pings_count != 0UL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 656ab33a-d895-41a2-aadc-92b7d09f3b06
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 853
    column: 9
    function: ping_all
  loop_invariant:
    string: -128 <= found
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: df114927-d6f6-458b-980c-b297dd13c8c1
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 853
    column: 9
    function: ping_all
  loop_invariant:
    string: -1 <= found
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e4d4b8ee-4b41-4c57-a0a0-4aa11cbabd2d
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 853
    column: 9
    function: ping_all
  loop_invariant:
    string: 1UL <= pings_count
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 15971f2c-2054-48d6-ad47-d6261d401e20
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 853
    column: 9
    function: ping_all
  loop_invariant:
    string: found <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d34d8d0-9f50-4411-9eef-d058334c6589
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 853
    column: 9
    function: ping_all
  loop_invariant:
    string: found != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 27f498ec-0f9e-41d1-994a-b004dec7e9f1
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 853
    column: 9
    function: ping_all
  loop_invariant:
    string: pings_count != 0UL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: acfb919c-5c95-401b-bb92-1800dbeff02a
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 889
    column: 9
    function: ping_all
  loop_invariant:
    string: -128 <= found
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 07d62a90-cc20-4899-aa7b-ad1fde153e4b
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 889
    column: 9
    function: ping_all
  loop_invariant:
    string: -1 <= found
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 908cc9d7-299e-4470-8258-6d64169fe4cd
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 889
    column: 9
    function: ping_all
  loop_invariant:
    string: 1UL <= pings_count
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e019447-1801-4637-be5a-33b2a7df3ba2
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 889
    column: 9
    function: ping_all
  loop_invariant:
    string: found <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b6960de7-dc34-4462-8bd4-9b87044c46d0
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 889
    column: 9
    function: ping_all
  loop_invariant:
    string: found != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c5f31761-cc2e-48a3-bcec-307b1b5025e4
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 889
    column: 9
    function: ping_all
  loop_invariant:
    string: pings_count != 0UL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b50358e1-d188-4123-b969-47a26f2ccd9c
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 1002
    column: 9
    function: do_binding
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ddff0aef-216c-49d7-986c-6b519867d00b
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 1024
    column: 9
    function: test_bindings
  loop_invariant:
    string: 0 <= lastcheck
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5be23ec8-ac1d-4d97-b271-749375ad6d36
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 1024
    column: 9
    function: test_bindings
  loop_invariant:
    string: lastcheck <= 899
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b024220-a1e4-4365-8407-d2838d7f1531
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 1060
    column: 9
    function: test_bindings_once
  loop_invariant:
    string: 0 <= lastcheck
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6796d59a-a6ab-4ac4-ad27-e576b26383f6
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 1060
    column: 9
    function: test_bindings_once
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f7cb1451-50ad-4867-935e-47a9c7206c46
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 1060
    column: 9
    function: test_bindings_once
  loop_invariant:
    string: lastcheck <= 899
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 26badd41-d078-4a6d-8c4d-363d475dc7ba
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 494
    column: 9
    function: main
  loop_invariant:
    string: 0 <= ypset
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f2946b2-29a9-4a60-9b7a-d93d830a4a66
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 494
    column: 9
    function: main
  loop_invariant:
    string: 0 <= debug_flag
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 210dafaf-fa3f-4cf0-ab06-51541954c617
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 494
    column: 9
    function: main
  loop_invariant:
    string: 0 <= broken_server
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 17cdb358-df76-4487-8f75-80ef0b1ed45d
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 494
    column: 9
    function: main
  loop_invariant:
    string: 0 <= use_broadcast
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: de245cd4-6204-4f57-8693-dc354335a496
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 494
    column: 9
    function: main
  loop_invariant:
    string: 0 <= local_only
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ffab2e8-9d9d-4c90-b1b9-f416ce736a64
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 494
    column: 9
    function: main
  loop_invariant:
    string: 0 <= configcheck_only
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4246ad09-dc49-4d1c-a23d-e4cbe59dfe52
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 494
    column: 9
    function: main
  loop_invariant:
    string: 1 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f9d8a3d-d663-4b40-8d9b-1df5ef86b1b9
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 494
    column: 9
    function: main
  loop_invariant:
    string: ypset <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ad681342-ae93-4616-b102-128094d0544a
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 494
    column: 9
    function: main
  loop_invariant:
    string: debug_flag <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3aaebfb6-735f-472a-9207-5ce727e46f02
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 494
    column: 9
    function: main
  loop_invariant:
    string: broken_server <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b629172b-7509-4c42-92c1-4b035bfd9c89
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 494
    column: 9
    function: main
  loop_invariant:
    string: use_broadcast <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: db50f483-ca2b-4353-98eb-d3cf0052e588
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 494
    column: 9
    function: main
  loop_invariant:
    string: local_only <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ba8de301-7056-4776-9956-234ec0ee114c
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: ypbind-mt.c
    file_hash: ""
    line: 494
    column: 9
    function: main
  loop_invariant:
    string: configcheck_only <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e6027d8-97ca-4322-b6dd-b49cb471bd07
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 184
    column: 9
    function: change_binding
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b28664f7-478a-4dc2-9623-14150e305ff2
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 246
    column: 9
    function: find_domain
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 336ff405-11c4-430a-be07-3c5e4a918dbe
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 257
    column: 2
    function: find_domain
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a2fc2ba4-c7b4-4db3-ad2e-fe438fbf7ebf
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 257
    column: 2
    function: find_domain
  loop_invariant:
    string: 0 <= count
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f0cf84f2-2c3e-4590-8607-1031d171bc53
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 257
    column: 2
    function: find_domain
  loop_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f9254af2-6347-4d47-940b-745746aa077a
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 257
    column: 2
    function: find_domain
  loop_invariant:
    string: count <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cab4825f-0ebb-40e6-b499-dcaa7185e6fe
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 331
    column: 11
    function: clear_server
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f5b5305f-fac3-451a-9f4f-e6bb4bf89110
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 333
    column: 13
    function: clear_server
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 151cea68-e4fd-4b50-96d2-0f156239eed3
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 333
    column: 13
    function: clear_server
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 550fef34-c757-4203-a6b3-88872f503d18
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 333
    column: 13
    function: clear_server
  loop_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 384d7ef2-3fdb-4c6c-be83-61dec7fe411d
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 333
    column: 13
    function: clear_server
  loop_invariant:
    string: j <= 30
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c7b3f1d2-bd14-4b2b-8341-fcdabfe5154e
    creation_time: 2023-02-02T15:13:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/ypbind_comb.c: 84da6840d830d07fe89e6229752c2608b1c9e0d30fa3ecabc9a2b941e1724727
      data_model: LP64
      language: C
  location:
    file_name: serv_list.c
    file_hash: ""
    line: 358
    column: 9
    function: get_entry
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
