- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 1d258c82-f5db-48cc-bed7-5ac1bffc1623
    creation_time: 2024-04-30T09:34:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
      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: ec81c44d-4a5d-4703-b246-890120ff1d7f
    creation_time: 2024-04-30T09:34:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
      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/26_stack_cas_longest-1.i
    file_hash: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
    line: 750
    column: 4
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c5e2fd3c-80a0-4f07-b2eb-e8b56c0315ba
    creation_time: 2024-04-30T09:34:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
      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/26_stack_cas_longest-1.i
    file_hash: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
    line: 696
    column: 1
    function: __VERIFIER_atomic_release
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 28b1d32c-230e-46f8-8c5f-976a447af37a
    creation_time: 2024-04-30T09:34:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
      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/26_stack_cas_longest-1.i
    file_hash: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
    line: 752
    column: 4
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 70cc4496-1430-4e1d-8050-b0318a39f11b
    creation_time: 2024-04-30T09:34:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
      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/26_stack_cas_longest-1.i
    file_hash: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
    line: 701
    column: 1
    function: __VERIFIER_atomic_CAS
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9525a92b-4ed2-426d-afb2-492e61eab1e7
    creation_time: 2024-04-30T09:34:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
      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/26_stack_cas_longest-1.i
    file_hash: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
    line: 695
    column: 1
    function: __VERIFIER_atomic_acquire
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 517909b7-4423-447e-9c20-fee625711ed9
    creation_time: 2024-04-30T09:34:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
      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: a44a368d-27d7-4910-93d6-782d6588f080
    creation_time: 2024-04-30T09:34:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
      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/26_stack_cas_longest-1.i
    file_hash: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
    line: 793
    column: 13
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f4289d28-da3e-4332-8eb4-e6c67e770001
    creation_time: 2024-04-30T09:34:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
      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/26_stack_cas_longest-1.i
    file_hash: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
    line: 691
    column: 1
    function: __VERIFIER_atomic_acquire
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1e39040d-475a-4194-92a7-d362161cc71d
    creation_time: 2024-04-30T09:34:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
      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/26_stack_cas_longest-1.i
    file_hash: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
    line: 715
    column: 1
    function: __VERIFIER_atomic_CAS
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cdff6791-9444-4c08-87b3-4120456fa517
    creation_time: 2024-04-30T09:34:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
      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/26_stack_cas_longest-1.i
    file_hash: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
    line: 764
    column: 1
    function: __VERIFIER_atomic_assert
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8eb4f4f1-bde4-42ee-a587-df6290d6b14b
    creation_time: 2024-04-30T09:34:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
      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/26_stack_cas_longest-1.i
    file_hash: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
    line: 700
    column: 1
    function: __VERIFIER_atomic_release
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 824c8f5a-a4ea-43fd-87f7-261a975b3470
    creation_time: 2024-04-30T09:34:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
      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/26_stack_cas_longest-1.i
    file_hash: 3efee66e785ce3d2f2ce0101e78a1cdae99209fb089cd0ed9c95f4aa53c186ea
    line: 761
    column: 1
    function: __VERIFIER_atomic_assert
