- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 4140584a-c986-4180-9f6d-88d5af029a5c
    creation_time: 2024-04-30T10:55:17Z
    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-ext/26_stack_cas_longer-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
      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: 52a0c48e-ccd3-4c16-8b9f-21224a11c2d9
    creation_time: 2024-04-30T10:55:17Z
    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-ext/26_stack_cas_longer-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
      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_longer-2.i
    file_hash: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
    line: 750
    column: 4
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ecd489ea-e23f-4920-a3fa-b9b94d2c5272
    creation_time: 2024-04-30T10:55:17Z
    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-ext/26_stack_cas_longer-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
      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_longer-2.i
    file_hash: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
    line: 696
    column: 1
    function: __VERIFIER_atomic_release
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a79a5a1b-12f3-42e1-92ba-43fbd6477130
    creation_time: 2024-04-30T10:55:17Z
    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-ext/26_stack_cas_longer-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
      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_longer-2.i
    file_hash: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
    line: 752
    column: 4
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b819cb82-2e51-47bb-8baa-4284899987b4
    creation_time: 2024-04-30T10:55:17Z
    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-ext/26_stack_cas_longer-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
      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_longer-2.i
    file_hash: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
    line: 701
    column: 1
    function: __VERIFIER_atomic_CAS
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: a5277d48-1e45-496f-8a8b-b4a63c9be673
    creation_time: 2024-04-30T10:55:17Z
    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-ext/26_stack_cas_longer-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
      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: e9ad497a-5403-4e46-bd2e-6bc3795f22f8
    creation_time: 2024-04-30T10:55:17Z
    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-ext/26_stack_cas_longer-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
      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_longer-2.i
    file_hash: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
    line: 793
    column: 13
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fbcf2420-ad57-4288-a0ae-04e1e16bbb62
    creation_time: 2024-04-30T10:55:17Z
    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-ext/26_stack_cas_longer-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
      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_longer-2.i
    file_hash: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
    line: 695
    column: 1
    function: __VERIFIER_atomic_acquire
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d8920d35-9c38-4b84-837e-a5fae7b19d63
    creation_time: 2024-04-30T10:55:17Z
    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-ext/26_stack_cas_longer-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
      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_longer-2.i
    file_hash: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
    line: 764
    column: 1
    function: __VERIFIER_atomic_assert
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a92522c7-df12-4f68-9b07-79b32c33b6ce
    creation_time: 2024-04-30T10:55:17Z
    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-ext/26_stack_cas_longer-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
      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_longer-2.i
    file_hash: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
    line: 691
    column: 1
    function: __VERIFIER_atomic_acquire
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bb93b5bd-b45a-48a4-b5ed-712bd7650428
    creation_time: 2024-04-30T10:55:17Z
    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-ext/26_stack_cas_longer-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
      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_longer-2.i
    file_hash: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
    line: 715
    column: 1
    function: __VERIFIER_atomic_CAS
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 86cedde5-0009-492e-aeb4-d718a6100144
    creation_time: 2024-04-30T10:55:17Z
    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-ext/26_stack_cas_longer-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
      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_longer-2.i
    file_hash: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
    line: 700
    column: 1
    function: __VERIFIER_atomic_release
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 43b2b3a8-a3b4-4441-9a5a-38bb969ec065
    creation_time: 2024-04-30T10:55:17Z
    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-ext/26_stack_cas_longer-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-2.i: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
      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_longer-2.i
    file_hash: f6a420ba5144c69cefe02db203552770c4018653c510d9792e57ffedc3dfc64e
    line: 761
    column: 1
    function: __VERIFIER_atomic_assert
