- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1459a96-2377-4ce2-bdc7-752055289836
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 1 <= i'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6001db1a-8822-475a-8533-659189acd2a4
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 1 <= i'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13993ff0-a4eb-4b2b-938f-35949c1f0d8b
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= cur'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af92c9f5-80f5-4de6-873f-058ade94fb87
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= cur'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64c01ad3-d436-4f2b-84c1-db1b8c1bf85d
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= x'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 430e4a91-d8ed-49d0-ba69-47d73af3e599
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= x'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71e89080-6068-45d4-bcad-9c72acd93799
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 1 <= j'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5a882da-9895-4098-85e1-de212e3aaa61
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 1 <= j'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8fdce78-7021-45bd-a131-da3291f15555
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= prev'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ccf24d70-58bc-467a-b3e0-599d4c952661
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= prev'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17568d45-885b-4b93-9a88-d92a4da0bae5
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (1 <= i && 1 <= j))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bea3a5db-31c1-488d-97a0-6304bf6f5971
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (1 <= i && 1 <= j))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 629bbb8a-70b3-41d8-aa93-cd6e37494551
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= q'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c32c69a-4d6e-4afc-9327-cb1e7efe3cb9
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= q'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50f4eab3-7ec4-4d5d-acb0-2646106f2b19
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= p'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd1561a8-c784-4899-bb19-98926c758eaa
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= p'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b6fa1b4-2e7b-4612-95f2-a26ac3cc1ae7
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= next'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26ce5050-040e-47a5-85df-5d074d3d3558
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= next'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 031a0a3c-3451-4724-8752-9205c2071199
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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: fc4e12b6-a2e7-4e47-8c7f-4837b9bc72d3
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 690
    column: 5
    function: t1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 346f1005-9ebc-4646-b350-5ec966384352
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 719
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 538d55a9-cdd6-4001-ab53-0e998fb757d2
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 688
    column: 5
    function: t1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e9e067f3-9d8b-4a1d-8c90-5fad132bd34d
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 698
    column: 5
    function: t2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: eff5a236-82ca-461f-986d-6a5841725248
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 696
    column: 5
    function: t2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8359dc9e-0845-4f70-ae2b-a0cf36143328
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 716
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: b454a1f7-35c1-499f-8267-3b00d6cc43a3
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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: f7b69863-72aa-418c-a48d-faee773a69e3
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 720
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a881f055-044d-447b-b60c-d88dde422d92
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 725
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b40a526d-8c14-496f-baa5-e5c859398320
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 717
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c4540f9f-f452-4b4f-90c5-a9756e9971f4
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 723
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a5abc774-aeac-4abd-a8ea-2d82c28fa4a5
    creation_time: 2024-04-26T10:36:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 714
    column: 3
    function: main
