- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 19972d26-cfe4-4d80-84c0-7c2555e57b53
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 30f3efe0-1262-45a0-959e-696b42ea89fe
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 46c5e9f1-2528-4dab-b53f-77785ffda155
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 4891fa4c-38ad-4e0e-804b-bfde0ff0cd4e
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: fa124baa-437b-4733-b544-19fbe57913ec
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c199209e-1aa5-4257-9eea-3af805bf13e7
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: f4bc4df3-8c3b-427e-bdb0-bf356f72704c
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: dbcd9441-13e6-45a4-a527-f718f6936012
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: b3e6dd85-c353-46ee-9acc-6c2e2a1ba2e6
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 48313d2d-a3dd-4fb1-8c6d-d4306e8b4001
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 19f6c24f-e05a-418b-b255-d87e7d0d0af5
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: id <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b83f2f9-6805-4220-b7db-217b3f207059
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 4dda28de-cfaf-429d-a72b-a5e1f2a9bf6d
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c71185c2-f3bc-44f2-9b52-5d1e87f4c14b
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: b6a3ecfe-1e8b-4193-870e-13cadc5c0979
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 9cf9bcf9-74b8-4d56-a4e7-f6a1534e395a
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 139b55a0-1068-4fa7-9fca-957d5b979664
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: fcb18415-102e-4a59-9f19-c5494a94e48b
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 4827a6a0-ed0e-4294-88f7-a6a721395a05
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6154a74d-d5d8-4ca5-8fc0-29287d78c56d
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 147deaf0-46ca-4fb5-be8c-5fcd7c9e0cde
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 186f4beb-d917-4d8b-a0ca-90d46404ab48
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 49dd42fb-035b-4adb-96eb-89110ab6fbb4
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: f13e6fcb-8134-41a3-913b-d33f0c6fe9b7
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: b09d4020-1b63-499f-ad40-6c9f7e9b826d
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: fba88847-7332-44dd-a3e3-eb7f9d862ff6
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 5e672303-f2a2-4834-842e-c168e0ad0ad7
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 1379e7c7-7fb3-4893-aca4-ad0426286ec9
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: a6fa0949-ed70-4b51-aa1d-202c361eff95
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 55dc4e9a-2c7e-465b-b979-db445d0c9a11
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 590c05f3-7219-49c2-a8db-8cccbde47dec
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 83ead0fa-ef52-42f1-92ff-919d608a9d7b
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 4b654c4b-413b-4f9e-b9bc-33fb92c52129
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 63b43111-7d42-4797-bf6b-3da4ae63edda
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6108ba79-7c3e-45f4-9d28-4479298f1dee
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: a533b281-f7b1-4323-836d-eae0f776c6ca
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 7cba93a6-7f37-47bf-ad56-052a791307b4
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: dc532592-dc73-4430-971e-146ae03fb537
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: b2f4ff1e-e5ff-49d0-bbe5-e8aee25b6c5c
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: dd233daf-a1a2-4155-819a-62c6a15b9844
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 3db71ff2-3438-49c0-9ff5-193f8650fc3a
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6dfa809c-a6cb-4c57-8cd3-3ef32acf48e4
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 5cb5c36f-aae6-469e-b97f-c941b78fc1f4
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 5a193228-9560-4c14-bd99-a71eb1d98f09
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 15ecaacc-7142-48a6-9950-3d83944c98bd
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: cc64ca48-a07b-41a9-aeca-e6cac3f1cc8f
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 3c7887cd-aed1-4c14-9da2-22b7ed900851
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6af52d22-7ab8-4145-b9fd-d07d4c520adf
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 12389eec-9137-4faa-8dc8-fa0e6009e8ee
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 63e92b6c-fe31-4cf5-b87a-49d37b03960d
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 522db0bc-8d4d-4c21-b90c-a56bf2981dd9
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c9744cca-9902-4517-8096-95cb5037c3fe
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 348a58d6-1e53-461e-8982-1001cdf1fbd1
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 610607de-9f14-47a4-abf9-819cb4605441
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 5df8e648-cdfe-42f6-8c2a-dfc879d49f69
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: e8dab333-5b6e-4516-854f-6f8b0f965339
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6f72b4aa-cd2b-4b7a-ab58-34e8cf963d82
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 5551a99c-231e-47e4-a23b-25c88326d0a1
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 35f4b96e-0411-4a2f-901c-248dce6205ac
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 0c0aa84c-983e-448a-b568-0fbd598b7ca3
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: b92aaad7-f618-4c31-bb48-48b9a6e24b87
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: ed962c8a-6801-4870-bf67-137a410890e8
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 1fae7c37-0cb7-4bc1-9b63-c158a96bb8ce
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6d0cc932-70fc-4fb6-90a5-2ef10817b055
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 43a88102-94ce-4d1f-a5fe-92bed084e90f
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 4fa48d55-d7a6-403c-81c3-1d59e2e346c3
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 717e1dea-8518-43eb-a145-88cb57de14e0
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: aff97294-6458-41f9-a3c0-355237aaadc3
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: d93961be-d19a-422c-bd48-dc90e7e72a4b
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: f6c2dce0-10da-4f59-a08c-205174910fb5
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: ca5fd899-40c0-4d92-b2fc-ddcf571e2574
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: a03a8b28-9ba6-4381-ab1f-efeb6900af69
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 445a3407-e71e-4b59-a2ed-2b5387906440
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 268e8fe9-052a-4d60-9dc8-194b6aa1f705
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 2cd0410e-aa5d-4c7c-b277-c91b51f33a3d
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 81f36712-57ab-4fed-850e-6dfe5ca54884
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6b594b17-377f-43d5-9e03-deeddec1141b
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 8df20b9b-c0a3-4e23-a5e1-2e4677cdf649
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 566315d8-be8c-4eef-8ea7-54b424d6ff4a
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 437af7d5-5f2a-4c1b-ab4e-06e4af0171b5
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: f5c8a91b-e11b-4857-bc36-7ecbeb5a3106
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 159df018-3428-419d-8253-89bc668b31d1
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: f5befd94-f4f1-4eab-bf56-6ed16dde9d48
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 66755a9f-d92a-4ce3-a0ad-cf7368bfc2b7
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 20d8a255-693f-4e46-8b87-a64612f6a42a
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 371b4b43-2455-493a-aed7-f3229ff919ed
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: f1a8ef0a-2055-400a-8df0-884c93232070
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 975ffc33-d46f-45f2-8037-0693324bd381
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: cec39f79-7fa1-45c5-84d5-20edcd3bb1b7
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: fbab7935-34e7-4287-9a81-7f91d2a56eb3
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 1f325beb-37cd-4163-a9b7-452d37a8bec7
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 89f34c56-fc66-498c-955a-d30dc34e49a5
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 2e8a0af9-dc17-47a6-b273-dec856147f64
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 1e2fcb32-54ee-47e7-942a-dec9a5e4197b
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 4ff70b67-9dca-416c-b62d-712b3ee0cc85
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: d38f9445-15b9-4678-aebb-8dcc937537fd
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 9dce136e-56b0-4018-b00f-c193563f3724
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: b9706d9b-13a2-4562-86ec-efd1edf64233
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: dc04a767-5e7a-4deb-b714-1e34a6299dd8
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 5b285791-ae6c-48f9-ac29-0fd0f819765d
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 18272973-2bf3-43f1-8c1e-4a0600179ff1
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: d0b7fabe-c761-40bc-afcc-fe9cf2357e5b
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: d2f095e7-ca7a-4ff4-a6b0-831ad20fd3fb
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 71aecc9b-4d85-465a-8887-802343044552
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6162e7fd-5895-4354-9289-58baba023521
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: eccfd1da-c521-4f08-8edc-dd3568ef9d7e
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 42ed6a5e-3ce2-40e2-92e6-80cdb2bf40fd
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 2dc0bc36-0eab-4bbe-b1d6-2250233ec716
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 2ccc6063-0438-4648-a6b7-6ab99e7a6105
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: a40091ea-0c47-4e8b-9d62-a37c2daab51b
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 8a7a05fe-1054-46ec-af82-a43382722e18
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 3a48024e-fbc4-44d1-bbe4-6b08dcf4c259
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6a36b400-b5cc-4409-b009-e17ed9b6300e
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 12eef515-8b37-4a1d-b2bf-2ed0a832131f
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 28c5c4b4-19e6-40c1-9e8b-b876fa6efef0
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c86713a0-5926-4047-b096-9f431da6b64e
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: b1eb9b57-4027-4d0d-b5ed-3124eb93c000
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6e054498-84e4-4939-97e2-45ac972b5cd9
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: ea19559d-445f-48a6-b58b-ef582c1f59f0
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 69da137a-f22d-4f70-9042-a2db5da93cae
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: cd1fb90d-d20b-4939-ae7c-8927b9621f16
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 936b2eb5-7867-4f9b-afdc-ca7218126d35
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: ec9685fd-e660-4f23-a825-9312c926e644
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 2437e070-ba10-43a9-8a8d-c5b0bbfcd0a5
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 62c74aea-a48c-45a1-9a03-8e763422744b
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 7eb57325-f4f9-4348-9d7e-e6e63c11d14e
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 1816726d-79df-4b6c-a968-ab8c992fe307
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: db01d5d4-ab55-4bcc-8465-99bcc75e3b19
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: d63ac380-1b6a-472f-b6c9-a6dbbcbe70a2
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: d55e81ad-7b3f-472c-8946-00f8b9e40fac
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 3080f2c7-b978-4c62-86e7-2e7c6137a8e2
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 346b008f-877f-4153-9270-83753749e852
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 65ba00ca-8ed9-44f9-8b55-aace80bd04cf
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: dd9e6bcd-e835-440b-a3d1-e8e62ec09c0c
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6e501e4f-f5d3-4c2c-92a9-2fd484a3b362
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: e469c6c5-030e-4d59-b17f-cd997a226b05
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 79611f64-74ec-480d-8a38-5f50244055b0
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c2f8f294-e4df-4507-8bf0-2ad709b36c3f
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: b9541f2e-6656-4b98-99f4-729a1d09f099
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: ce097260-bad5-4d01-aab2-dcde8da760d1
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 7a6b0c14-cc5d-4977-953b-d4106314e730
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: d5e28fb5-233f-4f26-93eb-3ccbe0043a5d
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 8c702c18-e99e-42be-9be4-6f796fa83d77
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: ca6a0a82-87cc-4d90-913a-8ad270e8f0d8
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 42de9a90-3d55-4448-bf37-3f842333392a
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 6fea1917-ff45-4285-b063-05c5368080f0
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 453b023d-6f1a-4c55-ab4b-2b10b6f67f68
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 50926e35-577c-41bd-b95b-9e810f7d0d91
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 08569622-550c-481a-8dd9-c984ee22daae
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: e6cba9ed-d060-4916-877c-3f295893c00a
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: c4e2d3b0-9870-4fa4-bfef-310cc5e6f9f4
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: ae95a077-b677-4994-983a-1a9bc619af67
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 51d3d4e7-5e41-4d6c-bf5a-57212c304313
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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: 14d96c69-7b0d-4ee8-ac3b-ec24cb46ad86
    creation_time: 2023-02-02T14:22:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''/mnt/thread-witnesses/replication/bench/pthread/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
