- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55fbb86c-324d-4e20-8a40-73e23d669ff5
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 8a2185b9-fcd1-4059-b60f-8063080e5cc8
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: e316e0a6-092d-44dc-bb1e-faeac742b42d
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 7aee4ac7-0110-43d3-a49d-19ed64369518
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 25840fea-0946-436a-96b2-3a96e8a79a40
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 445b1e04-311b-4895-a7ca-02ad1ffb61d4
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 3137be82-5abd-4465-ac3d-2267c1300779
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f391aea-70ac-4e0a-a358-b2e251e16311
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: fe07332f-a365-4620-90ad-baca2d293fe2
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 1b9170b7-56c7-4419-9f73-83be94914383
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 7c49cfc4-ca95-4f99-85ef-1684cac69d99
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: f53b09bf-8d6b-4a29-a271-8e7508694115
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: eff58eda-3390-40c4-9b69-3dd34530ab89
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: e98f0fc3-4247-4eab-8a8f-a60820f5957f
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: c9ffd3dc-0943-4cf0-9a40-7f1a12f15246
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 746602fe-9ab6-4f18-bb09-02b25b2b58d5
    creation_time: 2024-06-19T11:50:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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
