- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8096da84-0ba4-42cb-9da7-4cf39f2cda1d
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1615
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= unique_id'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 575ee01a-da56-4ea7-b4ea-17da2019bc86
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1616
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= unique_id'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5605cdb8-17e3-4fcf-b221-fed67831ddfe
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1617
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= unique_id'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0eff6d30-da2c-40ef-b6b7-32fc3d63e509
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1618
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= unique_id'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 74dc4d12-f39f-416a-9dea-6ed4da9d783c
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1619
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= unique_id'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8c8a57f-5232-4b64-bb24-bf769788ddac
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1620
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= unique_id'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64092625-55d3-400a-b756-85875cc74dd8
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1621
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= unique_id'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 5bc6fe78-44d3-4a90-850b-bd140dc8f41d
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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: 0e7b60ff-4b92-4f5f-8659-5dfe1d594db6
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1558
    column: 5
    function: Incr_Pop
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c39f4c87-7ef8-454f-b860-f6de4f86a865
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1490
    column: 5
    function: TryCollision
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2b0b8379-e37c-4de2-943f-ebe5769e2de3
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1518
    column: 5
    function: Push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f61cd22e-558d-42f3-a503-c54f97c0f827
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1516
    column: 5
    function: Push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7ecb152d-f27e-4a00-81a3-b7c0f77ea5fc
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1354
    column: 5
    function: atomic_int_cas
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8a7b91a0-4f56-440b-b3ef-39ff4cb3c794
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1373
    column: 5
    function: atomic_ti_cas
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 983ae42a-28f7-4238-b867-c9823265029a
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1470
    column: 13
    function: TryPerformStackOp
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 013e2fdc-9f5f-466d-92ec-fd4d67a3f9ac
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1551
    column: 5
    function: DecrIncr_Push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2f7aae92-5973-4de8-92b5-27767328d758
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1465
    column: 13
    function: TryPerformStackOp
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 66cdeb77-5c9e-4dac-9e1d-8b1654a3679d
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1486
    column: 5
    function: FinishCollision
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 95c1a644-6637-472c-94ca-2e3c4344fd03
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1413
    column: 5
    function: free_ThreadInfo
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5e98a0be-a388-4f02-8991-b23b3a5233ae
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1560
    column: 5
    function: Incr_Pop
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1274a1aa-de09-4fa6-82de-4e2763a59fa6
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1399
    column: 5
    function: malloc_ThreadInfo
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0b4aeffb-131d-4269-a3ce-2a866b9c597d
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1393
    column: 5
    function: atomic_c_cas
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d8e744dd-4b0b-4939-add1-27a55fb267e6
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1508
    column: 5
    function: TryCollision
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2ace76fe-2d02-47ef-b992-df8d587e28a5
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1527
    column: 5
    function: Pop
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4f4fe4a3-a1f1-4995-8e55-cd7e83d1bba1
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1366
    column: 5
    function: atomic_ti_cas
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3ba185c9-c110-4a7c-aa66-3f31312c4bc8
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1546
    column: 5
    function: Incr_Push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b6d8f261-d31c-4358-8bd4-607fae58837f
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1529
    column: 5
    function: Pop
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9e9d3b68-d1fa-4703-a9af-1b790aa64b91
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1567
    column: 5
    function: DecrIncr_Pop
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d3dea11a-9185-4358-a7b9-6731d5168d2e
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1408
    column: 5
    function: free_ThreadInfo
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6c7d1f74-1ab9-48d8-b8a2-f1debd03e6cd
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1361
    column: 5
    function: atomic_int_cas
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 797c5271-bf7c-4a70-b0e4-c38df697a46d
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1548
    column: 5
    function: Incr_Push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8288414e-3986-4091-945f-d41f14646aea
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1404
    column: 5
    function: malloc_ThreadInfo
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 31efbc76-f933-4d99-9e2a-aad4dd62b324
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1386
    column: 5
    function: atomic_c_cas
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2566cfe0-dd05-485a-8ab2-e535573f9624
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1555
    column: 5
    function: DecrIncr_Push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8cd1b7c8-10f7-4299-aa26-4a8a86a10514
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1480
    column: 5
    function: FinishCollision
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3a75300c-8086-4c11-bccb-151bbe6c91ba
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1563
    column: 5
    function: DecrIncr_Pop
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 30a100cf-2a94-46a9-b884-6288367dc949
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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: 46573379-b131-47b5-90a5-f880d67a4292
    creation_time: 2024-04-30T09:38:39Z
    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-complex/elimination_backoff_stack.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/elimination_backoff_stack.i: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
      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-complex/elimination_backoff_stack.i
    file_hash: 0a77b23de3110741cf9e339cfb9f72e965f6bc6bc082cff0044fedc6c4916cfb
    line: 1614
    column: 5
    function: main
