- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: acb9d2a4-1b47-4862-b160-954fcf0640a2
    creation_time: 2024-04-30T10:59:49Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      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: 3275ca63-da7e-48b8-b992-8450037dbe82
    creation_time: 2024-04-30T10:59:49Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      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-complex/safestack_relacy.i
    file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
    line: 1913
    column: 9
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 7037a54b-326a-4e6f-9cee-032b6da604d3
    creation_time: 2024-04-30T10:59:49Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      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: cd927872-630a-48f5-884f-df3a28f24b38
    creation_time: 2024-04-30T10:59:49Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      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-complex/safestack_relacy.i
    file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
    line: 1828
    column: 5
    function: atomic_compare_and_exchange
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 297f381b-e2c2-4b4e-8c31-14c3827822e0
    creation_time: 2024-04-30T10:59:49Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      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-complex/safestack_relacy.i
    file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
    line: 1808
    column: 5
    function: atomic_exchange
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ad0dd428-df7d-4125-a84d-6de1b5b4c925
    creation_time: 2024-04-30T10:59:49Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      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-complex/safestack_relacy.i
    file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
    line: 1817
    column: 5
    function: atomic_compare_and_exchange
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 23199085-087f-4237-95e5-e232ce7ad220
    creation_time: 2024-04-30T10:59:49Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      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-complex/safestack_relacy.i
    file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
    line: 1798
    column: 5
    function: atomic_store
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b9c26dc9-9a7f-4095-9d42-5890001b0c25
    creation_time: 2024-04-30T10:59:49Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      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-complex/safestack_relacy.i
    file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
    line: 1800
    column: 5
    function: atomic_store
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2ebc8d01-403e-4489-adcd-8156ba13f788
    creation_time: 2024-04-30T10:59:49Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      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-complex/safestack_relacy.i
    file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
    line: 1811
    column: 5
    function: atomic_exchange
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 04d437f4-0493-4bff-bb58-03710bc63ed7
    creation_time: 2024-04-30T10:59:49Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      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-complex/safestack_relacy.i
    file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
    line: 1836
    column: 5
    function: atomic_fetch_add
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b94d83c6-4ee6-4bcc-a8ea-d0ca16ed3c85
    creation_time: 2024-04-30T10:59:49Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      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-complex/safestack_relacy.i
    file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
    line: 1844
    column: 5
    function: atomic_fetch_sub
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c28e69ac-1ffb-4fe9-ae84-1b68122b7872
    creation_time: 2024-04-30T10:59:49Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      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-complex/safestack_relacy.i
    file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
    line: 1841
    column: 5
    function: atomic_fetch_sub
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 831d06b7-8809-4794-a1c3-4bb722d31e61
    creation_time: 2024-04-30T10:59:49Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      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-complex/safestack_relacy.i
    file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
    line: 1833
    column: 5
    function: atomic_fetch_add
