- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 6e647b94-9434-4365-9bf8-f3da6e0e0884
    creation_time: 2024-04-30T09:32:46Z
    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/08_rand_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
      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: 77a0c03a-b5b6-4abe-aa7d-78e4ceb15610
    creation_time: 2024-04-30T09:32:46Z
    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/08_rand_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
      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/08_rand_cas.i
    file_hash: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
    line: 725
    column: 1
    function: __VERIFIER_atomic_CAS
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 517488cd-3f1e-40f2-a30d-73f6e66b79e7
    creation_time: 2024-04-30T09:32:46Z
    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/08_rand_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
      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/08_rand_cas.i
    file_hash: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
    line: 749
    column: 3
    function: PseudoRandomUsingAtomic_monitor
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 47aabbce-0a9c-4f12-8415-100e029ec6f0
    creation_time: 2024-04-30T09:32:46Z
    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/08_rand_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
      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/08_rand_cas.i
    file_hash: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
    line: 747
    column: 3
    function: PseudoRandomUsingAtomic_monitor
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 07e4b745-b24b-4c1f-8456-51d3eb9a9fed
    creation_time: 2024-04-30T09:32:46Z
    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/08_rand_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
      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/08_rand_cas.i
    file_hash: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
    line: 701
    column: 1
    function: __VERIFIER_atomic_acquire
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 72fa5b8c-1d54-48d1-9956-9cd181a90186
    creation_time: 2024-04-30T09:32:46Z
    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/08_rand_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
      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/08_rand_cas.i
    file_hash: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
    line: 732
    column: 3
    function: PseudoRandomUsingAtomic_nextInt
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1eab6f64-0136-4d39-a00c-00561679b13e
    creation_time: 2024-04-30T09:32:46Z
    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/08_rand_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
      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/08_rand_cas.i
    file_hash: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
    line: 705
    column: 1
    function: __VERIFIER_atomic_acquire
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2e33111b-5c4e-4529-9f7c-2340b92aa6b3
    creation_time: 2024-04-30T09:32:46Z
    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/08_rand_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
      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/08_rand_cas.i
    file_hash: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
    line: 706
    column: 1
    function: __VERIFIER_atomic_release
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6a864cd6-b4b2-4027-94b8-d1aa6d45d16b
    creation_time: 2024-04-30T09:32:46Z
    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/08_rand_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
      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/08_rand_cas.i
    file_hash: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
    line: 730
    column: 3
    function: PseudoRandomUsingAtomic_nextInt
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: ba60f9a9-13d1-46a4-af16-73ac400eae5b
    creation_time: 2024-04-30T09:32:46Z
    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/08_rand_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
      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: 77022a48-5c58-41aa-933f-22ebcfbca63a
    creation_time: 2024-04-30T09:32:46Z
    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/08_rand_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
      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/08_rand_cas.i
    file_hash: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
    line: 785
    column: 13
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9e679052-0265-4847-8848-0b1066e7ca72
    creation_time: 2024-04-30T09:32:46Z
    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/08_rand_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
      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/08_rand_cas.i
    file_hash: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
    line: 711
    column: 1
    function: __VERIFIER_atomic_CAS
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dc3750ab-1cb6-4fb5-ac1d-159bf36c0965
    creation_time: 2024-04-30T09:32:46Z
    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/08_rand_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
      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/08_rand_cas.i
    file_hash: 111430583c5cad5728291a83d9964586feec908088fcc502d1f1ab24d409725c
    line: 710
    column: 1
    function: __VERIFIER_atomic_release
