- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 69a39cb3-87e9-4b07-bfc8-0f71cadff276
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1023
    column: 9
    function: process_client
  loop_invariant:
    string: 0 <= client
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: add773df-ba2f-4063-b679-a57c11df3ec4
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1023
    column: 9
    function: process_client
  loop_invariant:
    string: 0 <= request.closed
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4916577d-d711-4781-b001-569bddaf3c13
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1023
    column: 9
    function: process_client
  loop_invariant:
    string: 0 <= request.socket
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a4b7b529-7537-434b-8de6-ca171871a2bb
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1023
    column: 9
    function: process_client
  loop_invariant:
    string: 0 <= done
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f244c1a1-c382-4891-bbaa-ce9de6e1e26e
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1023
    column: 9
    function: process_client
  loop_invariant:
    string: 0 <= numrequests
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a0d22999-b64b-44e9-92d0-3340d802674b
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1023
    column: 9
    function: process_client
  loop_invariant:
    string: request.closed <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: eacdb819-8087-4f12-b49e-7be9d9f588d2
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1023
    column: 9
    function: process_client
  loop_invariant:
    string: done <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b84888d1-ae5b-4ff9-9a50-b7753749d392
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1023
    column: 9
    function: process_client
  loop_invariant:
    string: (unsigned int )request.version <= 1U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b72a14e6-cd36-4c86-a4b6-06d18a320ed5
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1088
    column: 9
    function: accept_loop
  loop_invariant:
    string: -1 <= id
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5720ffe0-da12-4adb-af3c-4b294f8be55b
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1088
    column: 9
    function: accept_loop
  loop_invariant:
    string: 0 <= s
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 457a347e-fa1f-44d6-82d9-c2aeabbf9b5c
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1249
    column: 11
    function: main
  loop_invariant:
    string: 0 <= argc
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b121656-5a13-43b1-937e-5b4e9b133a4f
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1249
    column: 11
    function: main
  loop_invariant:
    string: 0 <= s
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d231fb1-88e8-4c91-86f9-2c7caf5a149e
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1249
    column: 11
    function: main
  loop_invariant:
    string: 0 <= nthreads
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dae85726-209a-4a6a-bfb0-b1942e67b04a
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1249
    column: 11
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c4a30ef-9f4b-4833-9ab4-019bce778c46
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1249
    column: 11
    function: main
  loop_invariant:
    string: 3 <= argc
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 081aaafc-e381-406c-9585-e164232d1ebe
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1249
    column: 11
    function: main
  loop_invariant:
    string: argc <= 4
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a02edad8-3080-4f5e-a6cb-5319b2c52cf7
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1249
    column: 11
    function: main
  loop_invariant:
    string: argc <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 872a5f69-929d-4e5e-b7f8-8e985851ce6d
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1249
    column: 11
    function: main
  loop_invariant:
    string: argc != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e397b8f3-d17a-48a5-97d9-9f0f31765042
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 586
    column: 9
    function: http_parse
  loop_invariant:
    string: 0 <= result
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b9c8d7ba-b68e-44ba-aed6-a02c3be4a903
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 586
    column: 9
    function: http_parse
  loop_invariant:
    string: 0 <= done
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f46aeb69-2543-43bb-b7dc-965c038d8c2a
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 586
    column: 9
    function: http_parse
  loop_invariant:
    string: 0 <= state.socket
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d4c0dd7c-14ca-4cd3-b3bd-440d31a1e57f
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 586
    column: 9
    function: http_parse
  loop_invariant:
    string: done <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ad01af7-88ed-4390-82af-dbb166674a01
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1271
    column: 11
    function: main
  loop_invariant:
    string: 0 <= argc
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 351a8a36-b347-4ffb-848b-cacaa7e9a8f6
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1271
    column: 11
    function: main
  loop_invariant:
    string: 0 <= s
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ac566c06-b852-4468-b882-2c3f0807b17b
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1271
    column: 11
    function: main
  loop_invariant:
    string: 0 <= nthreads
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b88c05a4-6823-47f8-ae6a-9049a518ad81
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1271
    column: 11
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b51dfad8-4e6d-4ecf-99aa-242300c465c1
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1271
    column: 11
    function: main
  loop_invariant:
    string: 3 <= argc
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c5902a3-f15d-45c9-83df-1df06f0a3228
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1271
    column: 11
    function: main
  loop_invariant:
    string: argc <= 4
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6baa32f0-62b8-4c3c-9b81-7c10082d79d4
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1271
    column: 11
    function: main
  loop_invariant:
    string: argc <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4999ae24-ec04-44e4-968c-e7fcbc4011ea
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1271
    column: 11
    function: main
  loop_invariant:
    string: argc != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 56bfec5c-0dfb-48b3-b28e-f3a7bd10e20b
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 685
    column: 9
    function: input_get_line
  loop_invariant:
    string: 0 <= done
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a3e64d20-b248-4c44-ae45-ba496e1dcecf
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 685
    column: 9
    function: input_get_line
  loop_invariant:
    string: done <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b426b27-32c4-49a2-b10c-b2e6dbc50580
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_no_debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: da91ac22-e2ef-4634-a8a1-396a46853571
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_no_init_messages
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a429694-5d7a-40e9-a1ee-82022966c5fe
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_dump_blocking_graph
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f2be84d-5101-4d98-ac6e-310995eeac38
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_dump_timing_info
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c576c415-2810-414b-9778-8bf5330c543f
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_show_thread_stacks
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d29516a-35bb-4fe3-b55c-6d6f457eaa2f
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_show_thread_details
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f328432c-34c9-4cef-bc11-e2907cbc1c04
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_no_stacktrace
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 682acad8-f464-4453-b263-6c3ea966d91a
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_no_statcollect
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a0aaf98-2e9b-4783-a7ea-61d6abc31713
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_new_stack_kb_log2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 07be2e67-38e3-4af7-8fdf-f4402c42efa0
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: conf_no_debug <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 571ff1f3-280d-4e68-8f6d-ca98e6a8cf03
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: conf_no_init_messages <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b48109d8-5b15-4f24-8142-6dc4383379c5
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: conf_dump_blocking_graph <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 73c15b1c-0b33-434c-85d5-02675867c8ed
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: conf_dump_timing_info <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 77466804-8844-41d1-a5e3-e76b8cd210a8
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: conf_show_thread_stacks <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f845e9bd-5bb0-4026-a39d-cc8f7f5094e4
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: conf_show_thread_details <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ec89e90c-e63e-4aa7-82b0-6ee71301846b
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: conf_no_stacktrace <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7eca96c4-54ac-46ec-b385-7ad8b2483b16
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1483
    column: 9
    function: timing_loop
  loop_invariant:
    string: conf_no_statcollect <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cc2c90d6-b5d2-44c9-9b6d-f7aabe29db3c
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_no_debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e9efdf4d-b6c0-4e66-a56e-9f7c7e693773
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_no_init_messages
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2bf86bfa-7403-4294-a872-a6a88fab749f
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_dump_blocking_graph
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b66d76a-7ecc-4ead-a03b-a56bc90e7520
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_dump_timing_info
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e00358d8-b2f6-4c7b-8a53-092f9717bd17
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_show_thread_stacks
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3cede955-26ac-47e8-8896-19b2bead4e78
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_show_thread_details
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a9d7b3d1-37c3-4224-b98b-d540c65e76ac
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_no_stacktrace
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 55836ded-7724-4110-a49a-a8defa719126
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_no_statcollect
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 28b951e0-531c-4d31-b512-d02af2f62874
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_new_stack_kb_log2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5729e12c-4c16-4f10-812f-3b974fa6fc34
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_no_debug <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d7ea2ca7-5804-47cd-9038-715a065251ad
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_no_init_messages <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8844de08-a3bc-4819-b394-a3a5554388fb
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_dump_blocking_graph <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c683efb-8d74-4c45-a8a6-6290093f6e39
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_dump_timing_info <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: aba45248-f870-476d-b9ea-cacc2954439a
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_show_thread_stacks <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a8ce99d-371e-469d-ad8f-c1addbdea112
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_show_thread_details <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 18786a2d-dcd7-4faa-a99f-1f4ec6525267
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_no_stacktrace <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3922d935-11d9-4593-afef-1d76f71eb37e
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1486
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_no_statcollect <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 10852358-7ca1-4f40-b22e-92775a021202
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 793
    column: 9
    function: allow_file
  loop_invariant:
    string: 0 <= allow
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d77e2021-e062-4ffd-9127-1d1da1d41730
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 793
    column: 9
    function: allow_file
  loop_invariant:
    string: allow <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 99f21891-f86e-4173-bd0a-4194dcc1ed9d
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_no_debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 99c34abd-d8ff-40ad-8766-5927df679e10
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_no_init_messages
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 69fdb9cc-d06e-4af2-b014-4900a671a873
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_dump_blocking_graph
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d8abd24d-c595-4735-89a5-7c514561f7f2
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_dump_timing_info
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d6e6eefd-1298-40a9-8822-04dd37d1ed93
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_show_thread_stacks
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c3a67c22-7791-4f92-89ca-2dc85171783b
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_show_thread_details
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a9bc3a37-2a37-4e1c-af88-3032e61f45ef
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_no_stacktrace
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ee15d1bb-9f22-437b-9a78-1f092dac7846
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_no_statcollect
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d432a7a8-0e93-4450-89c0-8c640c68b024
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: 0 <= conf_new_stack_kb_log2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: baf8e52f-2874-44a6-8af3-27a4ff7e5647
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_no_debug <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ca71f2fc-c651-45f2-813a-b5b0c3d8f067
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_no_init_messages <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7286e254-9feb-448f-8c81-d230a7efc5ef
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_dump_blocking_graph <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f8fe884e-953a-4be5-8590-904f6798b3f6
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_dump_timing_info <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: abec08af-e63f-4fa5-83b4-6b7c1e91bea0
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_show_thread_stacks <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 42f22e1a-f83c-46d9-beb3-0f9205ee5eff
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_show_thread_details <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 840b119f-0b7e-4fdc-8c4a-78812bf9a193
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_no_stacktrace <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 28ee07ef-e883-4292-9e91-7fb98c261aff
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1493
    column: 11
    function: timing_loop
  loop_invariant:
    string: conf_no_statcollect <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 94245d9a-b019-485f-9427-1cb267f28f96
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: 0 <= conf_no_debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a905a9aa-9eab-4bc4-a50d-5a01be3cafad
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e29955d-fb9b-4803-b8a7-cc1dc1d33143
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: 0 <= conf_no_init_messages
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6399546f-1aa3-49bd-80eb-6492b38eee4c
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: 0 <= conf_dump_blocking_graph
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 39712c7a-d262-4591-b146-338a0e517c93
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: 0 <= conf_dump_timing_info
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f1a2b6e-8df3-4d78-bf6a-56d0386f7e7c
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: 0 <= conf_show_thread_stacks
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0efe9fdf-b997-4b81-9d41-aaa38eb4555e
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: 0 <= conf_show_thread_details
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 30834761-ece8-444e-af53-17362cebae5e
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: 0 <= conf_no_stacktrace
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f79f238f-21d2-4623-86af-ab88acba74c0
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: 0 <= conf_no_statcollect
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bd4ec4eb-a4d2-4449-a665-1b47175e4147
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: 0 <= conf_new_stack_kb_log2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 223b812f-5ab0-4817-8364-e23ad359950d
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: conf_no_debug <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 08b878b5-ca44-4ec3-b2b4-0f1dd24856cf
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: i <= 10
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2182a7cd-9c4b-46b5-a0c7-f19affe64f3c
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: conf_no_init_messages <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e3877589-7ee3-4f80-bd93-b54e14eb586f
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: conf_dump_blocking_graph <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ff8ff5a-bac6-464c-b70d-37b1623a74f9
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: conf_dump_timing_info <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 96313a25-2127-4c74-86eb-05d7736cb2aa
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: conf_show_thread_stacks <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 45610282-c874-4c96-a8c4-06e59c51a84f
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: conf_show_thread_details <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a80b08ca-7110-4a44-ab0c-ef7943c47a30
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: conf_no_stacktrace <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7952f584-6e90-4c26-95f0-62ebf3dc3f5e
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 1521
    column: 9
    function: init_cycle_clock
  loop_invariant:
    string: conf_no_statcollect <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 48dccc77-a947-48a9-b62d-8f1c4070c1d4
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_no_debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: febd6200-9dd2-41b4-9c1f-e2972495fca9
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_no_init_messages
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b134b5d1-8bea-4d3b-a085-09a7be5f5781
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_dump_blocking_graph
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b962f2f7-2b47-495c-8e7d-84a0964f366c
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_dump_timing_info
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e2d1ff86-a853-4c6f-bb39-02e10bd6cf7f
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_show_thread_stacks
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 65b89e17-d1d8-4622-ba02-4681044e3763
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_show_thread_details
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 40569289-9693-47ce-bfb6-7e5790c97f39
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_no_stacktrace
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 55063329-df89-4b77-9788-d874934e48cf
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_no_statcollect
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c0b143d-fd29-4953-9550-f120225b590e
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: conf_no_debug <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 128ddc80-d402-4f48-8538-36d3c04805c7
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: conf_no_init_messages <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 98bef47c-4090-48b2-a198-b6692ddf0d6a
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: conf_dump_blocking_graph <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f5c3ad8-61e6-48c9-9dfe-673142b65ed9
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: conf_dump_timing_info <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2821de48-f364-4543-a4b6-755edb134d3a
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: conf_show_thread_stacks <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 266e591c-921d-4d54-9b64-93224738ce14
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: conf_show_thread_details <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f3310137-375b-4898-977a-aefee640518e
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: conf_no_stacktrace <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 50e0b792-3530-4df2-ba0d-0544440c9a40
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2189
    column: 11
    function: read_config
  loop_invariant:
    string: conf_no_statcollect <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 727f179c-8fcd-4dbb-a242-d6339d049b90
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 891
    column: 11
    function: process_client_nocache
  loop_invariant:
    string: -2147483646 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5ec0fa99-f2cd-49a9-9818-65168f31a67b
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 891
    column: 11
    function: process_client_nocache
  loop_invariant:
    string: 0 <= client
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a8df795c-0068-46c4-8d7b-3db549c4a1aa
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 891
    column: 11
    function: process_client_nocache
  loop_invariant:
    string: 0 <= fd
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8045ef5f-6b83-4a75-83e2-0e8486ee8155
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 891
    column: 11
    function: process_client_nocache
  loop_invariant:
    string: 0 <= success
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e0a1ff92-0604-4a81-bd6f-915d3bf70dae
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 891
    column: 11
    function: process_client_nocache
  loop_invariant:
    string: 0 <= written
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ec4c4fb8-2048-4134-aece-e6593be461ae
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 891
    column: 11
    function: process_client_nocache
  loop_invariant:
    string: success <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b89cf046-e1fd-4e63-8b8e-35dc848c7676
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_no_debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d8b138b0-b35f-4aea-8ea8-4302f4785fc9
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_no_init_messages
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cce9b3b2-7197-46b5-8164-fbfec275925e
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_dump_blocking_graph
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8fdc23ab-7c4a-41f2-a2e5-315dc94fcd14
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_dump_timing_info
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cd35a874-d72f-4581-b414-09c5b39de17b
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_show_thread_stacks
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e2dd176-dc1c-4562-8463-1e566bebe8cb
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_show_thread_details
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bd6e6f45-8fbe-49eb-97f9-62821d679800
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_no_stacktrace
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a56c527-b2a0-4a72-872f-9d97f207b59e
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_no_statcollect
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f30efc26-5537-4126-a954-a64eebe99d18
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= conf_new_stack_kb_log2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8500e71e-e327-4a4a-9eec-db4e21296a77
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: 0 <= mult
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c4619875-56f0-4697-a4a5-16d34fed3662
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: 1 <= mult
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 98189ec7-0ecf-46dc-b06a-523fe8aacee1
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: conf_no_debug <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ba7d776a-22cf-4032-9838-02fceddbd3e6
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: conf_no_init_messages <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6fea9acb-c75c-4cdc-bc16-9c52f2123051
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: conf_dump_blocking_graph <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 547bbfae-8b46-4709-a33b-69701df62900
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: conf_dump_timing_info <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 744e0ef3-d716-45b9-8ef7-3025a0792f9d
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: conf_show_thread_stacks <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e7a4da28-3eb5-48d5-9bb9-0ef51002bb1b
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: conf_show_thread_details <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e4d081d9-a75c-4ba7-be08-326988b9c3e8
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: conf_no_stacktrace <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ee37fcf4-2f18-40db-a851-6cba2a0aaf8c
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: conf_no_statcollect <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c4f56f95-3fd2-40fd-a61b-032c0286d20a
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: mult <= 1048576
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ca51d667-5ee7-46f3-8677-22665c92e294
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 2228
    column: 11
    function: read_config
  loop_invariant:
    string: mult != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fe61cbf2-a4fe-4678-997d-2d8f471e5e02
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 899
    column: 13
    function: process_client_nocache
  loop_invariant:
    string: -2147483646 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b7b574bb-b3a9-4fec-b9a8-0711a2b9cdf2
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 899
    column: 13
    function: process_client_nocache
  loop_invariant:
    string: 0 <= client
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b99a35e-f350-4617-83e0-5e8af60d376f
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 899
    column: 13
    function: process_client_nocache
  loop_invariant:
    string: 0 <= fd
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3bd32cc3-ff58-4fb6-8c46-b42b447ff57b
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 899
    column: 13
    function: process_client_nocache
  loop_invariant:
    string: 0 <= success
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f1073781-81b6-48ad-947a-3b7939f96802
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 899
    column: 13
    function: process_client_nocache
  loop_invariant:
    string: 0 <= written
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e5987b3-29ed-4b25-9556-181e189ca2f9
    creation_time: 2023-02-02T15:12:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/knot_comb.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/knot_comb.c
    file_hash: 68e6a0a48049f7f4e4cf547422ad7e0617aaf8c37678f8ad3c5906cc6c9dcf4e
    line: 899
    column: 13
    function: process_client_nocache
  loop_invariant:
    string: success <= 1
    type: assertion
    format: C
