- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d4cfac2-ae6f-404b-8a84-423393b05df7
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 6c133c2b-9623-4b9e-a85f-24d36ce3c9a2
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 40658cf4-c9a7-419f-9c19-4f392d7b4ec8
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 79df50bf-b385-4751-a66d-eae02430eba4
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 3df12100-004f-46b2-8550-6bed19d34d51
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 4902c946-0a95-441d-85f9-b774f28eaaa7
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 8ac63777-53da-4b25-a329-2d515fba5858
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 5ed1d8a1-e7ca-4d36-9487-14eed88afab7
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 10939a87-2f93-4c0f-91f2-944124f9e0c6
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: d0ad8d00-fe50-4245-8832-7336f95fe81b
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 18f1e969-df71-4151-ad93-e4074c2fdf64
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: d49d760b-b138-4a94-8e8e-d73e8c68b7e9
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 13bbfbc0-5c5b-4901-93b3-feee95102502
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: a6bd2842-9b80-4132-ba01-1a62b48f3ea1
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 619733c4-4620-46c9-b39c-7d0817c529c9
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 01b8aadb-addc-4ab0-b74e-bc2f4c46894a
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 451e215c-fb7e-4888-b7d8-29ba8573bef3
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 642bc136-f150-4f3f-8dda-65f2ed918ae4
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    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: 08bbcec2-a2c6-44fc-ade3-6feb8b89e64d
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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: 2c958c27-edbb-4149-938d-157a25134a7b
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    line: 690
    column: 5
    function: t1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 42ba8e72-971c-4a22-a841-c1c09aebf4b0
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    line: 719
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 46e526f3-dbac-4ef7-8589-3952a4da9eee
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    line: 688
    column: 5
    function: t1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 54513e9a-b50d-4705-b170-46d0c6346b8e
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    line: 698
    column: 5
    function: t2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c8c80cc7-2098-497e-be3f-64a8d4d83936
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    line: 696
    column: 5
    function: t2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: de876d44-bf46-478e-ac4c-e1e4bb0713eb
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    line: 716
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: b0e2fd9a-6b8e-41d1-b213-262b5505532d
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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: ad9ba076-d942-4395-8e87-21ddcd70f3bb
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    line: 720
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8b36a4f6-7cfe-4aca-935d-4bc55ce7dfd8
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    line: 725
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6f92e345-bd23-431d-8a41-369f70d69235
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    line: 717
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 806502d3-3c16-4d59-a98d-65798c519d75
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    line: 723
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 26215b06-aa31-4c52-b57d-ad8952964e24
    creation_time: 2024-04-26T10:36:30Z
    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-5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-5.i: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
      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-5.i
    file_hash: e0f90189cbea201dcd094fc9e84327a00ade17017ada90c5df84c8712afaf176
    line: 714
    column: 3
    function: main
