- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76807523-c9c7-4e4c-b0f6-8c9ad4fd9597
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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 || (break_17 == (_Bool)0 || break_17 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 140d53d6-cded-453d-89f5-3e2d79022ca8
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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 || (break_17 == (_Bool)0 || break_17 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af0ac58e-3b9f-441a-bdbb-af36c0029b3e
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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 || (break_15 == (_Bool)0 || break_15 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 02f6c691-b662-4ea8-8338-eb0a975485af
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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 || (break_15 == (_Bool)0 || break_15 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47232e48-51ba-43d3-ac99-a401a429602a
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 33a36ba3-0a0a-482d-a8c9-6bb408782260
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 690b40e6-f79f-4a33-8c07-60f2afde63ce
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 65a817dd-fbfe-4b4e-b98b-e82e047970c1
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 4ab46413-f914-4428-aa89-6aa6ae946f3e
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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 || (break_12 == (_Bool)0 || break_12 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08255004-7c47-4536-af09-a3c206f6e35c
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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 || (break_12 == (_Bool)0 || break_12 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a41fdb1-acf1-4849-a879-4aebbe6fc31b
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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 || (break_10 == (_Bool)0 || break_10 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dcaa255f-6c33-45f7-8800-97b79d6951a0
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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 || (break_10 == (_Bool)0 || break_10 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 236d2e3d-d92d-451f-83ed-de5880622258
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 05d98be9-e3b6-4de1-89b6-ae874bebc142
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 75b75ad8-6ac7-42bc-8831-003620bf325e
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: c4611049-760a-49c9-b115-ec3badcc3731
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 0b002529-4c07-49ea-a175-5dea81c2181f
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 39279dd7-a2c5-4a94-a173-93eab0752d6c
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 620c8c16-d2a0-4a26-b86d-219f6543fb89
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 9c9fdc71-0e02-45a6-a1ef-54b2d45bfbc8
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 3e8c7978-00cb-4bf5-be8f-a4eaf3f52609
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 29f95033-7753-43ce-9203-a1558de0d2c3
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 2e7d9dd1-ebe3-4d6b-b684-5f897117bcf3
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 0a6b352e-f5a6-4508-8a65-e14481fca435
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: d59be0a2-2cf3-4f2b-a5eb-bd683c97580a
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: d2456895-e9f5-4fed-9f38-82f39726ba93
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 02c5b3c2-9731-4b1d-a515-831e15e362b5
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: e025adfd-7957-4ff9-8675-812f0cf514a6
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: cc1cda46-dc10-4faf-8731-4f8c9aa2374f
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: a0ac4120-208d-47eb-9147-23dc936b10f6
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 8a91b1ee-cab9-4074-bdd3-2f609dc3343e
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 52380b7b-a956-484c-b7f7-0ecf584dafe3
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 01b94ddf-fb24-4ccc-8f9e-cc6587067ea5
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: f7d127a3-0679-489f-ad20-2d836362c4a6
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 9c96f4b9-933b-4376-8921-91d54ea44e8a
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 5ae96411-2a3a-4c10-9c84-8a6bb532995a
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 310b567d-6896-42de-9f90-c3708b83eea8
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 5a58646a-c438-4cb6-9230-5486b5b07545
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: bc98f881-c454-4582-b074-6958ca0aab1f
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: e25dc0d0-5cdc-42d5-9c74-2abf515fd6bd
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: b5eea1e6-2444-4194-aef8-0ded0e3cf1d4
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: f269499a-cfcc-4507-acd2-345a535c6fcd
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 7921dd34-7fef-4234-b2a1-9f5805e877bb
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 17d02797-d098-4bcf-b282-e51e74c020fd
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 932c53f7-6ff5-4c1c-ac7c-90cbd175a874
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: c58de2bf-a4dd-4c8c-9f3e-2f243dd2661c
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 590023f5-1359-4adf-9f6b-0979abfdd7c1
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: ec4d1a72-23bf-4e6e-8495-015c31a45b07
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 3beec796-cd21-4358-829a-4ca6349626a8
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: a52f3ab8-2984-41e1-8506-76836eadcfb9
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 7a8e7656-30c9-4ee3-9ebe-2408fe821c43
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: c99edbc6-0b7c-4780-a881-7e04bca25fbc
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: c574ee4f-7325-41d3-9922-82533d3cb860
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: d1eed0cb-c16c-4e64-a801-34977279db53
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 0fa61dd2-0928-4230-8f80-23ed6c6cc584
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 26ff4ad2-6197-417a-858a-64d30343972d
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 29c9f6cb-cf44-40fb-9217-7cd511b358b5
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 7cb49495-66e7-468b-bb61-2d45cd2b483c
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 912341b7-c569-49b5-94ce-66fc514095cc
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: b657b69c-e0c3-4940-82ca-510a954812e3
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: cc0ee4f4-20ce-4d7e-9033-ecc09fe623b2
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: adaf2d41-ec81-4f29-bd27-be8cedb2004a
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 3711864f-38f5-4607-828c-ec1b4ee14252
    creation_time: 2024-04-25T07:42:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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
