- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 27bf7b1d-57f3-42f6-979d-fe518e733ed4
    creation_time: 2024-04-30T10:55:39Z
    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_longest-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
      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: c5fa5efe-024b-4a13-83bc-d99168c84e0e
    creation_time: 2024-04-30T10:55:39Z
    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_longest-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
      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_longest-2.i
    file_hash: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
    line: 750
    column: 4
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: afc47e38-cf56-4687-8f2e-4cf82779d292
    creation_time: 2024-04-30T10:55:39Z
    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_longest-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
      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_longest-2.i
    file_hash: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
    line: 696
    column: 1
    function: __VERIFIER_atomic_release
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 76b2bf12-d6fb-4e2d-881c-f20218353a22
    creation_time: 2024-04-30T10:55:39Z
    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_longest-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
      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_longest-2.i
    file_hash: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
    line: 752
    column: 4
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bc399983-01e5-4674-a876-7e39f522c288
    creation_time: 2024-04-30T10:55:39Z
    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_longest-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
      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_longest-2.i
    file_hash: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
    line: 701
    column: 1
    function: __VERIFIER_atomic_CAS
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 73988477-0392-4bbf-80d3-c0873cb087bb
    creation_time: 2024-04-30T10:55:39Z
    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_longest-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
      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: b5a44058-1f2c-4630-b69c-cc06ca650eb5
    creation_time: 2024-04-30T10:55:39Z
    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_longest-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
      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_longest-2.i
    file_hash: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
    line: 793
    column: 13
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6f3c76db-18ca-4f48-a7a1-99b4e9213682
    creation_time: 2024-04-30T10:55:39Z
    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_longest-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
      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_longest-2.i
    file_hash: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
    line: 695
    column: 1
    function: __VERIFIER_atomic_acquire
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a3d1c393-f547-4573-a115-aef6a2f16a63
    creation_time: 2024-04-30T10:55:39Z
    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_longest-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
      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_longest-2.i
    file_hash: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
    line: 764
    column: 1
    function: __VERIFIER_atomic_assert
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2a134c04-c9c3-4cb8-85f4-430e2afd6090
    creation_time: 2024-04-30T10:55:39Z
    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_longest-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
      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_longest-2.i
    file_hash: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
    line: 691
    column: 1
    function: __VERIFIER_atomic_acquire
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8bb41cc5-8d6e-486a-9d52-01f7ffafeec0
    creation_time: 2024-04-30T10:55:39Z
    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_longest-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
      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_longest-2.i
    file_hash: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
    line: 715
    column: 1
    function: __VERIFIER_atomic_CAS
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6126b0ef-fe7a-4170-80f2-6b5c9b32efda
    creation_time: 2024-04-30T10:55:39Z
    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_longest-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
      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_longest-2.i
    file_hash: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
    line: 700
    column: 1
    function: __VERIFIER_atomic_release
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3614718b-b629-4dd5-a8c4-913847c9ca43
    creation_time: 2024-04-30T10:55:39Z
    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_longest-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-2.i: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
      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_longest-2.i
    file_hash: 7f7f7b6ea5abe354543dc816b244a5041021350ff4076c6fd52a8208b97eac31
    line: 761
    column: 1
    function: __VERIFIER_atomic_assert
