- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf426efb-c157-4162-8021-c3abee5b3759
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 313ae4d8-9f8b-4951-8548-a2c0517a8abf
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 764e6060-32cf-44cc-96fd-18757e90434a
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 891c7065-24b9-4470-ba5a-8145d0ef1fb5
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 184db790-7d17-4bd2-844b-b2590ef3024e
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 23d54281-3521-4a0c-a43d-982ffadff713
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: eea7524b-27f0-41a1-979a-841c95ca71a5
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 67a61eb2-c101-4a13-8c96-cf8cba25b7a6
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 68ddc835-6d0d-47d2-90dc-bef3e7ad1cd6
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 7b0156ab-7e97-4f86-b50a-bb0981072a22
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 4eb151c5-2006-4046-885c-46b227674937
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: ae90a406-979a-44e3-aa56-e4ba2bf46d53
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 2f4ec5ba-47de-499e-a76f-926aecfeaf54
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: d2f36ad1-d8ed-4d79-b0bf-1a771460db04
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 4cc31fcf-0182-4da2-b1c7-8e13adaef59c
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 2d232f08-7f6d-4a7b-b4ca-49d918ae1dcf
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 54f72ee2-e672-4ae3-845d-9e7a5626953b
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 47dfa709-b894-45b0-9c31-1fe5ebae35d1
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: e8f99aee-0fc7-46cf-96dd-ad372ab81293
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 1b322000-6178-49ab-9eb5-ac74a7c889ea
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 3f06e108-42b7-476b-830c-3da548964bcf
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 3b4e3502-4435-404a-82db-b326f2b01e50
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c45fe258-8ec9-4dd8-a53d-57908992e2a9
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c6890d05-2786-4296-9d27-272f1e1e9c40
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 08c569bf-d288-414f-86cf-e12ff20d112f
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6256cee4-33a2-47ba-ab28-07c9625b6744
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: be0d0754-854e-4d69-9c0c-014725ebc217
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 93c6c93a-35a8-47e3-94a1-d3af31dac12d
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 792fabd7-1777-4a16-99c0-e8c92906c45a
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: cba33dab-99d4-4fc9-9904-34d551df35b1
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: a2722624-26e2-4e63-b088-35c376aabedc
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 4f35247d-9885-494e-8a40-df60719d1432
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 9c92e1c8-513c-4d9f-8060-029efeb15375
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 9077b6d9-5493-4704-bc73-ff6c2b6695db
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 8bb7067d-5631-4f6f-a73f-9e42de065a6a
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: ce1ffb82-76c6-4ef7-b668-b6f5f641f080
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: a7079b89-a6c8-4bd3-a94e-e938eb9023bb
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 5eeaec99-ba72-45e4-a5a4-868e65ca2189
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: a3f8bfcd-c789-43b1-a2f3-0f4e92dc5e2c
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: caa49962-8f2d-47f3-9114-7cd29c054b86
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 627fba47-51db-4c42-b85b-6531917d6f8f
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 02dd3209-46dd-4afd-8efe-fbbedf60acd3
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 33b64620-a020-4cd4-a6e6-a74bc086401d
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: ac4d382c-3c29-4d38-951b-7583a338d8da
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: bf002865-4d53-4be7-803a-89191f76de6d
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: e3e3b13c-fbca-4ede-8ece-cb45f3822007
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 1ea6f2ef-f580-4733-83ba-913c52a72312
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 1d976e86-83fb-47d0-a494-c629ea8ce69a
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 05be14c6-70b9-4116-8145-a7564c728849
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: fa154778-15c2-46cc-bf2f-3986ad51e0cf
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: a57f5230-9055-4d60-bc62-cfbed78e6da5
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 4ced1324-358d-419a-a756-30186049ac82
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 3ce44432-eccf-45e9-86f4-7cd499f2f125
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 60c8e64b-378f-404d-be6a-a316554d7a07
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 93e8ef27-fa3d-4ff8-878b-2eade8df3427
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 3c4a206a-639a-425f-8750-4bd84eaf5e1b
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: d1b395d0-7a1d-4b09-8c5f-21bc5552f7de
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 704b6040-e394-4d56-b5ef-1ed1a8d74672
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: bb19c5c9-6740-47f4-9a80-961edf09c134
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: f5e3e33e-39a0-4861-827c-36a3b615989e
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6b1d5b0e-feb1-40fa-9e29-77853980a5b8
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: dfa67d6a-da75-48e8-bfc5-691a28da51f4
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: bd08bf0d-e922-4759-b2d1-4d13bf6a6ad8
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 22c3e598-3730-4a2a-a4d8-112b8911c6ce
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c13ad006-5154-491b-85d2-e30ad6e392e6
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 601d9a1d-de21-4b39-afc5-ce196516d5dd
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c1e865d6-80f5-456a-a74e-fdc67826d154
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 806c59b4-219b-4479-b439-97931bbc0207
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: b33f7d0b-ec53-4859-bcd8-41277a256c31
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 19f26dec-2a26-4591-b4b8-c62bb71bf8bd
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: b6b28aeb-7370-4f66-abcd-8ad788f99c74
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 0404797e-1b4c-4412-8908-99c3fe4ec11d
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: a084be3f-c3db-48cd-b546-5f7d76d71e6d
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 895dea8e-557c-48f4-a6f2-e884f80106f4
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 36ca6048-77ad-4143-8cc4-65906153e948
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 466c242b-43c2-4505-bbfd-09988eaaca9d
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 71db55be-90ac-4f19-8f39-3f7532a1aa66
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 5d5d8fd0-846e-44f7-bc69-49d480bf9353
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 598a334e-a659-4aa2-9dfc-7251621b877d
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c6acc0a8-493e-46d5-b42d-be336d0ef829
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 1de6d22c-f586-44d3-862f-747d7b81801f
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: a5fb562a-e094-479e-b110-4dda85031c03
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: cda1b2e5-f6a1-49d4-8998-45dd378e3a50
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 64ebf888-206b-49a7-b9cb-cd57e020e7ed
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 22b164eb-dfaf-4235-9199-4239f5746856
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: b047b306-246e-44ed-820d-a45f8f1128b6
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 4a967a46-2995-4444-aff2-9072be1e5219
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: f3fa6446-8c03-4e48-9619-d41743ee7cec
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6160639f-2621-41ce-9560-ebb01905788b
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 7edaaebf-9152-4134-b61d-deea2de9d85d
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: b69ac3d5-faa2-45ba-a70d-6e7406512c1f
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6a3c53e6-3c3a-40d6-aa53-e2578925e2ae
    creation_time: 2023-02-02T14:22:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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
