- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: ddda57d9-2759-473d-ba59-7b27647696e9
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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: 296053c1-48f2-41a8-a349-6dd63c973d51
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 222
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0a57e670-d539-4fef-afc9-4e23954797f1
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 237
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a175477e-7786-4f54-a2f9-b453b7e388e7
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 189
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d693548a-6cdc-4a00-a3da-09789ad3b8c5
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 69
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8e566a8b-0a28-4725-ab02-1f736cc4e957
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 145
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2f26bb73-9da0-4e9e-8ad0-01765d2be7a0
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 229
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e2cd6264-4afe-445a-bb68-f8b69760e15a
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 75
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 30b71511-17a8-4bbe-aac4-c713a41db3b7
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 224
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4bf730c2-c3a9-4f05-bbac-f1507573b378
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 56
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3ecf7f24-46ec-4594-8eb7-bbdcf4e68dc8
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 243
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 016b0d18-cbde-427a-bfdc-e6d85081c551
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 90
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4ebb2c9f-8913-4108-bdab-0582f7d91b6b
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 234
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bf2d5826-7e5f-4066-bc88-c4e6b9c0e472
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 140
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 515298ab-6fec-4914-bff6-ffa92c359d08
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 256
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 138e701e-552b-4a34-ad2f-5e4437612b14
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 168
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6d44a7d5-9250-477f-9804-5cd94206be76
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 113
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fb29ff78-d1fb-412d-8e8c-a441fa4c6809
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 202
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f8ef0923-e633-41e4-b9a9-33c8aef72e26
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 110
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a04fb6f9-b6c7-4325-b908-1b709d4300c7
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 258
    column: 5
    function: thread3
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 6897c042-8b0a-4184-b6e7-8ab14ceeda04
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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: 3b625516-97b6-4d4e-8dfb-52da7de2642b
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 333
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0981dea0-c2ac-42cd-a432-c674b8f028c4
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 294
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 654d2306-08e3-4242-92cc-54dcf8fab721
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 180
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5e1ad8af-d82d-41a5-99ef-6d011943affd
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 270
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dedbc81e-d8cf-462e-8eec-4a904e3f262f
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 231
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 659d0552-0807-46f9-96a4-fe875b738803
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 61
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a7b2f9fd-94e1-4df2-9788-0e2522c69eab
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 172
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 98be8fae-4718-4b84-9bf1-880eefb1d5f2
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 210
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2cfc98f3-398f-4402-87fa-a07037fd75bb
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 240
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 032077db-13b6-4948-8660-c34ba2857eaf
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 105
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3cc01683-26fb-4909-9ca7-5b5e302c5124
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 121
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 32b721ee-7fd3-4ac6-8496-44f7b1db0b0e
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 88
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 77ff3071-2530-4536-b5fe-ec331e761860
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 50
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 213e9c6b-21e3-439c-aa7e-c9d0f810a942
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 72
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c3a090ba-c418-4908-beb5-086238717f21
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 261
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8dc3b87e-353e-42e9-941a-f24a90908edc
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 174
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0b5ce6dc-7e9b-4280-9c65-ece247b1d8dd
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 166
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 12692458-1457-4c6c-9747-f9fb03e7e257
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 264
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a811326e-fccc-4ae1-8dd0-c27a4776d782
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 156
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1a6e9af1-088e-4d52-bcb0-01c543a8ca58
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 84
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 993eb05a-1fd0-4a6c-9da5-8dcdfed190c3
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 66
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a88c81d9-9407-4e1b-9ab2-6dc5e15015f1
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 278
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f41e265d-3a87-40a5-9fc4-68d4cd8e9f01
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 252
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0aae7ff0-4e82-43f6-9bb8-60067fd46bd3
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 286
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 618c2457-49ac-43ba-a850-4bbb8cbcf6fb
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 205
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5b494220-3822-4500-9eaf-a6cd423c52d8
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 138
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d69e4b70-ec0c-44f4-94d6-99ff53052aea
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 289
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1804385b-bebc-4bb6-a167-7245808267c3
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 126
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 39cef639-a0b1-4415-8891-76d04f3bbf81
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 96
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7b81bc85-efed-4421-83c8-90beb1c13f80
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 153
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f8a70d85-405c-479c-b6af-70e162654371
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 93
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1d326f86-7976-4af8-ae17-5de47d2485dc
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 147
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: da7d966a-cedd-4c6f-a3ab-d1e24e78c26e
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 102
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 10568e41-63ea-4a8f-9a56-5f2bac2be3eb
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 186
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 32257dd4-57dc-4c73-a5f0-709b870fd643
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 150
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9808ffe6-38af-4c97-a6c9-ad37e9961e3b
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 134
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 86efd3c4-1644-4324-85eb-d4cb8f4718d8
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 177
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 95cc1f18-261c-45d7-89d9-39b79fd5e7cb
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 63
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ac2fc48a-8a87-4377-bbfb-94ac3c6c979b
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 194
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5599cc85-7af1-4ebd-b5b0-ac908f699098
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 197
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ea01373f-25fe-4127-89ef-0aa9c93cbde4
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 118
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4c3d6aa6-2f85-4d99-8158-556e13c1d3b1
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 82
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6da97f12-9908-41ab-a0b3-7ac335007ca7
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 250
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 76ea087a-d5aa-4fbc-b0d1-23cec9ee4cad
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 218
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6cc1e701-cc17-46e4-8b7c-5a9b2cfe42a7
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 273
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e31b3f1c-dec7-45f8-a9fb-38c6771811c2
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 54
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7f4a4eaf-70b7-42c0-b5dd-e554a023d03c
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 159
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ec48b920-188a-4695-b13f-d4a301659cbd
    creation_time: 2024-04-30T11:29:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-trans.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
      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-trans.wvr.c
    file_hash: 0028e6fa5bf865c1068c8d55bf1863ae46985780e15895ccbb76824c97a247a7
    line: 281
    column: 5
    function: thread3
