- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 4f987b2b-bbcd-430d-8eb8-34a266b533d3
    creation_time: 2024-04-30T10:55:01Z
    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-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
      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: 401a2931-bffd-42bd-8992-c5f886e14e0d
    creation_time: 2024-04-30T10:55:01Z
    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-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
      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-1.i
    file_hash: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
    line: 750
    column: 4
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f48b4dfd-e1b0-44ee-9111-143d4aedacf8
    creation_time: 2024-04-30T10:55:01Z
    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-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
      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-1.i
    file_hash: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
    line: 696
    column: 1
    function: __VERIFIER_atomic_release
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b4123c65-40c5-49b5-afdb-af67b0c6f5f6
    creation_time: 2024-04-30T10:55:01Z
    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-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
      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-1.i
    file_hash: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
    line: 752
    column: 4
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a690deb8-1b94-477d-be1f-aefcd8eccfb1
    creation_time: 2024-04-30T10:55:01Z
    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-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
      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-1.i
    file_hash: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
    line: 701
    column: 1
    function: __VERIFIER_atomic_CAS
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 90ecd9cb-e395-41b5-8376-0bdc66e53ccd
    creation_time: 2024-04-30T10:55:01Z
    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-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
      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-1.i
    file_hash: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
    line: 695
    column: 1
    function: __VERIFIER_atomic_acquire
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: e35f10b8-568b-4083-a60f-2d5dd4d0f0f0
    creation_time: 2024-04-30T10:55:01Z
    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-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
      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: 2779e811-ce5c-49ec-a21a-9006ac8a7233
    creation_time: 2024-04-30T10:55:01Z
    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-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
      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-1.i
    file_hash: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
    line: 793
    column: 13
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 55bb70a1-a53a-4a28-9718-16383a0855f4
    creation_time: 2024-04-30T10:55:01Z
    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-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
      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-1.i
    file_hash: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
    line: 691
    column: 1
    function: __VERIFIER_atomic_acquire
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 843d54d2-ca9c-449b-b9ef-1423f8d3684d
    creation_time: 2024-04-30T10:55:01Z
    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-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
      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-1.i
    file_hash: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
    line: 715
    column: 1
    function: __VERIFIER_atomic_CAS
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ec3c7126-d8fa-431b-95c5-467c404979e5
    creation_time: 2024-04-30T10:55:01Z
    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-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
      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-1.i
    file_hash: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
    line: 764
    column: 1
    function: __VERIFIER_atomic_assert
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5f750ee9-2b47-4186-82cb-f30d358d0798
    creation_time: 2024-04-30T10:55:01Z
    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-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
      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-1.i
    file_hash: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
    line: 700
    column: 1
    function: __VERIFIER_atomic_release
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a2da24f6-b142-424c-93d8-9987885acc3d
    creation_time: 2024-04-30T10:55:01Z
    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-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longer-1.i: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
      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-1.i
    file_hash: f66a662852389d8ac1f64241746e843d67de7f5d7507051fb5c8e68404b785cd
    line: 761
    column: 1
    function: __VERIFIER_atomic_assert
