- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f392d44-4e6b-47f4-8560-3d1a64bae07f
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 861
    column: 6
    function: scan_file
  location_invariant:
    string: fd <= -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8581704d-0014-47d0-ba8d-e9cbacfdf782
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 861
    column: 6
    function: scan_file
  location_invariant:
    string: fd != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0d3717e-b165-40c6-aa56-2ea8623ab2d4
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 873
    column: 6
    function: scan_file
  location_invariant:
    string: 0 <= fd
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82b87b63-6052-4963-a6e1-4322a1b7328f
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 892
    column: 6
    function: scan_file
  location_invariant:
    string: 0 <= fd
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c551db63-fa7b-4549-90ab-8934f30106cf
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 905
    column: 4
    function: scan_file
  location_invariant:
    string: 0 <= fd
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 77f6d9b2-793c-47b2-81ad-a85ff53dc451
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 181
    column: 9
    function: preBmBc
  loop_invariant:
    string: 0 <= debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3bc311c2-67f6-4f1d-98ea-03e32984a00f
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 181
    column: 9
    function: preBmBc
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bd5f1d4d-bd86-49ba-ad3c-72d3ac64c82b
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 181
    column: 9
    function: preBmBc
  loop_invariant:
    string: 0 <= verbose
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2bcf8377-8a84-4edf-aad1-e9d7d2671d8c
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 181
    column: 9
    function: preBmBc
  loop_invariant:
    string: 0 <= line_f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a6d3ee5b-b215-4047-9ee9-2871560e5b74
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 181
    column: 9
    function: preBmBc
  loop_invariant:
    string: 0 <= ignore_case
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 69a844f2-4955-464e-87a3-7e3caa4474e9
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 181
    column: 9
    function: preBmBc
  loop_invariant:
    string: 0 <= bmb.icase
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6908bace-4445-4da8-9cda-79bd11634a75
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 181
    column: 9
    function: preBmBc
  loop_invariant:
    string: i <= 256
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 46d32d89-c325-468f-8af5-dfec9601d5ac
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 181
    column: 9
    function: preBmBc
  loop_invariant:
    string: ignore_case <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ee3e13b-1183-4c20-8314-b5779fac8181
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 181
    column: 9
    function: preBmBc
  loop_invariant:
    string: bmb.icase <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 67e43592-2fd6-4de7-846b-c80a73a10662
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 186
    column: 9
    function: preBmBc
  loop_invariant:
    string: 0 <= debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f5ddc11f-ce6a-489c-805d-9f7cdc2a8b25
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 186
    column: 9
    function: preBmBc
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d06a5022-2281-46a4-b7f7-fdab98bc15fc
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 186
    column: 9
    function: preBmBc
  loop_invariant:
    string: 0 <= verbose
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a8ac832e-70b0-41df-852e-49a304fe6a21
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 186
    column: 9
    function: preBmBc
  loop_invariant:
    string: 0 <= line_f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 05d52087-90b4-4235-9300-986ba244b7c2
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 186
    column: 9
    function: preBmBc
  loop_invariant:
    string: 0 <= ignore_case
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e7cb3e6-6d66-4705-b7e3-6cfce61c912b
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 186
    column: 9
    function: preBmBc
  loop_invariant:
    string: 0 <= bmb.icase
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2855d3aa-964b-43da-8b18-ff4cc2d658e7
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 186
    column: 9
    function: preBmBc
  loop_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 740a5ade-2717-426c-bf71-e9c307e4ddc5
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 186
    column: 9
    function: preBmBc
  loop_invariant:
    string: ignore_case <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ec2d55a8-af95-4dc8-82fc-fa530961ef0d
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 186
    column: 9
    function: preBmBc
  loop_invariant:
    string: bmb.icase <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 57cf2f42-70a9-4fb8-ac65-90dbc54a6eb1
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 203
    column: 9
    function: suffixes
  loop_invariant:
    string: 0 <= debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cc04b542-e6a3-44a8-a6a4-69b19f44f523
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 203
    column: 9
    function: suffixes
  loop_invariant:
    string: 0 <= f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1da7f192-ab89-4ecb-bcd9-2e1a560e0b49
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 203
    column: 9
    function: suffixes
  loop_invariant:
    string: 0 <= verbose
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8109552b-233e-4246-b3f4-ea46f529e7e7
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 203
    column: 9
    function: suffixes
  loop_invariant:
    string: 0 <= line_f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 205268a5-2cdb-479d-ba1f-15190aa6cf03
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 203
    column: 9
    function: suffixes
  loop_invariant:
    string: 0 <= ignore_case
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8972202a-9e05-4585-a2de-de6d01f9c82a
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 203
    column: 9
    function: suffixes
  loop_invariant:
    string: 0 <= bmb.icase
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 00e3e0ed-5fe4-4d7e-8370-413708d57e88
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 203
    column: 9
    function: suffixes
  loop_invariant:
    string: g <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c2de1c9-721b-4060-acc9-10998b8633cb
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 203
    column: 9
    function: suffixes
  loop_invariant:
    string: i <= 2147483645
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1979fcd0-3d3d-4f71-9ac4-88259c05663d
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 203
    column: 9
    function: suffixes
  loop_invariant:
    string: ignore_case <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f538c60-316c-459e-9294-271efcce1ebb
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 203
    column: 9
    function: suffixes
  loop_invariant:
    string: bmb.icase <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dc15c7c6-01fe-466e-8a29-d6fa28761418
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 216
    column: 13
    function: suffixes
  loop_invariant:
    string: -2147483647 <= g
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 19d315de-e2c9-43d8-8103-964da429d8b2
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 216
    column: 13
    function: suffixes
  loop_invariant:
    string: 0 <= debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 882fe958-c984-45a8-8404-4e2210862c2c
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 216
    column: 13
    function: suffixes
  loop_invariant:
    string: 0 <= f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 862ff821-d96a-499e-8c4c-4a611f1fb6d4
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 216
    column: 13
    function: suffixes
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cbd42c3b-9c3a-4c2f-9332-28c1b9b20584
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 216
    column: 13
    function: suffixes
  loop_invariant:
    string: 0 <= verbose
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 928f8e15-8067-46e0-af50-81bd9ecdf9ff
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 216
    column: 13
    function: suffixes
  loop_invariant:
    string: 0 <= line_f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a12de7fc-b3cc-465a-99e0-dcd32acfc053
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 216
    column: 13
    function: suffixes
  loop_invariant:
    string: 0 <= ignore_case
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1cfb46fc-32fa-425d-8753-0b150c6bc62c
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 216
    column: 13
    function: suffixes
  loop_invariant:
    string: 0 <= bmb.icase
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 71e00749-a204-45ce-b192-954190d45cdb
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 216
    column: 13
    function: suffixes
  loop_invariant:
    string: f <= 2147483645
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 41a5fa65-6d35-4a9d-939d-f3cfe84fca5c
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 216
    column: 13
    function: suffixes
  loop_invariant:
    string: g <= 2147483645
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e284545-0699-4bd2-be30-623a2ef7c674
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 216
    column: 13
    function: suffixes
  loop_invariant:
    string: i <= 2147483645
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e1993e6f-918c-4f80-a1a9-3dd179f7cbb6
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 216
    column: 13
    function: suffixes
  loop_invariant:
    string: ignore_case <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 04d3ca80-10b1-4ed4-98b7-62a38406a8dd
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 216
    column: 13
    function: suffixes
  loop_invariant:
    string: bmb.icase <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 52839376-c4cb-4ba6-8737-489263913b38
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 247
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 615c28ae-b972-4fe1-91ee-4e3eb2b4e264
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 247
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 24b08a6e-4135-4c8b-ad9f-5d5f57a6ed6c
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 247
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= verbose
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 58ecd33c-a8ac-433c-ab57-1a84cf2f2d2e
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 247
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= line_f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6aa260d8-4d0b-40c5-8971-695ed40caacd
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 247
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= ignore_case
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: eab17a01-06c5-4dde-9563-bcf2c3cd6db1
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 247
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= bmb.icase
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1abefd9d-2598-4c4c-bd57-61e9c71cee3e
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 247
    column: 9
    function: preBmGs
  loop_invariant:
    string: ignore_case <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 91dd63c9-c95d-4d42-9357-66b6d79e080f
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 247
    column: 9
    function: preBmGs
  loop_invariant:
    string: bmb.icase <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e28cd27c-b623-433b-9a72-97b0cd5437cc
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 253
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ea0606d0-7d60-49cc-b451-ea0fd1114586
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 253
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 460177f1-b211-47b0-a805-6e77f66f11b2
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 253
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= verbose
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: eb50355d-7646-46a6-853d-0d66c74d1ffc
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 253
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= line_f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d50d5fcb-7770-4c86-bd14-e7830916e12c
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 253
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= ignore_case
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 15ef79f1-1e99-4966-9a69-bb94ae0cb144
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 253
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= bmb.icase
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4cfbcd17-357f-45a5-ae0d-3ec541c7d7fb
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 253
    column: 9
    function: preBmGs
  loop_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a56e80ba-5411-4691-b2ef-c90c26f7c59e
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 253
    column: 9
    function: preBmGs
  loop_invariant:
    string: ignore_case <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c38de65-073c-4dc5-ac16-ce95c93be7a7
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 253
    column: 9
    function: preBmGs
  loop_invariant:
    string: bmb.icase <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 15700076-76cd-4caf-a3cd-a795052a5b06
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 259
    column: 15
    function: preBmGs
  loop_invariant:
    string: -1 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bed99ab4-d7bc-4b16-8fcf-d63bec858518
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 259
    column: 15
    function: preBmGs
  loop_invariant:
    string: 0 <= debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dbb97c92-a59d-4127-9491-300c3710cf7a
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 259
    column: 15
    function: preBmGs
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: aa4b6c10-792e-48ed-ba86-69bcde4f22c8
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 259
    column: 15
    function: preBmGs
  loop_invariant:
    string: 0 <= verbose
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 18fd779f-2192-475e-9e5a-7ff2e53917d8
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 259
    column: 15
    function: preBmGs
  loop_invariant:
    string: 0 <= line_f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c0efe87a-ae24-4209-9245-4928de1ba6c5
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 259
    column: 15
    function: preBmGs
  loop_invariant:
    string: 0 <= ignore_case
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b9b505ea-e770-4d0e-8a8b-b43ad7bd7632
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 259
    column: 15
    function: preBmGs
  loop_invariant:
    string: 0 <= bmb.icase
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 65f5b6ab-f833-441f-9641-78997de3e330
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 259
    column: 15
    function: preBmGs
  loop_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d013def0-eefb-4844-afb3-db05d3f7e332
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 259
    column: 15
    function: preBmGs
  loop_invariant:
    string: ignore_case <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 84e9ac4b-a07d-4f98-aa68-f801ad608d7d
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 259
    column: 15
    function: preBmGs
  loop_invariant:
    string: bmb.icase <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b00097b-04b4-4d72-a438-60f723bbe68d
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 270
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2448fa30-66b6-4638-957c-cca54a7382e4
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 270
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 499f0d62-8dc2-41fb-bdb6-4747773ad0ef
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 270
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 38ec50f7-9a54-42d8-8889-642e788865f8
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 270
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= verbose
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 897c58dc-8c0c-4de0-b375-65f7912b3b9b
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 270
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= line_f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f32f8908-0b3f-4e9c-adfa-fc954e320685
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 270
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= ignore_case
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 516decae-ae2d-477b-af49-fda6167cb3e9
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 270
    column: 9
    function: preBmGs
  loop_invariant:
    string: 0 <= bmb.icase
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8843e620-306b-443b-a1f1-6a58538a247d
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 270
    column: 9
    function: preBmGs
  loop_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e7d90ffa-9741-4476-88ce-3a82342b3fa8
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 270
    column: 9
    function: preBmGs
  loop_invariant:
    string: ignore_case <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a03ac24-db4c-404a-b24e-30d85c5c15ab
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 270
    column: 9
    function: preBmGs
  loop_invariant:
    string: bmb.icase <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fce1bcd5-1cd6-4069-98f5-04f722c6800f
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 300
    column: 9
    function: bm_init
  loop_invariant:
    string: 0 <= debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c9b2b68-343d-4668-8243-9f881eb87adc
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 300
    column: 9
    function: bm_init
  loop_invariant:
    string: 0 <= icase
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 35cd548c-d3a2-49e0-bc2a-fa32947045fb
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 300
    column: 9
    function: bm_init
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 04893b02-d1a8-4e05-81e7-b27b68a53543
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 300
    column: 9
    function: bm_init
  loop_invariant:
    string: 0 <= verbose
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f6998dd-7464-4dd6-ac21-a69646c3e92c
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 300
    column: 9
    function: bm_init
  loop_invariant:
    string: 0 <= line_f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c0247f64-90b8-4c1d-b351-b23ae05bf9f7
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 300
    column: 9
    function: bm_init
  loop_invariant:
    string: 0 <= ignore_case
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 14db2203-edfb-485f-8e17-d3f9433706a8
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 300
    column: 9
    function: bm_init
  loop_invariant:
    string: 0 <= bmb.icase
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d87c1b49-4a59-41d4-a67d-3a105a1b2d08
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 300
    column: 9
    function: bm_init
  loop_invariant:
    string: icase <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1020f957-fdbf-4db7-8bc4-0d3d7e846a11
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 300
    column: 9
    function: bm_init
  loop_invariant:
    string: ignore_case <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3fd5e4ec-207d-4074-b69f-e3a41bdeb710
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 300
    column: 9
    function: bm_init
  loop_invariant:
    string: bmb.icase <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d2460483-44e5-4f30-afc3-94a87e029df1
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 349
    column: 9
    function: bm_search
  loop_invariant:
    string: 0 <= nm
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d20ef885-4155-49c9-9485-bd157478c6ef
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 351
    column: 11
    function: bm_search
  loop_invariant:
    string: 0 <= nm
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9293aa87-0f60-446c-8b30-9bf9358b6b20
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 351
    column: 11
    function: bm_search
  loop_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 27757570-50be-4447-8e75-530c12ab5e55
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1032
    column: 9
    function: main
  loop_invariant:
    string: 0 <= debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 37912125-f1a1-4c5c-afe4-721a2db364c1
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1032
    column: 9
    function: main
  loop_invariant:
    string: 0 <= verbose
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: aa7a5002-4a49-4fac-ad42-23f8e5a69a48
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1032
    column: 9
    function: main
  loop_invariant:
    string: 0 <= line_f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 83354b4c-d7bc-4187-b395-976aa3f0a576
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1032
    column: 9
    function: main
  loop_invariant:
    string: 0 <= ignore_case
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a8cc7fd9-fbf3-42dd-8858-28b1c9f4341c
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1032
    column: 9
    function: main
  loop_invariant:
    string: 1 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 936ca6d3-dd03-454e-9a8d-9a8b8ab61e3e
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1032
    column: 9
    function: main
  loop_invariant:
    string: ignore_case <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 81404368-7235-4922-9f15-cc85f3d77823
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1041
    column: 11
    function: main
  loop_invariant:
    string: -1 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 952ad523-b29e-4d94-b390-85160051c63d
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1041
    column: 11
    function: main
  loop_invariant:
    string: 0 <= debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c08e146-bf35-4c29-be0d-de54c12590d7
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1041
    column: 11
    function: main
  loop_invariant:
    string: 0 <= verbose
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6057111c-77a0-490f-865d-7aa309103493
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1041
    column: 11
    function: main
  loop_invariant:
    string: 0 <= line_f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 300a2c45-dcdf-4d42-be2c-8fbd8eb323ea
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1041
    column: 11
    function: main
  loop_invariant:
    string: 0 <= ignore_case
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e910e0d-bd64-4913-9353-575f9f45cfdf
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1041
    column: 11
    function: main
  loop_invariant:
    string: 1 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3fcf92bc-31e5-4db3-b856-a829427ff7b4
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1041
    column: 11
    function: main
  loop_invariant:
    string: 2 <= argc
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 249eb39a-741e-47dd-9af4-c18a762c9a48
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1041
    column: 11
    function: main
  loop_invariant:
    string: ignore_case <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5173ca80-df9d-43e4-bf54-cd9bb0cef437
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1041
    column: 11
    function: main
  loop_invariant:
    string: argc != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ca48320-5305-49f5-91cf-c8b9266fd925
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 511
    column: 9
    function: get_char_code
  loop_invariant:
    string: 0 <= debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c5ff2101-e82f-4388-9869-7ae0b645d9cc
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 511
    column: 9
    function: get_char_code
  loop_invariant:
    string: 0 <= verbose
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a42a82ca-0344-4a3a-b9d2-30a2462fdac2
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 511
    column: 9
    function: get_char_code
  loop_invariant:
    string: 0 <= line_f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 650a7c74-8131-4f49-b1c2-6ab356f90880
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 511
    column: 9
    function: get_char_code
  loop_invariant:
    string: 0 <= ignore_case
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 33bd9564-5de9-4fd0-9581-fc20b6e70e4e
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 511
    column: 9
    function: get_char_code
  loop_invariant:
    string: 0 <= base
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0da07b69-ea6a-4d8c-9a3c-18845eddcc43
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 511
    column: 9
    function: get_char_code
  loop_invariant:
    string: 0 <= len
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2342d397-8063-4f7d-977f-94955e7cef10
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 511
    column: 9
    function: get_char_code
  loop_invariant:
    string: 8 <= base
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 27b7b7c6-bc86-481b-963b-87dd08c0bf96
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 511
    column: 9
    function: get_char_code
  loop_invariant:
    string: ignore_case <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 009cb746-5c67-4979-a25a-ec5e14b098fb
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 511
    column: 9
    function: get_char_code
  loop_invariant:
    string: base <= 16
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 07615cf6-7e9a-4f44-b976-f3cb3897419f
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 511
    column: 9
    function: get_char_code
  loop_invariant:
    string: base <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 58f3c8bc-9c33-485f-9fb2-b65c32cb08ee
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 511
    column: 9
    function: get_char_code
  loop_invariant:
    string: len <= 3
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 32f2b339-f380-4766-9fba-333363876384
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 511
    column: 9
    function: get_char_code
  loop_invariant:
    string: base != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e436c23-2a03-4a1b-87ea-dd7136da6e2b
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1154
    column: 9
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a03b3006-bbfb-47ec-a18e-b7d181b6b1cb
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1154
    column: 9
    function: main
  loop_invariant:
    string: 2 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 30a1687b-1de9-4097-9a1e-d21ab1e56d94
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 637
    column: 9
    function: deslash
  loop_invariant:
    string: 0 <= debug
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b9b87972-be45-40d0-9500-97682cdbdd86
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 637
    column: 9
    function: deslash
  loop_invariant:
    string: 0 <= verbose
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b3fdfc7-dd33-403d-92d9-4be610942d76
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 637
    column: 9
    function: deslash
  loop_invariant:
    string: 0 <= line_f
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 403062b2-7217-49af-bf72-15f918b02f74
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 637
    column: 9
    function: deslash
  loop_invariant:
    string: 0 <= ignore_case
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 943b3e60-00f3-4133-9065-8ae6f29d2ccd
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 637
    column: 9
    function: deslash
  loop_invariant:
    string: ignore_case <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 86c758f2-9797-4c6e-ba15-e840a3675e7d
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1164
    column: 9
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d02cc519-2003-42d3-8a93-dc6257696150
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1164
    column: 9
    function: main
  loop_invariant:
    string: ((3 <= argc && 3 <= i) && argc != 0) || 2 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: be877759-55ad-48c2-af70-fc2e3362701a
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1181
    column: 9
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 03797b75-3260-4330-bf98-67753cd35095
    creation_time: 2023-02-02T14:22:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''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/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1181
    column: 9
    function: main
  loop_invariant:
    string: 2 <= i
    type: assertion
    format: C
