- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e4dde57-18d5-4842-9e2c-64704110ec1a
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 230
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i1_9'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c37d460-eba3-4538-a3ed-70c1696a3143
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 231
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i1_9'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 15b175ed-752c-42c0-9068-47f16a82b572
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 230
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i1_14'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 820f0e4e-645d-4571-a23c-20fc8c513272
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 231
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i1_14'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78aed799-b683-44dc-b0d7-4ecef7e4def8
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 230
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || i2_16 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76329354-5ecf-49b1-933c-7354fb2025ba
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 231
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || i2_16 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 290d1726-0200-4b23-a936-5d54451b0e4b
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 230
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || i2_11 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b66c8b33-5f5b-42b5-bfdd-21a80db5bf22
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 231
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || i2_11 == 0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: aa304f6c-77b1-48ff-90d8-349d39b7ac8a
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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: dbb546b6-d196-4162-8574-f7322c86a010
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 156
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3c4673c9-4a68-44a1-888a-33137e833f16
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 84
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 27fc8ba2-e2b7-43fb-a2c7-a29b48a45a80
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 66
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2b39b676-6cca-4c7a-b1a9-e5406cdc0d25
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 189
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b8d7a377-4873-4600-9d81-c5f4cf4e19c9
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 69
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 51b9ae97-733d-4299-83bb-ec91015a56d3
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 145
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4a9f1ec6-10b5-498a-a0f1-f9df3238d636
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 172
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2435ae3f-d05e-44b7-8437-e4f2208d7a58
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 75
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0cf5e152-4e5b-4358-bd27-0f8e217355ad
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 56
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d0b925f6-f03e-46ff-8824-27ea714a6d76
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 205
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 84193cf7-8521-4868-ada6-3ba2340a9ae3
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 138
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3c7001a9-4727-453b-9acd-924db71c9c08
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 90
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bf20b525-7faf-41a5-b19e-372ac5bcf7b1
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 140
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a6fe3c0c-5672-419b-96a6-1d65cd7f5d0c
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 88
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 09bbf6d7-2303-4ea2-a056-ee967935af12
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 168
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a616ae97-5918-4970-a8a0-0fdbb8a763b7
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 126
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3d14de15-1c2b-4a5e-84ea-cef08666d479
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 96
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 520294d7-9962-4123-940f-e96e8642747e
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 113
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0fecebaa-7666-4ca8-abb9-8a33e3e27880
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 153
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 402df8e6-5163-4065-895e-4096f075c7dd
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 202
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 48f08e05-c744-40a7-9c5c-7b23587255ff
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 110
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c53f3f3c-d22f-4603-a304-08a3696edf00
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 93
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 043401ac-906d-4f87-beb7-7f1ae1c87264
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 61
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d89708db-ccb8-4d1a-9314-f6f58c85946b
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 147
    column: 5
    function: thread2
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 06384ec7-4313-4727-9e3a-b9c567684de3
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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: 279eda0e-8a4b-4071-9698-d9b735eb93b2
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 229
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 32bdddb5-02c4-4d4a-9c40-35832efde0e3
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 180
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ac8126bc-81ff-4b12-bac8-573843908ec4
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 102
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b9e6842a-428f-4631-9554-1059cb6b2f78
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 210
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1584077d-0204-497b-91de-a9b08d3f7a0b
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 186
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d16f3172-9486-4d5d-8f05-be0104ac956b
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 150
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8992e7ea-6fb9-4096-89ed-830985e1fcf4
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 134
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1e572f4d-29aa-4baa-bdfc-3c7af70e8ac6
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 177
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a989dd2d-5d2d-47a6-bda0-f6a38734a399
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 63
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4b729c05-c439-4bb3-8faa-7afba78309ae
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 105
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 139d7a4e-938f-404e-bebd-c20e6c1f36d6
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 194
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dd1fd4ca-e168-4df2-8960-d62569082a00
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 121
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2926f2c8-03a3-4b43-ad1d-b68918687083
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 197
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 60193d65-a67a-4c5d-b63f-b2f1682b099d
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 118
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d9456010-9ef7-4051-ba88-16e754c57d97
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 50
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fbceee14-7410-4f3b-80fe-05a04c97e51b
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 72
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7386df2f-bca4-4f21-8d70-0bc2ad287803
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 82
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b980f33e-473f-46cd-987e-59ca23e9fdf0
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 174
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0d8ad7af-edf0-43da-a954-6c02f0e58f10
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 166
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a0acfe8a-aa7c-4822-9a4c-68f62c02e4a8
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 54
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 389af110-2da1-438c-b6c0-8f5d33b2ef9c
    creation_time: 2024-04-30T09:42:31Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
    file_hash: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
    line: 159
    column: 5
    function: thread2
