- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4815ae01-3733-49ff-b699-a76359094e3e
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 815
    column: 2
    function: matchfun
  location_invariant:
    string: 0 <= n_matches
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93279e86-fc82-46ac-8978-e4195616fee0
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 89d00ed8-f0a2-4cdb-b2a7-54b0a0665c07
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 4fbaaed1-8033-451b-8362-ec38cfdf8d99
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 50f125f3-ae23-47a2-9bd6-75021a5452c8
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 7d5b288b-15ed-4a7d-ae57-a3f21e9c8b00
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 79f6d638-aeb2-4583-87a3-b4b3d8a22b06
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: c0eac616-1ce2-4689-8e03-4f5a6f522a7e
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: d2321ce2-009d-4d53-8730-be14f47035e0
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 2f69776c-0133-4b26-b5f2-2d084f491b24
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: b1f9efed-2639-4096-9244-2e5c50b0f9c2
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 94dd2382-925b-486f-81af-94eab0ac4d5d
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 1a28bcfe-f259-49e0-9f26-978df9caa8b9
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: c1d62096-db69-43d8-99c3-3642a4b5a376
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 75387dad-b34f-47fc-a162-8976ff9dad8d
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 94d10b1f-189b-461b-b6d8-a8380c826417
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 957f3f3f-0fdd-4d57-be7e-dc7f63cadf50
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 69b9ccc6-8bd6-4702-a036-1011883728b7
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 18480b1f-449e-408c-a7f6-a82c96e9c077
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 6bec74ad-d7bd-47e6-bb0b-28e9b7a77e84
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: cbdfd2d6-39b0-47e9-aca5-7dffb1d27b23
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 4d87b779-f844-43be-a85c-c95e285918cf
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: f1f4e223-129b-44ae-afbe-71462f89dbc0
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: fd788a5b-ac26-4fb5-a7b2-6d9c2fdbc541
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: fc8ddfa7-2375-4cf3-8907-d5de9a5ed40c
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 2bb01621-a0c4-4299-a93a-474f0bc69d45
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 0b56a7df-f76d-4dd6-8e11-591cb2ff7cc9
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 0ea3f476-9694-44c1-8276-2139c0933679
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 838844b6-80b9-4c35-8448-abb146a979e6
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: df081a04-bd28-4afa-86a2-cfde48576ca7
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 2b2e05aa-659d-48a2-a72f-9deebf7c421f
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: acec1708-eac6-4520-bf46-427dec19b52e
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: e3cc2683-4eec-4a89-a654-371b3ab23881
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 5fbe743f-b58f-4c2f-b455-0604a6aa0781
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 27f2b1d7-346b-4e5c-9433-27d077867c88
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 65742790-2c8f-40fb-93c4-fdd43d2ea355
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 90578b53-cec9-4b37-91a0-e4f53a637f05
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 5a75a16d-e485-47d9-84fb-1f3df841e6b5
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: c2d16f57-63bb-4343-adc5-0daa14cb50b3
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: bc09bcff-3e2e-4c76-b1fd-3ae79baf7d8c
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: d489bc28-afda-49d0-b5d7-3a237c7e441f
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: b3b63e23-dac4-4a41-b85c-2cf4847a305d
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 4c42b4a2-4152-4492-8b14-0ca48cfea469
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 73d212f0-c38d-4f07-ad39-bdf235d27b79
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 3e7420eb-86ff-498c-a7b8-c1456bb8b395
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 78a58b7c-3e27-4a55-9072-554f75c14b24
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: f1001a6c-b64b-411a-bd74-d8a31569cbd1
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: db768609-8508-4662-9c7a-a926978f708a
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 78d2c9ba-263a-487d-883d-72ce0c4e8742
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 803b4ec1-35ce-4945-bc89-9ba84d8847e9
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 2c83751f-b34e-4759-9b84-3a705471c0f7
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 871f2ab4-5466-4446-bf16-6275eed39494
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: f1da2717-dbde-4ac9-8912-780ff952d972
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 2714cf7b-b8d8-46a0-8199-141f07a8d500
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: d85c796f-9657-40cb-955f-f77373444a86
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: bab6ca7f-c24d-4e60-91ee-8f9ef45351e3
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: b48e37a5-c19c-447c-a725-a4a6f9fbc778
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: a9f8c4eb-d575-46b8-92c8-3ee72bcb39c0
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 660b4303-6030-4983-9755-88f3a9078383
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 39455bd5-3a09-47f4-9ff5-4a68a662b749
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 5f3cbcad-9247-49ca-bc1f-f375ad7fc15c
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 83097dce-6919-41d3-9946-88c7420161ec
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: ee022072-e39d-42fe-b3d7-fefa1378368e
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: a75382b3-d3a3-42b8-8fe8-edc7c191b89e
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 71d4bdd6-c31b-42a3-9af9-449b5c30c0aa
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 4ae032a8-dbb2-4196-bd9a-006f698fac2c
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 6d001dbf-fe09-4315-ba81-d74f1447c290
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 6ceb2742-cb19-4b3d-988f-bd7c40849abb
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 13e5c3d6-d895-4523-a4ac-dce403ca1dd4
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: a199fbb6-b3b2-443b-8a29-2c9a92f54e45
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: f1e3b737-0fc7-4bd1-91b9-6612a0a74ba6
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 1de73103-737a-427c-befb-a50e488042c6
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 2c36e743-6a36-499e-9c45-92dcc3d8ce00
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: bb9395e7-cec5-4529-afa3-1822a3359ece
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 3c0fdebd-b867-4895-85c1-83f16d6e96a2
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 88a82470-5d17-4664-bead-f7c3855c633d
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 9c257e99-bf6a-47bf-98a9-c74823f6cbcc
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: c4a69fdb-e53b-4b0b-adf4-51d20fedd6d8
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: bfb1a78b-0101-4c74-b1f9-f3fe85166a7f
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: d7e50987-6c2b-4a18-9a7b-a228a7e22977
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 3e6838e0-c290-49fb-b2e1-9318547931b3
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 9186dec2-b7eb-4549-8717-7e6a4d9f142c
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 74249db6-98f8-47fc-96ba-10c1f14790e9
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: ff02f913-11d6-466b-b72b-ceccb72aa810
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 8f6c8bbc-806d-4ec9-9ba4-19a29c298d54
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 908e1280-9e71-4f1e-bf2e-af02e910b849
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: c61fc1a9-c54f-4c5b-9870-88d667f07891
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: bfd83723-4649-4975-9e61-b3913a742c1a
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: ded27e4a-0ad9-49d3-858c-4ac6cafd81ca
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 339b1d9c-04fa-4f7f-a80a-ca60b1e44437
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 6cf63c29-d9b6-4cd1-89fb-0f044cfcd113
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: babc8b7c-51a3-4362-8280-052282283a9c
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 39d0e786-d7ac-4df3-a3dc-cdd4bd27dd93
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: f3b5817c-7130-411a-8f01-5a4e53fb2c24
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 2a1daae6-e354-4bba-b135-a7ab44757fdb
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 1737c9de-1b8b-4e60-8ba9-1326a7f3f105
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: e1c571f3-94ae-492a-ac07-66dce420a595
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: ae338761-82db-4ad3-8cc1-2b29e8f58913
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: dd740278-1631-4e00-9c39-6088174205d8
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: b9664e49-c05a-474d-96fe-7adfcb57dc1d
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 67bf07b5-21a4-4e51-a4ee-1e20e78bee7b
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: e8d16d56-1080-4eb3-8717-9b64f50f00bb
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: a6c2c346-1715-4c56-9b15-b468898e0481
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: d865ed46-0b34-4d43-9e5f-a9a77f53017c
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 86c98e51-e632-4095-9d17-8b498c5bc43b
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 3af582b4-4aa3-4aeb-89f5-010943f049a7
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: fb540228-db92-4f1a-b9cb-b790951212ed
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: e34146e7-661c-4f92-aa17-e684fcbb238b
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: a9ee4022-459f-4f1b-a8d9-4091fda9fa9c
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: d6f5ed57-7c1e-4854-a944-94e176ebbf57
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: bfe213c8-89e9-4b97-86e4-ad69e3e214aa
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 43fb33dc-1627-48f7-ae38-c22add8df9be
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 3b79f644-6582-4fd8-b7f2-2d7cc0c79550
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: c6af872b-595b-4142-aa7c-d00ca174887d
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: fff002e9-f974-476e-bea4-48bc5894aa79
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 86662a1f-dc20-40f2-b593-a9b3d0efa4b2
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: e54caf70-2db7-4ab7-b47f-eba2279eb18a
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 0fff9682-d6c6-4ee2-a1e1-de92ced43aca
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: ea000b1b-e012-47cb-aa7c-686defe99e4b
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 393f0df3-f426-4a3a-a932-9cd3797a033e
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 6173955a-6d21-4429-913e-09521b3478b0
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 695c8363-f013-4cb3-96c0-ce65778ccc7a
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 00ae4bad-63d6-4850-b966-79e55c799be6
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: d103626a-6419-4c45-a5c9-f461a2a6171f
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 0d7ad915-5a66-4872-b15c-e3d61ddd066d
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 973ce033-3982-4364-8899-6fe08a3086f3
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: a1a43a78-4fb6-4342-9901-cbe20ef9fbcd
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 5dfd6fde-893a-4d10-9070-ff5ae86c0f02
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: cd791b95-8412-489f-8a45-b5e0344e2227
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 94e76de9-e374-4648-86e1-81a6b8defbed
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 3e5eae03-6f00-4343-928c-0237d65dec5b
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 66e026df-a901-4954-b477-8bbbb4a3453b
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: f64f6d0e-954e-4730-aa10-85b27857b689
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: 077c9716-6146-452a-b6f0-b30bcd78f7ce
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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: d5055a31-de34-4aec-ae4d-0714e85be453
    creation_time: 2023-02-02T15:11:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''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
