- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bcf6ac3c-b491-4b72-b39a-95c44cf73d87
    creation_time: 2024-04-30T10:59:49Z
    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-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: 2b7599ca-b528-4c58-8d05-8eee1d003afd
    creation_time: 2024-04-30T10:59:49Z
    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-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: 91255fcb-e4b3-4f20-a794-9464eda42fac
    creation_time: 2024-04-30T10:59:49Z
    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-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: 65f8d282-6b9e-451e-b8b6-9073f1d9d4b2
    creation_time: 2024-04-30T10:59:49Z
    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-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: 04bb4366-3dc5-4e48-810f-8a3aae90a204
    creation_time: 2024-04-30T10:59:49Z
    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-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: f40f637d-9221-4741-b6c2-644c27d289c3
    creation_time: 2024-04-30T10:59:49Z
    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-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: 65188bae-61bb-4080-981d-3fc9c617082b
    creation_time: 2024-04-30T10:59:49Z
    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-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: 90f9a17e-80d9-460c-a8b2-72d7dd4e521c
    creation_time: 2024-04-30T10:59:49Z
    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-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: 39ea7e0f-1656-46d9-828b-122e41b5d8ab
    creation_time: 2024-04-30T10:59:49Z
    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-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: 6d9b15a2-e3ee-43a7-9f9d-5362904d4e4d
    creation_time: 2024-04-30T10:59:49Z
    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-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: af384131-ceb3-420c-be67-497c3b3febc3
    creation_time: 2024-04-30T10:59:49Z
    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-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: b7147cd1-551d-4211-9ecc-e64b7decfcf3
    creation_time: 2024-04-30T10:59:49Z
    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-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: 7b3879eb-2d37-4dfc-9aa5-53e7c425e353
    creation_time: 2024-04-30T10:59:49Z
    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-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: faa7a514-b91a-4349-bb80-26da4498c657
    creation_time: 2024-04-30T10:59:49Z
    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-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: bf08d436-a18c-447b-9aff-f6d14308dba5
    creation_time: 2024-04-30T10:59:49Z
    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-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: ce7706ba-fc6d-44e0-b75a-eefeb4af4973
    creation_time: 2024-04-30T10:59:49Z
    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-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: ab8a9f72-86fb-49d2-81cd-88bd1f3ef8ce
    creation_time: 2024-04-30T10:59:49Z
    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-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: 34b22ef9-c44c-46ed-983c-274a576153c0
    creation_time: 2024-04-30T10:59:49Z
    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-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: e40aaeca-d40a-4771-81de-a18e4ebd3cef
    creation_time: 2024-04-30T10:59:49Z
    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-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: c365d562-f1c6-4f93-84f0-639e23ac196b
    creation_time: 2024-04-30T10:59:49Z
    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-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: 3dd9fcc7-fcca-44bb-8b1e-19ff680f87fc
    creation_time: 2024-04-30T10:59:49Z
    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-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: 9c0c14c5-3ec9-42d2-8298-5887fb142606
    creation_time: 2024-04-30T10:59:49Z
    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-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: 48e1bfa6-6935-4724-b624-d518d8b86d6d
    creation_time: 2024-04-30T10:59:49Z
    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-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: 7c6bd3a1-962b-4250-b0ed-ba803d0b0fe9
    creation_time: 2024-04-30T10:59:49Z
    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-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: 3dadea57-5265-460f-98f3-0aa4a13e7f70
    creation_time: 2024-04-30T10:59:49Z
    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-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: 7eaf2be2-eeb0-401d-b56d-8cd19aeb5c65
    creation_time: 2024-04-30T10:59:49Z
    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-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: 396fa84c-46bd-471e-a1af-48bc925a93cf
    creation_time: 2024-04-30T10:59:49Z
    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-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: 8b0e3be4-4eb5-41bf-ad65-3ffac68a7379
    creation_time: 2024-04-30T10:59:49Z
    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-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: 405c2d37-4c05-4458-be39-c9e0c744eed1
    creation_time: 2024-04-30T10:59:49Z
    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-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: c55eb61a-7c7f-438c-99ff-480a16234b27
    creation_time: 2024-04-30T10:59:49Z
    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-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: 1ed94f00-7a1f-4b3f-83e1-e3ad9cc5df05
    creation_time: 2024-04-30T10:59:49Z
    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-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: e6eae567-76e6-41a8-a007-f8cfecf0231f
    creation_time: 2024-04-30T10:59:49Z
    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-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: 13921504-a5d5-43e7-a221-af53b4e92083
    creation_time: 2024-04-30T10:59:49Z
    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-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: 227741ca-aeaa-4caf-ba09-d9864bcb0941
    creation_time: 2024-04-30T10:59:49Z
    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-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: 77a0db31-c8bf-4cdd-9c7d-5ab900f64689
    creation_time: 2024-04-30T10:59:49Z
    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-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: 43453607-da7b-4732-93de-ff7a691daad9
    creation_time: 2024-04-30T10:59:49Z
    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-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: 2a5c9dfa-afd2-4ee9-b2ac-aa5c4a6bf505
    creation_time: 2024-04-30T10:59:49Z
    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-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: dfe954d8-b722-4472-85f1-9110347e391b
    creation_time: 2024-04-30T10:59:49Z
    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-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
