- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: e567c3d4-1b33-4694-962e-865680b6667b
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      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: 20de92b6-3dfd-45b5-a801-e442d5576731
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      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/pthread-ext/25_stack-pthread.i
    file_hash: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
    line: 734
    column: 1
    function: __VERIFIER_atomic_assert
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 8a434cb9-a921-4d34-80c1-05f4b8b2f4a3
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e1097276-9a8b-4ca0-ba1a-7b48f3fe54a6
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
    file_hash: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
    line: 694
    column: 2
    function: index_malloc
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6e0f5bb7-650b-46e2-8e91-1f90748b9b63
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
    file_hash: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
    line: 701
    column: 3
    function: index_malloc
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: b848ac63-e087-45ba-9e53-4d4d1edf3b3e
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m2_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fa0397e9-0e4a-4ced-83e5-4db1ef856d9d
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m2_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
    file_hash: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
    line: 750
    column: 2
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bab0e30c-6500-47c3-9d63-79067480a9fe
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
    file_hash: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
    line: 727
    column: 3
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 726e3c3d-2b8e-4656-ac94-912412d60af0
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      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/pthread-ext/25_stack-pthread.i
    file_hash: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
    line: 724
    column: 3
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ce8181b1-adb8-4c1d-9cd0-4fde9e00a093
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      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/pthread-ext/25_stack-pthread.i
    file_hash: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
    line: 737
    column: 1
    function: __VERIFIER_atomic_assert
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ed1a10eb-701d-4cab-af4b-5050572f967a
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
    file_hash: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
    line: 696
    column: 3
    function: index_malloc
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 073867d3-4ec4-45f2-847e-dba6b2705450
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
    file_hash: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
    line: 721
    column: 3
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9fb119a2-8e5f-4545-9647-5a2c8bf35379
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m2_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
    file_hash: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
    line: 757
    column: 3
    function: thr1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 5144146d-0c1b-4c1e-9d60-209c9bd9a28b
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      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: 04562383-4045-4feb-a804-a66ceb90ae46
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      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/pthread-ext/25_stack-pthread.i
    file_hash: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
    line: 766
    column: 13
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 57455e48-be10-47e6-b430-300fa8806202
    creation_time: 2024-04-25T07:33:10Z
    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/pthread-ext/25_stack-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
      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/pthread-ext/25_stack-pthread.i
    file_hash: 6ceb3f3e6275485c63fced12b91c17e53ff4ff51a32d000ec6d2fb8f40929150
    line: 726
    column: 3
    function: push
