- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be521570-5e35-4ec7-92b4-9dc4e0adba62
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 120
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (g1 == (_Bool)0 || g1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d805a57f-422f-4e6b-9bcd-c859eb05e499
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 121
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (g1 == (_Bool)0 || g1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c38a89bc-6473-469b-a766-344696df4d6b
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 122
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (g1 == (_Bool)0 || g1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2fec8425-8d91-4d93-a0c4-6d673cf3d075
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 120
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (d3 == (_Bool)0 || d3 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1bc73af1-05cb-400f-a454-f9f4a4ce0dd2
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 121
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (d3 == (_Bool)0 || d3 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e6a8d0c-f703-49bf-a28a-9de3d1541a9b
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 122
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (d3 == (_Bool)0 || d3 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80b90d7b-a1eb-47ae-b7f7-2d68dd1d5603
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 120
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (d1 == (_Bool)0 || d1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71fa362a-1af2-4d81-96cc-c9cc7d1f0a2e
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 121
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (d1 == (_Bool)0 || d1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebc165d4-954c-4d06-ae5c-6285b58bad9f
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 122
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (d1 == (_Bool)0 || d1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec233c27-bca9-46d8-85f3-00fd99b0061d
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 120
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (g3 == (_Bool)0 || g3 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73aed3a5-3768-4af5-8fb2-4f25a657e146
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 121
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (g3 == (_Bool)0 || g3 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc244205-c9c2-41da-bbab-a1986b4b8c34
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 122
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (g3 == (_Bool)0 || g3 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3a045e0-fb3c-46e1-b36e-b40ae3334f77
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 120
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (g2 == (_Bool)0 || g2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c8e6428-5faa-4db2-b580-26c862a913e9
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 121
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (g2 == (_Bool)0 || g2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c1ab416-4ff7-4657-ad5a-ba839855582b
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 122
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (g2 == (_Bool)0 || g2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c66629dd-2907-4f44-bb10-a3c098cf066c
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 120
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (d2 == (_Bool)0 || d2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d87a48b-a5d7-4653-9dc2-05ed84a43741
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 121
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (d2 == (_Bool)0 || d2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d002a2c-c62d-43ba-98c0-f03d89bfe56e
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 122
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (d2 == (_Bool)0 || d2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 062fb61f-bb37-426a-adc8-06b6ecd31c11
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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: 36399dee-23b1-4e39-9cbb-0c4036b26e02
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 88
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cdd99d7e-9e91-46cf-9edc-566ab6fabcdf
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 92
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 30e23d58-fc66-4924-b635-e2c4a3247d00
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 44
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 452b1743-8894-4e2f-bc7e-6bca53629661
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 50
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 403d115d-7f75-42db-b360-97bd61fba6f7
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 70
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8ce8d93e-9d75-4dd4-96c4-6dc821b6c8b4
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 90
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bae23f8d-0175-4d30-aacb-8c7272d67309
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 66
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e39902e1-763a-4e0a-a4d9-d301f01d98f7
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 48
    column: 7
    function: thread1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 23e09efe-c128-471b-a19f-a7459dcf90d3
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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: d4960984-191b-484c-bae8-7502a754bcd2
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 119
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 949bc9cb-47b5-462e-a79f-d02cab27a32b
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 46
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0e4aa39e-d6ec-45e6-ad59-e69f5d77c01e
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 94
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6ee895a2-0e79-4a99-8435-40a6aa393027
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 72
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ea8c12d6-426a-421a-b02b-3b3069eb984e
    creation_time: 2024-04-25T07:42:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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/weaver/parallel-misc-3-extended.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-3-extended.wvr.c: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
      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/weaver/parallel-misc-3-extended.wvr.c
    file_hash: 1ac00c9540bbc99a446c9cb6c02e180c3a0ad4fef3c182d14bafdc7ea871c54c
    line: 68
    column: 7
    function: thread2
