- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 98372fff-61ba-4f75-af12-2ef2b0cf6771
    creation_time: 2024-04-30T09:34:43Z
    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/36_stack_cas_p0_vs_concur.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
      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: b5448374-635a-4655-904a-fb4117b5b285
    creation_time: 2024-04-30T09:34:43Z
    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/36_stack_cas_p0_vs_concur.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
      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/36_stack_cas_p0_vs_concur.i
    file_hash: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
    line: 731
    column: 6
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f6b20ff5-c4d4-4f62-bfbf-9b39244ce828
    creation_time: 2024-04-30T09:34:43Z
    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/36_stack_cas_p0_vs_concur.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
      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/36_stack_cas_p0_vs_concur.i
    file_hash: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
    line: 722
    column: 3
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d0080e06-f57a-45b0-9ecf-06e6733b3147
    creation_time: 2024-04-30T09:34:43Z
    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/36_stack_cas_p0_vs_concur.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
      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/36_stack_cas_p0_vs_concur.i
    file_hash: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
    line: 720
    column: 3
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fb8d75d1-f8a4-4b22-8a5c-925aa42c258d
    creation_time: 2024-04-30T09:34:43Z
    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/36_stack_cas_p0_vs_concur.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
      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/36_stack_cas_p0_vs_concur.i
    file_hash: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
    line: 733
    column: 6
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 88e45a06-0fcb-4727-984a-b8d6d1dfb9bf
    creation_time: 2024-04-30T09:34:43Z
    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/36_stack_cas_p0_vs_concur.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
      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/36_stack_cas_p0_vs_concur.i
    file_hash: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
    line: 690
    column: 1
    function: __VERIFIER_atomic_CAS
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 8b3a2f60-a223-41c5-bbf7-236775818d54
    creation_time: 2024-04-30T09:34:43Z
    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/36_stack_cas_p0_vs_concur.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
      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: f8b0b1fa-ab2e-4750-9b44-6ca5b04ec003
    creation_time: 2024-04-30T09:34:43Z
    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/36_stack_cas_p0_vs_concur.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
      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/36_stack_cas_p0_vs_concur.i
    file_hash: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
    line: 740
    column: 13
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0605b7e8-a2cc-47ba-bff4-e17b5dda19de
    creation_time: 2024-04-30T09:34:43Z
    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/36_stack_cas_p0_vs_concur.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
      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/36_stack_cas_p0_vs_concur.i
    file_hash: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
    line: 712
    column: 1
    function: __VERIFIER_atomic_index_malloc
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7ae5c848-b1e6-431c-adaa-4d6f88c9e3ae
    creation_time: 2024-04-30T09:34:43Z
    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/36_stack_cas_p0_vs_concur.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
      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/36_stack_cas_p0_vs_concur.i
    file_hash: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
    line: 704
    column: 1
    function: __VERIFIER_atomic_CAS
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0c15c3ee-478e-447d-ac1f-a333dc76544b
    creation_time: 2024-04-30T09:34:43Z
    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/36_stack_cas_p0_vs_concur.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/36_stack_cas_p0_vs_concur.i: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
      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/36_stack_cas_p0_vs_concur.i
    file_hash: 5bf99dd5722e6551de991a345b21615b777cf7cef3d452afb8b79773fd45d3d8
    line: 708
    column: 1
    function: __VERIFIER_atomic_index_malloc
