- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: af60115b-3b39-4a5e-9e3a-501c66985de5
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 09ec04cd-77f1-48f0-ae0f-5d92542d38d5
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 225
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 35fe891e-107d-402e-8dce-a684ecec83dc
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 240
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3114c50b-efe0-43b6-a390-9c8fef3c7ba0
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 192
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 40e1375e-e7eb-48a6-8605-eaff3841c6fd
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 72
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ae64a381-dd24-42e7-aa0d-68cb1783b918
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 148
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f2c49187-4ffe-4d5c-a229-31c3f634d0d4
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 232
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ef7b0b35-32dd-4c91-8619-d552a427add3
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 78
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9803e0e4-5004-4f96-9c93-86e355cf057c
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 227
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 334196da-0133-485d-a757-fc16c8fd6d1f
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 58
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: aaab8799-e1ca-4864-abb0-f9d1b1d77974
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 246
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cadeb126-b13d-47bb-be12-a3a2345cdb3d
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 93
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ffcdbb44-12c9-4ca2-a04e-31a2b327e73b
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 237
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 425675ba-f38a-4f74-bd15-31281b03bf26
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 143
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 733c13d6-419d-4ff5-b1e8-e56ed470ca0d
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 259
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0092aed0-2f04-41af-ab49-f624611a8f9e
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 171
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a10882d7-2cc3-4027-beba-a34a2467614a
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 116
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d5efecd3-2428-4d37-8ecf-53f7632a082e
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 205
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b6681949-4b4a-4d99-a500-3e7b04b3c678
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 113
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d36d95d0-6c9c-40a2-82bd-36660ee28253
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 261
    column: 5
    function: thread3
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 19c044d6-93ac-4e0a-9225-08a0f3fa9952
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 746b54ce-9081-4f4d-b6b7-6cd93e8b30df
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 336
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fa5b7202-fa9c-4db3-afdc-43fd87e0a58a
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 297
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 43f97d16-49a7-4e30-85ff-7cc071485474
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 183
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ed53450c-8d2a-4919-a06e-afecf2774dc4
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 273
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 601ef312-dd0c-4cbb-b936-bd6d529a5cd6
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 234
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: eaec3f3f-2fc6-47f7-a9bd-f0c188e84f0f
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 63
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a641729c-ca5e-4f79-9299-c2779cb9669c
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 175
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 60b7fadf-3894-4cfc-b8c1-b3cd2d428982
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 213
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0160cc7f-0d82-4dac-8839-0508c03b06bf
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 243
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: af9c6877-db36-4f36-b670-e9b58f4ffac0
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 108
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fe336d6a-88fa-4bce-8268-72580a29cdd8
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 124
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4c33f1a5-3076-4073-8ad8-be5d42ec4b32
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 91
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 067f6bad-5bd1-4a02-bba5-794b2e32c282
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 51
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 528b3de3-e1cf-4ac9-af47-f9943d6a57cf
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 75
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1800db42-a811-4788-8511-9133cc178263
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 264
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 33f1f9ca-c647-407e-85a7-ab1c5fa91217
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 177
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4999d113-6c31-4d2a-a148-2947b3c13cd8
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 169
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1a0ddf6e-4215-4638-9ac2-59e05ea01b7a
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 267
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 941b6fd8-0201-4f84-bfbf-27d80bf784f1
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 159
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a360b959-d21a-489a-8d51-ff513edc81cb
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 87
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 23c27c42-fd61-4e68-b502-2db73b76cac8
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 69
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 016cb47f-6bf7-49d5-809a-034f55ad2053
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 281
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 61738d8f-4aae-4535-a7a4-5030e6bc02f6
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 255
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fde58cdb-3703-40fc-bdcc-15ad18713958
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 289
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fbfb04f0-183c-4204-965d-9bc0eb668280
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 208
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 03415236-fe81-4e92-979d-2ec4f3e91392
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 141
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c206298b-91ac-4e85-9785-eb705a362d2e
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 292
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c35412db-9e8c-4561-91db-7d794223cef6
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 129
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 06630510-72c8-43de-8e8b-3dfce36a5ade
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 99
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 002668e1-dabf-49a9-9328-44a21a82972d
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 156
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 333abcdd-4abd-4329-b515-136b1e18a845
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 96
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 483b49fd-e075-45a6-9b23-30bbdef3da32
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 150
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 036270bd-a1ff-42c6-8665-f39386612804
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 105
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 706ef875-50d9-418e-ba8c-feee0a526880
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 189
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 03f34ba0-91ae-4b74-8782-457084056fc7
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 153
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0c623268-b852-4410-9dd8-224e3d1c4fce
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 137
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 08c810db-9cc6-4901-9c1a-83eb82098aa5
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 180
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5823d104-d111-4863-9384-3b363a9685b4
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 66
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8e5e3805-205f-484c-856c-9e8fee0bd246
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 197
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a6a3a24c-b4b9-4d59-b35d-e97fa4622a0c
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 200
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: eb3c5424-8a11-43be-83a5-e4dad6859ba0
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 121
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 125941ce-8d30-4e0c-9c9e-7a13f498770a
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 85
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f269fd67-9639-4313-add9-89efb794af03
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 253
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 827e8d00-f8c6-4325-b3de-f7441ae38503
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 221
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8f931115-3905-4801-81fc-edf36b420935
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 276
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 12cc46c1-0265-4e84-9a3d-7d81f5bdd1c5
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 55
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 675d155a-805d-4498-9d58-c08b5fa57bce
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 162
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 76c11a13-1f35-47a8-8d70-68e7b70407f8
    creation_time: 2024-04-30T09:42:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
    file_hash: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
    line: 284
    column: 5
    function: thread3
