- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 24dcb793-19cd-42ce-947f-2ba112614f62
    creation_time: 2024-04-29T10:56:59Z
    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/04_incdec_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
      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: 06962233-15f1-4d89-b05d-5d476c088695
    creation_time: 2024-04-29T10:56:59Z
    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/04_incdec_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
      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/04_incdec_cas.i
    file_hash: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
    line: 733
    column: 3
    function: dec
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a54be5d5-4075-4808-ac1c-dd8be7ae20e7
    creation_time: 2024-04-29T10:56:59Z
    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/04_incdec_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
      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/04_incdec_cas.i
    file_hash: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
    line: 715
    column: 3
    function: inc
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f5258af7-a812-4ff2-920a-7036fcc1928d
    creation_time: 2024-04-29T10:56:59Z
    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/04_incdec_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
      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/04_incdec_cas.i
    file_hash: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
    line: 735
    column: 3
    function: dec
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0ad7a52b-704b-4a55-8f73-d3380ffae6da
    creation_time: 2024-04-29T10:56:59Z
    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/04_incdec_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
      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/04_incdec_cas.i
    file_hash: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
    line: 729
    column: 1
    function: __VERIFIER_atomic_assert2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 22424d07-3836-43fa-a4d1-e21ce2595ee8
    creation_time: 2024-04-29T10:56:59Z
    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/04_incdec_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
      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/04_incdec_cas.i
    file_hash: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
    line: 713
    column: 3
    function: inc
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fa8c705d-36ba-409c-9bc3-51cd6f118551
    creation_time: 2024-04-29T10:56:59Z
    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/04_incdec_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
      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/04_incdec_cas.i
    file_hash: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
    line: 726
    column: 1
    function: __VERIFIER_atomic_assert2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 581781f5-c313-4d60-ae52-d08e2361195f
    creation_time: 2024-04-29T10:56:59Z
    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/04_incdec_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
      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/04_incdec_cas.i
    file_hash: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
    line: 709
    column: 1
    function: __VERIFIER_atomic_assert1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 664b8b29-d4df-46a7-8522-aa04f7c5c833
    creation_time: 2024-04-29T10:56:59Z
    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/04_incdec_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
      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/04_incdec_cas.i
    file_hash: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
    line: 702
    column: 1
    function: __VERIFIER_atomic_CAS
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9e634908-94d8-4628-a723-55c10f392de5
    creation_time: 2024-04-29T10:56:59Z
    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/04_incdec_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
      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/04_incdec_cas.i
    file_hash: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
    line: 706
    column: 1
    function: __VERIFIER_atomic_assert1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 36732c12-46a4-42a6-b8ea-2699873f2c05
    creation_time: 2024-04-29T10:56:59Z
    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/04_incdec_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
      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: c9c14cff-3c27-4e68-a75e-f097e729f079
    creation_time: 2024-04-29T10:56:59Z
    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/04_incdec_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
      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/04_incdec_cas.i
    file_hash: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
    line: 755
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 489898ae-1219-460a-821f-6d5fedfb796f
    creation_time: 2024-04-29T10:56:59Z
    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/04_incdec_cas.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/04_incdec_cas.i: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
      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/04_incdec_cas.i
    file_hash: a9295efc0d8bacfc5fb202511f0d3721ae5554ffb4def47cf5dbf45088356869
    line: 687
    column: 1
    function: __VERIFIER_atomic_CAS
