- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 972e457b-4aa4-4d54-b29b-d8c4fb166169
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: abbe1416-dab5-4dd6-af53-532d1bb08dba
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: d2980e23-f154-4565-b8d4-2ddf60f4cc9a
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: ff6f162f-4ab7-4b81-804c-dfbba7fb4796
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: e6769a44-7af7-4356-be66-b988d71a5550
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 5bab8199-f919-4659-b471-c671d09ad547
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc9022b3-a5ea-47ad-b707-cc9b7c6655cb
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1224
    column: 2
    function: pqueue_close
  location_invariant:
    string: -2147483640 <= pqb.qsize
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83cb6103-4e0a-4667-b6bd-2525d5277ade
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1224
    column: 2
    function: pqueue_close
  location_invariant:
    string: 0 <= pqb.closed
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aedd3a64-f41a-403c-8fd9-5cbe535ea8d8
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1224
    column: 2
    function: pqueue_close
  location_invariant:
    string: 0 <= pqb.nextin
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ad23ff0-cd46-43f2-9f7c-908255c3d483
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1224
    column: 2
    function: pqueue_close
  location_invariant:
    string: 0 <= pqb.nextout
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 16fb5dc9-6521-4b72-94ae-0dad3a5fb081
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1224
    column: 2
    function: pqueue_close
  location_invariant:
    string: 0 <= pqb.occupied
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e17e6cd0-f525-44e6-9894-f2286ddddf39
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1224
    column: 2
    function: pqueue_close
  location_invariant:
    string: pqb.closed <= 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c0625d4-6ad8-4574-87f9-3dd0227c2b37
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1235
    column: 6
    function: pqueue_put
  location_invariant:
    string: -2147483640 <= pqb.qsize
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25640eb4-bcb6-4f7c-8e22-382a1e1aea6f
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1235
    column: 6
    function: pqueue_put
  location_invariant:
    string: 0 <= pqb.closed
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d4eb7d8-27f2-44e5-b040-faf880581bea
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1235
    column: 6
    function: pqueue_put
  location_invariant:
    string: 0 <= pqb.nextin
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a44f227f-4c37-4439-b234-009054abcaa5
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1235
    column: 6
    function: pqueue_put
  location_invariant:
    string: 0 <= pqb.nextout
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 242f56a0-f477-430c-bfd7-e7e27ea87d82
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1235
    column: 6
    function: pqueue_put
  location_invariant:
    string: 0 <= pqb.occupied
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50121e99-2457-4986-abfd-f17311597738
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1235
    column: 6
    function: pqueue_put
  location_invariant:
    string: pqb.closed <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 65051b84-542f-4a50-8b28-fe9dce654a01
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: e51435a1-5829-4aef-bf95-13237696dcf6
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 1c428746-1cfe-4cd5-94a4-826596bdbe04
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 23e52e70-b543-46f7-a8fa-44f36e5f34d6
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: c32457ee-247c-408a-bc89-6a3944c5b1b8
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: eb88942e-7df6-4710-901e-9560206eab48
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: af9ceb08-c2d1-4aff-8876-678246189c3e
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 8b4fd4a7-3c27-469e-9b99-23e6166c3260
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 8d46c491-8ebe-4f66-9e50-fe6bf92d3a3c
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: f83383d4-d9a6-4983-b68c-2be079ed54f1
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 75e8c460-49ae-4a81-9c22-6efa9ac3b07c
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 21be7c84-ddc3-4783-83a5-f4a2ecfaa121
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 985d8863-f514-45f8-9957-e522edfd503d
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: ad8034db-6bd2-4c86-9ae1-a91d30e1a21b
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 624596f8-fb07-4774-9889-0349bf5d9acf
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 1561ffee-58ff-4068-8663-11bfd0f08a32
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 397a63aa-65bb-4078-8b67-43e142dcb6e3
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 62198e26-804e-4d7f-a054-2b1fec0c3b2b
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 2d715f3c-9aaf-45f6-808e-38e06e51494d
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: d5837e33-0ff3-4544-9bbc-d001dbd73d6c
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 9a4f1c32-1f3d-4a90-bd88-337303f1a1b0
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 13b89992-aaad-417d-8d7b-6d63fed4754d
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: baf0cbc8-5727-4f2c-940b-b02d543e8b64
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 3d419fd3-0ea3-4c1a-97d8-33a541295f29
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: f9abdcf2-dc31-44c7-a07b-590bbf19928a
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: b392fbd0-7f86-49ab-ad98-f69a7b2e92aa
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 43cd8890-a81b-439d-a082-4e4f59240436
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: c32a90b5-1d55-410f-ac12-f16cbe4911e2
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: d66621f2-701a-4637-afac-524bf7bc537f
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: c9d5c67b-db4e-46c9-ac9d-db154785f88e
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 2bad4532-bbcf-463b-8099-02e35631492b
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 1dda06f2-b138-4f5e-b608-ba239ce7472c
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 9d6246c5-7736-4f0b-a024-89048123c1a6
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: ba260c92-82b7-4fdb-9628-053f662ffd22
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 36238b9b-75c4-4203-ad49-4ee7ed7b9a20
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 3c2bc3a9-b2f8-4052-9657-a8cc5cf5b3d1
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: a9218af7-2ccc-4def-a453-c6d214317e01
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 9ef82bb6-8222-4e7f-bf34-87ae61de25d2
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 1257eb52-809b-45de-bc89-2784e2d21163
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 9e0dd9b3-9726-4cb2-8f2e-0a1c20c288e5
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: c4f87796-fed9-407a-af13-a01590d3de7c
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: bbcdc965-e692-4de4-804b-fb3faed90e88
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: b3ab76a6-d3c2-423c-8435-8610f0ad2f41
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 1d642460-7062-44d1-aea6-ab8fb5aa7508
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: cef833af-d9a2-4422-9ba9-a009f0567105
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 34869a38-839d-46c8-a9e0-749d1c869d40
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: bf10d96d-ab70-4eef-b755-824c7095b561
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 969e94ac-fa95-4862-b23a-59c3602ca8af
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: aa80c464-2e99-4006-8208-4af096643cc2
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 3f98776d-e4bf-4920-90fa-8952897e8f18
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 04166f7b-905a-4464-b308-ad2bc96290d5
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 4bfefbba-8474-4ea5-9696-3dd070485f99
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 5b0e1022-f76b-4251-bff7-6b15045c50f8
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 570dba3d-7257-4eea-9d2f-1c662a07eba1
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: af13dc14-f126-4f2a-9fd5-44a1bdf4649f
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 0ebb09fc-711a-499c-958d-603beae0b98e
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: c19e542f-990c-4e57-9d71-cfed2433b809
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 35e645bd-a96c-48ae-a5da-f6ff06d374d2
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: fa3725fb-08a6-449d-b431-c51e5898ceb3
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: f778f2d3-3b53-4644-a07a-a1d7c68087ec
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 203a3020-f89b-403c-bfeb-b0795ec32bd6
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 7bb5696f-4b64-4879-ac7a-c7c456c3ccbf
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 188dfe6e-23c9-47dd-a42f-4a19e2173cbe
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 0518b958-ddb1-490b-a7a1-d8aede5250ff
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: c9df452c-aa7c-4adf-a138-c2055ccc1cfa
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 72c7effa-6919-4df8-9510-98f837965166
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 9ba7e600-ac4a-49b6-a585-fc5dd59123ed
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: f87403a3-4e76-43c8-86bc-335c9ffa6f60
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: faa593c1-366b-492a-adfe-bfdb361d89b4
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 20f6e8fe-205f-48df-ae0e-771ef9707692
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 4978f391-1b99-4480-bb24-1ebbff429148
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 3c34819a-bf8b-441d-8c55-ca6d6f5b280e
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: ba1be516-f34a-446f-a626-127fdcbf3495
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 337ac465-98cc-4772-977e-c0e09e4b7e5d
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 7b78253e-8345-48d9-a1d7-43d0dc122e36
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 5794e941-a065-43cd-ba59-21ec6a433df3
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: d9595645-e20c-4283-9a2c-317d5cb41666
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 2ff08f58-e0cb-403e-9a45-88642a5c905c
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 18834874-6a5b-4ee1-baaf-7ec7c50ced3c
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 213b7310-b12f-4ba1-8596-8c41b5dd6c53
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: ba53a76d-9984-4f06-9692-bcf8d0b4486f
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 89ae11ea-af82-4ede-8ec4-8374596471b3
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 7c274359-19e2-4560-be37-d7fd9b8ca66a
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: bd81a33b-e3da-48d4-a606-debd214885bf
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: cbd6e586-1b15-4aed-86e8-1bc54eca4323
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 5db5514b-beb8-42d9-ac88-7370739f7aeb
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: c7e7d802-f40c-423d-a9f3-a5f9fcff30c4
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 21c9cfe5-901e-4678-b8dc-b35c213885bf
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: a6a37cd4-070f-438c-905e-6ac4613385f8
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: b7ed4120-ecfe-4737-a393-59a4cceaac5e
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: b1faaee0-8715-4d29-afb2-a14b9ef92ba2
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: e87672d7-4ed6-4b58-9950-75c35928b5e2
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: fd990dac-975b-4ddb-a0b8-90aa4c0a5bb0
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: a5ebb964-e2b1-4264-84c8-f5717840fe8b
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 3e41c6d5-8657-459b-b90e-ed3f80b25721
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 50cf934a-0957-450e-bed5-1afbe123fdef
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: ff13c6fb-b867-4aaf-b910-899a2541b889
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: fb8992f3-6a7f-4500-b542-7c4b4d75ea1d
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: e4abe8e3-2a2c-4910-8674-0f31dac82e0c
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 03546982-f3c8-44e8-a340-1c282a290a71
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: b8797379-2dc5-43fb-a819-b149dbd7fbde
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 091c1e36-57a9-4888-b4bb-f85773142284
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: ee6628d1-629c-494f-a309-dd7a6ab15408
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: b42303a5-21ee-44be-a623-10a48e8690fd
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 8f095951-8e9a-4e49-8ef3-2180ec4f2266
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 694df3da-dac0-4f09-8e02-b611c1ce694b
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 57408200-83ca-4e8a-8102-e0e3fbd441cb
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: dcf2ec07-d585-4fe9-8267-320be139f9fc
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 1a0e70df-d1a7-43eb-bfa4-18ab56526488
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 4db4429b-4e2f-41b8-9a95-fde9fdd8c59a
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 9e51cb17-fd21-474a-b1cf-b6731d4b975d
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: c6df6de1-7ab8-4ec9-88f4-7157dd8d0da0
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 7c67b689-972b-4092-b33e-c3df75f42080
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 3232b6b1-5589-4565-a3de-6268d2e368e9
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: a1200dc9-2f5e-4c8c-a9f5-b798339f3154
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: f291a9a3-42dd-4ce9-8f41-513c824d1464
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 41e8a673-2c8c-4725-a5ff-d7609085e368
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: e39dc0e5-6238-4c6b-b07d-98adf046a3a8
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: e692e294-3c3c-4771-82ff-5db11ffdc472
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 398e2210-045e-4ca5-94fa-a10735b5c95a
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: b29dd63c-6f3c-427e-b7c5-5b70f39075ce
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: cea57f0e-8fcb-44f5-8e11-94635f9cd1df
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: d4434137-635f-4b40-af21-fe7ddc656330
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 52d0996c-35ec-4b70-bfa1-fb48f38cd470
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: e1dad1a1-e86b-4f08-8a1b-9fdfd1412609
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 7d930b00-be80-43a8-86f9-15352e413889
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: bdecdd5f-e0b3-452a-81b1-8dab47a97357
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: 2 <= i || (((((((((-2147483640 <= pqb.qsize && 0 <= pqb.closed) && 0 <=
      pqb.nextin) && 0 <= pqb.nextout) && 0 <= pqb.occupied) && 3 <= argc) && 3 <=
      i) && pqb.closed <= 1) && pqb.closed != 0) && argc != 0)
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c4b6f92e-d20b-4045-8a8e-a355a21944c8
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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: cf7d4cb7-a679-49aa-bbe0-f7e111453c85
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_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
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 55c35dd9-0cd6-44dc-be34-4a2cc1f82366
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1238
    column: 9
    function: pqueue_put
  loop_invariant:
    string: -2147483640 <= pqb.qsize
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 06ff1bff-de2f-4e50-94e3-0d245054a42c
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1238
    column: 9
    function: pqueue_put
  loop_invariant:
    string: 0 <= pqb.closed
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dca667a2-0248-4265-aa83-dc1aeda6a9fc
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1238
    column: 9
    function: pqueue_put
  loop_invariant:
    string: 0 <= pqb.nextin
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 022fe9d9-7ba9-4a51-b4f2-479c102a6d27
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1238
    column: 9
    function: pqueue_put
  loop_invariant:
    string: 0 <= pqb.nextout
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d9ba5f6-1959-4b85-a0f3-09c46a09c1d2
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1238
    column: 9
    function: pqueue_put
  loop_invariant:
    string: 0 <= pqb.occupied
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 88981940-b338-4f26-8948-75fdd384a882
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1238
    column: 9
    function: pqueue_put
  loop_invariant:
    string: pqb.closed <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 25605313-acc9-48e6-9f27-75b4068c59ca
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1258
    column: 9
    function: pqueue_get
  loop_invariant:
    string: -2147483640 <= pqb.qsize
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 88f9961f-bd9c-42aa-b4d8-4576114f47d9
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1258
    column: 9
    function: pqueue_get
  loop_invariant:
    string: 0 <= pqb.closed
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 53195429-871b-45cc-a3b3-d50bcb858344
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1258
    column: 9
    function: pqueue_get
  loop_invariant:
    string: 0 <= pqb.nextin
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 74b38d38-01f5-4f19-950a-4dae9461ecd8
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1258
    column: 9
    function: pqueue_get
  loop_invariant:
    string: 0 <= pqb.nextout
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ba581f0-411f-4cad-a7fa-506a054fe6ef
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1258
    column: 9
    function: pqueue_get
  loop_invariant:
    string: 0 <= pqb.occupied
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1296f25b-a5ef-4a03-9de8-8247096e363a
    creation_time: 2023-02-02T15:11:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c''
        ''/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
      - /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
        /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c: f408fa73dcb71398930d72b962b11b40e8915ac10993d87ee6c2d7dcc266536d
      data_model: LP64
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c
    file_hash: b9cdd3fd4da214506118ebe7d1b10c0c44ace6970bb7e49741612a87b4a9c442
    line: 1258
    column: 9
    function: pqueue_get
  loop_invariant:
    string: pqb.closed <= 1
    type: assertion
    format: C
